diff options
Diffstat (limited to 'src/JavaGUI2/de/uka/ilkd/key/ocl')
| -rw-r--r-- | src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java | 43 | ||||
| -rw-r--r-- | src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java | 9 |
2 files changed, 45 insertions, 7 deletions
diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java index 5f3bc0a59..4362e9142 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java @@ -217,7 +217,9 @@ KeyListener, FocusListener { private JButton right = new JButton(">");
/** Moving the focus to the next metavariable */
private JButton rightMeta = new JButton(">?");
- private JLabel actionOnSubterm = new JLabel("Select Action on Subterm");
+ private final static String actionOnSubtermString = "Select Action on Subterm";
+ private JLabel subtermNameLabel = new JLabel();
+ private JLabel subtermDescLabel = new JLabel();
/** Refining with term or linearization from typed string or file */
private JButton read = new JButton("Read");
// private JButton parse = new JButton("Parse");
@@ -249,7 +251,7 @@ KeyListener, FocusListener { /** the panel that contains only the navigation buttons */
private JPanel middlePanelUp = new JPanel();
/** the panel that vontains the the explanatory text for the refinement menu */
- private JPanel middlePanelDown = new JPanel();
+ private JPanel middlePanelDown = new JPanel(new BorderLayout());
/** splits between tree and lin above and nav buttons and refinements below */
private JSplitPane centerPanel;
/** the window that contains the refinements when in split mode */
@@ -1071,7 +1073,8 @@ KeyListener, FocusListener { middlePanelUp.add(top);
middlePanelUp.add(right);
middlePanelUp.add(rightMeta);
- middlePanelDown.add(actionOnSubterm);
+ middlePanelDown.add(subtermNameLabel, BorderLayout.WEST);
+ middlePanelDown.add(subtermDescLabel, BorderLayout.CENTER);
middlePanel.setLayout(new BorderLayout());
middlePanel.add(middlePanelUp, BorderLayout.NORTH);
middlePanel.add(middlePanelDown, BorderLayout.CENTER);
@@ -2444,7 +2447,8 @@ KeyListener, FocusListener { top.setFont(newFont);
right.setFont(newFont);
rightMeta.setFont(newFont);
- actionOnSubterm.setFont(newFont);
+ subtermDescLabel.setFont(newFont);
+ subtermNameLabel.setFont(newFont);
read.setFont(newFont);
alpha.setFont(newFont);
random.setFont(newFont);
@@ -2630,13 +2634,13 @@ KeyListener, FocusListener { if (!node.isMeta()) {
childPrintname = this.printnameManager.getPrintname(node.getFun());
}
+ Printname parentPrintname = null;
if (childPrintname != null) {
//we know this one
and = new RefinedAstNodeData(childPrintname, node);
} else if (parent != null && node.isMeta()) {
//new child without refinement
AstNodeData parentAnd = (AstNodeData)parent.getUserObject();
- Printname parentPrintname = null;
if (parentAnd != null) {
parentPrintname = parentAnd.getPrintname();
}
@@ -2677,6 +2681,27 @@ KeyListener, FocusListener { if (treeLogger.isLoggable(Level.FINER)) {
treeLogger.finer("new selected index "+ index);
}
+
+ // set the description of the crrent parameter to a more
+ // prominent place
+ String paramName = null;
+ int paramPosition = -1;
+ if (parentPrintname != null) {
+ paramPosition = parent.getChildCount() - 1;
+ paramName = parentPrintname.getParamName(paramPosition);
+ }
+ if (paramName == null) {
+ subtermNameLabel.setText(actionOnSubtermString);
+ subtermDescLabel.setText("");
+ } else {
+ subtermNameLabel.setText("<html><b>" + paramName + ": </b></html>");
+ String paramDesc = parentPrintname.getParamDescription(paramPosition);
+ if (paramDesc == null) {
+ subtermDescLabel.setText("");
+ } else {
+ subtermDescLabel.setText("<html>" + paramDesc + "</html>");
+ }
+ }
}
}
}
@@ -3615,7 +3640,9 @@ KeyListener, FocusListener { File file = fc.getSelectedFile();
// importing a new grammar :
newObject = false;
- statusLabel.setText(status);
+ statusLabel.setText(status);
+ subtermDescLabel.setText("");
+ subtermNameLabel.setText("");
listModel.clear();
resetTree(tree);
resetNewCategoryMenu();
@@ -3654,7 +3681,9 @@ KeyListener, FocusListener { public void actionPerformed(ActionEvent e) {
newObject = false;
- statusLabel.setText(status);
+ statusLabel.setText(status);
+ subtermDescLabel.setText("");
+ subtermNameLabel.setText("");
listModel.clear();
resetTree(tree);
langMenuModel.resetLanguages();
diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java index 36250422a..9e4378057 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java @@ -429,6 +429,15 @@ class Printname { String result = "<html><dl>" + text + "</dl></html>"; return result; } + /** + * looks up the description for parameter number 'which' and returns it. + * Returns null, if no parameter description is present. + * @param which The number of the parameter + * @return s.a. + */ + public String getParamDescription(int which) { + return (String)paramTexts.get(which); + } /** * wraps all parameters together with their explanatory text into |