comparison dwtx/jface/text/source/projection/ProjectionAnnotation.d @ 145:02cd5f1224d3

...
author Frank Benoit <benoit@tionex.de>
date Sun, 24 Aug 2008 22:31:00 +0200
parents 7d818bd32d63
children 000f9136b8f7
comparison
equal deleted inserted replaced
144:16a71f577815 145:02cd5f1224d3
113 fIsRangeIndication= rangeIndication; 113 fIsRangeIndication= rangeIndication;
114 } 114 }
115 115
116 private void drawRangeIndication(GC gc, Canvas canvas, Rectangle r) { 116 private void drawRangeIndication(GC gc, Canvas canvas, Rectangle r) {
117 final int MARGIN= 3; 117 final int MARGIN= 3;
118 118
119 /* cap the height - at least on GTK, large numbers are converted to 119 /* cap the height - at least on GTK, large numbers are converted to
120 * negatives at some point */ 120 * negatives at some point */
121 int height= Math.min(r.y + r.height - MARGIN, canvas.getSize().y); 121 int height= Math.min(r.y + r.height - MARGIN, canvas.getSize().y);
122 122
123 gc.setForeground(canvas.getDisplay().getSystemColor(COLOR)); 123 gc.setForeground(canvas.getDisplay().getSystemColor(COLOR));
124 gc.setLineWidth(0); // NOTE: 0 means width is 1 but with optimized performance 124 gc.setLineWidth(0); // NOTE: 0 means width is 1 but with optimized performance
125 gc.drawLine(r.x + 4, r.y + 12, r.x + 4, height); 125 gc.drawLine(r.x + 4, r.y + 12, r.x + 4, height);
126 gc.drawLine(r.x + 4, height, r.x + r.width - MARGIN, height); 126 gc.drawLine(r.x + 4, height, r.x + r.width - MARGIN, height);
127 } 127 }
135 ImageUtilities.drawImage(image, gc, canvas, rectangle, DWT.CENTER, DWT.TOP); 135 ImageUtilities.drawImage(image, gc, canvas, rectangle, DWT.CENTER, DWT.TOP);
136 if (fIsRangeIndication) { 136 if (fIsRangeIndication) {
137 FontMetrics fontMetrics= gc.getFontMetrics(); 137 FontMetrics fontMetrics= gc.getFontMetrics();
138 int delta= (fontMetrics.getHeight() - image.getBounds().height)/2; 138 int delta= (fontMetrics.getHeight() - image.getBounds().height)/2;
139 rectangle.y += delta; 139 rectangle.y += delta;
140 rectangle.height -= delta; 140 rectangle.height -= delta;
141 drawRangeIndication(gc, canvas, rectangle); 141 drawRangeIndication(gc, canvas, rectangle);
142 } 142 }
143 } 143 }
144 } 144 }
145 145
156 } 156 }
157 157
158 private void initializeImages(Display display) { 158 private void initializeImages(Display display) {
159 if (fgCollapsedImage is null) { 159 if (fgCollapsedImage is null) {
160 160
161 ImageDescriptor descriptor= ImageDescriptor.createFromFile(ProjectionAnnotation.class, "images/collapsed.gif"); //$NON-NLS-1$ 161 ImageDescriptor descriptor= ImageDescriptor.createFromFile( getImportData!("images/collapsed.gif")); //$NON-NLS-1$
162 fgCollapsedImage= descriptor.createImage(display); 162 fgCollapsedImage= descriptor.createImage(display);
163 descriptor= ImageDescriptor.createFromFile(ProjectionAnnotation.class, "images/expanded.gif"); //$NON-NLS-1$ 163 descriptor= ImageDescriptor.createFromFile( getImportData!( "images/expanded.gif")); //$NON-NLS-1$
164 fgExpandedImage= descriptor.createImage(display); 164 fgExpandedImage= descriptor.createImage(display);
165 165
166 display.disposeExec(new DisplayDisposeRunnable()); 166 display.disposeExec(new DisplayDisposeRunnable());
167 } 167 }
168 } 168 }