From 1a100c47e5afb40b37eb96cede64ffa4bb45a510 Mon Sep 17 00:00:00 2001 From: hdaniels Date: Thu, 23 Jun 2005 15:23:32 +0000 Subject: [PATCH] Fixed double r 'refine ...' or even refine 'refine ...' --- .../de/uka/ilkd/key/ocl/gf/GFEditor2.java | 1 + .../de/uka/ilkd/key/ocl/gf/Printname.java | 21 ++++++++++++++++--- .../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,10 +38,15 @@ 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\\$adds the current subtree to the clipboard.
It is offered in the refinement menu if the expected type fits to the one of the current sub-tree."); - 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);