public abstract class SequentView
extends javax.swing.JEditorPane
Modifier and Type | Class and Description |
---|---|
(package private) class |
SequentView.PIO_age
Utility class consisting of a pair of the PosInOccurrence of a term, and its age.
|
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 |
---|---|
private java.lang.Object |
additionalJavaHighlight |
private java.util.HashMap<java.awt.Color,javax.swing.text.Highlighter.HighlightPainter> |
color2Highlight |
private ConfigChangeListener |
configChangeListener |
private java.lang.Object |
currentHighlight |
private java.lang.Object |
defaultHighlight |
java.lang.Object |
dndHighlight |
protected SequentPrintFilter |
filter |
private static java.awt.Color |
HEATMAP_COLOR |
private static float |
HEATMAP_DEFAULT_START_OPACITY |
protected static java.awt.Color |
INACTIVE_BACKGROUND_COLOR |
private java.awt.Point |
lastMousePosition
the last observed mouse position for which a highlight was created
|
private static int |
lineWidth |
private MainWindow |
mainWindow |
private SequentViewLogicPrinter |
printer |
boolean |
refreshHighlightning |
private static long |
serialVersionUID |
private HTMLSyntaxHighlighter |
syntaxHighlighter |
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
Constructor and Description |
---|
SequentView(MainWindow mainWindow) |
Modifier and Type | Method and Description |
---|---|
void |
addNotify() |
private java.awt.Color |
computeColorForAge(int max_age,
int age)
computes the appropriate color for a given age and maximum age.
|
int |
computeLineWidth()
computes the line width
|
private int |
computeSeqFormulaAge(Node node,
SequentFormula form,
int max_age)
computes the age of a given sequent formula, i.e.,
its distance to the root of the proof tree.
|
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) |
(package private) Range |
getHighlightRange(java.awt.Point p)
Get the character range to be highlighted for the given coordinate in the
displayed sequent.
|
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() |
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
|
(package private) 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() |
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.
|
void |
unregisterListener() |
protected void |
updateHeatMapHighlights() |
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, 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
protected static final java.awt.Color INACTIVE_BACKGROUND_COLOR
private static final java.awt.Color HEATMAP_COLOR
private static final float HEATMAP_DEFAULT_START_OPACITY
private final MainWindow mainWindow
private static int lineWidth
private final ConfigChangeListener configChangeListener
protected SequentPrintFilter filter
private SequentViewLogicPrinter printer
private HTMLSyntaxHighlighter syntaxHighlighter
public boolean refreshHighlightning
private final java.lang.Object defaultHighlight
private java.lang.Object currentHighlight
private final java.lang.Object additionalJavaHighlight
public final java.lang.Object dndHighlight
private final java.util.HashMap<java.awt.Color,javax.swing.text.Highlighter.HighlightPainter> color2Highlight
private java.awt.Point lastMousePosition
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 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)
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 coordinatesRange getHighlightRange(java.awt.Point p)
protected Range getFirstStatementRange(java.awt.Point p)
protected void updateHeatMapHighlights()
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)?private java.awt.Color computeColorForAge(int max_age, int age)
max_age
- the maximum age of a term / sf, specified in viewsettingsage
- the age of the given term / sfprivate int computeSeqFormulaAge(Node node, SequentFormula form, int max_age)
node
- the current nodeform
- the given sfmax_age
- the maximum age, specified in viewSettingspublic abstract void printSequent()
public void setFilter(SequentPrintFilter sequentPrintFilter)
protected SequentPrintFilter getFilter()
protected void updateHidingProperty()
public boolean isHiding()