| java.lang.Object
 de.uka.ilkd.key.ocl.gf.Hmsg
| Hmsg | | class Hmsg (Code) | | The parsed format of the hmsg, that GF sents, if a command in java mode
was prefixed with [something].
And that something gets parsed and stored in this representation.
author:
daniels |
| Constructor Summary | |
| public | Hmsg(String lastRead, String appendix, boolean onceAgain, boolean recurse, boolean newObject, boolean treeChanged, boolean clear)
|
| appendix | | String appendix(Code) | | the String that should be appended to all commands of the
next refinement menu
|
| clear | | boolean clear(Code) | | if the display should be cleared
|
| newObject | | boolean newObject(Code) | | if the newObject flag should be set
|
| onceAgain | | boolean onceAgain(Code) | | If the editor shall probe once again for missing subtyping witnesses.
Unused.
|
| recurse | | boolean recurse(Code) | | If false, no commands are executed automatically
in the next GF reading run
|
| treeChanged | | boolean treeChanged(Code) | | if the command changed the tree, so that it has to be rebuilt
|
| Hmsg | | public Hmsg(String lastRead, String appendix, boolean onceAgain, boolean recurse, boolean newObject, boolean treeChanged, boolean clear)(Code) | | A simple setter constructor
Parameters:
lastRead - The last read line
Parameters:
appendix - the String that should be appended to all commands of the next refinement menu
Parameters:
onceAgain -
Parameters:
recurse - If false, no commands are executed automaticallyin the next GF reading run
Parameters:
newObject - if the newObject flag should be set
Parameters:
treeChanged - if the command changed the tree, so that it has to be rebuilt
Parameters:
clear - if the display should get cleared |
|
|