public abstract class SequentView
extends javax.swing.JEditorPane
javax.swing.JEditorPane.AccessibleJEditorPane, javax.swing.JEditorPane.AccessibleJEditorPaneHTML, javax.swing.JEditorPane.JEditorPaneAccessibleHypertextSupport
javax.swing.text.JTextComponent.AccessibleJTextComponent, javax.swing.text.JTextComponent.DropLocation, javax.swing.text.JTextComponent.KeyBinding
javax.swing.JComponent.AccessibleJComponent
Modifier and Type | Field and Description |
---|---|
static java.awt.Color |
DND_HIGHLIGHT_COLOR |
java.lang.Object |
dndHighlight |
protected SequentPrintFilter |
filter |
protected static java.awt.Color |
INACTIVE_BACKGROUND_COLOR |
static java.awt.Point |
OUTSIDE_MOUSE_POSITION |
static java.awt.Color |
PERMANENT_HIGHLIGHT_COLOR |
static java.lang.String |
PROP_LAST_MOUSE_POSITION |
boolean |
refreshHighlightning |
protected static java.awt.Color |
UPDATE_HIGHLIGHT_COLOR |
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
Modifier | Constructor and Description |
---|---|
protected |
SequentView(MainWindow mainWindow) |
Modifier and Type | Method and Description |
---|---|
void |
addNotify() |
int |
computeLineWidth()
computes the line width
|
int |
correctedViewToModel(java.awt.Point p)
Return the character index for a certain coordinate.
|
void |
disableHighlight(java.lang.Object highlight)
removes highlight by setting it to position (0,0)
|
void |
disableHighlights()
removes the term and first statement highlighter by setting them to
position (0,0)
|
protected void |
finalize() |
java.lang.Object |
getColorHighlight(java.awt.Color color)
registers a highlighter that marks the regions specified by the returned
tag with the given color
|
java.lang.Object |
getCurrentHighlight()
returns the current tag used for highligthing
|
protected SequentPrintFilter |
getFilter() |
protected Range |
getFirstStatementRange(java.awt.Point p)
Get the character range to be highlighted for the first statement in a
java block at the given coordinate in the displayed sequent.
|
java.lang.String |
getHighlightedText() |
java.lang.String |
getHighlightedText(PosInSequent pos) |
PosInSequent |
getLastPosInSequent()
Get the PosInSequent object for the last observed
and highlighted mouse position.
|
static int |
getLineWidth() |
SequentViewLogicPrinter |
getLogicPrinter()
Return used LogicPrinter.
|
MainWindow |
getMainWindow() |
protected PosInSequent |
getPosInSequent(java.awt.Point p)
Get a PosInSequent object for a given coordinate of the displayed
sequent.
|
protected HTMLSyntaxHighlighter |
getSyntaxHighlighter() |
java.lang.String |
getText()
Returns the plain text of this sequent view.
|
abstract java.lang.String |
getTitle() |
java.lang.String |
getToolTipText(java.awt.event.MouseEvent event) |
VisibleTermLabels |
getVisibleTermLabels() |
void |
highlight(java.awt.Point p) |
boolean |
isHiding()
Does this component hide formulas from the sequent due to the set search
bar filter
|
protected boolean |
isInUserSelectionHighlight(java.awt.Point point) |
boolean |
isMainSequentView() |
void |
paintHighlight(Range range,
java.lang.Object highlighter)
highlights the elements in the given range using the specified
highlighter
|
void |
paintHighlights(java.awt.Point p)
the startposition and endposition+1 of the string to be highlighted
|
abstract void |
printSequent() |
void |
removeHighlight(java.lang.Object highlight) |
void |
removeNotify() |
protected void |
removeUserSelectionHighlight()
Removes the user selection.
|
void |
setCurrentHighlight(java.lang.Object tag)
sets the correct highlighter for the given color
|
void |
setFilter(SequentPrintFilter sequentPrintFilter) |
void |
setFont() |
static void |
setLineWidth(int i) |
protected void |
setLogicPrinter(SequentViewLogicPrinter p)
Set the LogicPrinter to be used.
|
protected void |
setUserSelectionHighlight(java.awt.Point point) |
protected void |
setUserSelectionHighlight(PosInSequent pis)
Highlights the term at the specified position as the user's selection.
|
void |
unregisterListener() |
protected void |
updateHeatMapHighlights()
Updates the head map highlights.
|
protected void |
updateHeatmapSFHighlights(int max_age,
boolean newest)
Highlights sequent formulas according to their age (if newest is false),
or the newest sequent formulas.
|
protected void |
updateHeatmapTermHighlights(int max_age,
boolean newest)
Highlights terms according to their age (if newest is false),
or the newest terms.
|
protected void |
updateHidingProperty()
To update the enclosing components that might print a warning on hidden
formulas, it suffices to repaint them.
|
void |
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, 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
public static final java.awt.Color PERMANENT_HIGHLIGHT_COLOR
public static final java.awt.Color DND_HIGHLIGHT_COLOR
protected static final java.awt.Color UPDATE_HIGHLIGHT_COLOR
protected static final java.awt.Color INACTIVE_BACKGROUND_COLOR
public static final java.lang.String PROP_LAST_MOUSE_POSITION
public static final java.awt.Point OUTSIDE_MOUSE_POSITION
protected SequentPrintFilter filter
public boolean refreshHighlightning
public final java.lang.Object dndHighlight
protected SequentView(MainWindow mainWindow)
public MainWindow getMainWindow()
public static void setLineWidth(int i)
public static int getLineWidth()
public VisibleTermLabels getVisibleTermLabels()
public final void setFont()
public void unregisterListener()
public java.lang.String getToolTipText(java.awt.event.MouseEvent event)
getToolTipText
in class javax.swing.text.JTextComponent
public void addNotify()
addNotify
in class javax.swing.JComponent
public void removeNotify()
removeNotify
in class javax.swing.text.JTextComponent
protected void finalize()
finalize
in class java.lang.Object
public void removeHighlight(java.lang.Object highlight)
public void paintHighlight(Range range, java.lang.Object highlighter)
range
- the Range to be highlightedhighlighter
- the Object painting the highlightpublic final java.lang.Object getColorHighlight(java.awt.Color color)
color
- the Color used to highlight regions of the sequentpublic abstract java.lang.String getTitle()
public java.lang.String getText()
getText
in class javax.swing.JEditorPane
public PosInSequent getLastPosInSequent()
protected PosInSequent getPosInSequent(java.awt.Point p)
public SequentViewLogicPrinter getLogicPrinter()
protected void setLogicPrinter(SequentViewLogicPrinter p)
p
- The LogicPrinter to be usedprotected HTMLSyntaxHighlighter getSyntaxHighlighter()
public java.lang.String getHighlightedText(PosInSequent pos)
public java.lang.String getHighlightedText()
public int correctedViewToModel(java.awt.Point p)
public void disableHighlight(java.lang.Object highlight)
public void disableHighlights()
public void setCurrentHighlight(java.lang.Object tag)
tag
- the Object used as tag for highlightingpublic java.lang.Object getCurrentHighlight()
public void paintHighlights(java.awt.Point p)
p
- the mouse pointer coordinatesprotected Range getFirstStatementRange(java.awt.Point p)
protected void updateHeatMapHighlights()
protected void setUserSelectionHighlight(java.awt.Point point)
protected void removeUserSelectionHighlight()
protected boolean isInUserSelectionHighlight(java.awt.Point point)
point
- a point.true
if and only if the argument points to the user selection.setUserSelectionHighlight(PosInSequent)
,
setUserSelectionHighlight(Point)
,
removeUserSelectionHighlight()
protected void setUserSelectionHighlight(PosInSequent pis)
pis
- the term to select.setUserSelectionHighlight(Point)
,
removeUserSelectionHighlight()
,
isInUserSelectionHighlight(Point)
public void highlight(java.awt.Point p)
public void updateUI()
updateUI
in class javax.swing.text.JTextComponent
public int computeLineWidth()
protected void updateHeatmapSFHighlights(int max_age, boolean newest)
max_age
- maximum age up to which sf's are highlighted, or number of recent sf's to highlight.newest
- Are newest sf's highlighted (true) or all up to max_age (false)?protected void updateHeatmapTermHighlights(int max_age, boolean newest)
max_age
- maximum age up to which terms are highlighted, or number of recent terms to highlight.newest
- Are newest terms highlighted (true) or all up to max_age (false)?public abstract void printSequent()
public void setFilter(SequentPrintFilter sequentPrintFilter)
protected SequentPrintFilter getFilter()
protected void updateHidingProperty()
public boolean isHiding()
public boolean isMainSequentView()
true
if this sequent view is supposed to be shown in the MainFrame
,
false
if it is only supposed to be shown in some other frame.Copyright © 2003-2019 The KeY-Project.