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 0e1da2828..a82560a19 100644
--- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java
+++ b/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");
- rbMenuItem.setActionCommand("short");
- rbMenuItem.addActionListener(longShortListener);
- menuGroup.add(rbMenuItem);
- modeMenu.add(rbMenuItem);
- modeMenu.addSeparator();
+ rbMenuItemShort = new JRadioButtonMenuItem("short");
+ rbMenuItemShort.setActionCommand("short");
+ rbMenuItemShort.setSelected(true);
+ rbMenuItemShort.addActionListener(longShortListener);
+ menuGroup.add(rbMenuItemShort);
+ 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 ");
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 fbaadb435..83cbfe652 100644
--- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java
+++ b/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 subcategory which is started with %
+ * The tooltip text 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\\$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");
+
+ 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());
}
diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameLoader.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameLoader.java
index ea12b185f..aeb0a442e 100644
--- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameLoader.java
+++ b/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
- *
- * TODO To change the template for this generated type comment go to
- * Window - Preferences - Java - Code Style - Code Templates
+ * asks GF to print all available printnames, parses that list and generates
+ * the suiting Printname objects.
*/
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;
diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameManager.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameManager.java
index c231ce214..c837c0684 100644
--- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameManager.java
+++ b/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(' ');
- String fun = line.substring(0, endFun);
+ final int endFun = line.indexOf(' ');
+ 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);
}
}
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 cfe1a0cfe..64a56fb42 100644
--- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RealCommand.java
+++ b/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
" + subtree);
+ this.printname = new Printname(this.getCommand(), subtree + "\\$paste the previously copied subtree here
" + 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;
}
diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ToolTipCellRenderer.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ToolTipCellRenderer.java
index a25aa1bc2..55da51b02 100644
--- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ToolTipCellRenderer.java
+++ b/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
- * first '$' character is.
+ * Returns a JLabel with a tooltip, which is given by the GFCommand
* @param list Well, the list this cell belongs to
* @param value value to display
* @param index cell index
diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/TypesLoader.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/TypesLoader.java
new file mode 100644
index 000000000..3310368c0
--- /dev/null
+++ b/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 , 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());
+ }
+ }
+
+}