public class InnerNodeView extends SequentView
JEditorPane.AccessibleJEditorPane, JEditorPane.AccessibleJEditorPaneHTML, JEditorPane.JEditorPaneAccessibleHypertextSupport
JTextComponent.AccessibleJTextComponent, JTextComponent.DropLocation, JTextComponent.KeyBinding
JComponent.AccessibleJComponent
Container.AccessibleAWTContainer
Component.AccessibleAWTComponent, Component.BaselineResizeBehavior, Component.BltBufferStrategy, Component.FlipBufferStrategy
Modifier and Type | Field and Description |
---|---|
(package private) static Highlighter.HighlightPainter |
IF_FORMULA_HIGHLIGHTER |
(package private) Node |
node |
private InitialPositionTable |
posTable |
(package private) static Highlighter.HighlightPainter |
RULEAPP_HIGHLIGHTER |
private static long |
serialVersionUID |
JTextArea |
tacletInfo |
dndHighlight, filter, INACTIVE_BACKGROUND_COLOR, refreshHighlightning
HONOR_DISPLAY_PROPERTIES, W3C_LENGTH_UNITS
DEFAULT_KEYMAP, FOCUS_ACCELERATOR_KEY
accessibleContext, listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH
Constructor and Description |
---|
InnerNodeView(Node node,
MainWindow mainWindow) |
Modifier and Type | Method and Description |
---|---|
String |
getTacletDescription(KeYMediator mediator,
Node node,
SequentPrintFilter filter)
Computes the text to show in this
JTextArea which consists of the
sequent including the applied rule. |
String |
getTitle() |
private void |
highlightIfFormulas(TacletApp tapp) |
private void |
highlightIfInsts(IBuiltInRuleApp bapp) |
private Range |
highlightPos(PosInOccurrence pos,
Highlighter.HighlightPainter light) |
private void |
highlightRuleAppPosition(RuleApp app) |
void |
printSequent() |
private static void |
writeSVModifiers(StringBuffer out,
SchemaVariable sv) |
private static void |
writeTacletSchemaVariable(StringBuffer out,
SchemaVariable schemaVar) |
private static void |
writeTacletSchemaVariablesHelper(StringBuffer out,
Taclet t) |
addNotify, computeLineWidth, correctedViewToModel, disableHighlight, disableHighlights, finalize, getColorHighlight, getCurrentHighlight, getFirstStatementRange, getHighlightedText, getHighlightedText, getHighlightRange, getLastPosInSequent, getLineWidth, getLogicPrinter, getMainWindow, getPosInSequent, getSyntaxHighlighter, getText, getVisibleTermLabels, highlight, paintHighlight, paintHighlights, removeHighlight, removeNotify, setCurrentHighlight, setFont, setLineWidth, setLogicPrinter, unregisterListener, updateUI
addHyperlinkListener, createDefaultEditorKit, createEditorKitForContentType, fireHyperlinkUpdate, getAccessibleContext, getContentType, getEditorKit, getEditorKitClassNameForContentType, getEditorKitForContentType, getHyperlinkListeners, getPage, getPreferredSize, getScrollableTracksViewportHeight, getScrollableTracksViewportWidth, getStream, getUIClassID, paramString, read, registerEditorKitForContentType, registerEditorKitForContentType, removeHyperlinkListener, replaceSelection, scrollToReference, setContentType, setEditorKit, setEditorKitForContentType, setPage, setPage, setText
addCaretListener, addInputMethodListener, addKeymap, copy, cut, fireCaretUpdate, getActions, getCaret, getCaretColor, getCaretListeners, getCaretPosition, getDisabledTextColor, getDocument, getDragEnabled, getDropLocation, getDropMode, getFocusAccelerator, getHighlighter, getInputMethodRequests, getKeymap, getKeymap, getMargin, getNavigationFilter, getPreferredScrollableViewportSize, getPrintable, getScrollableBlockIncrement, getScrollableUnitIncrement, getSelectedText, getSelectedTextColor, getSelectionColor, getSelectionEnd, getSelectionStart, getText, getToolTipText, getUI, isEditable, loadKeymap, modelToView, moveCaretPosition, paste, print, print, print, processInputMethodEvent, read, removeCaretListener, removeKeymap, restoreComposedText, saveComposedText, select, selectAll, setCaret, setCaretColor, setCaretPosition, setComponentOrientation, setDisabledTextColor, setDocument, setDragEnabled, setDropMode, setEditable, setFocusAccelerator, setHighlighter, setKeymap, setMargin, setNavigationFilter, setSelectedTextColor, setSelectionColor, setSelectionEnd, setSelectionStart, setUI, viewToModel, write
addAncestorListener, 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, getRegisteredKeyStrokes, getRootPane, getSize, getToolTipLocation, getToolTipText, getTopLevelAncestor, getTransferHandler, getVerifyInputWhenFocusTarget, getVetoableChangeListeners, getVisibleRect, getWidth, getX, getY, grabFocus, hide, isDoubleBuffered, isLightweightComponent, isManagingFocus, isOpaque, isOptimizedDrawingEnabled, isPaintingForPrint, isPaintingOrigin, isPaintingTile, isRequestFocusEnabled, isValidateRoot, paint, paintBorder, paintChildren, paintComponent, paintImmediately, paintImmediately, print, printAll, printBorder, printChildren, printComponent, processComponentKeyEvent, processKeyBinding, processKeyEvent, processMouseEvent, processMouseMotionEvent, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, 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
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, addKeyListener, addMouseListener, addMouseMotionListener, addMouseWheelListener, bounds, checkImage, checkImage, coalesceEvents, contains, createImage, createImage, createVolatileImage, createVolatileImage, disableEvents, dispatchEvent, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getBackground, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusCycleRootAncestor, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getForeground, getGraphicsConfiguration, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, 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, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, resize, resize, setBounds, setBounds, setCursor, setDropTarget, setFocusable, setFocusTraversalKeysEnabled, setIgnoreRepaint, setLocale, setLocation, setLocation, setName, setSize, setSize, show, show, size, toString, transferFocus, transferFocusBackward, transferFocusUpCycle
private static final long serialVersionUID
private InitialPositionTable posTable
public final JTextArea tacletInfo
Node node
static final Highlighter.HighlightPainter RULEAPP_HIGHLIGHTER
static final Highlighter.HighlightPainter IF_FORMULA_HIGHLIGHTER
public InnerNodeView(Node node, MainWindow mainWindow)
private static void writeSVModifiers(StringBuffer out, SchemaVariable sv)
private static void writeTacletSchemaVariable(StringBuffer out, SchemaVariable schemaVar)
private static void writeTacletSchemaVariablesHelper(StringBuffer out, Taclet t)
public final String getTacletDescription(KeYMediator mediator, Node node, SequentPrintFilter filter)
Computes the text to show in this JTextArea
which consists of the
sequent including the applied rule.
This information is also relevant for other tools like the Symbolic Execution Debugger.
mediator
- The KeYMediator
to use.node
- The Node
to use.filter
- The SequentPrintFilter
to use.private void highlightRuleAppPosition(RuleApp app)
private void highlightIfFormulas(TacletApp tapp) throws BadLocationException
tapp
- The taclet app for which the if formulae should be
highlighted.BadLocationException
private void highlightIfInsts(IBuiltInRuleApp bapp) throws BadLocationException
BadLocationException
private Range highlightPos(PosInOccurrence pos, Highlighter.HighlightPainter light) throws BadLocationException
pos
- the PosInOccurrence that should be highlighted.light
- the painter for the highlight.BadLocationException
public String getTitle()
getTitle
in class SequentView
public final void printSequent()
printSequent
in class SequentView