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);