| java.lang.Object
 de.uka.ilkd.key.ocl.gf.RefinementMenu
| RefinementMenu | | class RefinementMenu (Code) | | Takes care of managing the commands, that GF sent,
including subcategories and their menus.
Manages the graphical lists. To display them, they are reachable
via getRefinementListsContainer().
author:
hdaniels |
| Method Summary | |
| protected void | formRefinementMenu(Vector gfCommandVector, String toAppend, GfAstNode currentNode, boolean isAbstract, boolean easyAttributes, LinPosition focusPosition, GfCapsule gfCapsule)
Takes the StringTuples in gfCommandVector, creates the RealCommand
objects for them.
Goes through this list and groups the RealCommands
according to their subcategory tag (which starts with %)
If there is a "(" afterwards, everything until the before last
character in the printname will be used as the display name
for this subcategory. | | protected JSplitPane | getRefinementListsContainer()
| | protected JPopupMenu | producePopup()
Produces the popup menu that represents the current refinements. | | protected void | requestFocus()
| | protected void | reset()
| | protected void | setFont(Font newFont)
|
| popup2 | | public JPopupMenu popup2(Code) | | The cached popup menu containing the same stuff as the refinement list
|
| RefinementMenu | | protected RefinementMenu(GFEditor2 editor)(Code) | | Creates the panels for the refinement (subcat) menu
Parameters:
editor - the editor, that the refinement menu is part of |
| formRefinementMenu | | protected void formRefinementMenu(Vector gfCommandVector, String toAppend, GfAstNode currentNode, boolean isAbstract, boolean easyAttributes, LinPosition focusPosition, GfCapsule gfCapsule)(Code) | | Takes the StringTuples in gfCommandVector, creates the RealCommand
objects for them.
Goes through this list and groups the RealCommands
according to their subcategory tag (which starts with %)
If there is a "(" afterwards, everything until the before last
character in the printname will be used as the display name
for this subcategory. If this displayname is defined a second time,
it will get overwritten.
Sorting is also done here.
Adding additional special commands like InputCommand happens here too.
Parameters:
gfCommandVector - contains all RealCommands, that are availableat the moment
Parameters:
toAppend - will be appended to every command, that is sent to GF.Normally, toAppend will be the empty String "". But it can be a chain command's second part.
Parameters:
isAbstract - If the selected menu language is abstract or not
Parameters:
easyAttributes - if true, attributes of self will be added.
Parameters:
focusPosition - The current position of the focus in the AST. Needed for easy access to properties of self.
Parameters:
gfCapsule - The read/write encapsulation of the GF process.Needed for easy access to properties of self. |
| getRefinementListsContainer | | protected JSplitPane getRefinementListsContainer()(Code) | | Returns the refinementListsContainer,which will contain both JLists. |
| producePopup | | protected JPopupMenu producePopup()(Code) | | Produces the popup menu that represents the current refinements.
An alternative to the refinement list.
s.a. |
| requestFocus | | protected void requestFocus()(Code) | | Requests the focus for the refinement list
|
| reset | | protected void reset()(Code) | | clears the list model
|
| setFont | | protected void setFont(Font newFont)(Code) | | Applies newFont to the visible elements
Parameters:
newFont - The new font, what else? |
|
|