Package | Description |
---|---|
de.uka.ilkd.key.gui.sourceview |
Modifier and Type | Method and Description |
---|---|
SourceView.Highlight |
SourceView.addHighlight(java.net.URI fileURI,
int line,
java.awt.Color color,
int level)
Creates a new highlight.
|
Modifier and Type | Method and Description |
---|---|
java.util.Set<SourceView.Highlight> |
SourceView.addHighlightsForJMLStatement(java.net.URI fileURI,
int firstLine,
java.awt.Color color,
int level)
Creates a new set of highlights for a range of lines starting with
firstLine . |
Modifier and Type | Method and Description |
---|---|
void |
SourceView.changeHighlight(SourceView.Highlight highlight,
int newLine)
Moves an existing highlight to another line.
|
int |
SourceView.Highlight.compareTo(SourceView.Highlight other) |
boolean |
SourceView.removeHighlight(SourceView.Highlight highlight)
Removes a highlight.
|
Copyright © 2003-2019 The KeY-Project.