| javax.swing.JMenuItem de.uka.ilkd.key.gui.nodeviews.DefaultTacletMenuItem
DefaultTacletMenuItem | class DefaultTacletMenuItem extends JMenuItem implements TacletMenuItem(Code) | | this class extends JMenuItem. The objective is to store
the Taclet of each item in the item for easier access to the Taclet
if the item has been selected
|
DefaultTacletMenuItem | public DefaultTacletMenuItem(JMenuItem menu, TacletApp connectedTo, NotationInfo notationInfo)(Code) | | creates TacletMenuItem attached to a Taclet
Parameters: connectedTo - the TacletApp that is represented by the item Parameters: notationInfo - the NotationInfo used to print terms |
ascii2html | protected StringBuffer ascii2html(StringBuffer sb)(Code) | | Replaces <,>,& and new lines with their HTML masks.
Parameters: sb - The StringBuffer with forbidden HTML characters A new StringBuffer with the masked characters. |
|
|