de.uka.ilkd.key.gui.sourceview

Class SourceView

java.lang.Object

java.awt.Component

java.awt.Container

javax.swing.JComponent

de.uka.ilkd.key.gui.sourceview.SourceView

All Implemented Interfaces:

java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable

public final class SourceView
extends javax.swing.JComponent

This class is responsible for showing the source code and visualizing the symbolic execution path of the currently selected node. This is done by adding tabs containing the source code and highlighting the lines which were symbolically executed in the path from the root node down to the current node. In addition, by clicking on such a highlighted line the user can jump to the first node in the proof tree where a statement from this line is symbolically executed. Editing the source code in the tabs is currently not implemented (not supported by JavaDocument).

Author:

Wolfram Pfeifer

See Also:

Serialized Form

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	SourceView.TextPaneMouseAdapter This listener checks if a highlighted section is clicked.

Nested classes/interfaces inherited from class javax.swing.JComponent

javax.swing.JComponent.AccessibleJComponent

Nested classes/interfaces inherited from class java.awt.Container

java.awt.Container.AccessibleAWTContainer

Nested classes/interfaces inherited from class java.awt.Component

java.awt.Component.AccessibleAWTComponent, java.awt.Component.BaselineResizeBehavior, java.awt.Component.BltBufferStrategy, java.awt.Component.FlipBufferStrategy

Field Summary

Fields

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.

Fields inherited from class javax.swing.JComponent

listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW

Fields inherited from class java.awt.Component

accessibleContext, BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT

Fields inherited from interface java.awt.image.ImageObserver

ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SourceView(MainWindow mainWindow) Creates a new JComponent with the given MainWindow and adds change listeners.

Method Summary

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

Methods inherited from class javax.swing.JComponent

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

Methods inherited from class java.awt.Container

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

Methods inherited from class java.awt.Component

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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

instance

private static SourceView instance

the only instance of this singleton

TEXTPANE_TOOLTIP

private static final java.lang.String TEXTPANE_TOOLTIP

ToolTip for the textPanes containing the source code.

See Also:

Constant Field Values

NO_SOURCE

private static final java.lang.String NO_SOURCE

String to display in an empty source code textPane.

See Also:

Constant Field Values

TAB_SIZE

private static final int TAB_SIZE

Indicates how many spaces are inserted instead of one tab (used in source code window).

See Also:

Constant Field Values

NORMAL_HIGHLIGHT_COLOR

private static final java.awt.Color NORMAL_HIGHLIGHT_COLOR

The color of normal highlights in source code (light green).

MOST_RECENT_HIGHLIGHT_COLOR

private static final java.awt.Color MOST_RECENT_HIGHLIGHT_COLOR

The color of the most recent highlight in source code (green).

mainWindow

private final MainWindow mainWindow

The main window of KeY (needed to get the mediator).

tabs

private final javax.swing.JTabbedPane tabs

The container for the tabs containing source code.

textPanes

private final java.util.List<javax.swing.JTextPane> textPanes

Stores the actual textPanes of the tabs. Needed for correct updates when font (size) changes.

sourceStatusBar

private final javax.swing.JLabel sourceStatusBar

The status bar for displaying information about the current proof branch.

files

private java.util.HashMap<java.lang.String,java.io.File> files

HashMap mapping filenames to files (of the current proof!).

hashes

private java.util.HashMap<java.lang.String,java.lang.String> hashes

HashMap mapping filenames to hashes of the content (files of the current proof!).

sources

private java.util.HashMap<java.lang.String,java.lang.String> sources

HashMap mapping filenames to content strings (files of the current proof!).

lines

private java.util.LinkedList<Pair<Node,PositionInfo>> lines

Lines to highlight (contains all highlights of the current proof) and corresponding Nodes.

Constructor Detail

SourceView

private SourceView(MainWindow mainWindow)

Creates a new JComponent with the given MainWindow and adds change listeners.

Parameters:

mainWindow - the MainWindow of the GUI

Method Detail

paintSymbExHighlights

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. The most recently executed line is highlighted with a different color.

Parameters:

textPane - the JTextPane containing the source code

li - precalculated start indices of the lines

filename - the filename corresponding to the given JTextPane

hp - the painter to use for highlighting

paintSelectionHighlight

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.

Parameters:

textPane - the textPane to highlight lines

p - the current position of the mouse pointer

tag - the highlight to change

calculateLineRange

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.

Parameters:

textPane - the JTextPane with the text

p - the point to check

Returns:

the range of text (may be empty if there is just whitespace in the line)

calculateLineRange

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.

Parameters:

textPane - the JTextPane with the text

pos - the position to check

Returns:

the range of text (may be empty if there is just whitespace in the line)

clearCaches

private void clearCaches()

Clears cached files, lines, and existing tabs.

replaceTabs

private static java.lang.String replaceTabs(java.lang.String s)

Replaces each tab in the given String by TAB_SIZE spaces.

Parameters:

s - the String to replace

Returns:

the resulting String (without tabs)

initTextPane

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. In addition, listeners are added and highlights are painted.

Parameters:

entry - the HashMap entry containing the file

fillMaps

private void fillMaps()

Fills the HashMaps containing Files and translations from lines (in source code) to corresponding nodes in proof tree.

getSourceView

public static javax.swing.JComponent getSourceView(MainWindow mainWindow)

Returns the singleton instance of the SourceView.

Parameters:

mainWindow - KeY's main window

Returns:

the component responsible for showing source code and symbolic execution information

updateGUI

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

scrollNestedTextPaneToLine

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. If it exists, JTextPane is scrolled to the given line.

Parameters:

comp - the component of a JTabbedPane

line - the line to scroll to

f - the file of the JTextPane

constructLinesSet

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.

Parameters:

cur - the given node

Returns:

a linked list of pairs of PositionInfo objects containing the start and end positions for the highlighting and Nodes.

joinPositionsRec

private static PositionInfo joinPositionsRec(SourceElement se)

Joins all PositionInfo objects of the given SourceElement and its children.

Parameters:

se - the given SourceElement

Returns:

a new PositionInfo starting at the minimum of all the contained positions and ending at the maximum position

collectPathInformation

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
• ...

Parameters:

node - the current node

Returns:

a String containing the path information to display