public final class SourceView
extends javax.swing.JComponent
JavaDocument
).Modifier and Type | Class and Description |
---|---|
private class |
SourceView.TextPaneMouseAdapter
This listener checks if a highlighted section is clicked.
|
javax.swing.JComponent.AccessibleJComponent
Modifier and Type | Field and Description |
---|---|
private java.util.HashMap<java.lang.String,java.io.File> |
files
HashMap mapping filenames to files (of the current proof!).
|
private java.util.HashMap<java.lang.String,java.lang.String> |
hashes
HashMap mapping filenames to hashes of the content (files of the current proof!).
|
private static SourceView |
instance
the only instance of this singleton
|
private java.util.LinkedList<Pair<Node,PositionInfo>> |
lines
Lines to highlight (contains all highlights of the current proof) and corresponding Nodes.
|
private MainWindow |
mainWindow
The main window of KeY (needed to get the mediator).
|
private static java.awt.Color |
MOST_RECENT_HIGHLIGHT_COLOR
The color of the most recent highlight in source code (green).
|
private static java.lang.String |
NO_SOURCE
String to display in an empty source code textPane.
|
private static java.awt.Color |
NORMAL_HIGHLIGHT_COLOR
The color of normal highlights in source code (light green).
|
private static long |
serialVersionUID |
private java.util.HashMap<java.lang.String,java.lang.String> |
sources
HashMap mapping filenames to content strings (files of the current proof!).
|
private javax.swing.JLabel |
sourceStatusBar
The status bar for displaying information about the current proof branch.
|
private static int |
TAB_SIZE
Indicates how many spaces are inserted instead of one tab (used in source code window).
|
private javax.swing.JTabbedPane |
tabs
The container for the tabs containing source code.
|
private static java.lang.String |
TEXTPANE_TOOLTIP
ToolTip for the textPanes containing the source code.
|
private java.util.List<javax.swing.JTextPane> |
textPanes
Stores the actual textPanes of the tabs.
|
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
Modifier | Constructor and Description |
---|---|
private |
SourceView(MainWindow mainWindow)
Creates a new JComponent with the given MainWindow and adds change listeners.
|
Modifier and Type | Method and Description |
---|---|
private static Range |
calculateLineRange(javax.swing.JTextPane textPane,
int pos)
Calculates the range of actual text (not whitespace) in the line containing the given
position.
|
private static Range |
calculateLineRange(javax.swing.JTextPane textPane,
java.awt.Point p)
Calculates the range of actual text (not whitespace) in the line under the given point.
|
private void |
clearCaches()
Clears cached files, lines, and existing tabs.
|
private static java.lang.String |
collectPathInformation(Node node)
Collects the information from the tree to which branch the current node belongs:
Invariant Initially Valid
Body Preserves Invariant
Use Case
...
|
private static java.util.LinkedList<Pair<Node,PositionInfo>> |
constructLinesSet(Node cur)
Collects the set of lines to highlight starting from the given node in the proof tree.
|
private void |
fillMaps()
Fills the HashMaps containing Files and translations from lines (in source code) to
corresponding nodes in proof tree.
|
static javax.swing.JComponent |
getSourceView(MainWindow mainWindow)
Returns the singleton instance of the SourceView.
|
private void |
initTextPane(java.util.Map.Entry<java.lang.String,java.io.File> entry)
Initializes a new JTextPane with the source code from the file in the HashMap entry.
|
private static PositionInfo |
joinPositionsRec(SourceElement se)
Joins all PositionInfo objects of the given SourceElement and its children.
|
private static void |
paintSelectionHighlight(javax.swing.JTextPane textPane,
java.awt.Point p,
java.lang.Object tag)
Paints the highlight for the line where the mouse pointer currently points to.
|
private void |
paintSymbExHighlights(javax.swing.JTextPane textPane,
IOUtil.LineInformation[] li,
java.lang.String filename,
javax.swing.text.Highlighter.HighlightPainter hp)
Paints the highlights for symbolically executed lines.
|
private static java.lang.String |
replaceTabs(java.lang.String s)
Replaces each tab in the given String by TAB_SIZE spaces.
|
private static void |
scrollNestedTextPaneToLine(java.awt.Component comp,
int line,
java.io.File f)
Looks for a nested JTextPane in the component of the JTabbedPane.
|
private void |
updateGUI()
Performs an update of the GUI:
updates the TabbedPane with the source files used
highlights the symbolically executed lines
updates the source status bar of the main window with information about the current
branch
|
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
private static final long serialVersionUID
private static SourceView instance
private static final java.lang.String TEXTPANE_TOOLTIP
private static final java.lang.String NO_SOURCE
private static final int TAB_SIZE
private static final java.awt.Color NORMAL_HIGHLIGHT_COLOR
private static final java.awt.Color MOST_RECENT_HIGHLIGHT_COLOR
private final MainWindow mainWindow
private final javax.swing.JTabbedPane tabs
private final java.util.List<javax.swing.JTextPane> textPanes
private final javax.swing.JLabel sourceStatusBar
private java.util.HashMap<java.lang.String,java.io.File> files
private java.util.HashMap<java.lang.String,java.lang.String> hashes
private java.util.HashMap<java.lang.String,java.lang.String> sources
private java.util.LinkedList<Pair<Node,PositionInfo>> lines
private SourceView(MainWindow mainWindow)
mainWindow
- the MainWindow of the GUIprivate void paintSymbExHighlights(javax.swing.JTextPane textPane, IOUtil.LineInformation[] li, java.lang.String filename, javax.swing.text.Highlighter.HighlightPainter hp)
textPane
- the JTextPane containing the source codeli
- precalculated start indices of the linesfilename
- the filename corresponding to the given JTextPanehp
- the painter to use for highlightingprivate static void paintSelectionHighlight(javax.swing.JTextPane textPane, java.awt.Point p, java.lang.Object tag)
textPane
- the textPane to highlight linesp
- the current position of the mouse pointertag
- the highlight to changeprivate static Range calculateLineRange(javax.swing.JTextPane textPane, java.awt.Point p)
textPane
- the JTextPane with the textp
- the point to checkprivate static Range calculateLineRange(javax.swing.JTextPane textPane, int pos)
textPane
- the JTextPane with the textpos
- the position to checkprivate void clearCaches()
private static java.lang.String replaceTabs(java.lang.String s)
s
- the String to replaceprivate void initTextPane(java.util.Map.Entry<java.lang.String,java.io.File> entry)
entry
- the HashMap entry containing the fileprivate void fillMaps()
public static javax.swing.JComponent getSourceView(MainWindow mainWindow)
mainWindow
- KeY's main windowprivate void updateGUI()
private static void scrollNestedTextPaneToLine(java.awt.Component comp, int line, java.io.File f)
comp
- the component of a JTabbedPaneline
- the line to scroll tof
- the file of the JTextPaneprivate static java.util.LinkedList<Pair<Node,PositionInfo>> constructLinesSet(Node cur)
cur
- the given nodeprivate static PositionInfo joinPositionsRec(SourceElement se)
se
- the given SourceElementprivate static java.lang.String collectPathInformation(Node node)
node
- the current node