public abstract class SequentView extends JEditorPane
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 |
---|---|
private Object |
additionalJavaHighlight |
private HashMap<Color,DefaultHighlighter.DefaultHighlightPainter> |
color2Highlight |
private ConfigChangeListener |
configChangeListener |
private Object |
currentHighlight |
private Object |
defaultHighlight |
Object |
dndHighlight |
(package private) SequentPrintFilter |
filter |
protected static Color |
INACTIVE_BACKGROUND_COLOR |
private 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 |
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 |
---|
SequentView(MainWindow mainWindow) |
Modifier and Type | Method and Description |
---|---|
void |
addNotify() |
int |
computeLineWidth()
computes the line width
|
int |
correctedViewToModel(Point p)
Return the character index for a certain coordinate.
|
void |
disableHighlight(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() |
Object |
getColorHighlight(Color color)
registers a highlighter that marks the regions specified by the returned
tag with the given color
|
Object |
getCurrentHighlight()
returns the current tag used for highligthing
|
protected Range |
getFirstStatementRange(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.
|
String |
getHighlightedText() |
String |
getHighlightedText(PosInSequent pos) |
(package private) Range |
getHighlightRange(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(Point p)
Get a PosInSequent object for a given coordinate of the displayed
sequent.
|
protected HTMLSyntaxHighlighter |
getSyntaxHighlighter() |
String |
getText()
Returns the plain text of this sequent view.
|
abstract String |
getTitle() |
VisibleTermLabels |
getVisibleTermLabels() |
void |
highlight(Point p) |
(package private) void |
paintHighlight(Range range,
Object highlighter)
highlights the elements in the given range using the specified
highlighter
|
void |
paintHighlights(Point p)
the startposition and endposition+1 of the string to be highlighted
|
abstract void |
printSequent() |
void |
removeHighlight(Object highlight) |
void |
removeNotify() |
void |
setCurrentHighlight(Object tag)
sets the correct highlighter for the given color
|
void |
setFont() |
static void |
setLineWidth(int i) |
protected void |
setLogicPrinter(SequentViewLogicPrinter p)
Set the LogicPrinter to be used.
|
void |
unregisterListener() |
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 Color INACTIVE_BACKGROUND_COLOR
private final MainWindow mainWindow
private static int lineWidth
private final ConfigChangeListener configChangeListener
SequentPrintFilter filter
private SequentViewLogicPrinter printer
private HTMLSyntaxHighlighter syntaxHighlighter
public boolean refreshHighlightning
private final Object defaultHighlight
private Object currentHighlight
private final Object additionalJavaHighlight
public final Object dndHighlight
private final HashMap<Color,DefaultHighlighter.DefaultHighlightPainter> color2Highlight
private 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 JComponent
public void removeNotify()
removeNotify
in class JTextComponent
public void removeHighlight(Object highlight)
void paintHighlight(Range range, Object highlighter)
range
- the Range to be highlightedhighlighter
- the Object painting the highlightpublic final Object getColorHighlight(Color color)
color
- the Color used to highlight regions of the sequentpublic abstract String getTitle()
public String getText()
getText
in class JEditorPane
public PosInSequent getLastPosInSequent()
protected PosInSequent getPosInSequent(Point p)
public SequentViewLogicPrinter getLogicPrinter()
protected void setLogicPrinter(SequentViewLogicPrinter p)
p
- The LogicPrinter to be usedprotected HTMLSyntaxHighlighter getSyntaxHighlighter()
public String getHighlightedText(PosInSequent pos)
public String getHighlightedText()
public int correctedViewToModel(Point p)
public void disableHighlight(Object highlight)
public void disableHighlights()
public void setCurrentHighlight(Object tag)
tag
- the Object used as tag for highlightingpublic Object getCurrentHighlight()
public void paintHighlights(Point p)
p
- the mouse pointer coordinatesRange getHighlightRange(Point p)
protected Range getFirstStatementRange(Point p)
public void highlight(Point p)
public void updateUI()
updateUI
in class JTextComponent
public int computeLineWidth()
public abstract void printSequent()