| java.lang.Object de.uka.ilkd.key.ocl.gf.ReadDialog
ReadDialog | class ReadDialog implements ActionListener(Code) | | Takes care of reading in Strings that are to be parsed and terms.
author: daniels |
ReadDialog | protected ReadDialog(GFEditor2 owner)(Code) | | creates a modal dialog
Parameters: owner - The parent for which this dialog shall be modal. |
actionPerformed | public void actionPerformed(ActionEvent ae)(Code) | | the ActionListener method that does the user interaction
|
setFont | protected void setFont(Font font)(Code) | | Sets the font of all GUI elements to font
Parameters: font - |
show | protected void show()(Code) | | Shows this modal dialog.
The previous input text will be there again.
|
|
|