public final class SourceView
extends javax.swing.JComponent
JavaDocument
).Modifier and Type | Class and Description |
---|---|
static class |
SourceView.Highlight
An object of this class represents a highlight of a specific line in the
SourceView . |
javax.swing.JComponent.AccessibleJComponent
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
Modifier and Type | Method and Description |
---|---|
SourceView.Highlight |
addHighlight(java.net.URI fileURI,
int line,
java.awt.Color color,
int level)
Creates a new highlight.
|
java.util.Set<SourceView.Highlight> |
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 . |
void |
changeHighlight(SourceView.Highlight highlight,
int newLine)
Moves an existing highlight to another line.
|
static SourceView |
getSourceView(MainWindow mainWindow)
Returns the singleton instance of the SourceView.
|
void |
openFile(java.net.URI fileURI)
Adds an additional tab for the specified file.
|
void |
openFiles(java.util.Set<java.net.URI> fileURIs)
Adds additional tabs for the specified files.
|
boolean |
removeHighlight(SourceView.Highlight highlight)
Removes a highlight.
|
addAncestorListener, addNotify, addVetoableChangeListener, computeVisibleRect, contains, createToolTip, disable, enable, firePropertyChange, firePropertyChange, firePropertyChange, fireVetoableChange, getActionForKeyStroke, getActionMap, getAlignmentX, getAlignmentY, getAncestorListeners, getAutoscrolls, getBaseline, getBaselineResizeBehavior, getBorder, getBounds, getClientProperty, getComponentGraphics, getComponentPopupMenu, getConditionForKeyStroke, getDebugGraphicsOptions, getDefaultLocale, getFontMetrics, getGraphics, getHeight, getInheritsPopupMenu, getInputMap, getInputMap, getInputVerifier, getInsets, getInsets, getListeners, getLocation, getMaximumSize, getMinimumSize, getNextFocusableComponent, getPopupLocation, getPreferredSize, getRegisteredKeyStrokes, getRootPane, getSize, getToolTipLocation, getToolTipText, getToolTipText, getTopLevelAncestor, getTransferHandler, getUIClassID, getVerifyInputWhenFocusTarget, getVetoableChangeListeners, getVisibleRect, getWidth, getX, getY, grabFocus, hide, isDoubleBuffered, isLightweightComponent, isManagingFocus, isOpaque, isOptimizedDrawingEnabled, isPaintingForPrint, isPaintingOrigin, isPaintingTile, isRequestFocusEnabled, isValidateRoot, paint, paintBorder, paintChildren, paintComponent, paintImmediately, paintImmediately, paramString, print, printAll, printBorder, printChildren, printComponent, processComponentKeyEvent, processKeyBinding, processKeyEvent, processMouseEvent, processMouseMotionEvent, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, removeNotify, removeVetoableChangeListener, repaint, repaint, requestDefaultFocus, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resetKeyboardActions, reshape, revalidate, scrollRectToVisible, setActionMap, setAlignmentX, setAlignmentY, setAutoscrolls, setBackground, setBorder, setComponentPopupMenu, setDebugGraphicsOptions, setDefaultLocale, setDoubleBuffered, setEnabled, setFocusTraversalKeys, setFont, setForeground, setInheritsPopupMenu, setInputMap, setInputVerifier, setMaximumSize, setMinimumSize, setNextFocusableComponent, setOpaque, setPreferredSize, setRequestFocusEnabled, setToolTipText, setTransferHandler, setUI, setVerifyInputWhenFocusTarget, setVisible, unregisterKeyboardAction, update, updateUI
add, add, add, add, add, addContainerListener, addImpl, addPropertyChangeListener, addPropertyChangeListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalKeys, getFocusTraversalPolicy, getLayout, getMousePosition, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, printComponents, processContainerEvent, processEvent, remove, remove, removeAll, removeContainerListener, setComponentZOrder, setFocusCycleRoot, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setLayout, transferFocusDownCycle, validate, validateTree
action, add, addComponentListener, addFocusListener, addHierarchyBoundsListener, addHierarchyListener, addInputMethodListener, addKeyListener, addMouseListener, addMouseMotionListener, addMouseWheelListener, bounds, checkImage, checkImage, coalesceEvents, contains, createImage, createImage, createVolatileImage, createVolatileImage, disableEvents, dispatchEvent, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getAccessibleContext, getBackground, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusCycleRootAncestor, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getForeground, getGraphicsConfiguration, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocale, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getToolkit, getTreeLock, gotFocus, handleEvent, hasFocus, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isPreferredSizeSet, isShowing, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, postEvent, prepareImage, prepareImage, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, resize, resize, setBounds, setBounds, setComponentOrientation, setCursor, setDropTarget, setFocusable, setFocusTraversalKeysEnabled, setIgnoreRepaint, setLocale, setLocation, setLocation, setName, setSize, setSize, show, show, size, toString, transferFocus, transferFocusBackward, transferFocusUpCycle
public static SourceView getSourceView(MainWindow mainWindow)
mainWindow
- KeY's main windowpublic SourceView.Highlight addHighlight(java.net.URI fileURI, int line, java.awt.Color color, int level) throws javax.swing.text.BadLocationException, java.io.IOException
Creates a new highlight.
If the are multiple highlights for a given line, they are drawn on top of each other, starting with the one with the lowest level.
The highlights added by the SourceView
itself have level 0
,
except for the highlight that appears when the user moves the mouse over a line,
which has level Integer.maxValue() - 1
.
fileURI
- the URI of the file in which to create the highlight.line
- the line to highlight.color
- the color to use for the highlight.level
- the level of the highlight.javax.swing.text.BadLocationException
- if the line number is invalid.java.io.IOException
- if the file cannot be read.public java.util.Set<SourceView.Highlight> addHighlightsForJMLStatement(java.net.URI fileURI, int firstLine, java.awt.Color color, int level) throws javax.swing.text.BadLocationException, java.io.IOException
Creates a new set of highlights for a range of lines starting with firstLine
.
This method applies a heuristic to try and highlight the complete JML statement
starting in firstLine
.
fileURI
- the URI of the file in which to create the highlights.firstLine
- the first line to highlight.color
- the color to use for the highlights.level
- the level of the highlights.javax.swing.text.BadLocationException
- if the line number is invalid.java.io.IOException
- if the file cannot be read.public void changeHighlight(SourceView.Highlight highlight, int newLine) throws javax.swing.text.BadLocationException
highlight
- the highlight to change.newLine
- the line to move the highlight to.javax.swing.text.BadLocationException
- if the line number is invalid.public boolean removeHighlight(SourceView.Highlight highlight)
highlight
- the highlight to remove.true
iff
this SourceView
previously contained the specified highlight.public void openFile(java.net.URI fileURI) throws java.io.IOException
fileURI
- the URI of the file to open.java.io.IOException
- if the file cannot be opened.public void openFiles(java.util.Set<java.net.URI> fileURIs) throws java.io.IOException
fileURIs
- the URIs of the files to open.java.io.IOException
- if one of the files cannot be opened.Copyright © 2003-2019 The KeY-Project.