typed menu entries even with printnames, on exit one is asked if 'text' instead of 'constraint' should be saved

src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java

@@ -276,9 +276,16 @@ KeyListener, FocusListener {
         private JMenu fileMenu= new JMenu("File");
         /** stores whether the refinement list should be in 'long' format */
         private JRadioButtonMenuItem rbMenuItemLong;
+        /** stores whether the refinement list should be in 'short' format */
+        private JRadioButtonMenuItem rbMenuItemShort;
         // private JRadioButtonMenuItem rbMenuItemAbs;
         /** stores whether the refinement list should be in 'untyped' format */
         private JRadioButtonMenuItem rbMenuItemUnTyped;
+        /** 
+         * linked to rbMenuItemUnTyped. 
+         * Is true if type information should be appended in the refinement menu
+         */
+        private boolean typedMenuItems = false;
         /** stores whether the AST is visible or not */
         private JCheckBoxMenuItem treeCbMenuItem;
         /** in the save dialog whether to save as a Term or as linearized Text */
@@ -523,7 +530,7 @@ KeyListener, FocusListener {
          */
         private void resetPrintnames(boolean replayState) {
                 this.printnameManager = new PrintnameManager();
-                PrintnameLoader pl = new PrintnameLoader(this.fromProc, this.toProc, this.printnameManager);
+                PrintnameLoader pl = new PrintnameLoader(this.fromProc, this.toProc, this.printnameManager, this.typedMenuItems);
                 if (!selectedMenuLanguage.equals("Abstract")) {
                         String sendString = selectedMenuLanguage;
                         pl.readPrintnames(sendString);
@@ -766,16 +773,16 @@ KeyListener, FocusListener {
                 menuGroup = new ButtonGroup();
                 rbMenuItemLong = new JRadioButtonMenuItem("long");
                 rbMenuItemLong.setActionCommand("long");
-                rbMenuItemLong.setSelected(true);
                 rbMenuItemLong.addActionListener(longShortListener);
                 menuGroup.add(rbMenuItemLong);
                 modeMenu.add(rbMenuItemLong);
-                rbMenuItem = new JRadioButtonMenuItem("short");
+                rbMenuItemShort = new JRadioButtonMenuItem("short");
-                rbMenuItem.setActionCommand("short");
+                rbMenuItemShort.setActionCommand("short");
-                rbMenuItem.addActionListener(longShortListener);
+                rbMenuItemShort.setSelected(true);
-                menuGroup.add(rbMenuItem);
+                rbMenuItemShort.addActionListener(longShortListener);
-                modeMenu.add(rbMenuItem);
+                menuGroup.add(rbMenuItemShort);
-                modeMenu.addSeparator();              
+                modeMenu.add(rbMenuItemShort);
+                modeMenu.addSeparator();
                 
                 /**
                  * switches GF to either display the refinement menu with or 
@@ -786,6 +793,12 @@ KeyListener, FocusListener {
                                 String action = e.getActionCommand();
                                 if ((action.equals("typed")) || (action.equals("untyped"))) {
                                         send("mt " + action);
+                                        if ((action.equals("typed"))) {
+                                                typedMenuItems = true;
+                                        } else {
+                                                typedMenuItems = false;
+                                        }
+                                        resetPrintnames(true);
                                         return;
                                 } else {
                                         logger.error("RadioListener on wrong object: " + action + "should either be 'typed' or 'untyped'");
@@ -1617,7 +1630,18 @@ KeyListener, FocusListener {
          * possibly sending something back to KeY 
          */
         protected void endProgram(){
-                int returnStatus = JOptionPane.showConfirmDialog(this, "Save constraint?", "Save before quitting?", JOptionPane.YES_NO_CANCEL_OPTION, JOptionPane.QUESTION_MESSAGE  );
+                String saveQuestion;
+                if (this.callback == null) {
+                        saveQuestion = "Save text before exiting?";
+                } else {
+                        saveQuestion = "Save constraint before exiting?";
+                }
+                int returnStatus;
+                if (this.newObject) {
+                        returnStatus = JOptionPane.showConfirmDialog(this, saveQuestion, "Save before quitting?", JOptionPane.YES_NO_CANCEL_OPTION, JOptionPane.QUESTION_MESSAGE  );
+                } else {
+                        returnStatus = JOptionPane.NO_OPTION;
+                }
                 if (returnStatus == JOptionPane.CANCEL_OPTION) {
                         return;
                 } else if (returnStatus == JOptionPane.NO_OPTION) {
@@ -3572,8 +3596,9 @@ KeyListener, FocusListener {
                                         resetNewCategoryMenu();                                        
                                         langMenuModel.resetLanguages();
                                         selectedMenuLanguage = "Abstract";
-                                        rbMenuItemLong.setSelected(true);
+                                        rbMenuItemShort.setSelected(true);
                                         rbMenuItemUnTyped.setSelected(true);
+                                        typedMenuItems = false;
                                         
                                         fileString="";
                                         grammar.setText("No Topic          ");
@@ -3611,8 +3636,9 @@ KeyListener, FocusListener {
                                 resetNewCategoryMenu();
                                 selectedMenuLanguage = "Abstract";
                                 
-                                rbMenuItemLong.setSelected(true);
+                                rbMenuItemShort.setSelected(true);
                                 rbMenuItemUnTyped.setSelected(true);
+                                typedMenuItems = false;
                                 
                                 fileString="";
                                 grammar.setText("No Topic          ");

src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java

@@ -11,11 +11,11 @@ import org.apache.log4j.Logger;
  * A Printname allows easy access for all the information that is crammed
  * into a printname in the GF grammars.
  * This information consists of (in this order!)
- *   The tooltip text which is started with $
+ *   The tooltip text which is started with \\$
- * 	 The subcategory which is started with %
+ * 	 The subcategory which is started with \\%
  *   The longer explanation for the subcategory which directly follows the
  *     subcategory and is put into parantheses
- *   The parameter descriptions, which start with #name and is followed
+ *   The parameter descriptions, which start with \\#name and is followed
  *     by their actual description.
  * HTML can be used inside the descriptions and the tooltip text 
  */
@@ -25,6 +25,8 @@ 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");
+        
+        protected final String type;
 
         /** 
          * The character that is the borderline between the text that
@@ -128,13 +130,15 @@ class Printname {
          * @param myFun the function name
          * @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
+         * names for the shortnames like \\%PREDEF
+         * @param type TODO
          */
-        public Printname(String myFun, String myPrintname, Hashtable myFullnames) {
+        public Printname(String myFun, String myPrintname, Hashtable myFullnames, String type) {
                 myFun = myFun.trim();
                 myPrintname = myPrintname.trim();
                 this.printname = myPrintname;
                 this.subcatNameHashtable = myFullnames;
+                this.type = type;
 
                 //parse the fun name
                 {
@@ -225,6 +229,7 @@ class Printname {
                 this.subcat = null;
                 this.module = "";
                 this.printname = explanation;
+                this.type = null;
         }
         
         /**
@@ -238,7 +243,8 @@ class Printname {
                 this.subcatNameHashtable =  null;
                 this.subcat = null;
                 this.module = null;
-                this.printname = bound + "$insert the bound variable" + bound;
+                this.printname = bound;
+                this.type = null;
         }
         
         /** the text that is to be displayed in the refinement lists */
@@ -277,7 +283,7 @@ class Printname {
          * @return the tooltip
          */
         public static String extractTooltipText(String myPrintname) {
-                //if the description part of the fun has no \$ to denote a tooltip,
+                //if the description part of the fun has no \\$ to denote a tooltip,
                 //but the subcat description has one, than we must take extra
                 //caution
                 final int indTT = Utils.indexOfNotEscaped(myPrintname, TT_START);
@@ -439,7 +445,7 @@ class Printname {
                 String SandS = "boolean 'and' for sentences$true iff both of the two given sentences is equivalent to true%BOOL#alpha the first of the two and-conjoined sentences#beta the second of the and-conjoined sentences";
                 String FandS = "andS";
                 Hashtable ht = new Hashtable();
-                Printname pn = new Printname(FandS, SandS, ht);
+                Printname pn = new Printname(FandS, SandS, ht, null);
                 System.out.println(pn);
                 for (int i = 0; i < pn.paramNames.size(); i++) {
                         System.out.println(pn.htmlifySingleParam(i));
@@ -447,7 +453,7 @@ class Printname {
                 System.out.println(pn.getTooltipText());
                 SandS = "boolean 'and' for sentences$true iff both of the two given sentences is equivalent to true%BOOL";
                 FandS = "andS";
-                pn = new Printname(FandS, SandS, ht);
+                pn = new Printname(FandS, SandS, ht, null);
                 System.out.println("*" + pn.getTooltipText());
         }
         

src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameLoader.java

@@ -3,27 +3,31 @@ package de.uka.ilkd.key.ocl.gf;
 import java.io.BufferedReader;
 import java.io.BufferedWriter;
 import java.io.IOException;
-
+import java.util.Hashtable;
 import org.apache.log4j.Logger;
 
 /**
  * @author daniels
- *
+ * asks GF to print all available printnames, parses that list and generates
- * TODO To change the template for this generated type comment go to
+ * the suiting Printname objects.
- * Window - Preferences - Java - Code Style - Code Templates
  */
 public class PrintnameLoader extends AbstractProber {
         protected final PrintnameManager printnameManager;
-        protected static Logger nogger = Logger.getLogger(Printname.class.getName());
+        protected final static Logger nogger = Logger.getLogger(Printname.class.getName());
+        protected final Hashtable funTypes = new Hashtable();
+        protected final boolean loadTypes;
         /**
          * @param fromGf The GF process
          * @param toGf The GF process
          * @param pm The PrintnameManager on which the read Printnames
          * will be registered with their fun name.
+         * @param withTypes true iff the Printnames should have their type 
+         * appended to their display names
          */
-        public PrintnameLoader(BufferedReader fromGf, BufferedWriter toGf, PrintnameManager pm) {
+        public PrintnameLoader(BufferedReader fromGf, BufferedWriter toGf, PrintnameManager pm, boolean withTypes) {
                 super(fromGf, toGf);
                 this.printnameManager = pm;
+                this.loadTypes = withTypes;
         }
         
         /** 
@@ -42,7 +46,7 @@ public class PrintnameLoader extends AbstractProber {
                                 if (result.startsWith("printname fun ")) {
                                         //unescape backslashes. Probably there are more
                                         result = GFEditor2.unescapeTextFromGF(result);
-                                        this.printnameManager.addNewPrintnameLine(result);
+                                        this.printnameManager.addNewPrintnameLine(result, this.funTypes);
                                 }
                                 
                                 result = this.fromProc.readLine();
@@ -67,9 +71,12 @@ public class PrintnameLoader extends AbstractProber {
          * If lang is "" or null, the last read grammar module is used. 
          */
         public void readPrintnames(String lang) {
-                //send("gf pg -lang=FromUMLTypesOCL -printer=printnames");
+                //before, we want the types to be read.
+                if (this.loadTypes) {
+		                TypesLoader tl = new TypesLoader(fromProc, toProc, this.funTypes);
+		                tl.readTypes();
+                }
                 //prints the printnames of the last loaded grammar,
-                //which can be another one than FromUMLTypesOCL
                 String sendString = "gf pg -printer=printnames";
                 if (lang != null && !("".equals(lang))) {
                         sendString = sendString + " -lang=" + lang;

src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameManager.java

@@ -1,6 +1,5 @@
 package de.uka.ilkd.key.ocl.gf;
 import java.util.Hashtable;
-
 import org.apache.log4j.Logger;
 
 /**
@@ -35,21 +34,23 @@ class PrintnameManager {
          * printname fun neq = "<>," ++ ("parametrized" ++ ("disequality$to" ++ ("compare" ++ ("two" ++ ("instances" ++ ("on" ++ ("a" ++ ("specific" ++ "type%COMP"))))))))
          * and needs to get like
          * printname fun neq = "<>, parametrized disequality$to compare two instances on a specific type%COMP"
+         * @param funTypes contains funs, mapped to their types
          */
-        public void addNewPrintnameLine(String line) {
+        public void addNewPrintnameLine(String line, Hashtable funTypes) {
                 line = removePluses(line);
                 
             	//remove "printname fun " (the frontMatter)
-            	int index = line.indexOf(frontMatter);
+            	final int index = line.indexOf(frontMatter);
             	line = line.substring(index + frontMatter.length()).trim();
 
             	//extract fun name
-            	int endFun = line.indexOf(' ');
+            	final int endFun = line.indexOf(' ');
-            	String fun = line.substring(0, endFun);
+            	final String fun = line.substring(0, endFun);
+            	final String type = (String)funTypes.get(fun);
             	//extract printname
             	String printname = line.substring(line.indexOf('"') + 1, line.lastIndexOf('"'));
 
-            	addNewPrintname(fun, printname);
+            	addNewPrintname(fun, printname, type);
         }
         
         /**
@@ -71,11 +72,11 @@ class PrintnameManager {
          * @param myFun the GF abstract fun name
          * @param myPrintname the printname given by GF
          */
-        protected void addNewPrintname(String myFun, String myPrintname) {
+        protected void addNewPrintname(String myFun, String myPrintname, String type) {
                 if (logger.isDebugEnabled()) {
                         logger.debug("addNewPrintname, myFun = '" + myFun + "' , myPrintname = '" + myPrintname + "'");
                 }
-                Printname printname = new Printname(myFun, myPrintname, this.subcatNames);
+                Printname printname = new Printname(myFun, myPrintname, this.subcatNames, type);
                 if (logger.isDebugEnabled()) {
                         logger.debug("printname = '" + printname + "'");
                 }
@@ -109,7 +110,7 @@ class PrintnameManager {
                         // which does not occur in the refinement menu.
                         // if that is not wanted, don't call this method!
                         if (!myFun.startsWith("?")) {
-                                logger.warn("no printname for '" + myFun + "', pretend that it is a bound variable");
+                                logger.info("no printname for '" + myFun + "', pretend that it is a bound variable");
                                 return new Printname(myFun);
                         }
                 }

src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RealCommand.java

@@ -30,7 +30,7 @@ class RealCommand extends GFCommand {
          * @param mlAbstract is true, iff the menu language is set to Abstract
          * Then no preloaded printnames are used.
          */
-        public RealCommand(final String myCommand, HashSet processedSubcats, final PrintnameManager manager, final String myShowText, boolean mlAbstract) {
+        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("ch", "change head");
@@ -91,10 +91,10 @@ class RealCommand extends GFCommand {
                         this.printname = Printname.printhistory;
                 } else if (this.commandType.equals("rc")) {
                         String subtree = this.showText.substring(3);
-                        this.printname = new Printname(this.getCommand(), subtree + "$paste the previously copied subtree here<br>" + subtree);
+                        this.printname = new Printname(this.getCommand(), subtree + "\\$paste the previously copied subtree here<br>" + subtree);
                 } else if (mlAbstract) {
                         //create a new Printname
-                        this.printname = new Printname(funName, myShowText, null);
+                        this.printname = new Printname(funName, myShowText, null, null);
                 } else {
                         this.printname = manager.getPrintname(funName);
                 }
@@ -124,6 +124,9 @@ class RealCommand extends GFCommand {
                         String insertion = " as argument " + (this.argument + 1);
                         result = result + insertion;
                 }
+                if (this.printname.type != null) {
+                        result = result + " : " + this.printname.type;
+                }
                 return result;
         }
 

src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ToolTipCellRenderer.java

@@ -22,8 +22,7 @@ public class ToolTipCellRenderer extends JLabel implements ListCellRenderer {
         protected static Logger logger = Logger.getLogger(ToolTipCellRenderer.class.getName());
         
         /**
-         * Returns a JLabel with a tooltip in which everything after the 
+         * Returns a JLabel with a tooltip, which is given by the GFCommand
-         * first '$' character is.
          * @param list Well, the list this cell belongs to
          * @param value value to display
          * @param index cell index

src/JavaGUI2/de/uka/ilkd/key/ocl/gf/TypesLoader.java

@@ -0,0 +1,97 @@
+package de.uka.ilkd.key.ocl.gf;
+
+import java.io.BufferedReader;
+import java.io.BufferedWriter;
+import java.io.IOException;
+import java.util.Hashtable;
+
+import org.apache.log4j.Logger;
+
+/**
+ * @author daniels
+ * asks GF to print all available printnames, parses that list and generates
+ * the suiting Printname objects.
+ */
+public class TypesLoader extends AbstractProber {
+        protected final Hashtable hashtable;
+        protected static Logger nogger = Logger.getLogger(Printname.class.getName());
+        /**
+         * @param fromGf The GF process
+         * @param toGf The GF process
+         * @param myHashMap The hash in which the funs as keys and 
+         * types as values get saved. Both are Strings.
+         */
+        public TypesLoader(BufferedReader fromGf, BufferedWriter toGf, Hashtable myHashMap) {
+                super(fromGf, toGf);
+                this.hashtable = myHashMap;
+        }
+        
+        /** 
+         * Reads the tree child of the XML from beginning to end.
+         * Sets autocompleted to false, if the focus position is open.
+         */
+        protected void readMessage() {
+                try {
+                        String result = this.fromProc.readLine();
+                        if (nogger.isDebugEnabled()) {
+                                nogger.debug("7 " + result);
+                        }
+                        //first read line is <message>, but this one gets filtered out in the next line
+                        while (result.indexOf("/message")==-1){       
+                                result = result.trim();
+                                if (result.startsWith("fun ")) {
+                                        //unescape backslashes. Probably there are more
+                                        readType(result);
+                                }
+                                
+                                result = this.fromProc.readLine();
+                                if (nogger.isDebugEnabled()) {
+                                        nogger.debug("7 " + result);
+                                }
+                        }
+                        if (nogger.isDebugEnabled()) {
+                                nogger.debug("finished loading printnames");
+                        }
+                } catch(IOException e){
+                        System.err.println(e.getMessage());
+                        e.printStackTrace();
+                }
+
+        }
+        
+        /**
+         * asks GF to print a list of all available printnames and 
+         * calls the registered PrintnameManager to register those.
+         */
+        public void readTypes() {
+                //prints the last loaded grammar,
+                String sendString = "gf pg";
+                nogger.info("collecting types :" + sendString);
+                send(sendString);
+                readGfedit();
+        }
+
+        /**
+         * Reads a fun line from pg and puts it into hashMap with the fun
+         * as the key and the type as the value
+         * @param line One line which describes the signature of a fun
+         */
+        private void readType(String line) {
+                final int funStartIndex = 4; //length of "fun "
+                final String fun = line.substring(funStartIndex, line.indexOf(" : "));
+                final int typeStartIndex = line.indexOf(" : ") + 3;
+                final int typeEndIndex = line.lastIndexOf(" = ");
+                try {
+                final String type = line.substring(typeStartIndex, typeEndIndex);
+                this.hashtable.put(fun, type);
+                } catch (StringIndexOutOfBoundsException e) {
+                        System.err.println("line: '" + line + "'");
+                        System.err.println("fun: '" + fun + "'");                        
+                        System.err.println("typeStartIndex: " + typeStartIndex);
+                        System.err.println("typeEndIndex: " + typeEndIndex);
+                        
+                        System.err.println(e.getLocalizedMessage());
+                }
+        }
+
+}