|
| |
|
| javax.swing.JEditorPane
 de.uka.ilkd.key.gui.nodeviews.SequentView
| SequentView | | public class SequentView extends JEditorPane implements Autoscroll(Code) | | The sequent view displays the sequent of an open goal and allows selection of
formulas as well as the application of rules. It offers services for highlighting
formulas, selecting applicable rules (in particular taclets) and drag'n drop
instantiation of taclets.
|
| DEFAULT_HIGHLIGHT_COLOR | | final public static Color DEFAULT_HIGHLIGHT_COLOR(Code) | | |
| UPDATE_HIGHLIGHT_COLOR | | final public static Color UPDATE_HIGHLIGHT_COLOR(Code) | | |
| SequentView | | public SequentView(KeYMediator mediator)(Code) | | creates a viewer for a sequent
Parameters:
mediator - the KeYMediator allowing access to thecurrent system status |
| autoscroll | | public void autoscroll(Point loc)(Code) | | used for autoscrolling when performing drag and drop actions.
Computes the rectangle to be made visible.
|
| correctedViewToModel | | public int correctedViewToModel(Point p)(Code) | | Return the character index for a certain coordinate. The
usual viewToModel is focussed on inter-character spaces, not
characters, so it returns the correct index in the
left half of the glyph but one too many in the right half.
Therefore, we get width of character before the one given
by viewToModel, substract it from the given x value, and get
the character at the new position. That is the correct one.
|
| disableHighlight | | public void disableHighlight(Object highlight)(Code) | | removes highlight by setting it to position (0,0)
|
| disableHighlights | | public void disableHighlights()(Code) | | removes the term and first statement highlighter by setting them to
position (0,0)
|
| getAutoscrollInsets | | public Insets getAutoscrollInsets()(Code) | | used to define the area in which autoscrolling will be
initialized
|
| getColorHighlight | | public Object getColorHighlight(Color color)(Code) | | registers a highlighter that marks the regions specified by the returned
tag with the given color
Parameters:
color - the Color used to highlight regions of the sequent the highlight for the specified color |
| getCurrentHighlight | | public Object getCurrentHighlight()(Code) | | returns the current tag used for highligthing
the current tag used for highlighting |
| getDefaultHighlight | | public Object getDefaultHighlight()(Code) | | returns the default tag used for highligthing
the default tag used for highlighting |
| getFirstStatementRange | | protected synchronized Range getFirstStatementRange(Point p)(Code) | | Get the character range to be highlighted for the first
statement in a java block at the given
coordinate in the displayed sequent. Returns null
if there is no java block there.
|
| getHighlightRange | | synchronized Range getHighlightRange(Point p)(Code) | | Get the character range to be highlighted for the given
coordinate in the displayed sequent.
|
| getLastHighlightedCaretPos | | int getLastHighlightedCaretPos()(Code) | | |
| getPosInSequent | | protected synchronized PosInSequent getPosInSequent(Point p)(Code) | | Get a PosInSequent object for a given coordinate of the
displayed sequent.
|
| mediator | | public KeYMediator mediator()(Code) | | returns the mediator of this view
the KeYMediator |
| modalDragNDropEnabled | | public synchronized boolean modalDragNDropEnabled()(Code) | | Checks whether drag'n'drop of highlighted subterms in the sequent window
currently is enabled..
true iff drag'n'drop is enabled. |
| paintHighlight | | void paintHighlight(Range range, Object highlighter)(Code) | | highlights the elements in the given range using the specified
highlighter
Parameters:
range - the Range to be highlighted
Parameters:
highlighter - the Object painting the highlight |
| paintHighlights | | public void paintHighlights(Point p)(Code) | | the startposition and endposition+1 of the string to be
highlighted
Parameters:
p - the mouse pointer coordinates |
| printSequent | | public synchronized void printSequent()(Code) | | sets the text being printed
|
| printSequentImmediately | | public synchronized void printSequentImmediately()(Code) | | sets the text being printed
|
| printer | | public LogicPrinter printer()(Code) | | return used LogicPrinter
the LogicPrinter that is used |
| removeHighlight | | public void removeHighlight(Object highlight)(Code) | | d a highlighter that marks the regions specified by the returned
tag with the given color
Parameters:
highlight - the Object used as tag for the highlight |
| selectedTaclet | | void selectedTaclet(TacletApp taclet, PosInSequent pos)(Code) | | selected rule to apply
Parameters:
taclet - the selected Taclet
Parameters:
pos - the PosInSequent describes the position where to apply the rule |
| setCurrentHighlight | | public void setCurrentHighlight(Object tag)(Code) | | sets the correct highlighter for the given color
Parameters:
tag - the Object used as tag for highlighting |
| setLastHighlightedCaretPos | | void setLastHighlightedCaretPos(int pos)(Code) | | |
| setModalDragNDropEnabled | | public synchronized void setModalDragNDropEnabled(boolean allowDragNDrop)(Code) | | Enables drag'n'drop of highlighted subterms in the sequent window.
Parameters:
allowDragNDrop - enables drag'n'drop iff set to true. |
| setPrinter | | public void setPrinter(LogicPrinter sp, Sequent s)(Code) | | sets the LogicPrinter to use
Parameters:
sp - the LogicPrinter that is used |
| setPrinter | | public void setPrinter(LogicPrinter sp, SequentPrintFilter f, Sequent s)(Code) | | sets the LogicPrinter to use
Parameters:
sp - the LogicPrinter that is used
Parameters:
f - the SequentPrintFilter that is used |
| updateUI | | public void updateUI()(Code) | | |
| updateUpdateHighlights | | public void updateUpdateHighlights()(Code) | | updates all updateHighlights. Firstly removes all displayed ones and
then gets a new list of updates to highlight
|
|
|
|