Attachment 34574 Details for Bug 19602 – SWT portion of the patch

Some Eclipse Foundation services are deprecated, or will be soon. Please ensure you've read this important communication.

[patch] SWT portion of the patch

swtPrintMarginsPatch.txt (text/plain), 22.24 KB, created by Steven Wasleski

on 2006-02-13 11:07:40 EST

(hide)

Description:

Filename:

MIME Type:

Creator: Steven Wasleski

Created: 2006-02-13 11:07:40 EST

Size: 22.24 KB

patch

obsolete

>### Eclipse Workspace Patch 1.0
>#P org.eclipse.swt
>Index: Eclipse SWT Custom Widgets/common/org/eclipse/swt/custom/StyledText.java
>===================================================================
>RCS file: /cvsroot/eclipse/org.eclipse.swt/Eclipse SWT Custom Widgets/common/org/eclipse/swt/custom/StyledText.java,v
>retrieving revision 1.322
>diff -u -r1.322 StyledText.java
>--- Eclipse SWT Custom Widgets/common/org/eclipse/swt/custom/StyledText.java	19 Jan 2006 22:59:30 -0000	1.322
>+++ Eclipse SWT Custom Widgets/common/org/eclipse/swt/custom/StyledText.java	13 Feb 2006 15:48:03 -0000
>@@ -164,6 +164,27 @@
> 		IS_GTK = "gtk".equals(platform);
> 		IS_MOTIF = "motif".equals(platform);
> 	}
>+	
>+	/**
>+	 * This class' definition must be kept in sync with
>+	 * <code>org.eclipse.swt.custom.StyledTextPrintMarginDecorator</code>. This
>+	 * class is used to contain all the decoration information after widget to
>+	 * printer conversion.
>+	 */
>+	static class ConvertedPrintMarginDecorator {
>+		public int alignment;
>+
>+		public int gutter;
>+
>+		public String[] marginText;
>+
>+		public TextStyle marginTextStyle;
>+
>+		// This field is calculated and contains the horizontal coordinates
>+		// of the margin.
>+		public Rectangle marginRect;
>+
>+	}
> 
> 	/**
> 	 * The Printing class implements printing of a range of text.
>@@ -194,6 +215,9 @@
> 		Point selection = null;					// selected text
> 		boolean mirrored;						// indicates the printing gc should be mirrored
> 		int lineSpacing;
>+		ConvertedPrintMarginDecorator leftPrintDecorator = null;
>+		ConvertedPrintMarginDecorator rightPrintDecorator = null;
>+		TextStyle defaultMarginStyle = null;
> 
> 	/**
> 	 * Creates an instance of <class>Printing</class>.
>@@ -269,7 +293,68 @@
> 		Point screenDPI = styledText.getDisplay().getDPI();
> 		Point printerDPI = printer.getDPI();
> 		resources = new Hashtable ();
>+		// Prepare to convert widget margin decorators to print decorators  
>+		StyledTextPrintMarginDecorator leftWidgetDecorator = null;
>+		StyledTextPrintMarginDecorator rightWidgetDecorator = null;
>+		if (mirrored) {
>+			leftWidgetDecorator = printOptions.printTrailMarginDecorator;
>+			rightWidgetDecorator = printOptions.printLeadMarginDecorator;
>+		} else {
>+			leftWidgetDecorator = printOptions.printLeadMarginDecorator;
>+			rightWidgetDecorator = printOptions.printTrailMarginDecorator;
>+		}
>+		// Convert left decorator
>+		boolean hasLeftMarginText = false;
>+		if (leftWidgetDecorator != null) {
>+			hasLeftMarginText = true;
>+			// Left margin alignment conversion
>+			leftPrintDecorator = new ConvertedPrintMarginDecorator();
>+			leftPrintDecorator.alignment = leftWidgetDecorator.getAlignment();
>+			switch (leftPrintDecorator.alignment) {
>+			case StyledTextPrintMarginDecorator.FLOAT_INWARD:
>+			case StyledTextPrintMarginDecorator.FORCE_RIGHT:
>+				leftPrintDecorator.alignment = SWT.RIGHT;
>+				break;
>+			case StyledTextPrintMarginDecorator.FLOAT_OUTWARD:
>+			case StyledTextPrintMarginDecorator.FORCE_LEFT:
>+				leftPrintDecorator.alignment = SWT.LEFT;
>+				break;
>+			case StyledTextPrintMarginDecorator.CENTER:
>+				leftPrintDecorator.alignment = SWT.CENTER;
>+			default:
>+				break;
>+			}
>+			convertRemainingDecorator(leftWidgetDecorator, screenDPI, leftPrintDecorator, printerDPI, lineCount, styledText);
>+		}
>+		// Convert right decorator
>+		boolean hasRightMarginText = false;
>+		if (rightWidgetDecorator != null) {
>+			hasRightMarginText = true;
>+			// Right margin alignment conversion.
>+			rightPrintDecorator = new ConvertedPrintMarginDecorator();
>+			rightPrintDecorator.alignment = rightWidgetDecorator.getAlignment();
>+			switch (rightPrintDecorator.alignment) {
>+			case StyledTextPrintMarginDecorator.FLOAT_INWARD:
>+			case StyledTextPrintMarginDecorator.FORCE_LEFT:
>+				rightPrintDecorator.alignment = SWT.LEFT;
>+				break;
>+			case StyledTextPrintMarginDecorator.FLOAT_OUTWARD:
>+			case StyledTextPrintMarginDecorator.FORCE_RIGHT:
>+				rightPrintDecorator.alignment = SWT.RIGHT;
>+				break;
>+			case StyledTextPrintMarginDecorator.CENTER:
>+				rightPrintDecorator.alignment = SWT.CENTER;
>+			default:
>+				break;
>+			}
>+			convertRemainingDecorator(rightWidgetDecorator, screenDPI, rightPrintDecorator, printerDPI, lineCount, styledText);
>+		}
> 		for (int i = 0; i < lineCount; i++) {
>+			// Get margin text
>+			if (hasLeftMarginText)
>+				leftPrintDecorator.marginText[i] = leftWidgetDecorator.getMarginText(i);
>+			if (hasRightMarginText)
>+				rightPrintDecorator.marginText[i] = rightWidgetDecorator.getMarginText(i);
> 			Color color = printerRenderer.getLineBackground(i, null);
> 			if (color != null) {
> 				if (printOptions.printLineBackground) {
>@@ -340,6 +425,100 @@
> 		lineSpacing = styledText.lineSpacing * printerDPI.y / screenDPI.y;
> 	}
> 	/**
>+	 * Creates and returns a text style based on the font and foreground
>+	 * settings.
>+	 * @param styledText the StyledText control being printed
>+	 * @return the default margin text style
>+	 */
>+	TextStyle getDefaultMarginStyle(StyledText styledText) {
>+		if (defaultMarginStyle == null) {
>+			defaultMarginStyle = new TextStyle(styledText.getFont(),
>+				styledText.getForeground(), null);
>+			convertTextStyle(defaultMarginStyle, null, null, null); // null to avoid infinite recursion
>+		}
>+		return defaultMarginStyle;
>+	}
>+	/**
>+	 * Converts a TextStyle from widget appropriate values to printer
>+	 * appropriate values. The passed style is converted in place. The resources
>+	 * cache is utilized and updated.
>+	 * 
>+	 * @param textStyle the text style to convert
>+	 * @param styledText a styled text widget for getting defaults
>+	 * @param screenDPI the x and y DPI for the screen (if null no rise or glyph metric conversion performed)
>+	 * @param printerDPI the x and y DPI for the printer (if null no rise or glyph metric conversion performed)
>+	 */
>+	void convertTextStyle(TextStyle textStyle, StyledText styledText, Point screenDPI, Point printerDPI) {
>+		if (resources == null)
>+			resources = new Hashtable();
>+		if (textStyle.background != null) {
>+			Color printerColor = (Color)resources.get(textStyle.background);
>+			if (printerColor == null) {
>+				printerColor = new Color (printer, textStyle.background.getRGB());
>+				resources.put(textStyle.background, printerColor); 
>+			}
>+			textStyle.background = printerColor;
>+		}
>+		if (textStyle.foreground == null) {
>+			if (styledText != null)
>+				textStyle.foreground = getDefaultMarginStyle(styledText).foreground;
>+		} else {
>+			Color printerColor = (Color)resources.get(textStyle.foreground);
>+			if (printerColor == null) {
>+				printerColor = new Color (printer, textStyle.foreground.getRGB());
>+				resources.put(textStyle.foreground, printerColor); 
>+			}
>+			textStyle.foreground = printerColor;
>+		}
>+		if (textStyle.font == null) {
>+			if (styledText != null)
>+				textStyle.font = getDefaultMarginStyle(styledText).font;
>+		} else {
>+			Font printerFont = (Font)resources.get(textStyle.font);
>+			if (printerFont == null) {
>+				printerFont = new Font (printer, textStyle.font.getFontData());
>+				resources.put(textStyle.font, printerFont);					
>+			}
>+			textStyle.font = printerFont;
>+		}
>+		if ((screenDPI != null) && (printerDPI != null)) {
>+			textStyle.rise = textStyle.rise * printerDPI.y / screenDPI.y;
>+			GlyphMetrics metrics = textStyle.metrics;
>+			if (metrics != null) {
>+				metrics.ascent = metrics.ascent * printerDPI.y / screenDPI.y;
>+				metrics.descent = metrics.descent * printerDPI.y / screenDPI.y;
>+				metrics.width = metrics.width * printerDPI.x / screenDPI.x;
>+			}
>+		}
>+	}
>+	/**
>+	 * Converts the widget decorator to a print decorator except for the
>+	 * alignment. That must be handled separately.
>+	 * 
>+	 * @param widgetDecorator the widget decorator to convert
>+	 * @param screenDPI the screen DPI
>+	 * @param printDecorator the target print decorator
>+	 * @param printerDPI the printer DPI
>+	 * @param lineCount number of lines being printed
>+	 * @param styledText the widget
>+	 */
>+	void convertRemainingDecorator(
>+			StyledTextPrintMarginDecorator widgetDecorator,
>+			Point screenDPI, ConvertedPrintMarginDecorator printDecorator,
>+			Point printerDPI, int lineCount, StyledText styledText) {
>+		// Gutter conversion
>+		printDecorator.gutter = widgetDecorator.getGutter() * printerDPI.x / screenDPI.x;
>+		// Prepare for margin text acquisition
>+		printDecorator.marginText = new String[lineCount];
>+		// Style conversion
>+		printDecorator.marginTextStyle = widgetDecorator.getMarginTextStyle();
>+		if (printDecorator.marginTextStyle == null)
>+			printDecorator.marginTextStyle = getDefaultMarginStyle(styledText);
>+		else
>+			convertTextStyle(printDecorator.marginTextStyle, styledText,
>+					screenDPI, printerDPI);
>+	}
>+	/**
> 	 * Copies the text of the specified <class>StyledTextContent</class>.
> 	 * </p>
> 	 * @param original the <class>StyledTextContent</class> to copy.
>@@ -394,14 +573,40 @@
> 		// one inch margin around text
> 		clientArea.x = dpi.x + trim.x; 				
> 		clientArea.y = dpi.y + trim.y;
>-		clientArea.width -= (clientArea.x + trim.width);
>-		clientArea.height -= (clientArea.y + trim.height); 
>+		// Code in the if branch is the old code for calculating the
>+		// right and bottom margin setting.  It does NOT leave a one
>+		// inch margin as the comment above suggests.  It leaves smaller
>+		// margins.  When implementing margin decoration, I did not want
>+		// to change existing behavior, so if there is no right margin
>+		// decoration, continue to use the old incorrect calculation.
>+		// Otherwise, use a correct calculation in order to leave room
>+		// on the right for the right margin decoration.
>+		if (rightPrintDecorator == null) {
>+			clientArea.width -= (clientArea.x + trim.width);
>+			clientArea.height -= (clientArea.y + trim.height); 
>+		} else {
>+			Rectangle bounds = printer.getBounds();
>+			clientArea.width = bounds.width - (dpi.x * 2);
>+			clientArea.height = bounds.height - (dpi.y * 2);
>+		}
>+		
>+		// Calculate margin rectangles.
>+		if (leftPrintDecorator != null) {
>+			leftPrintDecorator.marginRect = new Rectangle(0, 0, clientArea.x - leftPrintDecorator.gutter, 0);
>+		}
>+		if (rightPrintDecorator != null) {
>+			rightPrintDecorator.marginRect = new Rectangle(clientArea.x + clientArea.width + rightPrintDecorator.gutter, 0, 0, 0);
>+			rightPrintDecorator.marginRect.width = pageWidth - rightPrintDecorator.marginRect.x;
>+		}
> 
> 		int style = mirrored ? SWT.RIGHT_TO_LEFT : SWT.LEFT_TO_RIGHT;
> 		gc = new GC(printer, style);
> 		gc.setFont(printerFont);
> 		printerRenderer.setFont(printerFont, tabLength);
> 		int lineHeight = printerRenderer.getLineHeight();
>+		// TODO is shrinking the client area (increasing the top and bottom
>+		// margin size) the right way to acquire space for the header and
>+		// footer?  These should probably be printed in the existing margin.
> 		if (printOptions.header != null) {
> 			clientArea.y += lineHeight * 2;
> 			clientArea.height -= lineHeight * 2;
>@@ -438,6 +643,25 @@
> 		int page = startPage;
> 		int pageBottom = clientArea.y + clientArea.height;
> 		int orientation =  gc.getStyle() & (SWT.RIGHT_TO_LEFT | SWT.LEFT_TO_RIGHT);
>+		// Create text layout objects suitable for all margin text entries.
>+		TextLayout leftMarginLayout = null;
>+		if (leftPrintDecorator != null) {
>+			leftMarginLayout = new TextLayout(printer);
>+			leftMarginLayout.setAlignment(leftPrintDecorator.alignment);
>+			leftMarginLayout.setFont(leftPrintDecorator.marginTextStyle.font);
>+			//TODO verify orientation setting
>+			if (mirrored) leftMarginLayout.setOrientation(SWT.RIGHT_TO_LEFT);
>+			leftMarginLayout.setWidth(leftPrintDecorator.marginRect.width);
>+		}
>+		TextLayout rightMarginLayout = null;
>+		if (rightPrintDecorator != null) {
>+			rightMarginLayout = new TextLayout(printer);
>+			rightMarginLayout.setAlignment(rightPrintDecorator.alignment);
>+			rightMarginLayout.setFont(rightPrintDecorator.marginTextStyle.font);
>+			//TODO verify orientation setting
>+			if (mirrored) rightMarginLayout.setOrientation(SWT.RIGHT_TO_LEFT);
>+			rightMarginLayout.setWidth(rightPrintDecorator.marginRect.width);
>+		}
> 		
> 		
> 		for (int i = startLine; i <= endLine && page <= endPage; i++) {
>@@ -450,6 +674,8 @@
> 			int paragraphBottom = paintY + layout.getBounds().height; 
> 			if (paragraphBottom <= pageBottom) {
> 				//normal case, the whole paragraph fits in the current page
>+				printMarginDecoration(i, paintY, layout, leftMarginLayout, leftPrintDecorator);
>+				printMarginDecoration(i, paintY, layout, rightMarginLayout, rightPrintDecorator);
> 				printLine(paintX, paintY, gc, foreground, lineBackground, layout);
> 				paintY = paragraphBottom;
> 			} else {
>@@ -467,10 +693,14 @@
> 						printer.startPage();
> 						printDecoration(page, true);
> 						paintY = clientArea.y;
>+						printMarginDecoration(i, paintY, layout, leftMarginLayout, leftPrintDecorator);
>+						printMarginDecoration(i, paintY, layout, rightMarginLayout, rightPrintDecorator);
> 						printLine(paintX, paintY, gc, foreground, lineBackground, layout);
> 						paintY += layout.getBounds().height;
> 					}
> 				} else {
>+					printMarginDecoration(i, paintY, layout, leftMarginLayout, leftPrintDecorator);
>+					printMarginDecoration(i, paintY, layout, rightMarginLayout, rightPrintDecorator);
> 					//draw paragraph top in the current page and paragraph bottom in the next
> 					gc.setClipping(paintX, paintY, clientArea.width, paragraphBottom - paintY);
> 					printLine(paintX, paintY, gc, foreground, lineBackground, layout);
>@@ -481,9 +711,17 @@
> 						printer.startPage();
> 						printDecoration(page, true);
> 						paintY = clientArea.y;
>-						int height = layout.getBounds().height - paragraphBottom;
>+						// This old line was wrong.  paragraphBottom holds the bottom offset
>+						// of what was just printed on the previous page.  This calculation
>+						// leads to a large negative number.
>+						//int height = layout.getBounds().height - paragraphBottom;
>+						// Here is the correction (lineCount holds the number of lines to be printed on the new page).
>+						int totalHeight = layout.getBounds().height;
>+						int height = (int)(totalHeight * ((float)lineCount / layout.getLineCount()));
> 						gc.setClipping(paintX, paintY, clientArea.width, height);
>-						printLine(paintX, paintY, gc, foreground, lineBackground, layout);
>+						// Also needed to adjust the y print point upward.
>+						//printLine(paintX, paintY, gc, foreground, lineBackground, layout);
>+						printLine(paintX, paintY - (totalHeight - height), gc, foreground, lineBackground, layout);
> 						paintY += height;
> 					}
> 					gc.setClipping((Rectangle)null);
>@@ -496,8 +734,46 @@
> 			printDecoration(page, false);
> 			printer.endPage();
> 		}
>+		if (leftMarginLayout != null) leftMarginLayout.dispose();
>+		if (rightMarginLayout != null) rightMarginLayout.dispose();
> 	}
> 	/**
>+	 * Print given margin decoration. Nothing is printed if any of lineLayout,
>+	 * marginLayout and decorator are null.
>+	 * 
>+	 * @param line the line being printed
>+	 * @param lineY the y coordinate of the line
>+	 * @param lineLayout the text layout for the line
>+	 * @param marginLayout the text layout for the margin
>+	 * @param decorator the converted decorator for the margin
>+	 */
>+		void printMarginDecoration(int line, int lineY, TextLayout lineLayout,
>+				TextLayout marginLayout, ConvertedPrintMarginDecorator decorator) {
>+			if ((lineLayout != null) && (marginLayout != null)
>+					&& (decorator != null)) {
>+				String text = decorator.marginText[line];
>+				if ((text != null) && (text.length() > 0)) {
>+					marginLayout.setText(text);
>+					marginLayout.setStyle(decorator.marginTextStyle, 0, text.length() - 1);
>+					FontMetrics lineMetrics = lineLayout.getLineMetrics(0);
>+					FontMetrics marginMetrics = marginLayout.getLineMetrics(0);
>+					int baselineOffset = (lineMetrics.getAscent() + lineMetrics.getLeading())
>+							- (marginMetrics.getAscent() + marginMetrics.getLeading());
>+					int paintY = lineY + Math.max(0, baselineOffset);
>+					if (decorator.marginTextStyle.background != null) {
>+						Rectangle rect = marginLayout.getLineBounds(0);
>+						rect.x = decorator.marginRect.x;
>+						rect.y = paintY;
>+						rect.width = decorator.marginRect.width;
>+						gc.setBackground(decorator.marginTextStyle.background);
>+						gc.fillRectangle(rect);
>+					}
>+					gc.setForeground(decorator.marginTextStyle.foreground);
>+					marginLayout.draw(gc, decorator.marginRect.x, paintY);
>+				}
>+			}
>+		}
>+	/**
> 	 * Print header or footer decorations.
> 	 * 
> 	 * @param page page number to print, if specified in the StyledTextPrintOptions header or footer.
>Index: Eclipse SWT Custom Widgets/common/org/eclipse/swt/custom/StyledTextPrintOptions.java
>===================================================================
>RCS file: /cvsroot/eclipse/org.eclipse.swt/Eclipse SWT Custom Widgets/common/org/eclipse/swt/custom/StyledTextPrintOptions.java,v
>retrieving revision 1.8
>diff -u -r1.8 StyledTextPrintOptions.java
>--- Eclipse SWT Custom Widgets/common/org/eclipse/swt/custom/StyledTextPrintOptions.java	28 Feb 2005 21:56:44 -0000	1.8
>+++ Eclipse SWT Custom Widgets/common/org/eclipse/swt/custom/StyledTextPrintOptions.java	13 Feb 2006 15:48:03 -0000
>@@ -1,5 +1,5 @@
> /*******************************************************************************
>- * Copyright (c) 2000, 2003 IBM Corporation and others.
>+ * Copyright (c) 2000, 2006 IBM Corporation and others.
>  * All rights reserved. This program and the accompanying materials
>  * are made available under the terms of the Eclipse Public License v1.0
>  * which accompanies this distribution, and is available at
>@@ -83,4 +83,21 @@
> 	 * Print the line background color. Default value is <code>false</code>.
> 	 */
> 	public boolean printLineBackground = false;
>+	/**
>+	 * Print lead margin decorator (left margin in left-to-right orientation).
>+	 * See StyledTextPrintMarginDecorator for more information. A
>+	 * <code>null</code> setting means no lead margin text will be printed.
>+	 * 
>+	 * @since 3.2
>+	 */
>+	public StyledTextPrintMarginDecorator printLeadMarginDecorator = null;
>+	/**
>+	 * Print trail margin decorator (right margin in left-to-right orientation).
>+	 * See StyledTextPrintMarginDecorator for more information. A
>+	 * <code>null</code> setting means no trail margin text will be printed.
>+	 * 
>+	 * @since 3.2
>+	 */
>+	public StyledTextPrintMarginDecorator printTrailMarginDecorator = null;
>+	// TODO Should probably add a margin size option.
> }
>Index: Eclipse SWT Custom Widgets/common/org/eclipse/swt/custom/StyledTextPrintMarginDecorator.java
>===================================================================
>RCS file: Eclipse SWT Custom Widgets/common/org/eclipse/swt/custom/StyledTextPrintMarginDecorator.java
>diff -N Eclipse SWT Custom Widgets/common/org/eclipse/swt/custom/StyledTextPrintMarginDecorator.java
>--- /dev/null	1 Jan 1970 00:00:00 -0000
>+++ Eclipse SWT Custom Widgets/common/org/eclipse/swt/custom/StyledTextPrintMarginDecorator.java	1 Jan 1970 00:00:00 -0000
>@@ -0,0 +1,92 @@
>+/*******************************************************************************
>+ * Copyright (c) 2006 IBM Corporation and others.
>+ * All rights reserved. This program and the accompanying materials
>+ * are made available under the terms of the Eclipse Public License v1.0
>+ * which accompanies this distribution, and is available at
>+ * http://www.eclipse.org/legal/epl-v10.html
>+ *
>+ * Contributors:
>+ *     IBM Corporation - initial API and implementation
>+ *******************************************************************************/
>+package org.eclipse.swt.custom;
>+
>+import org.eclipse.swt.graphics.TextStyle;
>+
>+/**
>+ * Use StyledTextPrintMarginDecorator along with StyledTextPrintOptions to
>+ * specify decorators for the lead and trail margins of a StyledText print job
>+ * when using the StyledText.print(Printer, StyledTextPrintOptions) API. The
>+ * StyledTextPrintOptions class includes two properties of this type. One for
>+ * the lead margin and one for the trail.
>+ * 
>+ * @since 3.2
>+ */
>+public interface StyledTextPrintMarginDecorator {
>+	/**
>+	 * Return value for getAlignment. If the text is in the left (not lead)
>+	 * margin the text will be right aligned (floats toward the document text).
>+	 * If the text is in the right (not trail) margin the text will be left
>+	 * aligned (floats toward the document text).
>+	 */
>+	static final int FLOAT_INWARD = 0;
>+
>+	/**
>+	 * Return value for getAlignment. If the text is in the left (not lead)
>+	 * margin the text will be left aligned (floats away from the document
>+	 * text). If the text is in the right (not trail) margin the text will be
>+	 * right aligned (floats away from the document text).
>+	 */
>+	static final int FLOAT_OUTWARD = 1;
>+
>+	/**
>+	 * Return value for getAlignment. Forces left alignment in either margin.
>+	 */
>+	static final int FORCE_LEFT = 2;
>+
>+	/**
>+	 * Return value for getAlignment. Forces right alignment in either margin.
>+	 * This value is particularly useful for line number alignment.
>+	 */
>+	static final int FORCE_RIGHT = 3;
>+
>+	/**
>+	 * Return value for getAlignment. Uses center alignment in either margin.
>+	 */
>+	static final int CENTER = 4;
>+
>+	/**
>+	 * Returns the alignment of the margin text (<code>FLOAT_INWARD</code>,
>+	 * <code>FLOAT_OUTWARD</code>, <code>FORCE_LEFT</code>,
>+	 * <code>FORCE_RIGHT</code>, or <code>CENTER</code>).
>+	 * 
>+	 * @return the alignment
>+	 */
>+	public int getAlignment();
>+
>+	/**
>+	 * Returns the gutter width to be placed between the margin text and the
>+	 * document text. This must be specified in widget DPI. The print job will
>+	 * convert the value to printer DPI.
>+	 */
>+	public int getGutter();
>+
>+	/**
>+	 * The margin text for the print job. Implementations may return
>+	 * <code>null</code> for no text.
>+	 * 
>+	 * @param line the widget line number of the text. Implementors should map
>+	 *            this to their document model line number.
>+	 * @return the text for the margin
>+	 */
>+	public String getMarginText(int line);
>+
>+	/**
>+	 * Implementations may return the style to be used for all margin text. If
>+	 * <code>null</code> is returned, a style derived from the StyledText
>+	 * widget's font and foreground color settings will be used.
>+	 * 
>+	 * @return the style for all margin text
>+	 */
>+	public TextStyle getMarginTextStyle();
>+
>+}

Actions: View | Diff

Attachments on bug 19602: 26998 | 34574 | 34575 | 34576 | 34577 | 59913 | 80953