com.borland.primetime.editor
Class BookmarkManager.EditorMark
java.lang.Object
|
+--com.borland.primetime.editor.LineMark
|
+--com.borland.primetime.editor.GutterMark
|
+--com.borland.primetime.editor.BookmarkManager.EditorMark
- Enclosing class:
- BookmarkManager
- protected class BookmarkManager.EditorMark
- extends GutterMark
This class is an extension of GutterMark that represents a particular
bookmark within the editor.
Methods inherited from class com.borland.primetime.editor.LineMark |
addEditor, displayInEditor, getDocument, getMarkLine, getStyle, isLightweight, removeEditor, removeEditor, removeEditor, setDisplayPriority, setDocument, setStyle |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
BookmarkManager.EditorMark
public BookmarkManager.EditorMark(javax.swing.Icon icon)
- Create a new EditorMark with the specified icon.
- Parameters:
icon
- The icon to use when the mark is displayed in the gutter.
setEditor
public void setEditor(EditorPane editor)
getEditor
public EditorPane getEditor()
setPosition
public void setPosition(javax.swing.text.Position pos)
getPosition
public javax.swing.text.Position getPosition()
getDisplayPriority
public int getDisplayPriority()
- Description copied from class:
LineMark
- Describes the logical priority this mark belongs to for ordering purposes.
Marks with a higher priority paint over marks with a lower priority, if
both are on the same line.
For reference, here are some of the defined priority values:
- Executable Line: 100
- Bookmark: 300
- Unspecified:500
- DisabledBreakpoint: 400
- InvalidBreakpoint: 650
- VerifiedBreakpoint: 700
- Execution point: 800
- Overrides:
getDisplayPriority
in class LineMark
- Following copied from class:
com.borland.primetime.editor.LineMark
- Returns:
- An int value specifying the display priority of this mark.