diff options
| author | hdaniels <unknown> | 2005-06-23 15:23:32 +0000 |
|---|---|---|
| committer | hdaniels <unknown> | 2005-06-23 15:23:32 +0000 |
| commit | 5d6bb705e66343a030ba242175a031e839be2aee (patch) | |
| tree | 859d071f3a4f0560446c5da255666dc3c7bfe811 /src/JavaGUI2/de/uka/ilkd/key | |
| parent | 8dbdf17270e988c93c1dfd642baa76f2f888f8fe (diff) | |
Fixed double r 'refine ...' or even refine 'refine ...'
Diffstat (limited to 'src/JavaGUI2/de/uka/ilkd/key')
| -rw-r--r-- | src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java | 1 | ||||
| -rw-r--r-- | src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java | 21 | ||||
| -rw-r--r-- | src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RealCommand.java | 17 |
3 files changed, 30 insertions, 9 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 4362e9142..02d8d07a4 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java @@ -589,6 +589,7 @@ KeyListener, FocusListener { //Add listener to components that can bring up popup menus.
MouseListener popupListener2 = new PopupListener();
linearizationArea.addMouseListener(popupListener2);
+ htmlLinPane.addMouseListener(popupListener2);
//now for the menus
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 9e4378057..774566e7e 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java @@ -38,11 +38,16 @@ class Printname { public static final Printname delete = new Printname("d", "delete current sub-tree"); public static final Printname addclip = new Printname("ac", "add to clipboard\\$<html>adds the current subtree to the clipboard.<br>It is offered in the refinement menu if the expected type fits to the one of the current sub-tree.</html>"); - public static final Printname printhistory = new Printname("ph", "print history\\$prints all previous command in the linearization area"); + public static final Printname printhistory = new Printname("ph", "peel head\\$removes this fun and moves its first argument at its place instead"); protected final String type; /** + * If the command type will already + * be present in the display name and does not need to be added. + */ + protected final boolean funPresent; + /** * The character that is the borderline between the text that * is to be displayed in the JList and the ToolTip text */ @@ -145,7 +150,8 @@ class Printname { * @param myPrintname the printname given for this function * @param myFullnames the Hashtable for the full names for the category * names for the shortnames like \\%PREDEF - * @param type TODO + * @param type The type of this fun. + * If null, it won't be displayed in the refinement menu. */ public Printname(String myFun, String myPrintname, Hashtable myFullnames, String type) { myFun = myFun.trim(); @@ -153,7 +159,14 @@ class Printname { this.printname = myPrintname; this.subcatNameHashtable = myFullnames; this.type = type; - + if (myFullnames == null) { + //if the menu language is abstract, no fullnames are loaded + //and the fun will be in the used showname + this.funPresent = true; + } else { + this.funPresent = false; + } + //parse the fun name { int index = myFun.indexOf('.'); @@ -244,6 +257,7 @@ class Printname { this.module = ""; this.printname = explanation; this.type = null; + this.funPresent = false; } /** @@ -259,6 +273,7 @@ class Printname { this.module = null; this.printname = bound; this.type = null; + this.funPresent = false; } /** the text that is to be displayed in the refinement lists */ diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RealCommand.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RealCommand.java index 1e4634fd3..c2ba33955 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RealCommand.java +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RealCommand.java @@ -44,6 +44,7 @@ class RealCommand extends GFCommand { public RealCommand(final String myCommand, final HashSet processedSubcats, final PrintnameManager manager, final String myShowText, final boolean mlAbstract) { if (fullnames.isEmpty()) { fullnames.put("w", "wrap"); + fullnames.put("r", "refine"); fullnames.put("ch", "change head"); fullnames.put("rc", "refine from history:"); } @@ -124,12 +125,16 @@ class RealCommand extends GFCommand { /** the text that is to be displayed in the refinement lists */ public String getDisplayText() { String result = ""; - if (fullnames.containsKey(this.commandType)) { - result = fullnames.get(this.commandType) + " '"; - } - result = result + this.printname.getDisplayText(); - if (fullnames.containsKey(this.commandType)) { - result = result + "'"; + if (this.printname.funPresent) { + result = this.printname.getDisplayText(); + } else { + if (fullnames.containsKey(this.commandType)) { + result = fullnames.get(this.commandType) + " '"; + } + result = result + this.printname.getDisplayText(); + if (fullnames.containsKey(this.commandType)) { + result = result + "'"; + } } if (this.commandType.equals("w")) { String insertion = " as argument " + (this.argument + 1); |