some deep java editor sources added

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/AbstractProber.java

@@ -0,0 +1,182 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.io.IOException;
+import java.util.logging.*;
+
+/**
+ * A class that offers a basic readGfEdit method with a lot of
+ * hot spots where subclasses can plug in 
+ * @author daniels
+ *
+ */
+abstract class AbstractProber {
+        /**
+         * reference to the editor whose readRefinementMenu method is used
+         */
+        protected final GfCapsule gfCapsule;
+        protected static Logger logger = Logger.getLogger(AbstractProber.class.getName());        
+        
+        /**
+         * A constructor which sets some fields
+         * @param gfCapsule The encapsulation of GF
+         */
+        public AbstractProber(GfCapsule gfCapsule) {
+                this.gfCapsule = gfCapsule;
+        }
+        
+        /**
+         * reads the hmsg part
+         * @param readresult the first line
+         * @return the first line of the next XML child.
+         * if no hmsg is present @see readresult is returned.
+         */
+        protected String readHmsg(String readresult) {
+                if (readresult.equals("<hmsg>")) {
+                        gfCapsule.skipChild("<hmsg>");
+                        try {
+                                String next = gfCapsule.fromProc.readLine();
+                                if (logger.isLoggable(Level.FINER)) {
+                                        logger.finer("2 " + next);
+                                }
+                                return next;
+                        } catch (IOException e) {
+                                System.err.println("Could not read from external process:\n" + e);
+                                return "";
+                        }
+                } else {
+                        return readresult;
+                }
+        }
+        
+        /**
+         * reads the linearization subtree.
+         * The first line should be already read
+         * @param readresult the first line with the opening tag
+         */
+        protected void readLinearizations(String readresult) {
+                gfCapsule.skipChild("<linearizations>");
+        }
+
+        /** 
+         * Reads the tree child of the XML from beginning to end 
+         */
+        protected void readTree() {
+                gfCapsule.skipChild("<tree>");
+        }
+
+        /** 
+         * Reads the message child of the XML from beginning to end 
+         */
+        protected void readMessage() {
+                gfCapsule.skipChild("<message>");
+        }
+        
+        /** 
+         * Reads the menu child of the XML from beginning to end 
+         */
+        protected void readMenu() {
+                gfCapsule.skipChild("<menu>");
+        }
+        
+        /**
+         * reads the output from GF starting with &gt;gfedit&lt; 
+         * and last reads &gt;/gfedit&lt;. 
+         */
+        protected void readGfedit() {
+                try {
+                        String next = "";
+                        //read <gfedit>
+                        String readresult = gfCapsule.fromProc.readLine();
+                        if (logger.isLoggable(Level.FINER)) {
+                                logger.finer("1 " + next);
+                        }
+                        //read either <hsmg> or <lineatization>
+                        readresult = gfCapsule.fromProc.readLine();
+                        if (logger.isLoggable(Level.FINER)) {
+                                logger.finer("1 " + next);
+                        }
+                        
+                        Hmsg hmsg = gfCapsule.readHmsg(readresult); 
+                        next = hmsg.lastline;
+                        
+                        //in case there comes sth. unexpected before <linearizations>
+                        //usually the while body is never entered
+                        // %%%
+                        while ((next!=null)&&((next.length()==0)||(!next.trim().equals("<linearizations>")))) {
+                                next = gfCapsule.fromProc.readLine();
+                                if (next!=null){
+                                        if (logger.isLoggable(Level.FINER)) {
+                                                logger.finer("1 " + next);
+                                        }
+                                } else {
+                                        System.exit(0);
+                                }
+                        }
+                        readLinearizations(next);
+                        readTree();
+                        readMessage();
+                        readMenu();
+                        
+                        for (int i=0; i<3 && !next.equals(""); i++){ 
+                                next = gfCapsule.fromProc.readLine();
+                                if (logger.isLoggable(Level.FINER)) {
+                                        logger.finer("1 " + next);
+                                }
+                        }
+                        
+                } catch (IOException e) {
+                        System.err.println("Could not read from external process:\n" + e);
+                }
+                
+        }
+        
+        /**
+         * send a command to GF
+         * @param text the command, exactly the string that is going to be sent
+         */
+        protected void send(String text) {
+                if (logger.isLoggable(Level.FINE)) {
+                        logger.fine("## send: '" + text + "'");
+                }
+                gfCapsule.realSend(text);
+        }
+
+        /**
+         * Just reads the complete output of a GF run and ignores it.	 
+         */	 
+        protected void readAndIgnore() {	 
+                try {
+                        StringBuffer debugCollector = new StringBuffer();
+                        String readresult = gfCapsule.fromProc.readLine();
+                        debugCollector.append(readresult).append('\n');
+                        if (logger.isLoggable(Level.FINER)) logger.finer("14 "+readresult);
+                        while (readresult.indexOf("</gfedit>") == -1) {
+                                readresult = gfCapsule.fromProc.readLine();
+                                debugCollector.append(readresult).append('\n');
+                                if (logger.isLoggable(Level.FINER)) logger.finer("14 "+readresult);	 
+                        }
+                        //read trailing newline:	 
+                        readresult = gfCapsule.fromProc.readLine();
+                        debugCollector.append(readresult).append('\n');
+                        if (logger.isLoggable(Level.FINER)) logger.finer("14 "+readresult);
+                        
+                } catch (IOException e) {	 
+                        System.err.println("Could not read from external process:\n" + e);	 
+                }	 
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/AstNodeData.java

@@ -0,0 +1,105 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.logging.*;
+
+/**
+ * @author hdaniels
+ * An object of this type knows how it self should be rendered,
+ * via Printname how its children should be rendered.
+ * This means the tooltip information it got from there.
+ * Knows nothing directly of the type of the node, which an object of this class
+ * represents. That's whats GfAstNode is for.
+ */
+abstract class AstNodeData {
+        protected static Logger logger = Logger.getLogger(DynamicTree2.class.getName());
+        /**
+         * @return the printname associated with this object
+         */
+        public abstract Printname getPrintname();
+
+        /**
+         * @return the parameter tooltip that this node has as a child
+         * of its parent (who gave it to it depending on its position)
+         */
+        public abstract String getParamTooltip();
+
+        /**
+         * keeps track of the number of children of this node.
+         * It has to be increased whenever a new child of this node is
+         * added.
+         */
+        public int childNum = 0;
+        /**
+         * The position String in the GF AST for this node
+         * in Haskell notation.
+         */
+        public final String position;
+        /**
+         * the GF node connected to this NodeData, not the JTree node
+         */
+        public final GfAstNode node;
+        
+        /**
+         * If a subtyping witness is missing, then this flag is false
+         */
+        public boolean subtypingStatus = true;
+        
+        /**
+         * if this is the active, selected, focused node
+         */
+        public final boolean selected;
+        
+        /**
+         * The constraint, that is valid on this node.
+         * If this node introduced a node itself and did not just inherit
+         * one, they are just concatenated.
+         * Until now, only the presence of a non-empty string here is used,
+         * so that is not important yet.
+         */
+        public final String constraint;
+
+        /**
+         * some nodes like coerce should, if possible, be covered from the
+         * users eyes. If this variable is greater than -1, the child
+         * with that number is shown instead of this node.
+         * This node will not appear in the tree.
+         */
+        public int showInstead = -1;
+        
+        /**
+         * A simple setter constructor, that sets the fields of this class (except showInstead)
+         * @param node the GF node connected to this NodeData, not the JTree node
+         * @param pos The position String in the GF AST for this node
+         * in Haskell notation.
+         * @param selected if this is the active, selected, focused node
+         * @param constraint The GF constraint introduced in this node
+         */
+        protected AstNodeData(GfAstNode node, String pos, boolean selected, String constraint) {
+                this.node = node;
+                this.position = pos;
+                this.selected = selected;
+                // I have no better idea, how to clutch them together, since
+                // I don't need the content of this field right now.
+                this.constraint = node.constraint + constraint; 
+        }
+        
+        public String toString() {
+                return this.node.getLine();
+        }
+
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/ChainCommandTuple.java

@@ -0,0 +1,60 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * @author hdaniels
+ * For chain commands, it is not just enough, to save the command sent to GF
+ * and the respective show text.
+ * Then it would be unclear, which fun should determine the used printname.
+ * If none is given, the last one of a chain command is taken.
+ * But if a solve for example is to follow, this does not work.
+ * Thus, this class has some other fields to define the appearance of a 
+ * chain command.
+ */
+class ChainCommandTuple extends StringTuple {
+        /**
+         * the fun, that selects the printname
+         */
+        final public String fun;
+        /**
+         * Here the subcat of fun can be overwritten.
+         * Is used for the attributes of self.
+         */
+        final public String subcat;
+        /**
+         * normally, the ';;' are counted. But if we know, how many commands we
+         * chain to each other, we can skip that step and use undoSteps instead
+         */
+        final public int undoSteps;
+        
+        /**
+         * A simple setter constructor
+         * @param command The command sent to GF
+         * @param showtext The text, that GF would display if no matching 
+         * printname is found.
+         * @param fun The fun that selects the used printname
+         * @param subcat the subcategory for the refinement menu, overwrites
+         * the one defined in the printname
+         * @param undoSteps how many undos are needed to undo this command
+         */
+        public ChainCommandTuple(String command, String showtext, String fun, String subcat, int undoSteps) {
+                super(command, showtext);
+                this.fun = fun;
+                this.subcat = subcat;
+                this.undoSteps = undoSteps;
+        }
+
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/ConstraintCallback.java

@@ -0,0 +1,64 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.logging.*;
+
+/**
+ * @author daniels
+ * Offers the interface that GFEditor2 uses to send back the constraint after editing.
+ * Has no dependancies on KeY or TogetherCC.
+  */
+abstract class ConstraintCallback {
+
+        /**
+         * Does the logging. What else should it do? 
+         */
+        protected static Logger logger = Logger.getLogger(ConstraintCallback.class.getName());
+
+        /**
+         * The path name of the directory where the grammars reside
+         */
+        String grammarsDir;
+        /**
+         * sets the directory where the grammars reside
+         * @param grammarsDir
+         */
+        void setGrammarsDir(final String grammarsDir)  {
+                this.grammarsDir = grammarsDir;
+        }
+        
+        /**
+         * gets the directory where the grammars reside
+         */
+        String getGrammarsDir()  {
+                return this.grammarsDir;
+        }
+        
+        /**
+         * Sends the finished OCL constraint back to Together to save it 
+         * as a JavaDoc comment.
+         * @param constraint The OCL constraint in question.
+         */
+        abstract void sendConstraint(String constraint);
+        
+        /**
+         * Sends the unfinished OCL constraint back to Together to save it 
+         * as a GF tree as a JavaDoc comment.
+         * @param abs The GF tree in question
+         */
+        abstract void sendAbstract(String abs);
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/Display.java

@@ -0,0 +1,249 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.awt.Font;
+import java.awt.Rectangle;
+import java.util.Vector;
+import javax.swing.JEditorPane;
+
+/**
+ * @author daniels
+ * Takes care of collecting the linearized text and the length calculations
+ */
+class Display {
+        /**
+         * If the linearization should be displayed as pure text
+         */
+        private boolean doText;
+        /**
+         * If the linearization should be displayed as HTML
+         */
+        private boolean doHtml;
+        /** 
+         * collects the linearization after each append.
+         * what's in here are Strings 
+         */
+        private Vector linStagesHtml = new Vector();
+        /** 
+         * collects the linearization after each append.
+         * what's in here are Strings 
+         */
+        private Vector linStagesText = new Vector();
+        /** 
+         * Is used to calculate the length of a HTML snipplet.
+         * This pane is not displayed in hope to avoid any actual renderings
+         * which would just slow the length calculation down.
+         * Perhaps that's an abuse ...
+         * And perhaps this pane is not needed
+         */
+        private JEditorPane htmlLengthPane = new JEditorPane();
+        
+        /** 
+         * initializes this object, nothing special 
+         * @param dt 1 if only text is to be shown, 2 for only HTML, 3 for both.
+         * Other values are forbidden.
+         */
+        public Display(int dt) {
+                setDisplayType(dt);
+                this.htmlLengthPane.setContentType("text/html");
+                this.htmlLengthPane.setEditable(false);
+        }
+
+        /**
+         * (de-)activates display of text and HTML according to dt
+         * @param dt 1 if only text is to be shown, 2 for only HTML, 3 for both.
+         */
+        protected void setDisplayType(int dt) {
+                switch (dt) {
+                        case 1: 
+                                doText = true;
+                                        doHtml = false;
+                                        break;
+                        case 2: 
+                                doText = false;
+                                        doHtml = true;
+                                        break;
+                        case 3: 
+                                doText = true;
+                                                doHtml = true;
+                                                break;
+                        default: 
+                                doText = true;
+                                        doHtml = true;
+                                        break;
+                }
+        }
+        /**
+         * Resets the stored text, but leaves the scroll markers untouched.
+         */
+        public void resetLin() {
+                linStagesHtml.clear();
+                linStagesText.clear();
+                htmlLengthPane.setText("");
+        }
+        
+        /**
+         * @param font The Font, that is to be used. If null, the default of JTextPane is taken.
+         * @return the collected HTML text, that has been added to this object.
+         * <html> tags are wrapped around the result, if not already there.
+         */
+        protected String getHtml(Font font) {
+                if (!doHtml) {
+                        return "";
+                }
+                String result;
+                if (this.linStagesHtml.size() > 0) {
+                        String fontface;
+                        if (font != null) {
+                                //fontface = " style=\"font-size:" + font.getSize()+ "pt\""; 
+                                fontface = " style=\"font: " + font.getSize()+ "pt " + font.getName() + "\"";
+                        } else {
+                                fontface = "";
+                        }
+                        result ="<html><body" + fontface + ">" + this.linStagesHtml.get(this.linStagesHtml.size() - 1).toString() + "</body></html>";
+                } else {
+                        result = "";
+                }
+                return result;
+        }
+
+        /**
+         * @return The collected pure text, that has been added to this object.
+         */
+        protected String getText() {
+                if (!doText) {
+                        return "";
+                }
+                String result;
+                if (this.linStagesText.size() > 0) {
+                        result = this.linStagesText.lastElement().toString();
+                } else {
+                        result = "";
+                }
+                return result;
+        }
+        
+        /**
+         * Appends the given text to the respective fields from
+         * where it can be displayed later
+         * @param text The pure text that is to be appended.
+         * @param html The HTML text that is to be appended. 
+         * Most likely the same as text
+         */
+        protected void addToStages(final String text, final String html) {
+                //add to HTML
+                if (doHtml) {
+		                final String newStageHtml;
+		                if (this.linStagesHtml.size() > 0) {
+		                        newStageHtml = this.linStagesHtml.get(this.linStagesHtml.size() - 1) + html;
+		                } else {
+		                        newStageHtml = html;
+		                }
+		                this.linStagesHtml.add(newStageHtml);
+                }
+                
+                //add to Text
+                if (doText) {
+		                final String newStageText;
+		                if (this.linStagesText.size() > 0) {
+		                        newStageText = linStagesText.get(linStagesText.size() - 1) + text;
+		                } else {
+		                        newStageText = text;
+		                }                                
+		                this.linStagesText.add(newStageText);
+                }
+        }        
+        
+        /**
+         * Adds toAdd to both the pure text as the HTML fields, they are inherently the same, 
+         * since they are mapped to the same position in the AST.
+         * On the way of adding, some length calculations are done, which are used to
+         * create an HtmlMarkedArea object, which is ready to be used in GFEditor2.
+         * @param toAdd The String that the to-be-produced MarkedArea should represent
+         * @param position The position String in Haskell notation
+         * @param language the language of the current linearization
+         * @return the HtmlMarkedArea object that represents the given information
+         * and knows about its beginning and end in the display areas.
+         */
+        protected MarkedArea addAsMarked(String toAdd, LinPosition position, String language) {
+                /** the length of the displayed HTML before the current append */
+                int oldLengthHtml = 0;
+                if (doHtml) {
+		                if (this.linStagesHtml.size() > 0) {
+		                        // is still in there. Does not absolutely need to be
+		                        // cached in a global variable
+		                        oldLengthHtml = this.htmlLengthPane.getDocument().getLength();
+		                } else {
+		                        oldLengthHtml = 0;
+		                }
+                }
+                /** the length of the text before the current append */
+                int oldLengthText = 0;
+                if (doText) {
+		                if (this.linStagesText.size() > 0) {
+		                        // is still in there. Does not absolutely need to be
+		                        // cached in a global variable
+		                        oldLengthText = this.linStagesText.lastElement().toString().length();
+		                } else {
+		                        oldLengthText = 0;
+		                }
+                }
+                addToStages(toAdd, toAdd);
+                //calculate beginning and end
+                //for HTML
+                int newLengthHtml = 0;
+                if (doHtml) {
+		                final String newStageHtml = this.linStagesHtml.lastElement().toString();
+		                final String newHtml = Printname.htmlPrepend(newStageHtml, "");
+		                //yeah, daniels admits, this IS expensive
+		                this.htmlLengthPane.setText(newHtml);
+		                newLengthHtml = htmlLengthPane.getDocument().getLength();
+		                if (newLengthHtml < oldLengthHtml) {
+		                        newLengthHtml = oldLengthHtml;
+		                }
+                }
+                //for text
+                int newLengthText = 0;
+                if (doText) {
+                        newLengthText = this.linStagesText.lastElement().toString().length();
+                }
+                final MarkedArea hma = new MarkedArea(oldLengthText, newLengthText, position, toAdd, oldLengthHtml, newLengthHtml, language);
+                return hma;
+        }
+        /**
+         * To store the scroll state of the pure text linearization area
+         */
+        Rectangle recText = new Rectangle();
+        /**
+         * To store the scroll state of the HTML linearization area
+         */
+        Rectangle recHtml = new Rectangle();
+        /**
+         * To store the scroll state of the pure text linearization area
+         */
+        int scrollText = 0;
+        /**
+         * To store the scroll state of the HTML linearization area
+         */
+        int scrollHtml = 0;
+
+        
+        
+        public String toString() {
+                return getText();
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/DynamicTree2.java

@@ -0,0 +1,366 @@
+//Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+/*
+ * This code is based on an example provided by Richard Stanford, 
+ * a tutorial reader.
+ */
+
+import java.awt.*;
+import javax.swing.*;
+import javax.swing.tree.*;
+import javax.swing.event.*;
+
+import java.util.logging.*;
+
+//import de.uka.ilkd.key.util.KeYResourceManager;
+
+import java.awt.event.*;
+
+/**
+ * A GUI class, does store the tree, but does not create it.
+ * The tree is created in GFEditor2.
+ * This class displays the tree and let the user interact with it via mouse clicks.
+ */
+public class DynamicTree2 extends JPanel implements KeyListener {
+        protected static Logger logger = Logger.getLogger(DynamicTree2.class.getName());
+
+        public DefaultMutableTreeNode rootNode;
+        private DefaultTreeModel treeModel;
+        public JTree tree;
+        private Toolkit toolkit = Toolkit.getDefaultToolkit();
+        private GFEditor2 gfeditor;
+        protected TreePath oldSelection = null;
+        
+        /**
+         * Initializes the display state of the tree panel, sets up the 
+         * event handlers.
+         * Does not initialize the tree.
+         * @param gfe The editor object this object belongs to.
+         */
+        public DynamicTree2(GFEditor2 gfe) {
+                
+                this.gfeditor = gfe;
+                rootNode = new DefaultMutableTreeNode("Root Node");
+                treeModel = new DefaultTreeModel(rootNode);
+                treeModel.addTreeModelListener(new MyTreeModelListener());
+                
+                tree = new JTree(treeModel);
+                tree.setRootVisible(false);
+                tree.setEditable(false);
+                tree.getSelectionModel().setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION);
+                tree.addKeyListener(this);
+                
+                //Add listener to components that can bring up popup menus.
+                MouseListener popupListener = new PopupListener();
+                tree.addMouseListener(popupListener);
+                
+                tree.addTreeSelectionListener(new TreeSelectionListener() {
+                        /**
+                         * Moves to the position of the selected node in GF.
+                         * the following is assumed:
+                         * gfeditor.nodeTable contains the positions for all selectionPathes.
+                         */
+                        public void valueChanged(TreeSelectionEvent e) {
+                                if ((tree.getSelectionPath() != null) && tree.getSelectionPath().equals(oldSelection)) {
+                                        //nothing to be done here, probably
+                                        //triggered by showTree
+                                        return;
+                                }
+                                if (tree.getSelectionRows() != null) {
+                                        if (tree.getSelectionPath() == null) {
+                                                if (logger.isLoggable(Level.FINER)) {
+                                                        logger.finer("null root path");
+                                                }
+                                        } else {
+                                                if (logger.isLoggable(Level.FINER)) {
+                                                        logger.finer("selected path" + tree.getSelectionPath());
+                                                }
+                                        }
+                                        String pos = gfeditor.getNodePosition(tree.getSelectionPath());
+                                        if (pos == null || "".equals(pos)) {
+                                                //default to sth. sensible
+                                                pos = "[]";
+                                        }
+                                        gfeditor.send("[t] mp " + pos);
+                                }
+                                oldSelection = tree.getSelectionPath();
+                        }
+                });
+                
+                tree.setCellRenderer(new MyRenderer());
+                tree.setShowsRootHandles(true);
+                ToolTipManager.sharedInstance().registerComponent(tree);
+                ToolTipManager.sharedInstance().setDismissDelay(60000);
+                setPreferredSize(new Dimension(200, 100));
+                JScrollPane scrollPane = new JScrollPane(tree);
+                setLayout(new GridLayout(1,0));
+                add(scrollPane);
+        }
+        
+        /**
+         * Remove all nodes in the tree and
+         * form a dummy tree in treePanel
+         */
+        protected void resetTree() {
+                ((DefaultTreeModel)(tree.getModel())).setRoot(new DefaultMutableTreeNode("Root"));
+                ((DefaultTreeModel)(tree.getModel())).reload();
+        }
+        
+        /** Remove all nodes except the root node. */
+        public void clear() {
+                ((DefaultTreeModel)(tree.getModel())).setRoot(null);
+                oldSelection = null;
+                //((DefaultTreeModel)(tree.getModel())).reload();
+        }
+        
+        /** Remove the currently selected node. */
+        public void removeCurrentNode() {
+                TreePath currentSelection = tree.getSelectionPath();
+                if (currentSelection != null) {
+                        DefaultMutableTreeNode currentNode = (DefaultMutableTreeNode)
+                        (currentSelection.getLastPathComponent());
+                        MutableTreeNode parent = (MutableTreeNode)(currentNode.getParent());
+                        if (parent != null) {
+                                treeModel.removeNodeFromParent(currentNode);
+                                return;
+                        }
+                } 
+                
+                // Either there was no selection, or the root was selected.
+                toolkit.beep();
+        }
+        
+        /**
+         * Add child to the root node.
+         * It will come last in this node.
+         * @param child the payload of the new node
+         * @return the tree node having child as the node data
+         */
+        public DefaultMutableTreeNode addObject(Object child) {
+                DefaultMutableTreeNode parentNode = null;
+                TreePath parentPath = tree.getSelectionPath();
+                
+                if (parentPath == null) {
+                        parentNode = rootNode;
+                } else {
+                        parentNode = (DefaultMutableTreeNode)
+                        (parentPath.getLastPathComponent());
+                }
+                
+                return addObject(parentNode, child, true);
+        }
+        
+        /** 
+         * Add a new node containing child to the node parent.
+         * It will come last in this node.
+         * This method gets actually called 
+         * @param parent the parent node of the to be created node
+         * @param child the wannabe node data
+         * @return the tree node having child as the node data and parent as the parent
+         */
+        public DefaultMutableTreeNode addObject(DefaultMutableTreeNode parent,
+                        Object child) {
+                return addObject(parent, child, false);
+        }
+        
+        /**
+         * Add child to the currently selected node (parent?).
+         * It will come last in this node.
+         * @param parent the parent node of the to be created node
+         * @param child the wannabe node data
+         * @param shouldBeVisible true iff the viewport should show the 
+         * new node afterwards
+         * @return the tree node having child as the node data and parent 
+         * as the parent
+         */
+        public DefaultMutableTreeNode addObject(DefaultMutableTreeNode parent, Object child, boolean shouldBeVisible) {
+                if (logger.isLoggable(Level.FINER)) {
+                        logger.finer("node added: '" + child + "', parent: '" + parent + "'");
+                }
+                DefaultMutableTreeNode childNode = new DefaultMutableTreeNode(child);
+                
+                if (parent == null) {
+                        parent = rootNode;
+                }
+                
+                treeModel.insertNodeInto(childNode, parent, 
+                                parent.getChildCount());
+                
+                // Make sure the user can see the lovely new node.
+                if (shouldBeVisible) {
+                        tree.scrollPathToVisible(new TreePath(childNode.getPath()));
+                }
+                return childNode;
+        }
+        
+        class MyTreeModelListener implements TreeModelListener {
+                public void treeNodesChanged(TreeModelEvent e) {
+                        DefaultMutableTreeNode node;
+                        node = (DefaultMutableTreeNode)
+                        (e.getTreePath().getLastPathComponent());
+                        
+                        /*
+                         * If the event lists children, then the changed
+                         * node is the child of the node we've already
+                         * gotten.  Otherwise, the changed node and the
+                         * specified node are the same.
+                         */
+                        try {
+                                int index = e.getChildIndices()[0];
+                                node = (DefaultMutableTreeNode)(node.getChildAt(index));
+                        } catch (NullPointerException exc) {
+                                System.err.println(exc.getMessage());
+                                exc.printStackTrace();
+                        }
+                        
+                        if (logger.isLoggable(Level.FINER)) {
+                                logger.finer("The user has finished editing the node.");
+                                logger.finer("New value: " + node.getUserObject());
+                        }
+                }
+                public void treeNodesInserted(TreeModelEvent e) {
+                        //nothing to be done here
+                }
+                public void treeNodesRemoved(TreeModelEvent e) {
+                        //nothing to be done here
+                }
+                public void treeStructureChanged(TreeModelEvent e) {
+                        //nothing to be done here
+                }
+        }
+        
+        /**
+         * This tree cell renderer got overwritten to make it possible to show
+         * tooltips according to the user object
+         */
+        private class MyRenderer extends DefaultTreeCellRenderer {
+                //int counter = 0;
+                //final ImageIcon iconFilled;
+                //final ImageIcon iconOpen;
+                
+//                public MyRenderer() {
+//                        final URL urlOpen = KeYResourceManager.getManager().getResourceFile(DynamicTree2.class, "metal_leaf_open.png");
+//                        final URL urlFilled = KeYResourceManager.getManager().getResourceFile(DynamicTree2.class, "metal_leaf_filled.png");
+//                        iconOpen = new ImageIcon(urlOpen);
+//                        iconFilled = new ImageIcon(urlFilled);
+//                }
+
+                /**
+                 * The heart of this class, sets display and tooltip text
+                 * depending on the user data
+                 */
+                public Component getTreeCellRendererComponent(
+                                JTree tree,
+                                Object value,
+                                boolean sel,
+                                boolean expanded,
+                                boolean leaf,
+                                int row,
+                                boolean hasFocus) {
+                        
+                        super.getTreeCellRendererComponent(
+                                        tree, value, sel,
+                                        expanded, leaf, row,
+                                        hasFocus);
+                        if (value instanceof DefaultMutableTreeNode) {
+                                DefaultMutableTreeNode node = (DefaultMutableTreeNode)value;
+                                if (node.getUserObject() instanceof AstNodeData) {
+				                        AstNodeData and = (AstNodeData)node.getUserObject();
+				                        String ptt = and.getParamTooltip();
+				                        if (!and.subtypingStatus ) {
+				                                this.setForeground(Color.RED);
+				                                ptt = Printname.htmlAppend(ptt, "<p>Subtyping proof is missing. <br>If no refinements are offered here, then there is a subtyping error.");
+				                        }
+				                        this.setToolTipText(ptt);
+				                        this.setText(and.toString());
+//				                        if (and.isMeta()) {
+//				                                this.setLeafIcon(this.iconOpen);
+//				                        } else {
+//				                                this.setLeafIcon(this.iconFilled);
+//				                        }
+                                } else {
+				                        this.setToolTipText(null);
+				                        this.setText(value.toString());
+                                }
+                        } else {
+		                        this.setToolTipText(null);
+		                        this.setText(value.toString());
+                        }
+                        return this;
+                }
+                
+                /** 
+                 * Checks if the current node represents an open metavariable
+                 * or question mark
+                 * @param value The payload of the node
+                 * @return true iff value begins with a '?'
+                 */
+                protected boolean isMetavariable(Object value) {
+                        try {
+                                DefaultMutableTreeNode node =
+                                        (DefaultMutableTreeNode)value;
+                                String nodeInfo = 
+                                        (String)(node.getUserObject());
+                                if (nodeInfo.indexOf("?") == 0) {
+                                        return true;                                        
+                                } 
+                        } catch (Exception e) {
+                                e.printStackTrace();
+                                return false;
+                        }
+                        
+                        return false;
+                }
+                
+        }//class
+        
+        class PopupListener extends MouseAdapter {
+                public void mousePressed(MouseEvent e) {
+                        gfeditor.maybeShowPopup(e);
+                }
+                
+                public void mouseReleased(MouseEvent e) {
+                        //nothing to be done here
+                }
+        }
+
+        /** 
+         * Handle the key pressed event. 
+         */
+        public void keyPressed(KeyEvent e) {
+                int keyCode = e.getKeyCode();   
+                switch (keyCode){ 
+                        case KeyEvent.VK_SPACE	:  gfeditor.send("'"); break;
+                        case KeyEvent.VK_DELETE	: gfeditor.send("d"); break;
+                }
+        }
+        /** 
+         * Handle the key typed event. 
+         */
+        public void keyTyped(KeyEvent e) {
+                //nothing to be done here
+        }
+        /** 
+         * Handle the key released event. 
+         */
+        public void keyReleased(KeyEvent e) {
+                //nothing to be done here
+        }
+        
+}
+
+

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/ExportFormatMenu.java

@@ -0,0 +1,67 @@
+// This file is part of KeY - Integrated Deductive Software Design
+// Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
+//                         Universitaet Koblenz-Landau, Germany
+//                         Chalmers University of Technology, Sweden
+//
+// The KeY system is protected by the GNU General Public License. 
+// See LICENSE.TXT for details.
+//
+
+package de.uka.ilkd.key.ocl.gf;
+
+import javax.swing.*;
+import java.awt.*;
+import java.awt.event.*;
+
+/** Provide a choice of output formats: OCL or Natural Language. NL can be
+  * formatted using either HTML or LaTeX.
+  */
+public class ExportFormatMenu extends JPanel
+{
+    public static int OCL = 0, HTML=1, LATEX=2;
+
+    private static String[] menuStrings = { "OCL",
+        "Natural Language/HTML (requires GF)",
+        "Natural Language/LaTeX (requires GF)"
+    };
+    
+    private JComboBox formatMenu;
+    private int selection;
+    
+    private ActionListener al = new ActionListener() {
+        public void actionPerformed(ActionEvent e) {
+            JComboBox cb = (JComboBox) e.getSource();
+            String s = (String) cb.getSelectedItem();
+            if (s.equals("OCL")) {
+                selection = OCL;
+            } else if (s.equals("Natural Language/HTML (requires GF)")) {
+                selection = HTML;
+            } else if (s.equals("Natural Language/LaTeX (requires GF)")) {
+                selection = LATEX;
+            } else { // should never occur
+                selection = OCL;
+            };
+        }
+    };
+    
+    public ExportFormatMenu() 
+    {
+        super();
+        this.setLayout(new BoxLayout(this,BoxLayout.Y_AXIS));
+        formatMenu = new JComboBox(menuStrings);
+        formatMenu.setSelectedIndex(0);
+        formatMenu.addActionListener(al);
+        this.add(Box.createVerticalGlue());
+        JLabel text = new JLabel("Choose output format:");
+        this.add(text);
+        text.setAlignmentX(Component.CENTER_ALIGNMENT);
+        this.add(formatMenu);
+    }
+    
+
+    public int getSelection()
+    {
+        return selection;
+    }
+}
+

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFCommand.java

@@ -0,0 +1,137 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+/**
+ * @author daniels
+ * A class that represents a GF command together with its printname.
+ * It also gives easy access to all the abuses of the printname like
+ * the subcategory, the tooltip, it knows about wrapping and so on.
+ * 
+ * The static stuff could produce problems if the editor is started
+ * several times without closing it first. It probably should be moved
+ * into a manager class.
+ * Or the instances that get generated during one run all share the same
+ * "pseudo-static" Hashtables. This is probably better.
+ *
+ */
+abstract class GFCommand implements Comparable{
+        
+        /** 
+         * the subcategory of this command
+         */
+        public abstract String getSubcat();
+        /** 
+         * the type of the command, r,w,ch,d,ac,... 
+         */
+        protected String commandType;
+        /** 
+         * the type of the command, r,w,ch,d,ac,... 
+         */
+        public String getCommandType(){
+                return commandType;
+        }
+        /** 
+         * for wrap, the number of the argument the current node should become 
+         */
+        protected int argument;
+        
+        /**
+         * the actual command that this object should represent 
+         */
+        protected String command;
+        /**
+         * the actual command that this object should represent 
+         */
+        public String getCommand() {
+                return command;
+        }
+        
+        /**
+         * the Printname corresponding to the GF fun of this command
+         */
+        protected Printname printname;
+        /**
+         * the Printname corresponding to the GF fun of this command
+         */
+        public Printname getPrintname(){
+                return printname;
+        }
+        
+        /**
+         * the text that is to be displayed as the tooltip 
+         */
+        public abstract String getTooltipText();
+        
+        /**
+         * the text that is to be displayed in the refinement lists 
+         */
+        public abstract String getDisplayText();
+        
+        /** 
+         * the name of the fun that is used in this command 
+         */
+        protected String funName;
+        
+        /** 
+         * if this is the first occurence of the current subcat 
+         */
+        protected boolean newSubcat;
+        
+        /** 
+         * if this is the first occurence of the current subcat 
+         */
+        public boolean isNewSubcat() {
+                return newSubcat;
+        }
+        
+        /**
+         * Compares two GFCommands.
+         * LinkCommands are the least. Then the InputCommand (more than one
+         * does not happen). If that does not decide, the display name as a String does.
+         * @param o the other command.
+         * @return see above.
+         */
+        public int compareTo(Object o) {
+                if (this.equals(o)) {
+                        return 0;
+                }
+                if (this instanceof LinkCommand && !(o instanceof LinkCommand)) {
+                        return -1;
+                }
+                if (!(this instanceof LinkCommand) && (o instanceof LinkCommand)) {
+                        return 1;
+                }
+                //LinkCommands are dealt with, so from now on, they don't occur
+                if (this instanceof InputCommand && !(o instanceof InputCommand)) {
+                        return -1;
+                }
+                if (!(this instanceof InputCommand) && (o instanceof InputCommand)) {
+                        return 1;
+                }
+                if (! (o instanceof GFCommand)) {
+                        //This should never occur!
+                        return -1;
+                } else {
+                        GFCommand ocmd = (GFCommand)o;
+                        return this.getDisplayText().compareTo(ocmd.getDisplayText());
+                }
+        }
+        
+        public String toString() {
+                return getDisplayText() + " \n " + getTooltipText();
+        }
+        
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/GfAstNode.java

@@ -0,0 +1,121 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * @author daniels
+ * This Class represents a parsed node in the GF AST.
+ * It knows about types, bound variables, funs.
+ * But nothing about printnames. That's what AstNodeData is for.
+ */
+class GfAstNode {
+        /**
+         * contains the types of the bound variables in the order of their occurence
+         */
+        protected final String[] boundTypes;
+        /**
+         * contains the names of the bound variables in the order of their occurence
+         */
+        protected final String[] boundNames;
+        /** 
+         * The type of this AST node 
+         */
+        private final String type;
+        /**
+         * @return The type of this AST node
+         */
+        protected String getType() {
+                return type;
+        }
+        /** 
+         * the fun represented in this AST node 
+         */
+        private final String fun;
+
+        /**
+         * @return the fun represented in this AST node.
+         * Can be a metavariable like "?1"
+         */
+        protected String getFun() {
+                return fun;
+        }
+        
+        /**
+         * @return true iff the node is a metavariable, i.e. open and not
+         * yet refined.
+         */
+        protected boolean isMeta() {
+                return fun.startsWith("?");
+        }
+        /** 
+         * the line that was used to build this node 
+         */
+        private final String line;
+        /**
+         * @return the line that was used to build this node
+         */
+        protected String getLine() {
+                return line;
+        }
+        
+        /**
+         * The constraint attached to this node
+         */
+        public final String constraint;
+
+        /**
+         * feed this constructor the line that appears in the GF AST and
+         * it will get chopped at the right points.
+         * @param line The line from GF without the * in the beginning.
+         */
+        protected GfAstNode(final String line) {
+                this.line = line.trim();
+                final int index = this.line.lastIndexOf(" : ");
+                String typeString = this.line.substring(index + 3);
+                final int constraintIndex = typeString.indexOf(" {");
+                if (constraintIndex > -1) {
+                        this.constraint = typeString.substring(constraintIndex + 1).trim();
+                        this.type = typeString.substring(0, constraintIndex).trim();
+                } else {
+                        this.constraint = "";
+                        this.type = typeString;
+                }
+                String myFun = this.line.substring(0, index);
+                if (myFun.startsWith("\\(")) {
+                        final int end = myFun.lastIndexOf(") -> ");
+                        String boundPart = myFun.substring(2, end);
+                        String[] bounds = boundPart.split("\\)\\s*\\,\\s*\\(");
+                        this.boundNames = new String[bounds.length];
+                        this.boundTypes = new String[bounds.length];
+                        for (int i = 0; i < bounds.length;i++) {
+                                //System.out.print("+" + bounds[i] + "-");
+                                int colon = bounds[i].indexOf(" : ");
+                                this.boundNames[i] = bounds[i].substring(0, colon);
+                                this.boundTypes[i] = bounds[i].substring(colon + 3);
+                                //System.out.println(boundNames[i] + " ;; " + boundTypes[i]);
+                        }
+                        myFun = myFun.substring(end + 5);
+                } else {
+                        this.boundNames = new String[0];
+                        this.boundTypes = new String[0];
+                }
+                this.fun = myFun;
+        }
+        
+        public String toString() {
+                return this.line;
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/GfCapsule.java

@@ -0,0 +1,621 @@
+//Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.io.BufferedReader;
+import java.io.BufferedWriter;
+import java.io.File;
+import java.io.IOException;
+import java.io.InputStreamReader;
+import java.io.OutputStreamWriter;
+import java.util.Vector;
+import java.util.logging.Level;
+import java.util.logging.Logger;
+
+import javax.swing.JFrame;
+import javax.swing.JOptionPane;
+import javax.swing.ProgressMonitor;
+
+class GfCapsule {
+        /** 
+         * XML parsing debug messages  
+         */
+        private static Logger xmlLogger = Logger.getLogger(GfCapsule.class.getName() + ".xml");
+        /** 
+         * generic logging of this class  
+         */
+        private static Logger logger = Logger.getLogger(GfCapsule.class.getName());
+        /** 
+         * The output from GF is in here.
+         * Only the read methods, initializeGF and the prober objects access this. 
+         */
+        BufferedReader fromProc;
+        /** 
+         * Used to leave messages for GF here. 
+         * But <b>only</b> in send and special probers that clean up with undo
+         * after them (or don't change the state like PrintnameLoader).
+         */
+        BufferedWriter toProc;
+
+        /**
+         * Starts GF with the given command gfcmd in another process.
+         * Sets up the reader and writer to that process.
+         * Does in it self not read anything from GF.
+         * @param gfcmd The complete command to start GF, including 'gf' itself.
+         */
+        public GfCapsule(String gfcmd){
+                try {
+                        Process extProc = Runtime.getRuntime().exec(gfcmd); 
+                        InputStreamReader isr = new InputStreamReader(
+                                        extProc.getInputStream(),"UTF8");
+                        this.fromProc = new BufferedReader (isr);
+                        String defaultEncoding = isr.getEncoding();
+                        if (logger.isLoggable(Level.FINER)) {
+                                logger.finer("encoding "+defaultEncoding);
+                        }
+                        this.toProc = new BufferedWriter(new OutputStreamWriter(extProc.getOutputStream(),"UTF8"));
+                } catch (IOException e) {
+                        JOptionPane.showMessageDialog(new JFrame(), "Could not start " + gfcmd+
+                                        "\nCheck your $PATH", "Error", 
+                                        JOptionPane.ERROR_MESSAGE);
+                        throw new RuntimeException("Could not start " + gfcmd+
+                        "\nCheck your $PATH");
+                }
+        }
+
+        
+        /**
+         * Does the actual writing of command to the GF process via STDIN
+         * @param command exactly the string that is going to be sent
+         */
+        protected void realSend(String command) {
+                try {
+                        toProc.write(command, 0, command.length());
+                        toProc.newLine();
+                        toProc.flush();
+                } catch (IOException e) {
+                        System.err.println("Could not write to external process " + e);
+                }  
+                
+        }
+        
+        /**
+         * reads the part between &gt;gfinit&lt; and &gt;/gfinit&lt; 
+         * @return the data for the new category menu
+         */
+        protected NewCategoryMenuResult readGfinit() {
+                try {
+                        //read <hmsg> or <newcat> or <topic> (in case of no grammar loaded)
+                        String readresult = fromProc.readLine();
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("12 "+readresult);
+                        //when old grammars are loaded, the first line looks like
+                        //"reading grammar of old format letter.Abs.gfreading old file letter.Abs.gf<gfinit>"
+                        if (readresult.indexOf("<gfinit>") > -1) {
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("12 "+readresult);
+                        }
+                        //no command appendix expected or applicable here, so appendix is discarded
+                        Hmsg hmsg = readHmsg(readresult);
+                        String next = hmsg.lastline;
+                        //no hmsg supported here. Wouldn't be applicable.
+                        //the reading above is to silently ignore it intead of failing.
+                        //formHmsg(hmsg);
+
+                        if ((next!=null) && ((next.indexOf("newcat") > -1) 
+                                        || (next.indexOf("topic") > -1))) {
+                                NewCategoryMenuResult ncmr = readNewMenu();
+                                return ncmr;
+                        }
+                        
+                } catch (IOException e) {
+                        System.err.println("Could not read from external process:\n" + e);
+                }
+                return null;
+        }
+
+        /**
+         * reads the greeting text from GF
+         * @return S tuple with first = the last read GF line, 
+         * which should be the first loading line
+         * and second = The greetings string
+         */
+        protected StringTuple readGfGreetings() {
+                try {
+                        String readresult = "";
+                        StringBuffer outputStringBuffer = new StringBuffer();
+                        readresult = fromProc.readLine();
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("1 "+readresult);
+                        while ((readresult.indexOf("gf")==-1) && (readresult.trim().indexOf("<") < 0)){                          
+                                outputStringBuffer.append(readresult).append("\n");
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("1 "+readresult);
+                        }
+                        return new StringTuple(readresult, outputStringBuffer.toString());
+                } catch (IOException e) {
+                        System.err.println("Could not read from external process:\n" + e);
+                        return new StringTuple("", e.getLocalizedMessage());
+                }
+                
+        }
+
+        /**
+         * reads the loading and compiling messages from GF
+         * @param readresult the first loading line
+         * @param pm to monitor the loading progress. May be null
+         * @return A tuple with first = the first line from &gt;gfinit&lt; or &gt;gfedit&lt;
+         * and second = the loading message as pure text
+         */
+        protected StringTuple readGfLoading(String readresult, ProgressMonitor pm) {
+                try {
+                        // in case nothing has been loaded first, the that has to be done now
+                        if (readresult == null) {
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("1 " + readresult);
+                        }
+                        StringBuffer textPure = new StringBuffer();
+                        int progress = 5300;
+                        while (!(readresult.indexOf("<gfinit>") > -1 || (readresult.indexOf("<gfmenu>") > -1))){
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("1 "+readresult);
+                                textPure.append(readresult).append("\n");
+                                progress += 12;
+                                Utils.tickProgress(pm, progress, null);
+                        }
+                        //when old grammars are loaded, the first line looks like
+                        //"reading grammar of old format letter.Abs.gfreading old file letter.Abs.gf<gfinit>"
+                        //without newlines
+                        final int beginInit = readresult.indexOf("<gfinit>"); 
+                        if (beginInit > 0) {
+                                textPure.append(readresult.substring(0, beginInit)).append("\n");
+                                //that is the expected result
+                                readresult = "<gfinit>";
+                        }
+                        return new StringTuple(readresult, textPure.toString());
+                } catch (IOException e) {
+                        System.err.println("Could not read from external process:\n" + e);
+                        return new StringTuple("", e.getLocalizedMessage());
+                }
+
+        }
+
+        
+        /**
+         * Reads the &lt;gfedit&gt; part from GF's XML output.
+         * The different subtags are put into the result
+         * @param newObj If a new object in the editor has been started.
+         * If the to-be-read hmsg contains the newObject flag, 
+         * that overwrites this parameter
+         * @return the read tags, partially halfy parsed, partially raw.
+         * The way the different form methods expect it.
+         */
+        protected GfeditResult readGfedit(boolean newObj) {
+                try {
+                        String next = "";
+                        //read <gfedit>
+                        String readresult = fromProc.readLine();
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("11 "+readresult);
+                        //read either <hsmg> or <lineatization>
+                        readresult = fromProc.readLine();
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("11 "+readresult);
+                        
+                        //hmsg stuff
+                        final Hmsg hmsg = readHmsg(readresult);
+                        next = hmsg.lastline;
+                        
+                        //reading <linearizations>
+                        //seems to be the only line read here
+                        //this is here to give as some sort of catch clause.
+                        while ((next!=null)&&((next.length()==0)||(next.indexOf("<linearizations>")==-1))) {
+                                next = fromProc.readLine();
+                                if (next!=null){
+                                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("10 "+next);
+                                } else {
+                                        System.exit(0);
+                                }
+                        }
+                        readresult = next;
+                        String lin = readLin();
+                        final String treeString = readTree();
+                        final String message = readMessage();
+                        //read the menu stuff
+                        Vector gfCommandVector;
+                        if (newObj || hmsg.newObject) {
+                                gfCommandVector = readRefinementMenu();
+                        } else {
+                                while(readresult.indexOf("</menu")==-1) {
+                                        readresult = fromProc.readLine();
+                                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("12 " + readresult);                    
+                                }
+                                gfCommandVector = null;
+                        }
+                        // "" should occur quite fast, but it has not already been read,
+                        // since the last read line is "</menu>"
+                        for (int i = 0; i < 3 && !readresult.equals(""); i++){ 
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("11 " + readresult);                    
+                        }
+                        //all well, return the read stuff
+                        return new GfeditResult(gfCommandVector, hmsg, lin, message, treeString);
+                        
+                } catch (IOException e) {
+                        System.err.println("Could not read from external process:\n" + e);
+                }
+                //nothing well, return bogus stuff
+                return new GfeditResult(new Vector(), new Hmsg("", "", false, false, false, false, true), "", "", "");
+                
+        }        
+
+        /**
+         * reads the linearizations in all language.
+         * seems to expect the first line of the XML structure 
+         * (< lin) already to be read
+         * Accumulates the GF-output between <linearization> </linearization>  tags
+         */
+        protected String readLin(){
+                StringBuffer lins = new StringBuffer();
+                try {
+                        //read <linearizations>
+                        String readresult = fromProc.readLine();             
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 " + readresult);
+                        lins.append(readresult).append('\n');
+                        readresult = fromProc.readLine();
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);
+                        while ((readresult != null) && (readresult.indexOf("/linearization") == -1)){       
+                                lins.append(readresult).append('\n');
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);                     
+                        }
+                } catch(IOException e){
+                        System.err.println(e.getMessage());
+                        e.printStackTrace();
+                }
+                return lins.toString();
+        }
+        
+        /**
+         * reads in the tree and calls formTree without start end end tag of tree
+         * expects the first starting XML tag tree to be already read
+         * @return the read tags for the tree or null if a read error occurs
+         */
+        protected String readTree(){
+                String treeString = "";
+                try {
+                        //read <tree>
+                        String readresult = fromProc.readLine();             
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);          
+                        readresult = fromProc.readLine();
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);
+                        while (readresult.indexOf("/tree") == -1){       
+                                treeString += readresult + "\n";           
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);                     
+                        }
+                        return treeString;
+                } catch(IOException e){
+                        System.err.println(e.getMessage());
+                        e.printStackTrace();
+                        return null;
+                }
+        }
+        
+        /**
+         * Parses the GF-output between <message> </message>  tags
+         * and returns it.
+         * @return The read message.
+         */
+        protected String readMessage(){
+                String s ="";
+                try {
+                        // read <message>
+                        String readresult = fromProc.readLine();             
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);          
+                        readresult = fromProc.readLine();
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 " + readresult);
+                        while (readresult.indexOf("/message") == -1){       
+                                s += readresult + "\n";           
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 " + readresult);                     
+                        }
+                        return s;
+                } catch(IOException e){
+                        System.err.println(e.getLocalizedMessage());
+                        e.printStackTrace();
+                        return e.getLocalizedMessage();
+                }
+        }
+ 
+        /**
+         * reads the cat entries and puts them into result.menuContent, 
+         * after that reads
+         * the names of the languages and puts them into the result.languages
+         * The loaded grammar files are put into result.paths,
+         * a guessed grammar name into result.grammarName 
+         * Parses the GF-output between <gfinit> tags
+         */
+        protected NewCategoryMenuResult readNewMenu () {
+                //here the read stuff is sorted into
+                String grammarName = "";
+                final Vector languages = new Vector();
+                final Vector menuContent = new Vector();
+                final Vector paths = new Vector();
+                
+                boolean more = true;
+                try {
+                        //read first cat
+                        String readresult = fromProc.readLine();
+                        if (xmlLogger.isLoggable(Level.FINER)) {
+                                xmlLogger.finer("2 " + readresult);
+                        }
+                        if (readresult.indexOf("(none)") > -1) {
+                                //no topics present
+                                more = false;
+                        }
+                        
+                        while (more){
+                                //adds new cat s to the menu
+                                if (readresult.indexOf("topic") == -1) {
+                                        final String toAdd = readresult.substring(6);
+                                        menuContent.add(toAdd);
+                                } else { 
+                                        more = false;
+                                }
+                                //read </newcat
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("2 " + readresult);
+                                //read <newcat (normally)
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("3 " + readresult); 
+                                if (readresult.indexOf("topic") != -1) {
+                                        //no more categories
+                                        more = false; 
+                                }
+                                //read next cat / topic
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("4 " + readresult);       
+                        }
+                        //set topic
+                        grammarName = readresult.substring(4) + "          ";
+                        //read </topic>
+                        readresult = fromProc.readLine();
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("2 " + readresult);
+                        //read <language>
+                        readresult = fromProc.readLine();
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("3 " + readresult);
+                        //read actual language
+                        readresult = fromProc.readLine();             
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("4 " + readresult);       
+                        
+                        //read the languages and select the last non-abstract
+                        more = true;
+                        while (more){
+                                if ((readresult.indexOf("/gfinit") == -1) 
+                                                && (readresult.indexOf("lin") == -1)) {         
+                                        //form lang and Menu menu:
+                                        final String langName = readresult.substring(4);
+                                        languages.add(langName);
+                                } else { 
+                                        more = false;
+                                }
+                                // read </language>
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("2 " + readresult); 
+                                // read <language> or </gfinit...>
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("3 " + readresult); 
+                                if ((readresult.indexOf("/gfinit") != -1) 
+                                                || (readresult.indexOf("lin") != -1)) { 
+                                        more = false; 
+                                }
+                                // registering the file name:
+                                if (readresult.indexOf("language") != -1) {
+                                        String path = readresult.substring(readresult.indexOf('=') + 1,
+                                                        readresult.indexOf('>')); 
+                                        path = path.substring(path.lastIndexOf(File.separatorChar) + 1);
+                                        if (xmlLogger.isLoggable(Level.FINE)) xmlLogger.fine("language: " + path);
+                                        paths.add(path);
+                                }
+                                // in case of finished, read the final "" after </gfinit>, 
+                                // otherwise the name of the next language
+                                readresult = fromProc.readLine();             
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("4 " + readresult);               
+                        }
+                } catch(IOException e){
+                        xmlLogger.warning(e.getMessage());
+                }
+                String[] menuContentArray = Utils.vector2Array(menuContent);
+                String[] languagesArray = Utils.vector2Array(languages);
+                String[] pathsArray = Utils.vector2Array(paths);
+                NewCategoryMenuResult result = new NewCategoryMenuResult(grammarName, menuContentArray, languagesArray, pathsArray);
+                return result;
+        }
+
+        /**
+         * Reads the hmsg part of the XML that is put out from GF.
+         * Everything in [] given in front of a GF command will be rewritten here.
+         * This method does nothing when no hmsg part is present.
+         * 
+         * If a '$' appears in this string, everything that comes after it
+         * will be in result.second.
+         * ;; and [] don't work in the [] for the hmsg, 
+         * therfore the following replacements are done:
+         *   %% for ;;
+         *   (  for [
+         *   )  for ]
+         * 
+         * If one of the characters c,t,n comes before, the following is done:
+         *   c The output will be cleared before the linearization (TODO: done anyway?)
+         *   t The treeChanged flag will be set to true
+         *   n The newObject flag will be set to true
+         *   p No other probing run should be done (avoid cycles)
+         *   r To prevent the execution of automatically triggered commands to prevent recursion
+         *  
+         * @param prevreadresult The last line read from GF
+         * @return first: the last line this method has read;
+         * second: the string after $, null if that is not present
+         */
+        protected Hmsg readHmsg(String prevreadresult){
+                if ((prevreadresult!=null)&&(prevreadresult.indexOf("<hmsg>") > -1)) {
+                        StringBuffer s =new StringBuffer("");
+                        String commandAppendix = null;
+                        try {
+                                boolean onceAgain = true;
+                                boolean recurse = true;
+                                boolean newObj = false;
+                                boolean treeCh = false;
+                                boolean clear = false;
+                                String readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 "+readresult);
+                                while (readresult.indexOf("/hmsg")==-1){       
+                                        s.append(readresult).append('\n');           
+                                        readresult = fromProc.readLine();
+                                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 "+readresult);                     
+                                }
+                                int commandAppendixStart = s.indexOf("$"); 
+                                if (commandAppendixStart > -1 && commandAppendixStart < s.length() - 1) { //present, but not the last character
+                                        commandAppendix = s.substring(commandAppendixStart + 1, s.indexOf("\n")); //two \n trail the hmsg
+                                        //;; and [] don't work in the [] for the hmsg
+                                        commandAppendix = Utils.replaceAll(commandAppendix, "%%", ";;");
+                                        commandAppendix = Utils.replaceAll(commandAppendix, "(", "[");
+                                        commandAppendix = Utils.replaceAll(commandAppendix, ")", "]");
+                                } else {
+                                        commandAppendixStart = s.length();
+                                }
+                                if (s.indexOf("c") > -1 && s.indexOf("c") < commandAppendixStart) {
+                                        //clear output before linearization
+                                        clear = true;
+                                }
+                                if (s.indexOf("t") > -1 && s.indexOf("t") < commandAppendixStart) {
+                                        //tree has changed
+                                        treeCh = true;
+                                }
+                                if (s.indexOf("p") > -1 && s.indexOf("p") < commandAppendixStart) {
+                                        //we must not probe again
+                                        onceAgain = false;
+                                }
+                                if (s.indexOf("r") > -1 && s.indexOf("r") < commandAppendixStart) {
+                                        //we must not probe again
+                                        recurse = false;
+                                }
+
+                                if (s.indexOf("n") > -1 && s.indexOf("n") < commandAppendixStart) {
+                                        //a new object has been created
+                                        newObj = true;
+                                }
+                                if (logger.isLoggable(Level.FINE)) {
+                                        if (commandAppendix != null) {
+                                                logger.fine("command appendix read: '" + commandAppendix + "'");
+                                        }
+                                }
+                                return new Hmsg(readresult, commandAppendix, onceAgain, recurse, newObj, treeCh, clear);
+                        } catch(IOException e){
+                                System.err.println(e.getMessage());
+                                e.printStackTrace();
+                                return new Hmsg("", null, false, true, false, true, false);
+                        }
+                } else {
+                        return new Hmsg(prevreadresult, null, true, true, false, true, false);
+                }
+        }
+
+        /**
+         * Parses the GF-output between <menu> and </menu>  tags
+         * and puts a StringTuple for each show/send pair into the
+         * return vector.
+         * @return A Vector of StringTuple as described above
+         */
+        protected Vector readRefinementMenu (){
+                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("list model changing! ");      
+                String s ="";
+                Vector printnameVector = new Vector();
+                Vector commandVector = new Vector();
+                Vector gfCommandVector = new Vector();
+                try {
+                        //read <menu>
+                        String readresult = fromProc.readLine();             
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 " + readresult);          
+                        //read item
+                        readresult = fromProc.readLine();
+                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
+                        while (readresult.indexOf("/menu")==-1){
+                                //read show
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
+                                while (readresult.indexOf("/show") == -1){          
+                                        readresult = fromProc.readLine();
+                                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("9 " + readresult);
+                                        if (readresult.indexOf("/show") == -1) {
+                                                if (readresult.length()>8)
+                                                        s += readresult.trim();
+                                                else
+                                                        s += readresult;    
+                                        }
+                                }            
+                                //          if (s.charAt(0)!='d')
+                                //            listModel.addElement("Refine " + s);
+                                //          else 
+                                String showText = s;
+                                printnameVector.addElement(s);
+                                s = "";
+                                //read /show
+                                //read send
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
+                                String myCommand = readresult;
+                                commandVector.add(readresult);
+                                //read /send (discarded)
+                                readresult = fromProc.readLine();             
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);          
+                                
+                                // read /item
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
+                                readresult = fromProc.readLine();
+                                if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
+                                
+                                StringTuple st = new StringTuple(myCommand.trim(), showText);
+                                gfCommandVector.addElement(st);
+                        }
+                } catch(IOException e){
+                        System.err.println(e.getMessage());
+                        e.printStackTrace();
+                }
+                return gfCommandVector;
+        }
+        /**
+         * Reads the output from GF until the ending tag corresponding to the
+         * given opening tag is read. 
+         * @param opening tag in the format of &gt;gfinit&lt;
+         */
+        protected void skipChild(String opening) {
+                String closing = (new StringBuffer(opening)).insert(1, '/').toString();
+                try {
+                        String nextRead = fromProc.readLine();
+                        if (logger.isLoggable(Level.FINER)) {
+                                logger.finer("3 " + nextRead);
+                        }
+                        while (!nextRead.trim().equals(closing)) {
+                                nextRead = fromProc.readLine();
+                                if (logger.isLoggable(Level.FINER)) {
+                                        logger.finer("3 " + nextRead);
+                                }
+                        }
+                } catch (IOException e) {
+                        System.err.println("Could not read from external process:\n" + e);
+                }
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/GfeditResult.java

@@ -0,0 +1,61 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.Vector;
+/**
+ * Encapsulates the <gfedit> XML tree from GF.
+ * @author hdaniels
+ */
+class GfeditResult {
+        /**
+         * The fully parsed  <hmsg> subtree
+         */
+        final Hmsg hmsg;
+        /**
+         * A Vector of StringTuple where first is the command for GF
+         * and second is the show text
+         */
+        final Vector gfCommands;
+        /**
+         * The tree from GF isn't XML anyway, so here it is in all its raw glory
+         */
+        final String treeString;
+        /**
+         * if GF had something extra to tell, it can be found here
+         */
+        final String message;
+        /**
+         * The XML for the linearizations in all languages
+         */
+        final String linearizations;
+        /**
+         * A simple setter constructor
+         * @param gfCommands A Vector of StringTuple where first is the command for GF
+         * and second is the show text
+         * @param hmsg The fully parsed  <hmsg> subtree
+         * @param linearizations The XML for the linearizations in all languages
+         * @param message the GF message
+         * @param treeString The tree from GF
+         */
+        public GfeditResult(Vector gfCommands, Hmsg hmsg, String linearizations, String message, String treeString) {
+                this.gfCommands = gfCommands;
+                this.hmsg = hmsg;
+                this.linearizations = linearizations;
+                this.message = message;
+                this.treeString = treeString;
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/GrammarFilter.java

@@ -0,0 +1,46 @@
+//Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.io.File;
+import javax.swing.filechooser.*;
+
+public class GrammarFilter extends FileFilter {
+        
+        // Accept all directories and all gf, gfcm files.
+        public boolean accept(File f) {
+                if (f.isDirectory()) {
+                        return true;
+                }
+                
+                String extension = Utils.getExtension(f);
+                if (extension != null) {
+                        if (extension.equals(Utils.gf) ||
+                                        extension.equals(Utils.gfcm)) {
+                                return true;
+                        } else {
+                                return false;
+                        }
+                }
+                
+                return false;
+        }
+        
+        // The description of this filter
+        public String getDescription() {
+                return "Just Grammars (*.gf, *.gfcm)";
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/Hmsg.java

@@ -0,0 +1,77 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * The parsed format of the hmsg, that GF sents, if a command in java mode
+ * was prefixed with [something].
+ * And that something gets parsed and stored in this representation.
+ * @author daniels
+  */
+class Hmsg {
+        /**
+         * The last read line
+         */
+        String lastline = "";
+        /**
+         * the String that should be appended to all commands of the 
+         * next refinement menu
+         */
+        String appendix = null;
+        /**
+         *  If the editor shall probe once again for missing subtyping witnesses.
+         *  Unused.
+         */
+        boolean onceAgain = false;
+        /**
+         * If false, no commands are executed automatically
+         * in the next GF reading run 
+         */
+        boolean recurse = false;
+        /**
+         * if the newObject flag should be set
+         */
+        boolean newObject = false;
+        /**
+         * if the command changed the tree, so that it has to be rebuilt
+         */
+        boolean treeChanged = false;
+        /**
+         * if the display should be cleared
+         */
+        boolean clear = false;
+        /**
+         * A simple setter constructor
+         * @param lastRead The last read line
+         * @param appendix the String that should be appended to all commands of the 
+         * next refinement menu
+         * @param onceAgain
+         * @param recurse If false, no commands are executed automatically
+         * in the next GF reading run 
+         * @param newObject if the newObject flag should be set
+         * @param treeChanged if the command changed the tree, so that it has to be rebuilt
+         * @param clear if the display should get cleared
+         */
+        public Hmsg(String lastRead, String appendix, boolean onceAgain, boolean recurse, boolean newObject, boolean treeChanged, boolean clear) {
+                this.lastline = lastRead;
+                this.appendix = appendix;
+                this.onceAgain = onceAgain;
+                this.recurse = recurse;
+                this.newObject = newObject;
+                this.treeChanged = treeChanged;
+                this.clear = clear;
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/InputCommand.java

@@ -0,0 +1,141 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+import java.util.HashSet;
+
+/**
+ * @author daniels
+ *
+ *  This class represents a fake command, i.e. nothing is send to GF here.
+ *  Instead this class acts more like a placeholder for the input dialog.
+ *  This dialog is handled in GFEditor2 when a InputCommand is executed.
+ *  Reason: No GUI stuff in the command.
+ */
+class InputCommand extends GFCommand {
+        public static InputCommand intInputCommand = new InputCommand("read in Integer", 
+                        "opens a dialog window in which an Integer can be entered", 
+                        int.class, 
+                        "Please enter an Integer");
+        public static InputCommand stringInputCommand = new InputCommand("read in String", 
+                        "opens a dialog window in which a String can be entered", 
+                        String.class, 
+                        "Please enter a String");
+        
+        protected InputCommand(final String description, final String ttt, Class type, final String title) {
+                this.type = type;
+                this.tooltipText = ttt;
+                this.displayText = description;
+                this.titleText = title;
+                this.command = type.getName();
+        }
+        
+        protected Class type;
+
+        /**
+         * the text that is to be displayed as the title in the input window 
+         */        
+        protected final String titleText;
+        /**
+         * the text that is to be displayed as the title in the input window 
+         */
+        public String getTitleText() {
+                return titleText;
+        }
+        
+        /**
+         * stores the entered values, so they can be offered to the user
+         * the next time, in case, he wants them again.
+         */
+        protected final HashSet enteredValues = new HashSet();
+        
+        /**
+         * the text that is to be displayed as the tooltip 
+         */        
+        protected final String tooltipText;
+        /**
+         * the text that is to be displayed as the tooltip 
+         */
+        public String getTooltipText() {
+                return tooltipText;
+        }
+        
+        /** 
+         * the text that is to be displayed in the refinement lists 
+         */
+        protected final String displayText;
+        /** 
+         * the text that is to be displayed in the refinement lists 
+         */
+        public String getDisplayText() {
+                return displayText;
+        }
+        /** 
+         * the subcategory of this command 
+         */
+        public String getSubcat() {
+                return null;
+        }
+        
+        /**
+         * Checks if the given String can be converted into
+         * the Type of this InputCommand (int or String).
+         * If that is possible, the converted object is saved
+         * in enteredValues for later redisplay for the user.
+         * @param o The String the user has typed
+         * @param reason If the entered String is not parseable as the expected
+         * type, an error message is appended to this StringBuffer, so better
+         * give an empty one.
+         * @return an Object whose toString() should send the right
+         * thing to GF. 
+         * Maybe null, if this "conversion" failed.
+         */
+        protected Object validate(String o, StringBuffer reason) {
+                Object result = null;
+                if (type == int.class) {
+                        int i;
+                        try {
+                              i = Integer.parseInt(o);
+                              result = new Integer(i);
+                        } catch (NumberFormatException e) {
+                                reason.append("Input format error: '" + o + "' is no Integer");
+                        }
+                } else if (type == String.class) {
+                        if (o != null) {
+                                result = "\"" + o.toString() + "\"";
+                        }
+                }
+                if (result != null) {
+                        this.enteredValues.add(result);
+                }
+                return result;
+        }
+        
+        /**
+         * selects the suiting InputCommand for the given full name of a type
+         * @param typeName at the moment, either int.class.getName() or String.class.getName()
+         * @return intInputCommand for int, stringInputCommand for String or null otherwise 
+         */
+        protected static InputCommand forTypeName(String typeName) {
+                InputCommand ic = null;
+                if (typeName.equals(int.class.getName())) {
+                        ic = InputCommand.intInputCommand;
+                } else if (typeName.equals(String.class.getName())) {
+                        ic = InputCommand.stringInputCommand;
+                }
+                return ic;
+        }
+        
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/LanguageManager.java

@@ -0,0 +1,39 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * Sadly, this class is a hack.
+ * It serves as the pointer type to an inner class of GFEditor2.
+ * Two of its methods are needed outside after refactoring.
+ * @author daniels
+ *
+ */
+interface LanguageManager {
+        /**
+         * @param myLang The language in question
+         * @return true iff the language is present and set to active,
+         * false otherwise.
+         */        
+        public boolean isLangActive(String myLang);
+        /**
+         * Checks if myLang is already present, and if not,
+         * adds it. In that case, myActive is ignored.
+         * @param myLang The name of the language
+         * @param myActive whether the language is displayed or not
+         */
+        public void add(String myLang, boolean myActive);
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinPosition.java

@@ -0,0 +1,157 @@
+//Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * represents a position in the AST in Haskell notation together
+ * with a flag that indicates whether at least one constraint does not hold or
+ * if all hold (correct/incorrect). 
+ * Class is immutable.
+ */
+class LinPosition {
+        /**
+         * a position in the AST in Haskell notation
+         */
+        final public String position;
+
+        /**
+         * true means green, false means red (janna guesses)
+         */
+        final public boolean correctPosition;
+        
+        /**
+         * creates a LinPosition 
+         * @param p the position in the AST in Haskell notation like [0,1,2]
+         * @param cor false iff there are violated constraints
+         */
+        LinPosition(String p, boolean cor) {
+                position = p;
+                correctPosition = cor;
+        }
+        
+        /**
+         * Creates a position string in Haskell notation for the argument 
+         * number nr of this node.
+         * @param nr The number of the wanted argument
+         * @return the position string for the nrth child
+         */
+        public String childPosition(int nr) {
+                return calculateChildPosition(this.position, nr);
+        }
+        
+        /**
+         * Creates a position string in Haskell notation for the argument 
+         * number nr for the position pos
+         * @param pos The position of the to be parent
+         * @param nr The number of the wanted argument
+         * @return the position string for the nrth child of pos
+         */
+        protected static String calculateChildPosition(String pos, int nr) {
+                if ("[]".equals(pos)) {
+                        return "[" + nr + "]";
+                } else {
+                        return pos.trim().substring(0, pos.length() - 1) + "," + nr + "]";
+                }
+        }
+
+        /**
+         * Creates a position string in Haskell notation for the argument 
+         * number nr for the position pos' parent, i.e. brethren number nr.
+         * Example: calculateBrethrenPosition("[0,0,1]", 3).equals("[0,0,3]")
+         * @param pos The position of a brethren of the wanted
+         * @param nr The number of the wanted brethren
+         * @return the position string for the nrth brother of pos
+         */
+        protected static String calculateBrethrenPosition(String pos, int nr) {
+                if ("[]".equals(pos)) {
+                        return "[]"; //no brethren possible here
+                } else if (pos.lastIndexOf(',') == -1) {
+                        return "[" + nr + "]"; //one below top
+                } else {
+                        final String newPos = pos.substring(0, pos.lastIndexOf(',') + 1) + nr + "]";  
+                        return newPos;
+                }
+                
+        }
+
+        /**
+         * compares two position strings and returns true, if superPosition is
+         * a prefix of subPosition, that is, if subPosition is in a subtree of
+         * superPosition
+         * @param superPosition the position String in Haskell notation 
+         * ([0,1,0,4]) of the to-be super-branch of subPosition
+         * @param subPosition the position String in Haskell notation 
+         * ([0,1,0,4]) of the to-be (grand-)child-branch of superPosition
+         * @return true iff superPosition denotes an ancestor of subPosition 
+         */
+        public static boolean isSubtreePosition(final LinPosition superPosition, final LinPosition subPosition) {
+                if (superPosition == null || subPosition == null) {
+                        return false;
+                }
+                String superPos = superPosition.position;
+                String subPos = subPosition.position;
+                if (superPos.length() < 2 || subPos.length() < 2 ) {
+                        return false;
+                }
+                superPos = superPos.substring(1, superPos.length() - 1);
+                subPos = subPos.substring(1, subPos.length() - 1);
+                boolean result = subPos.startsWith(superPos);
+                return result;
+        }     
+        
+        /** 
+         * Returns the biggest position of first and second.
+         * Each word in the linearization area has the corresponding
+         * position in the tree. The position-notion is taken from 
+         * GF-Haskell, where empty position ("[]") 
+         * represents tree-root, "[0]" represents  first child of the root,
+         * "[0,0]" represents the first grandchild of the root etc.
+         * So comparePositions("[0]","[0,0]")="[0]"
+         */
+        public static String maxPosition(String first, String second) {
+                String common ="[]";
+                int i = 1; 
+                while ((i<Math.min(first.length()-1,second.length()-1))&&(first.substring(0,i+1).equals(second.substring(0,i+1)))) {
+                        common=first.substring(0,i+1); 
+                        i+=2;
+                }
+                if (common.charAt(common.length()-1)==']') {
+                        return common;
+                } else { 
+                        return common+"]";
+                }
+        }
+        
+        /**
+         * @return The Haskell position string for the parent of this position.
+         * If self is already the top node, [] is returned.
+         */
+        public String parentPosition() {
+                if (this.position.equals("[]")) {
+                        return this.position;
+                } else if (this.position.lastIndexOf(',') == -1) {
+                        return "[]"; //one below top
+                } else {
+                        final String newPos = this.position.substring(0, this.position.lastIndexOf(',')) + "]";  
+                        return newPos;
+                }
+        }
+        
+        public String toString() {
+                return position + (correctPosition ? " correct" : " incorrect");
+        }
+}
+

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/Linearization.java

@@ -0,0 +1,760 @@
+//Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.Vector;
+import java.util.logging.Level;
+import java.util.logging.Logger;
+
+/**
+ * Encapsulates everything that has to do with the linearization.
+ * It is parsed here, and also the indices for click-in for pure text and HTML
+ * are managed here. They get calculated in GfCapsule.
+ * The result can be directly displayed, and this class has methods to translate
+ * the indices back to the respective tree positions.
+ * @author daniels
+  */
+class Linearization {
+        /** 
+         * linearization marking debug messages 
+         */
+        protected static Logger logger = Logger.getLogger(Linearization.class.getName());
+
+        /**
+         * contains all the linearization pieces as HtmlMarkedArea
+         * Needed to know to which node in the AST a word in the linHtmlPane 
+         * area belongs.
+         */
+        private Vector htmlOutputVector = new Vector();
+        /**
+         * the GF-output between <linearization> </linearization>  tags is stored here.
+         * Must be saved in case the displayed languages are changed.
+         * Only written in readLin
+         */
+        private String linearization = "";
+        /** 
+         * stack for storing the current position:
+         * When displaying, we start with the root of the AST.
+         * Whenever we start to display a node, it is pushed, and when it is completely displayed, we pop it.
+         * Only LinPositions are stored in here
+         * local in formLin?
+         * */
+        private Vector currentPosition = new Vector();
+
+        /**
+         * Must be the same Display as GFEditor2 uses
+         */
+        private Display display;
+        /**
+         *  to collect the linearization strings 
+         */
+        private HashMap linearizations = new HashMap();
+
+        
+        
+        /**
+         * Initializes this object and binds it to the given Display
+         * @param display The display, that the editor uses
+         */
+        public Linearization(Display display) {
+                this.display = display;
+        }
+        
+        /**
+         * @return Returns the linearizations.
+         */
+        HashMap getLinearizations() {
+                return linearizations;
+        }
+        
+        /**
+         * @param linearization The linearization to set.
+         */
+        void setLinearization(String linearization) {
+                this.linearization = linearization;
+        }
+
+        /**
+         * resets the output mechanism.
+         */
+        void reset() {
+                htmlOutputVector = new Vector();
+        }
+
+        /**
+         * Returns the widest position (see comments to comparePositions) 
+         * covered in the string from begin to end in the 
+         * linearization area.
+         * @param begin The index in htmlOutputVector of the first MarkedArea, that is possibly the max
+         * @param end The index in htmlOutputVector of the last MarkedArea, that is possibly the max
+         * @return the position in GF Haskell notation (hdaniels guesses)
+         */
+        private String findMax(int begin, int end) {
+                String max = (((MarkedArea)this.htmlOutputVector.elementAt(begin)).position).position;
+                for (int i = begin+1; i <= end; i++)
+                        max = LinPosition.maxPosition(max,(((MarkedArea)this.htmlOutputVector.elementAt(i)).position).position);
+                return max;
+        }
+        
+        /**
+         * Appends the string restString to display.
+         * It parses the subtree tags and registers them.
+         * The focus tag is expected to be replaced by subtree.
+         * @param restString string to append, with tags in it.
+         * @param clickable if true, the text is appended and the subtree tags are
+         * parsed. If false, the text is appended, but the subtree tags are ignored. 
+         * @param doDisplay true iff the output is to be displayed. 
+         * Implies, if false, that clickable is treated as false.
+         * @param language the current linearization language
+         */
+        private String appendMarked(String restString, final boolean clickable, boolean doDisplay, String language) {
+                String appendedPureText = "";
+                if (restString.length()>0) {
+                        /** 
+                         * the length of what is already displayed of the linearization.
+                         * Alternatively: What has been processed in restString since
+                         * subtreeBegin
+                         */
+                        int currentLength = 0;
+                        /** position of &lt;subtree */
+                        int subtreeBegin;
+                        /** position of &lt;/subtree */
+                        int subtreeEnd;
+                        
+                        if (clickable && doDisplay) {
+                                subtreeBegin = Utils.indexOfNotEscaped(restString, "<subtree");
+                                subtreeEnd = Utils.indexOfNotEscaped(restString, "</subtree");
+                                // cutting subtree-tags:
+                                while ((subtreeEnd>-1)||(subtreeBegin>-1)) {
+                                        /** 
+                                         * length of the portion that is to be displayed
+                                         * in the current run of appendMarked.
+                                         * For HTML this would have to be calculated
+                                         * in another way.
+                                         */
+                                        final int newLength;
+
+                                        if ((subtreeEnd==-1)||((subtreeBegin<subtreeEnd)&&(subtreeBegin>-1))) {
+                                                final int subtreeTagEnd = Utils.indexOfNotEscaped(restString, ">",subtreeBegin);                                      
+                                                final int nextOpeningTagBegin = Utils.indexOfNotEscaped(restString, "<", subtreeTagEnd);
+                                                
+                                                //getting position:
+                                                final int posStringBegin = Utils.indexOfNotEscaped(restString, "[",subtreeBegin);
+                                                final int posStringEnd = Utils.indexOfNotEscaped(restString, "]",subtreeBegin);
+                                                final LinPosition position = new LinPosition(restString.substring(posStringBegin,posStringEnd+1),
+                                                                restString.substring(subtreeBegin,subtreeTagEnd).indexOf("incorrect")==-1);
+                                                
+                                                // is something before the tag?
+                                                // is the case in the first run
+                                                if (subtreeBegin-currentLength>1) {
+                                                        if (logger.isLoggable(Level.FINER)) {
+                                                                logger.finer("SOMETHING BEFORE THE TAG");
+                                                        }
+                                                        if (this.currentPosition.size()>0)
+                                                                newLength = register(currentLength, subtreeBegin, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString, language);
+                                                        else
+                                                                newLength = register(currentLength, subtreeBegin, new LinPosition("[]",
+                                                                                restString.substring(subtreeBegin,subtreeTagEnd).indexOf("incorrect")==-1), restString, language);
+                                                } else {       // nothing before the tag:
+                                                        //the case in the beginning
+                                                        if (logger.isLoggable(Level.FINER)) {
+                                                                logger.finer("NOTHING BEFORE THE TAG");             
+                                                        }
+                                                        if (nextOpeningTagBegin>0) {
+                                                                newLength = register(subtreeTagEnd+2, nextOpeningTagBegin, position, restString, language);
+                                                        } else {
+                                                                newLength = register(subtreeTagEnd+2, restString.length(), position, restString, language);
+                                                        }
+                                                        restString = removeSubTreeTag(restString,subtreeBegin, subtreeTagEnd+1);
+                                                }
+                                                currentLength += newLength ;
+                                        } else {
+                                                // something before the </subtree> tag:
+                                                if (subtreeEnd-currentLength>1) {
+                                                        if (logger.isLoggable(Level.FINER)) {
+                                                                logger.finer("SOMETHING BEFORE THE </subtree> TAG");
+                                                        }
+                                                        if (this.currentPosition.size()>0)
+                                                                newLength = register(currentLength, subtreeEnd, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString, language);
+                                                        else
+                                                                newLength = register(currentLength, subtreeEnd, new LinPosition("[]",
+                                                                                restString.substring(subtreeBegin,subtreeEnd).indexOf("incorrect")==-1), restString, language);
+                                                        currentLength += newLength ;
+                                                }
+                                                // nothing before the tag:
+                                                else 
+                                                        // punctuation after the </subtree> tag:
+                                                        if (restString.substring(subtreeEnd+10,subtreeEnd+11).trim().length()>0)
+                                                        {
+                                                                if (logger.isLoggable(Level.FINER)) {
+                                                                        logger.finer("PUNCTUATION AFTER THE </subtree> TAG"
+                                                                                        + "/n" + "STRING: " + restString);
+                                                                }
+                                                                //cutting the tag first!:
+                                                                if (subtreeEnd>0) {
+                                                                        restString =  removeSubTreeTag(restString,subtreeEnd-1, subtreeEnd+9); 
+                                                                } else {
+                                                                        restString = removeSubTreeTag(restString,subtreeEnd, subtreeEnd+9);
+                                                                }
+                                                                if (logger.isLoggable(Level.FINER)) {
+                                                                        logger.finer("STRING after cutting the </subtree> tag: "+restString);
+                                                                }
+                                                                // cutting the space in the last registered component:
+                                                                if (this.htmlOutputVector.size()>0) {
+                                                                        ((MarkedArea)this.htmlOutputVector.elementAt(this.htmlOutputVector.size()-1)).end -=1; 
+                                                                        if (currentLength>0) {
+                                                                                currentLength -=1; 
+                                                                        }
+                                                                }
+                                                                if (logger.isLoggable(Level.FINER)) {
+                                                                        logger.finer("currentLength: " + currentLength);
+                                                                }
+                                                                // register the punctuation:
+                                                                if (this.currentPosition.size()>0) {
+                                                                        newLength = register(currentLength, currentLength+2, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString, language);
+                                                                } else {
+                                                                        newLength = register(currentLength, currentLength+2, new LinPosition("[]",
+                                                                                        true), restString, language);
+                                                                }
+                                                                currentLength += newLength ;
+                                                        } else {
+                                                                // just cutting the </subtree> tag:
+                                                                restString = removeSubTreeTag(restString,subtreeEnd, subtreeEnd+10);
+                                                        }
+                                        }
+                                        subtreeEnd = Utils.indexOfNotEscaped(restString, "</subtree");
+                                        subtreeBegin = Utils.indexOfNotEscaped(restString, "<subtree");
+                                        //          if (debug2) 
+                                        //                System.out.println("/subtree index: "+l2 + "<subtree"+l);
+                                        if (logger.isLoggable(Level.FINER)) { 
+                                                logger.finer("<-POSITION: "+subtreeBegin+" CURRLENGTH: "+currentLength
+                                                                + "\n STRING: "+restString.substring(currentLength));
+                                        }
+                                } //while
+                        } else { //no focus, no selection enabled (why ever)
+                                //that means, that all subtree tags are removed here.
+                                if (logger.isLoggable(Level.FINER)) {
+                                        logger.finer("NO SELECTION IN THE TEXT TO BE APPENDED!");
+                                }
+                                //cutting tags from previous focuses if any:
+                                int r = Utils.indexOfNotEscaped(restString, "</subtree>");
+                                while (r>-1) {
+                                        // check if punktualtion marks like . ! ? are at the end of a sentence:
+                                        if (restString.charAt(r+10)==' ')
+                                                restString = restString.substring(0,r)+restString.substring(r+11);
+                                        else
+                                                restString = restString.substring(0,r)+restString.substring(r+10);
+                                        r = Utils.indexOfNotEscaped(restString, "</subtree>");
+                                }
+                                r = Utils.indexOfNotEscaped(restString, "<subtree");
+                                while (r>-1) {
+                                        int t = Utils.indexOfNotEscaped(restString, ">", r);
+                                        if (t<restString.length()-2)
+                                                restString = restString.substring(0,r)+restString.substring(t+2);
+                                        else 
+                                                restString = restString.substring(0,r);
+                                        r = Utils.indexOfNotEscaped(restString, "<subtree");
+                                }
+                        }
+                        // appending:
+                        restString = unescapeTextFromGF(restString);
+                        if (logger.isLoggable(Level.FINER)) {
+                                logger.finer(restString);
+                        }
+                        appendedPureText = restString.replaceAll("&-","\n ");
+                        //display the text if not already done in case of clickable
+                        if (!clickable && doDisplay) {
+                                // the text has only been pruned from markup, but still needs
+                                // to be displayed
+                                this.display.addToStages(appendedPureText, appendedPureText);
+                        }
+                } // else: nothing to append
+                return appendedPureText;
+        }
+        
+        /**
+         * Replaces a number of escaped characters by an unescaped version
+         * of the same length
+         * @param string The String with '\' as the escape character
+         * @return the same String, but with escaped characters removed
+         * 
+         */
+        static String unescapeTextFromGF(String string) {
+                final String more = "\\"+">";
+                final String less = "\\"+"<";
+                //%% by daniels, linearization output will be changed drastically 
+                //(or probably will), so for now some hacks for -> and >=
+                string = Utils.replaceAll(string, "-" + more, "-> ");
+                string = Utils.replaceAll(string, "-" + more,"-> ");
+                string = Utils.replaceAll(string, more," >");
+                string = Utils.replaceAll(string, less," <");
+                //an escaped \ becomes a single \
+                string = Utils.replaceAll(string, "\\\\"," \\");
+                return string;
+        }
+        
+
+
+        /**
+         * The substring from start to end in workingString, together with
+         * position is saved as a MarkedArea in this.htmlOutputVector.
+         * The information from where to where the to be created MarkedArea
+         * extends, is calculated in this method.
+         * @param start The position of the first character in workingString
+         * of the part, that is to be registered.
+         * @param end The position of the last character in workingString
+         * of the part, that is to be registered.
+         * @param position the position in the tree that corresponds to
+         * the to be registered text
+         * @param workingString the String from which the displayed
+         * characters are taken from
+         * @param language the current linearization language
+         * @return newLength, the difference between end and start
+         */
+        private int register(int start, int end, LinPosition position, String workingString, String language) {
+                /**
+                 * the length of the piece of text that is to be appended now
+                 */
+                final int newLength = end-start;
+                // the tag has some words to register:
+                if (newLength>0) {
+                        final String stringToAppend = workingString.substring(start,end);
+                        //if (stringToAppend.trim().length()>0) {
+
+                        //get oldLength and add the new text
+                        String toAdd = unescapeTextFromGF(stringToAppend);
+                        final MarkedArea hma = this.display.addAsMarked(toAdd, position, language);
+                        this.htmlOutputVector.add(hma);
+                        if (logger.isLoggable(Level.FINER)) {
+                                logger.finer("HTML added  :      " + hma);
+                        }
+                } //some words to register
+                return newLength;
+        }
+        
+        /**
+         * removing subtree-tag in the interval start-end 
+         * and updating the coordinates after that
+         * basically part of appendMarked
+         * No subtree is removed, just the tag. 
+         * @param s The String in which the subtree tag should be removed
+         * @param start position in restString
+         * @param end position in restString
+         * @return the String without the subtree-tags in the given interval
+         */
+        private String removeSubTreeTag (final String s, final int start, final int end) {
+                String restString = s;
+                if (logger.isLoggable(Level.FINER)) { 
+                        logger.finer("removing: "+ start +" to "+ end);
+                }
+                int difference =end-start+1;
+                int positionStart, positionEnd;
+                if (difference>20) {
+                        positionStart = Utils.indexOfNotEscaped(restString, "[", start);
+                        positionEnd = Utils.indexOfNotEscaped(restString, "]", start);
+                        
+                        currentPosition.addElement(new LinPosition(
+                                        restString.substring(positionStart, positionEnd+1),
+                                        restString.substring(start,end).indexOf("incorrect")==-1));
+                } else if (currentPosition.size()>0) {
+                                currentPosition.removeElementAt(currentPosition.size()-1);
+                }
+                if (start>0) {
+                        restString = restString.substring(0,start)+restString.substring(end+1);
+                } else{
+                        restString = restString.substring(end+1);
+                }
+                return restString;
+        }
+        
+        /**
+         * Goes through the list of MarkedAreas and creates MarkedAreaHighlightingStatus
+         * objects for them, which contain fields for incorrect constraints
+         * and if they belong to the selected subtree.
+         * @param focusPosition The AST position of the selected node
+         * @return a Vector of MarkedAreaHighlightingStatus
+         */
+        Vector calculateHighlights(LinPosition focusPosition) {
+                Vector result = new Vector();
+                final HashSet incorrectMA = new HashSet();
+                for (int i = 0; i<htmlOutputVector.size(); i++)  {
+                        final MarkedArea ma = (MarkedArea)this.htmlOutputVector.elementAt(i);
+                        //check, if and how ma should be highlighted
+                        boolean incorrect = false;
+                        boolean focused = false;
+                        if (logger.isLoggable(Level.FINER)) {
+                                logger.finer("Highlighting: " + ma);
+                        }
+                        if (!ma.position.correctPosition) {
+                                incorrectMA.add(ma);
+                                incorrect = true;
+                        } else {
+                                //This could be quadratic, but normally on very
+                                //few nodes constraints are introduced, so
+                                //incorrectMA should not contain many elements.
+                                MarkedArea incMA;
+                                for (Iterator it = incorrectMA.iterator(); !incorrect && it.hasNext();) {
+                                        incMA = (MarkedArea)it.next();
+                                        if (LinPosition.isSubtreePosition(incMA.position, ma.position)) {
+                                                incorrect = true;
+                                        }
+                                }
+                        }
+                        if (LinPosition.isSubtreePosition(focusPosition, ma.position)) {
+                                focused = true;
+                        }
+                        MarkedAreaHighlightingStatus mahs = new MarkedAreaHighlightingStatus(focused, incorrect, ma);
+                        result.add(mahs);
+                }
+                return result;
+        }
+
+        /**
+         * Parses the linearization XML and calls outputAppend
+         * @param langMan The LangMenuModel, but that is an inner class and only
+         * the methods in the Interface LanguageManager are used here.
+         */
+        void parseLin(LanguageManager langMan) {
+                linearizations.clear();
+                boolean firstLin=true; 
+                //read first line like '    <lin lang=Abstract>'
+                String readResult = linearization.substring(0,linearization.indexOf('\n'));
+                //the rest of the linearizations
+                String lin = linearization.substring(linearization.indexOf('\n')+1);
+                //extract the language from readResult
+                int ind = Utils.indexOfNotEscaped(readResult, "=");
+                int ind2 = Utils.indexOfNotEscaped(readResult, ">");
+                /** The language of the linearization */
+                String language = readResult.substring(ind+1,ind2);
+                //the first direct linearization
+                readResult = lin.substring(0,lin.indexOf("</lin>"));
+                //the rest
+                lin = lin.substring(lin.indexOf("</lin>"));
+                while (readResult.length()>1) {
+                        langMan.add(language,true);
+                        // selected?
+                        boolean visible = langMan.isLangActive(language);
+                        if (visible && !firstLin) {   
+                                // appending sth. linearizationArea
+                                this.display.addToStages("\n************\n", "<br><hr><br>");
+                        }
+                        if (logger.isLoggable(Level.FINER)) {
+                                logger.finer("linearization for the language: "+readResult);
+                        }
+
+                        // change the focus tag into a subtree tag.
+                        // focus handling now happens in GFEditor2::formTree
+                        String readLin = readResult;
+                        readLin = Utils.replaceNotEscaped(readLin, "<focus", "<subtree");
+                        readLin = Utils.replaceNotEscaped(readLin, "</focus", "</subtree");
+                        
+                        final boolean isAbstract = "Abstract".equals(language);                        
+                        // now do appending and registering
+                        String linResult = appendMarked(readLin + '\n', !isAbstract, visible, language);
+
+                        if (visible) {
+                                firstLin = false;
+                        }
+                        linearizations.put(language, linResult);
+                        // read </lin>
+                        lin = lin.substring(lin.indexOf('\n')+1);
+                        // read lin or 'end'
+                        if (lin.length()<1) {
+                                break;
+                        }
+                        
+                        readResult = lin.substring(0,lin.indexOf('\n'));
+                        lin = lin.substring(lin.indexOf('\n')+1);
+                        if (readResult.indexOf("<lin ")!=-1){
+                                //extract the language from readResult
+                                ind = readResult.indexOf('=');
+                                ind2 = readResult.indexOf('>');
+                                language = readResult.substring(ind+1,ind2);
+                                readResult = lin.substring(0,lin.indexOf("</lin>"));
+                                lin = lin.substring(lin.indexOf("</lin>"));
+                        }  
+                }
+        }
+
+        /**
+         * 
+         * @param language The concrete language of choice
+         * @return The linearization of the subtree starting with the currently
+         * selected node in the given language.
+         */
+        String getSelectedLinearization(final String language, final LinPosition focusPosition) {
+                StringBuffer sel = new StringBuffer();
+                for (int i = 0; i<htmlOutputVector.size(); i++)  {
+                        final MarkedArea ma = (MarkedArea)htmlOutputVector.elementAt(i);
+                        if (language.equals(ma.language) && LinPosition.isSubtreePosition(focusPosition, ma.position)) {
+                                sel.append(ma.words);
+                        }
+                }
+                return sel.toString();
+        }
+
+        /**
+         * Takes the index of a caret position in the linearization area
+         * and returns the language of the clicked linearization.
+         * GF lists the different concrete languages one after the other,
+         * and this method looks at the linearization snipplets to get
+         * the language.
+         * If somehow no language can be found out, 'Abstract' is returned
+         * @param pos The index of the caret position
+         * @param htmlClicked If the HTML JTextPane has been clicked,
+         * false for the JTextArea
+         * @return the name of the concrete grammar (language) or Abstract
+         * (see above).
+         */
+        String getLanguageForPos(int pos, final boolean htmlClicked) {
+                final String language;
+                MarkedArea ma = null;
+                if (htmlClicked) {
+                        //HTML
+                        for (int i = 0; i < htmlOutputVector.size(); i++) {
+                                if ((pos >= ((MarkedArea)htmlOutputVector.get(i)).htmlBegin) && (pos <= ((MarkedArea)htmlOutputVector.get(i)).htmlEnd)) {
+                                        ma = (MarkedArea)htmlOutputVector.get(i);
+                                        break;
+                                }
+                        }
+                } else {
+                        //assumably pure text
+                        for (int i = 0; i < htmlOutputVector.size(); i++) {
+                                if ((pos >= ((MarkedArea)htmlOutputVector.get(i)).begin) && (pos <= ((MarkedArea)htmlOutputVector.get(i)).end)) {
+                                        ma = (MarkedArea)htmlOutputVector.get(i);
+                                        break;
+                                }
+                        }
+                        
+                }
+                if (ma != null && ma.language != null) {
+                        language = ma.language;
+                } else {
+                        language = "Abstract";
+                }
+                return language;
+        }
+
+        /**
+         * The user has either just clicked in the linearization area,
+         * which means start == end, or he has selected a text, so that 
+         * start < end.
+         * This method figures out the smallest subtree whose linearization
+         * completely encompasses the area from start to end.
+         * This method is for the HTML linearization area.
+         * @param start The index of the caret position at the begin of the selection
+         * @param end The index of the caret position at the end of the selection
+         * @return The 'root' of the subtree described above
+         */
+        String markedAreaForPosHtml(int start, int end) {
+                if (htmlOutputVector.isEmpty()) {
+                        return null;
+                }
+                String position = null; //the result
+                String jPosition ="", iPosition="";
+                MarkedArea jElement = null;
+                MarkedArea iElement = null;
+                int j = 0;
+                int i = htmlOutputVector.size()-1;
+
+                if (logger.isLoggable(Level.FINER))
+                        for (int k=0; k < htmlOutputVector.size(); k++) { 
+                                logger.finer("element: "+k+" begin "+((MarkedArea)htmlOutputVector.elementAt(k)).htmlBegin+" "
+                                                + "\n-> end: "+((MarkedArea)htmlOutputVector.elementAt(k)).htmlEnd+" "       
+                                                + "\n-> position: "+(((MarkedArea)htmlOutputVector.elementAt(k)).position).position+" "   
+                                                + "\n-> words: "+((MarkedArea)htmlOutputVector.elementAt(k)).words);   
+                        }
+                // localizing end:
+                while ((j < htmlOutputVector.size()) && (((MarkedArea)htmlOutputVector.elementAt(j)).htmlEnd < end)) {
+                        j++;
+                }
+                // localising start:
+                while ((i >= 0) && (((MarkedArea)htmlOutputVector.elementAt(i)).htmlBegin > start)) {
+                        i--;
+                }
+                if (logger.isLoggable(Level.FINER)) { 
+                        logger.finer("i: "+i+" j: "+j);
+                }
+                if ((j < htmlOutputVector.size())) {
+                        jElement = (MarkedArea)htmlOutputVector.elementAt(j);
+                        jPosition = jElement.position.position;
+                        // less & before:
+                        if (i == -1) { // less:
+                                if (end>=jElement.htmlBegin) {
+                                        iElement = (MarkedArea)htmlOutputVector.elementAt(0);
+                                        iPosition = iElement.position.position;
+                                        if (logger.isLoggable(Level.FINER)) { 
+                                                logger.finer("Less: "+jPosition+" and "+iPosition);
+                                        }
+                                        position = findMax(0,j);
+                                        if (logger.isLoggable(Level.FINER)) { 
+                                                logger.finer("SELECTEDTEXT: "+position+"\n");
+                                        }
+                                } else { // before: 
+                                        if (logger.isLoggable(Level.FINER)) { 
+                                                logger.finer("BEFORE vector of size: "+htmlOutputVector.size());
+                                        }
+                                }
+                        } else { // just: 
+                                iElement = (MarkedArea)htmlOutputVector.elementAt(i);
+                                iPosition = iElement.position.position;
+                                if (logger.isLoggable(Level.FINER)) { 
+                                        logger.finer("SELECTED TEXT Just: "+iPosition +" and "+jPosition+"\n");
+                                }
+                                position = findMax(i,j);
+                                if (logger.isLoggable(Level.FINER)) { 
+                                        logger.finer("SELECTEDTEXT: "+position+"\n");
+                                }
+                        }
+                }  else if (i>=0) { // more && after:
+                        iElement = (MarkedArea)htmlOutputVector.elementAt(i);
+                        iPosition = iElement.position.position;
+                        // more
+                        if (start<=iElement.htmlEnd) { 
+                                jElement = (MarkedArea)htmlOutputVector.elementAt(htmlOutputVector.size()-1);
+                                jPosition = jElement.position.position;
+                                if (logger.isLoggable(Level.FINER)) { 
+                                        logger.finer("MORE: "+iPosition+ " and "+jPosition);
+                                }
+                                position = findMax(i,htmlOutputVector.size()-1);
+                                if (logger.isLoggable(Level.FINER)) { 
+                                        logger.finer("SELECTEDTEXT: "+position+"\n");
+                                }
+                                // after:
+                        } else if (logger.isLoggable(Level.FINER)) { 
+                                logger.finer("AFTER vector of size: "+htmlOutputVector.size());
+                        }
+                } else { // bigger:
+                        iElement = (MarkedArea)htmlOutputVector.elementAt(0);
+                        iPosition = iElement.position.position;
+                        jElement = (MarkedArea)htmlOutputVector.elementAt(htmlOutputVector.size()-1);
+                        jPosition = jElement.position.position;
+                        if (logger.isLoggable(Level.FINER)) { 
+                                logger.finer("BIGGER: "+iPosition +" and "+jPosition+"\n"         
+                                                + "\n-> SELECTEDTEXT: []\n");
+                        }
+                        position = "[]";
+                }
+                return position;
+        }
+
+        /**
+         * The user has either just clicked in the linearization area,
+         * which means start == end, or he has selected a text, so that 
+         * start < end.
+         * This method figures out the smallest subtree whose linearization
+         * completely encompasses the area from start to end.
+         * This method is for the pure text linearization area.
+         * @param start The index of the caret position at the begin of the selection
+         * @param end The index of the caret position at the end of the selection
+         * @return The 'root' of the subtree described above
+         */
+        String markedAreaForPosPureText(int start, int end) {
+                if (htmlOutputVector.isEmpty()) {
+                        return null;
+                }
+                //the result
+                String position = null;
+                //variables for confining the searched MarkedArea from 
+                //start and end (somehow ...)
+                int j = 0;
+                int i = htmlOutputVector.size() - 1;
+                String jPosition ="", iPosition="";
+                MarkedArea jElement = null;
+                MarkedArea iElement = null;
+                
+                if (logger.isLoggable(Level.FINER))
+                        for (int k = 0; k < htmlOutputVector.size(); k++) { 
+                                logger.finer("element: " + k + " begin " + ((MarkedArea)htmlOutputVector.elementAt(k)).begin + " "
+                                + "\n-> end: " + ((MarkedArea)htmlOutputVector.elementAt(k)).end+" "       
+                                + "\n-> position: " + (((MarkedArea)htmlOutputVector.elementAt(k)).position).position+" "   
+                                + "\n-> words: " + ((MarkedArea)htmlOutputVector.elementAt(k)).words);   
+                        }
+                // localizing end:
+                while ((j < htmlOutputVector.size()) && (((MarkedArea)htmlOutputVector.elementAt(j)).end < end)) {
+                        j++;
+                }
+                // localising start:
+                while ((i >= 0) && (((MarkedArea)htmlOutputVector.elementAt(i)).begin > start))
+                        i--;
+                if (logger.isLoggable(Level.FINER)) { 
+                        logger.finer("i: " + i + " j: " + j);
+                }
+                if ((j < htmlOutputVector.size())) {
+                        jElement = (MarkedArea)htmlOutputVector.elementAt(j);
+                        jPosition = jElement.position.position;
+                        // less & before:
+                        if (i==-1) { // less:
+                                if (end>=jElement.begin) {
+                                        iElement = (MarkedArea)htmlOutputVector.elementAt(0);
+                                        iPosition = iElement.position.position;
+                                        if (logger.isLoggable(Level.FINER)) { 
+                                                logger.finer("Less: "+jPosition+" and "+iPosition);
+                                        }
+                                        position = findMax(0,j);
+                                        if (logger.isLoggable(Level.FINER)) { 
+                                                logger.finer("SELECTEDTEXT: "+position+"\n");
+                                        }
+                                } else  if (logger.isLoggable(Level.FINER)) { // before: 
+                                                logger.finer("BEFORE vector of size: " + htmlOutputVector.size());
+                                        }
+                        } else { // just: 
+                                iElement = (MarkedArea)htmlOutputVector.elementAt(i);
+                                iPosition = iElement.position.position;
+                                if (logger.isLoggable(Level.FINER)) { 
+                                        logger.finer("SELECTED TEXT Just: "+iPosition +" and "+jPosition+"\n");
+                                }
+                                position = findMax(i,j);
+                                if (logger.isLoggable(Level.FINER)) { 
+                                        logger.finer("SELECTEDTEXT: "+position+"\n");
+                                }
+                        }
+                } else if (i>=0) { // more && after:
+                                iElement = (MarkedArea)htmlOutputVector.elementAt(i);
+                                iPosition = iElement.position.position;
+                                // more
+                                if (start<=iElement.end) { 
+                                        jElement = (MarkedArea)htmlOutputVector.elementAt(htmlOutputVector.size() - 1);
+                                        jPosition = jElement.position.position;
+                                        if (logger.isLoggable(Level.FINER)) { 
+                                                logger.finer("MORE: "+iPosition+ " and "+jPosition);
+                                        }
+                                        position = findMax(i, htmlOutputVector.size()-1);
+                                        if (logger.isLoggable(Level.FINER)) { 
+                                                logger.finer("SELECTEDTEXT: "+position+"\n");
+                                        }
+                                } else if (logger.isLoggable(Level.FINER)) { // after: 
+                                        logger.finer("AFTER vector of size: " + htmlOutputVector.size());
+                                }
+                        } else {
+                                // bigger:
+                                iElement = (MarkedArea)htmlOutputVector.elementAt(0);
+                                iPosition = iElement.position.position;
+                                jElement = (MarkedArea)htmlOutputVector.elementAt(htmlOutputVector.size()-1);
+                                jPosition = jElement.position.position;
+                                if (logger.isLoggable(Level.FINER)) { 
+                                        logger.finer("BIGGER: "+iPosition +" and "+jPosition+"\n"         
+                                                        + "\n-> SELECTEDTEXT: []\n");
+                                }
+                                position = "[]";
+                        }
+                return position;
+        }
+        
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinkCommand.java

@@ -0,0 +1,85 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * @author daniels
+ * This class represents a link to a subcategory submenu. 
+ * When it is encountered as the executed command, the corresponding
+ * menu gets opened.
+ */
+public class LinkCommand extends GFCommand {
+        
+        /**
+         * Since LinkCommand is not a real command, that is sent to GF,
+         * most fields are given dummy values here.
+         * The subcat is assigned its full display name and tooltip
+         * @param subcat The subcategory of the menu behind this command
+         * @param manager The PrintnameManager, that can map subcat to its
+         * full name
+         */
+        public LinkCommand(final String subcat, final PrintnameManager manager) {
+                this.command = subcat;
+                this.newSubcat = false;
+                this.commandType = Printname.SUBCAT;
+                this.argument = -1;
+                this.funName = null;
+                this.printname = null;
+                
+                String dtext;
+                String ttext;
+                String fullname = manager.getFullname(subcat);
+                if (fullname == null) {
+                        dtext = getSubcat();
+                        ttext = "open submenu " + getSubcat();
+                } else {
+                        ttext = Printname.htmlPrepend(Printname.extractTooltipText(fullname), "<i>open submenu</i> <br> ");
+                        dtext = Printname.extractDisplayText(fullname);
+                }
+                this.tooltipText = ttext;
+                this.displayText = dtext;
+                
+        }
+        
+        /**
+         * the text that is to be displayed as the tooltip 
+         */        
+        protected final String tooltipText;
+        /**
+         * the text that is to be displayed as the tooltip 
+         */
+        public String getTooltipText() {
+                return tooltipText;
+        }
+        
+        /** 
+         * the text that is to be displayed in the refinement lists 
+         */
+        protected final String displayText;
+        /** 
+         * the text that is to be displayed in the refinement lists 
+         */
+        public String getDisplayText() {
+                return displayText;
+        }
+        /** 
+         * the subcategory of this command 
+         */
+        public String getSubcat() {
+                return this.command;
+        }
+        
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/MarkedArea.java

@@ -0,0 +1,84 @@
+//Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * Stores quasi a piece of the linearization area, that has a word, a beginning
+ * and an end in the linearization area and a position in the AST. It is used
+ * for clicking in the text
+ * 
+ * @author janna, daniels
+ */
+class MarkedArea {
+        /** 
+         * The starting position of the stored words 
+         */
+        final public int begin;
+        /** 
+         * The ending position of the stored words. 
+         * Not final because of some punctuation issue daniels 
+         * does not understand
+         */
+        public int end;
+        /** 
+         * The position in the AST 
+         */
+        final public LinPosition position;
+        /** 
+         * The actual text of this area 
+         */
+        final public String words;
+        /** 
+         * the concrete grammar (or better, its linearization) 
+         * this MarkedArea belongs to
+         */
+        final public String language;
+        
+        /** 
+         * the start index in the HTML area 
+         */
+        final public int htmlBegin;
+        /** 
+         * the end index in the HTML area 
+         */
+        final public int htmlEnd;
+        
+        /**
+         * A stand-alone constuctor which takes all values as arguments
+         * @param begin The starting position of the stored words
+         * @param end The ending position of the stored words
+         * @param position The position in the AST
+         * @param words The actual text of this area
+         * @param htmlBegin the start index in the HTML area
+         * @param htmlEnd the end index in the HTML area
+         * @param language the language of the current linearization
+         */
+        public MarkedArea(int begin, int end, LinPosition position, String words, int htmlBegin, int htmlEnd, String language) {
+                this.begin = begin;
+                this.end = end;
+                this.position = position;
+                this.words = words;
+                this.language = language;
+                this.htmlBegin = htmlBegin;
+                this.htmlEnd = htmlEnd;
+        }
+        
+        
+        public String toString() {
+                return begin + " - " + end + " : " + position + " = '" + words + "' ; HTML: " + htmlBegin + " - " + htmlEnd;
+        }
+}
+

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/MarkedAreaHighlightingStatus.java

@@ -0,0 +1,48 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * Stores a MarkedArea together with some status fields, which tell
+ * how it should get highlighted.
+ * No direct highlighting stuff in here, that's done in GFEditor2 
+ * @author daniels
+ */
+class MarkedAreaHighlightingStatus {
+        /**
+         * The MarkedArea, which contains the highlighting information
+         */
+        final MarkedArea ma;
+        /**
+         * whether this MarkedArea is a subnode of the currently focused node
+         */
+        final boolean focused;
+        /**
+         * whether this MarkedArea has (inherited) a GF constraint
+         */
+        final boolean incorrect;
+        /**
+         * Initializes this immutable record class
+         * @param focused whether this MarkedArea is a subnode of the currently focused node
+         * @param incorrect whether this MarkedArea has (inherited) a GF constraint
+         * @param ma The MarkedArea, which contains the highlighting information
+         */
+        public MarkedAreaHighlightingStatus(boolean focused, boolean incorrect, MarkedArea ma) {
+                this.focused = focused;
+                this.incorrect = incorrect;
+                this.ma = ma;
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/NewCategoryMenuResult.java

@@ -0,0 +1,57 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * GF sends the new menu as XML.
+ * After this has been parsed by GfCapsule, it is sent in this representation
+ * to GFEditor2.
+ * @author daniels
+ *
+ */
+class NewCategoryMenuResult {
+        /**
+         * The actual entries of the newMenu
+         */
+        final String[] menuContent;
+        /**
+         * The languages, that GF sent
+         */
+        final String[] languages;
+        /**
+         * the constituents of the import path?
+         */
+        final String[] paths;
+        /**
+         * the name of the abstract grammar, also called topic
+         */
+        final String grammarName;
+
+        /**
+         * Just sets the attributes of this class
+         * @param grammarName the name of the abstract grammar, also called topic
+         * @param menuContent The actual entries of the newMenu
+         * @param languages The languages, that GF sent
+         * @param paths the constituents of the import path?
+         */
+        public NewCategoryMenuResult(String grammarName, String[] menuContent, String[] languages, String paths[]) {
+                this.grammarName = grammarName;
+                this.menuContent = menuContent;
+                this.languages = languages;
+                this.paths = paths;
+        }
+        
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/NoLineBreakFormatter.java

@@ -0,0 +1,23 @@
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.logging.Formatter;
+import java.util.logging.LogRecord;
+
+/**
+ * @author daniels
+ * A simple Formatter class, that does not introduce linebreaks, so that
+ * continous lines can be read under each other.
+ */
+public class NoLineBreakFormatter extends Formatter {
+
+        /** 
+         * @see java.util.logging.Formatter#format(java.util.logging.LogRecord)
+         */
+        public String format(LogRecord record) {
+                final String shortLoggerName = record.getLoggerName().substring(record.getLoggerName().lastIndexOf('.') + 1);
+                return record.getLevel() + " : "
+                + shortLoggerName + " "
+                + record.getSourceMethodName() + " -:- "
+                + record.getMessage() + "\n";
+        }
+}

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

@@ -0,0 +1,569 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.Hashtable;
+import java.util.Vector;
+import java.util.logging.*;
+
+/**
+ * @author daniels
+ *
+ * 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 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
+ *     by their actual description.
+ * HTML can be used inside the descriptions and the tooltip text 
+ */
+class Printname {
+        private static Logger subcatLogger = Logger.getLogger(Printname.class.getName());
+        
+        /**
+         * delete is always the same and only consists of one letter, therefore static.
+         */
+        public static final Printname delete = new Printname("d", "delete current sub-tree", false);
+        /**
+         * The ac command i always the same, therefore static
+         */
+        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>", false);
+
+        /**
+         * @param arg The number of the argument, 
+         * that will take the place of the selected fun
+         * @return a Printname for the 'ph arg' command
+         */
+        public static Printname peelHead(int arg) {
+                final String cmd = "ph " + arg;
+                final String show = "peel head " + arg + "\\$removes this fun and moves its " + (arg + 1) + ". argument at its place instead";
+                return new Printname(cmd, show, true);
+        }
+        
+        /**
+         * the type of the fun behind that printname (if applicable)
+         */
+        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
+         */
+        public final static String TT_START = "\\$";
+        /** 
+         * the string that is followed by the sub-category shorthand
+         * in the refinement menu
+         */ 
+        public final static String SUBCAT = "\\%";
+        /**
+         * The string that is followed by a new parameter to the GF function
+         */
+        public final static String PARAM = "\\#";
+        /**
+         * If that follows "\#" in the parameter descriptions, then do an
+         * auto-coerce when this param is meta and selected 
+         */
+        public final static String AUTO_COERCE = "!";
+        
+        /** 
+         * the name of the fun that is used in this command 
+         */
+        protected final String fun;
+
+        /** 
+         * the printname of this function 
+         */
+        protected final String printname;
+        
+        /** 
+         * to cache the printname, once it is constructed 
+         */
+        protected String displayedPrintname = null;
+        /** 
+         * the name of the module the fun belongs to
+         * null means that the function is saved without module information,
+         * "" means that a GF command is represented
+         */
+        protected final String module;
+        /** 
+         * the name of the module the fun belongs to
+         * null means that the function is saved without module information,
+         * "" means that a GF command is represented
+         */
+        public String getModule() {
+                return module;
+        }
+        
+        
+        /** the qualified function name, not needed yet */
+        /*
+        public String getFunQualified() {
+                if (module != null && !module.equals("")) {
+                        return module + "." + fun;
+                } else {
+                        return fun;
+                }
+        }
+        */
+        
+        /** 
+         * the subcategory of this command 
+         */
+        protected final String subcat;
+        /** 
+         * the subcategory of this command 
+         */
+        public String getSubcat() {
+                return subcat;
+        }
+
+        /**
+         * The hashmap for the names of the sub categories, 
+         * with the shortname starting with '%' as the key.
+         * It is important that all Printnames of one session share the same
+         * instance of Hashtable here. 
+         * This field is not static because there can be several instances of
+         * the editor that shouldn't interfere.
+         */
+        protected final Hashtable subcatNameHashtable;
+
+        /**
+         * contains the names of the paramters of this function (String).
+         * Parallel with paramTexts
+         */
+        protected final Vector paramNames = new Vector();
+        
+        /**
+         * fetches the name of the nth parameter
+         * @param n the number of the wanted paramter
+         * @return the corresponding name, null if not found
+         */
+        public String getParamName(int n) {
+                String name = null;
+                try {
+                        name = (String)this.paramNames.get(n);
+                } catch (ArrayIndexOutOfBoundsException e) {
+                        subcatLogger.fine(e.getLocalizedMessage());
+                }
+                return name;
+        }
+        /**
+         * contains the descriptions of the paramters of this function (String).
+         * Parallel with paramNames
+         */
+        protected final Vector paramTexts = new Vector();
+
+        /**
+         * tells, whether the nth parameter should be auto-coerced
+         * @param n the number of the parameter in question
+         * @return whether the nth parameter should be auto-coerced
+         */
+        public boolean getParamAutoCoerce(int n) {
+                boolean result = false;
+                try {
+                        result = ((Boolean)this.paramAutoCoerce.get(n)).booleanValue();
+                } catch (ArrayIndexOutOfBoundsException e) {
+                        subcatLogger.fine(e.getLocalizedMessage());
+                }
+                return result;
+        }
+        
+        /**
+         * stores for the parameters whether they should be auto-coerced or not.
+         * parallel with paramNames
+         */
+        protected final Vector paramAutoCoerce = new Vector();
+        
+        /**
+         * Creates a Printname for a normal GF function
+         * @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
+         * @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();
+                myPrintname = myPrintname.trim();
+                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('.');
+                        if (index > -1) {
+                                //a valid fun name must not be empty
+                                this.fun = myFun.substring(index + 1);
+                                this.module = myFun.substring(0, index);
+                        } else {
+                                this.fun = myFun;
+                                this.module = null;
+                        }
+                }
+                
+                //parse the parameters and cut that part
+                {
+                        int index = Utils.indexOfNotEscaped(myPrintname, PARAM);
+                        if (index > -1) {
+                                String paramPart = myPrintname.substring(index);
+                                String splitString;
+                                //split takes a regexp as an argument. So we have to escape the '\' again.
+                                if (PARAM.startsWith("\\")) {
+                                        splitString = "\\" + PARAM;
+                                } else {
+                                        splitString = PARAM;
+                                }
+                                String[] params = paramPart.split(splitString);
+                                //don't use the first split part, since it's empty
+                                for (int i = 1; i < params.length; i++) {
+                                        String current = params[i];
+                                        boolean autocoerce = false;
+                                        if (AUTO_COERCE.equals(current.substring(0,1))) {
+                                                autocoerce = true;
+                                                //cut the !
+                                                current = current.substring(1);
+                                        }
+                                        int nameEnd = current.indexOf(' ');
+                                        int nameEnd2 = Utils.indexOfNotEscaped(current, PARAM);
+                                        if (nameEnd == -1) {
+                                                nameEnd = current.length();
+                                        }
+                                        String name = current.substring(0, nameEnd);
+                                        String description;
+                                        if (nameEnd < current.length() - 1) {
+                                                description = current.substring(nameEnd + 1).trim();
+                                        } else {
+                                                description = "";
+                                        }
+                                        this.paramNames.addElement(name);
+                                        this.paramTexts.addElement(description);
+                                        this.paramAutoCoerce.addElement(new Boolean(autocoerce));
+                                }
+                                myPrintname = myPrintname.substring(0, index);
+                        }
+                }
+                
+                
+                //extract the subcategory part and cut that part
+                {
+                        int index = Utils.indexOfNotEscaped(myPrintname, SUBCAT);
+                        if (index > -1) {
+                                String subcatPart = myPrintname.substring(index);
+                                myPrintname = myPrintname.substring(0, index);
+                                int indFull = subcatPart.indexOf('{');
+                                if (indFull > -1) {
+                                        int indFullEnd = subcatPart.indexOf('}', indFull + 1);
+                                        if (indFullEnd == -1) {
+                                                indFullEnd = subcatPart.length();
+                                        }
+                                        String fullName = subcatPart.substring(indFull + 1, indFullEnd);
+                                        this.subcat = subcatPart.substring(0, indFull).trim();
+                                        this.subcatNameHashtable.put(this.subcat, fullName);
+                                        if (subcatLogger.isLoggable(Level.FINER)) {
+                                                subcatLogger.finer("new fullname '" + fullName + "' for category (shortname) '" + this.subcat + "'");
+                                        }
+                                } else {
+                                        subcat = subcatPart.trim();
+                                }
+                                
+                        } else {
+                                this.subcat = null; 
+                        }
+                }
+        }
+
+        /**
+         * a constructor for GF command that don't represent functions,
+         * like d, ph, ac
+         * @param command the GF command
+         * @param explanation an explanatory text what this command does
+         * @param funPresent If explanation already contains the fun.
+         * If true, the fun won't be printed in the refinement menu.
+         */
+        protected Printname(String command, String explanation, boolean funPresent) {
+                this.fun = command;
+                this.subcatNameHashtable = null;
+                this.subcat = null;
+                this.module = "";
+                this.printname = explanation;
+                this.type = null;
+                this.funPresent = funPresent;
+        }
+        
+        /**
+         * Special constructor for bound variables.
+         * These printnames don't get saved since they don't always exist and
+         * also consist of quite few information.
+         * @param bound The name of the bound variable
+         */
+        public Printname(String bound) {
+                this.fun = bound;
+                this.subcatNameHashtable =  null;
+                this.subcat = null;
+                this.module = null;
+                this.printname = bound;
+                this.type = null;
+                this.funPresent = false;
+        }
+        
+        /** 
+         * the text that is to be displayed in the refinement lists 
+         */
+        public String getDisplayText() {
+                String result;
+                result = extractDisplayText(this.printname);
+                return result;
+        }
+
+        /**
+         * the text that is to be displayed as the tooltip.
+         * Will always be enclosed in &lt;html&gt; &lt;/html&gt; tags.
+         */
+        public String getTooltipText() {
+                if (this.displayedPrintname != null) {
+                        return this.displayedPrintname;
+                } else {
+	                String result;
+	                result = extractTooltipText(this.printname);
+	                if (this.paramNames.size() > 0) {
+	                        String params = htmlifyParams();
+	                        //will result in <html> wrapping
+	                        result = htmlAppend(result, params);
+	                } else {
+	                        //wrap in <html> by force
+	                        result = htmlAppend(result, "");
+	                }
+	                this.displayedPrintname = result;
+	                return result;
+                }
+        }
+
+        /**
+         * extracts the part of the body of the printname that is the tooltip
+         * @param myPrintname the body of the printname
+         * @return the tooltip
+         */
+        public static String extractTooltipText(String myPrintname) {
+                //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);
+                final int indSC = Utils.indexOfNotEscaped(myPrintname, SUBCAT);
+                int ind;
+                if ((indSC > -1) && (indSC < indTT)) {
+                        ind = -1;
+                } else {
+                        ind = indTT;
+                }
+                String result;
+                if (ind > -1) {
+                        result = myPrintname.substring(ind + TT_START.length());
+                } else {
+    	                result = myPrintname;
+                }
+                ind = Utils.indexOfNotEscaped(result, SUBCAT);
+                if (ind > -1) {
+	                result = result.substring(0, ind);
+                }
+                ind = Utils.indexOfNotEscaped(result, PARAM);
+                if (ind > -1) {
+	                result = result.substring(0, ind);
+                }
+                return result;                
+        }
+        
+        /**
+         * extracts the part of the body of the printname that is the 
+         * text entry for the JList
+         * @param myPrintname the body of the printname
+         * @return the one-line description of this Printname's fun
+         */
+        public static String extractDisplayText(String myPrintname) {
+                String result;
+                int ind = Utils.indexOfNotEscaped(myPrintname, TT_START);
+                if (ind > -1) {
+                        result = myPrintname.substring(0, ind);
+                } else {
+    	                result = myPrintname;
+                }
+                ind = Utils.indexOfNotEscaped(result, SUBCAT);
+                if (ind > -1) {
+	                result = result.substring(0, ind);
+                }
+                ind = Utils.indexOfNotEscaped(result, PARAM);
+                if (ind > -1) {
+	                result = result.substring(0, ind);
+                }
+                
+                return result;                
+        }
+        
+        /**
+         * Appends the given string insertion to original and 
+         * returns the result. If original is already HTML, the appended
+         * text will get right before the &lt;/html&gt; tag.
+         * If original is no HTML, it will be enclosed in &lt;html&gt;
+         * @param original The String that is to come before insertion
+         * @param insertion the String to be appended
+         * @return the aforementioned result.
+         */
+        public static String htmlAppend(String original, String insertion) {
+                StringBuffer result;
+                if (original != null) {
+                        result = new StringBuffer(original);
+                } else {
+                        result = new StringBuffer();
+                }
+                int htmlindex = result.indexOf("</html>");
+                
+                if (htmlindex > -1) {
+                        result.insert(htmlindex, insertion);
+                } else {
+                        result.insert(0,"<html>").append(insertion).append("</html>");
+                }
+                return result.toString();
+                
+        }
+
+        /**
+         * Prepends the given string insertion to original and 
+         * returns the result. If original is already HTML, the appended
+         * text will get right after the &lt;html&gt; tag.
+         * If original is no HTML, it will be enclosed in &lt;html&gt;
+         * @param original The String that is to come after insertion
+         * @param insertion the String to be appended
+         * @return the aforementioned result.
+         */
+        public static String htmlPrepend(String original, String insertion) {
+                StringBuffer result = new StringBuffer(original);
+                int htmlindex = result.indexOf("<html>");
+                
+                if (htmlindex > -1) {
+                        result.insert(htmlindex, insertion);
+                } else {
+                        result.insert(0,insertion).insert(0,"<html>").append("</html>");
+                }
+                return result.toString();
+                
+        }
+
+        /**
+         * wraps a single parameter with explanatory text
+         * into &lt;dt&gt; and &lt;dd&gt; tags
+         * @param which the number of the parameter
+         * @return the resulting String, "" if the wanted parameter
+         * is not stored (illegal index)
+         */
+        protected String htmlifyParam(int which) {
+                try {
+                        String result = "<dt>" + this.paramNames.get(which) + "</dt>"
+                        + "<dd>" + this.paramTexts.get(which) + "</dd>";
+                        return result;
+                } catch (ArrayIndexOutOfBoundsException e) {
+                        subcatLogger.fine(e.getLocalizedMessage());
+                        return "";
+                }
+                
+        }
+        
+        /**
+         * wraps a single parameter together with its explanatory text into
+         * a HTML definition list (&lt;dl&gt; tags).
+         * Also the result is wrapped in &lt;html&gt; tags.
+         * @param which the number of the parameter
+         * @return the resulting definition list, null if the param is not found.
+         */
+        public String htmlifySingleParam(int which) {
+                String text = htmlifyParam(which);
+                if (text.equals("")) {
+                        return null;
+                }
+                String result = "<html><dl>" + text + "</dl></html>";
+                return result;
+        }
+        /**
+         * looks up the description for parameter number 'which' and returns it. 
+         * Returns null, if no parameter description is present.
+         * @param which The number of the parameter
+         * @return s.a.
+         */
+        public String getParamDescription(int which) {
+                 return (String)paramTexts.get(which);
+        }
+        
+        /**
+         * wraps all parameters together with their explanatory text into
+         * a HTML definition list (&lt;dl&gt; tags).
+         * No &lt;html&gt; tags are wrapped around here, that is sth. the caller
+         * has to do!
+         * @return the resulting definition list, "" if which is larger than
+         * the amount of stored params
+         */
+        public String htmlifyParams() {
+                if (this.paramNames.size() == 0) {
+                        return "";
+                }
+                StringBuffer result = new StringBuffer("<h4>Parameters:</h4><dl>");
+                for (int i = 0; i < this.paramNames.size(); i++) {
+                        result.append(htmlifyParam(i));
+                }
+                result.append("</dl>");
+                return result.toString();
+        }
+        
+        /**
+         * a testing method that is not called from KeY.
+         * Probably things like this should be automated via JUnit ...
+         * @param args not used
+         */
+        public static void main(String[] args) {
+                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, null);
+                System.out.println(pn);
+                for (int i = 0; i < pn.paramNames.size(); i++) {
+                        System.out.println(pn.htmlifySingleParam(i));
+                }
+                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, null);
+                System.out.println("*" + pn.getTooltipText());
+        }
+        
+        public String toString() {
+                return getDisplayText() + "  \n  " + getTooltipText() + " (" + this.paramNames.size() + ")";
+        }
+
+}

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

@@ -0,0 +1,112 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.io.IOException;
+import java.util.Hashtable;
+import java.util.logging.*;
+/**
+ * @author daniels
+ * asks GF to print all available printnames, parses that list and generates
+ * the suiting Printname objects.
+ */
+public class PrintnameLoader extends AbstractProber {
+        private final static Logger nogger = Logger.getLogger(Printname.class.getName());
+        /**
+         * The PrintnameManager on which the read Printnames
+         * will be registered with their fun name.
+         */
+        private final PrintnameManager printnameManager;
+        /**
+         * Here, the funs with their types get stored
+         */
+        private final Hashtable funTypes = new Hashtable();
+        /**
+         * if the Printnames should have their type appended to their display names
+         */
+        private final boolean loadTypes;
+        /**
+         * an initializing constructor, does nothing except setting fields
+         * @param gfCapsule the read/write encapsulation of GF
+         * @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(GfCapsule gfCapsule, PrintnameManager pm, boolean withTypes) {
+                super(gfCapsule);
+                this.printnameManager = pm;
+                this.loadTypes = withTypes;
+        }
+        
+        /** 
+         * 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 = gfCapsule.fromProc.readLine();
+                        if (nogger.isLoggable(Level.FINER)) {
+                                nogger.finer("1 " + 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("printname fun ")) {
+                                        //unescape backslashes. Probably there are more
+                                        result = Linearization.unescapeTextFromGF(result);
+                                        this.printnameManager.addNewPrintnameLine(result, this.funTypes);
+                                }
+                                
+                                result = gfCapsule.fromProc.readLine();
+                                if (nogger.isLoggable(Level.FINER)) {
+                                        nogger.finer("1 " + result);
+                                }
+                        }
+                        if (nogger.isLoggable(Level.FINER)) {
+                                nogger.finer("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.
+         * @param lang The module for which the grammars should be printed. 
+         * If lang is "" or null, the last read grammar module is used. 
+         */
+        protected void readPrintnames(String lang) {
+                //before, we want the types to be read.
+                if (this.loadTypes) {
+		                TypesLoader tl = new TypesLoader(gfCapsule, this.funTypes);
+		                tl.readTypes();
+                }
+                //prints the printnames of the last loaded grammar,
+                String sendString = "gf pg -printer=printnames";
+                if (lang != null && !("".equals(lang))) {
+                        sendString = sendString + " -lang=" + lang;
+                }
+                nogger.fine("collecting printnames :" + sendString);
+                send(sendString);
+                readGfedit();
+        }
+
+
+}

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

@@ -0,0 +1,174 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+import java.util.Hashtable;
+import java.util.logging.*;
+
+/**
+ * @author daniels
+ *
+ * An object of this class manages a bunch of printlines which is comprised of 
+ * storage and retrieval. Also giving the subcategory shortnames their long
+ * counterpart is done here.
+ */
+class PrintnameManager {
+        /**
+        * This constructor is a bit of a hack.
+        * It puts the \%SELF subcat into this.printnames.
+        * This subcat does not appear in the grammars and thus is
+        * introduced here. If it is defined there although, this
+        * definition is used. So it does not hurt.
+        */
+        public PrintnameManager() {
+                this.subcatNames.put(SELF_SUBCAT, "properties of self\\$shortcuts to the properties of self, that have a fitting type");
+        }
+        
+        /**
+         * The name of the subcat, that is used for the easy property access
+         * of self. 
+         */
+        static final String SELF_SUBCAT = "\\%SELF";
+        
+        private static Logger logger = Logger.getLogger(Printname.class.getName());
+        
+        protected final static String frontMatter = "printname fun ";
+        
+        /**
+         * The hashmap for the names of the sub categories, 
+         * with the shortname starting with '%' as the key.
+         * It is important that all Printnames of one session share the same
+         * instance of Hashtable here. 
+         * This field is not static because there can be several instances of
+         * the editor that shouldn't interfere.
+         */
+        protected final Hashtable subcatNames = new Hashtable();
+        
+        /** 
+         * contains all the Printnames with the fun names as keys 
+         */
+        protected final Hashtable printnames = new Hashtable();
+
+        /**
+         * processes a line from the "gf pg -printer=printnames" command
+         * @param line the read line from GF
+         * Should look like 
+         * 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, Hashtable funTypes) {
+                line = removePluses(line);
+                
+            	//remove "printname fun " (the frontMatter)
+            	final int index = line.indexOf(frontMatter);
+            	line = line.substring(index + frontMatter.length()).trim();
+
+            	//extract fun name
+            	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, type);
+        }
+        
+        /**
+         * The printname printer of pg spits out no String, but a wrapping of 
+         * small Strings conjoined with ++ which includes lots of parantheses.
+         * @param line The GF line from pg -printer=printnames
+         * @return a String representing the actual printname without the clutter
+         */
+        protected static String removePluses(String line) {
+                line = line.replaceAll("\"\\)*\\s*\\+\\+\\s*\\(*\""," ");
+            	int index = line.lastIndexOf('"');
+            	line = line.substring(0, index + 1);
+            	return line;
+        }
+        
+        
+        /**
+         * Constructs the actual printname and puts it into printnames
+         * @param myFun the GF abstract fun name
+         * @param myPrintname the printname given by GF
+         */
+        protected void addNewPrintname(String myFun, String myPrintname, String type) {
+                if (logger.isLoggable(Level.FINER)) {
+                        logger.finer("addNewPrintname, myFun = '" + myFun + "' , myPrintname = '" + myPrintname + "'");
+                }
+                Printname printname = new Printname(myFun, myPrintname, this.subcatNames, type);
+                if (logger.isLoggable(Level.FINER)) {
+                        logger.finer("printname = '" + printname + "'");
+                }
+                this.printnames.put(myFun, printname);
+        }
+        
+        /**
+         * looks for the Printname corresponding to the given fun.
+         * If the fun is qualified with a module and no Printname
+         * is found with module, another lookup without the module part
+         * is made.
+         * @param myFun the GF abstract fun name (with or without qualification)
+         * @return the corresponding Printname iff that one exists, null otherwise
+         */
+        public Printname getPrintname(String myFun) {
+                Printname result = null;
+                if (this.printnames.containsKey(myFun)) {
+                        result = (Printname)this.printnames.get(myFun);
+                } else {
+                        int index = myFun.indexOf('.');
+                        if (index > -1) {
+                                //a valid fun name must not be empty
+                                String fun = myFun.substring(index + 1);
+                                if (printnames.containsKey(fun)) {
+                                        result =  (Printname)this.printnames.get(fun);
+                                }
+                        }
+                }
+                if (result == null) {
+                        //?n indicates that myFun is a metavariable of GF, 
+                        // which does not occur in the refinement menu.
+                        // if that is not wanted, don't call this method!
+                        if (!myFun.startsWith("?")) {
+                                logger.fine("no printname for '" + myFun + "', pretend that it is a bound variable");
+                                return new Printname(myFun);
+                        }
+                }
+                return result;
+        }
+        
+        /**
+         * looks up the full name for the subcategory name shortname.
+         * This is the %SOMETHING from the printname.
+         * @param shortname The subcat name which should get expanded
+         * @return the corresponding full name, maybe null!
+         */
+        public String getFullname(String shortname) {
+                String result = (String)this.subcatNames.get(shortname);
+                return result;
+        }
+
+        public static void main(String[] args) {
+                String a = "printname fun stringLiteral = \"arbitrary\" ++ (\"String$click\" ++ (\"read\" ++ (\"and\" ++ (\"enter\" ++ (\"the\" ++ (\"String\" ++ (\"in\" ++ (\"the\" ++ (\"dialog\" ++ (\"TODO%STRING(String\" ++ \"operations)\"))))))))))";
+                System.out.println(a);
+                System.out.println(removePluses(a));
+                a = "printname fun count = \"count\" ++ (\"the\" ++ (\"occurances\" ++ (\"of\" ++ (\"an\" ++ (\"object\" ++ (\"in\" ++ (\"the\" ++ \"collection.\")))))))++ (\"%COLL\" ++ (\"#collElemType\" ++ (\"The\" ++ (\"official\" ++ (\"element\" ++ (\"type\" ++ (\"of\" ++ (\"<i>coll</i>.<br>That\" ++ (\"is,\" ++ (\"the\" ++ (\"parameter\" ++ (\"type\" ++ (\"of\" ++ \"<i>coll</i>\")))))))))))++ (\"#set\" ++ (\"The\" ++ (\"Set\" ++ (\"in\" ++ (\"which\" ++ (\"occurances\" ++ (\"of\" ++ (\"<i>elem</i>\" ++ (\"are\" ++ (\"to\" ++ (\"be\" ++ \"counted.\")))))))))) ++ (\"#elem\" ++ (\"The\" ++ (\"instance\" ++ (\"of\" ++ (\"which\" ++ (\"the\" ++ (\"occurances\" ++ (\"in\" ++ (\"<i>coll</i>\" ++ (\"are\" ++ \"counted.\")))))))))))))";
+                System.out.println(a);
+                System.out.println(removePluses(a));
+        }
+        
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/ReadDialog.java

@@ -0,0 +1,200 @@
+//Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.awt.BorderLayout;
+import java.awt.Dimension;
+import java.awt.Font;
+import java.awt.GridLayout;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
+import java.io.File;
+
+import javax.swing.ButtonGroup;
+import javax.swing.JButton;
+import javax.swing.JDialog;
+import javax.swing.JFileChooser;
+import javax.swing.JLabel;
+import javax.swing.JPanel;
+import javax.swing.JRadioButton;
+import javax.swing.JTextField;
+
+import java.util.logging.*;
+
+/**
+ * Takes care of reading in Strings that are to be parsed and terms.
+ * @author daniels
+ *
+ */
+class ReadDialog implements ActionListener{
+        /** XML parsing debug messages  */
+        private static Logger xmlLogger = Logger.getLogger(GFEditor2.class.getName() + "_XML");
+        /** The window to which this class belongs */
+        private final GFEditor2 owner;
+        /** is the main thing of this class */
+        private final JDialog readDialog;
+        /** main area of the Read dialog (content pane)*/
+        private final JPanel inputPanel = new JPanel();
+        /** OK, Cancel, Browse in the Read dialog */
+        private final JPanel inputPanel2 = new JPanel();
+        /** in the Read dialog the OK button */
+        private final JButton ok = new JButton("OK");
+        /** in the Read dialog the Cancel button */
+        private final JButton cancel = new JButton("Cancel");
+        /** in the Read dialog the Browse button */
+        private final JButton browse = new JButton("Browse...");
+        /** groups inputField and inputLabel */
+        private final JPanel inputPanel3 = new JPanel();   
+        /** for 'Read' to get the input */
+        private final JTextField inputField = new JTextField();
+        /** "Read: " */
+        private final JLabel inputLabel = new JLabel("Read: ");
+        /** the radio group in the Read dialog to select Term or String */
+        private final ButtonGroup readGroup = new ButtonGroup();
+        /** to select to input a Term in the Read dialog */
+        private final JRadioButton termReadButton = new JRadioButton("Term");
+        /** to select to input a String in the Read dialog */
+        private final JRadioButton stringReadButton = new JRadioButton("String");
+        /** used for new Topic, Import and Browse (readDialog) */
+        private final JFileChooser fc = new  JFileChooser("./");
+        /**
+         * if a user sends a custom command to GF, he might want to do this 
+         * again with the same command.
+         * Therefore it is saved.
+         */
+        private String parseInput = "";
+        /**
+         * if the user enters a term, he perhaps wants to input the same text again.
+         * Therefore it is saved.
+         */        
+        private String termInput = "";
+        
+        /**
+         * creates a modal dialog
+         * @param owner The parent for which this dialog shall be modal.
+         */
+        protected ReadDialog(GFEditor2 owner) {
+                this.owner = owner;
+                readDialog= new JDialog(owner, "Input", true);
+                readDialog.setLocationRelativeTo(owner);
+                readDialog.getContentPane().add(inputPanel);
+                readDialog.setSize(480,135);
+
+                termReadButton.setActionCommand("term");
+                stringReadButton.setSelected(true);  
+                stringReadButton.setActionCommand("lin");
+                // Group the radio buttons.
+                readGroup.add(stringReadButton);
+                readGroup.add(termReadButton);
+                JPanel readButtonPanel = new JPanel();
+                readButtonPanel.setLayout(new GridLayout(3,1));
+                readButtonPanel.setPreferredSize(new Dimension(70, 70));
+                readButtonPanel.add(new JLabel("Format:"));
+                readButtonPanel.add(stringReadButton);
+                readButtonPanel.add(termReadButton);
+                inputPanel.setLayout(new BorderLayout(10,10));
+                inputPanel3.setLayout(new GridLayout(2,1,5,5));
+                inputPanel3.add(inputLabel);
+                inputPanel3.add(inputField);
+                ok.addActionListener(this);
+                browse.addActionListener(this);
+                cancel.addActionListener(this);
+                inputField.setPreferredSize(new Dimension(300,23));
+                inputPanel.add(inputPanel3, BorderLayout.CENTER);
+                inputPanel.add(new JLabel(" "), BorderLayout.WEST);
+                inputPanel.add(readButtonPanel, BorderLayout.EAST);
+                inputPanel.add(inputPanel2, BorderLayout.SOUTH);
+                inputPanel2.add(ok);
+                inputPanel2.add(cancel);
+                inputPanel2.add(browse);
+        }
+        
+        /**
+         * Shows this modal dialog.
+         * The previous input text will be there again.
+         *
+         */
+        protected void show() {
+                if (stringReadButton.isSelected()) {
+                        inputField.setText(this.parseInput);
+                } else {
+                        inputField.setText(this.termInput);        
+                }
+                this.readDialog.setVisible(true);
+        }
+        
+        /**
+         * Sets the font of all GUI elements to font
+         * @param font
+         */
+        protected void setFont(Font font) {
+                ok.setFont(font);  
+                cancel.setFont(font);  
+                inputLabel.setFont(font);  
+                browse.setFont(font);  
+                termReadButton.setFont(font);  
+                stringReadButton.setFont(font);  
+        }
+        
+        /**
+         * the ActionListener method that does the user interaction
+         */
+        public void actionPerformed(ActionEvent ae) {  
+                Object obj = ae.getSource();
+
+                if ( obj == cancel ) {
+                        readDialog.setVisible(false);
+                }
+                
+                if ( obj == browse ) {
+                        if (fc.getChoosableFileFilters().length<2)
+                                fc.addChoosableFileFilter(new GrammarFilter()); 
+                        int returnVal = fc.showOpenDialog(owner);
+                        if (returnVal == JFileChooser.APPROVE_OPTION) {
+                                File file = fc.getSelectedFile();
+                                inputField.setText(file.getPath().replace('\\','/'));
+                        }
+                }
+                
+                if ( obj == ok ) {
+                        if (termReadButton.isSelected()) { 
+                                termInput = inputField.getText();
+                                if (termInput.indexOf(File.separatorChar)==-1){
+                                        owner.send("[t] g "+termInput); 
+                                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("sending term  string");
+                                } else {
+                                        owner.send("[t] tfile "+termInput);                           
+                                        if (xmlLogger.isLoggable(Level.FINER)) {
+                                                xmlLogger.finer("sending file term: "+termInput);
+                                        }
+                                }
+                        } else { //String selected
+                                parseInput = inputField.getText();
+                                if (parseInput.indexOf(File.separatorChar)==-1){
+                                        owner.send("[t] p "+parseInput);        
+                                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("sending parse string: "+parseInput);
+                                }   
+                                else {
+                                        owner.send("[t] pfile "+parseInput);           
+                                        if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("sending file parse string: "+parseInput);        
+                                }
+                        }
+                        readDialog.setVisible(false);
+                }
+
+        }
+
+}

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

@@ -0,0 +1,255 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.HashSet;
+import java.util.HashMap;
+import java.util.logging.*;
+
+/**
+ * @author daniels
+ * This class represents a command, that is sent to GF.
+ * TODO Refactor the chain command stuff out of this class and make it a subclass
+ */
+class RealCommand extends GFCommand {
+        
+        /**
+         * maps shorthands to fullnames
+         */
+        private final static HashMap fullnames = new HashMap();
+
+        private final static Logger logger = Logger.getLogger(Printname.class.getName());
+        
+        /**
+         * The number of undo steps that is needed to undo this fun call
+         */
+        public final int undoSteps;
+
+        /**
+         * The text that GF sent to describe the command
+         */
+        protected final String showText;
+        
+        protected final String subcat;
+        
+        /**
+         * Creates a Command that stands for a GF command, no link command
+         * sets all the attributes of this semi-immutable class.
+         * @param myCommand the actual GF command
+         * @param processedSubcats
+         * @param manager maps funs to previously read Printnames. 
+         * Thus needs to be the same object.
+         * @param myShowText The text GF prints in the show part of the XML
+         * which should be the command followed by the printname
+         * @param mlAbstract is true, iff the menu language is set to Abstract
+         * Then no preloaded printnames are used.
+         * @param toAppend will be appended to the command, that is sent to GF.
+         * Normally, toAppend will be the empty String "". 
+         * But it can be a chain command's second part. 
+         * It will not be shown to the user.
+         */
+        public RealCommand(final String myCommand, final HashSet processedSubcats, final PrintnameManager manager, final String myShowText, final boolean mlAbstract, final String toAppend) {
+                this(myCommand, processedSubcats, manager, myShowText, mlAbstract, toAppend, 1, null, null);
+        }
+        
+        /**
+         * Creates a Command that stands for a GF command, no link command
+         * sets all the attributes of this semi-immutable class.
+         * @param myCommand the actual GF command
+         * @param processedSubcats
+         * @param manager maps funs to previously read Printnames. 
+         * Thus needs to be the same object.
+         * @param myShowText The text GF prints in the show part of the XML
+         * which should be the command followed by the printname
+         * @param mlAbstract is true, iff the menu language is set to Abstract
+         * Then no preloaded printnames are used.
+         * @param toAppend will be appended to the command, that is sent to GF.
+    	 * Normally, toAppend will be the empty String "". 
+    	 * But it can be a chain command's second part. 
+    	 * It will not be shown to the user.
+         * @param undoSteps The number of undo steps that is needed to undo this fun call
+         * @param printnameFun If the fun, that selects the printname, should not be read from
+         * myCommand. For single commands, this is the only fun. For chain command, the last is
+         * taken. With this parameter, this behaviour can be overwritten
+         * @param subcat Normally, every fun has its own Printname, which has a fixed
+         * category. Sometimes, for the properies of self for example, 
+         * this should be overwritten. If null, the subcat from the printname is used.
+         */
+        public RealCommand(final String myCommand, final HashSet processedSubcats, final PrintnameManager manager, final String myShowText, final boolean mlAbstract, String toAppend, int undoSteps, String printnameFun, String subcat) {
+                if (fullnames.isEmpty()) {
+                        fullnames.put("w", "wrap");
+                        fullnames.put("r", "refine");
+                        fullnames.put("ch", "change head");
+                        fullnames.put("rc", "refine from history:");
+                        fullnames.put("ph", "peel head");
+                }
+                if (logger.isLoggable(Level.FINEST)) {
+                        logger.finest("new RealCommand: " + myCommand);                        
+                }
+                //if we have a ChainCommand, but undoSteps is just 1, count the undoSteps. 
+                if ((undoSteps == 1) && (myCommand.indexOf(";;") > -1)) {
+                        int occ = Utils.countOccurances(Utils.removeQuotations(myCommand), ";;") + 1;
+                        this.undoSteps = occ;
+                } else {
+                        this.undoSteps = undoSteps;
+                }
+                this.command = myCommand.trim();
+                this.showText = myShowText;
+                this.subcat = subcat;
+
+                //handle chain commands. 
+                //Only the last command counts for the printname selection
+                final String lastCommand;
+                if (this.undoSteps > 1) {
+                        //TODO: sth. like refine " f ;;d" ;; mp [2] will break here.
+                        final int chainIndex = this.command.lastIndexOf(";;");
+                        lastCommand = this.command.substring(chainIndex + 2).trim();
+                } else {
+                        lastCommand = this.command;
+                }
+                
+                //extract command type
+                int ind = lastCommand.indexOf(' ');
+                if (ind > -1) {
+                        this.commandType = lastCommand.substring(0, ind);
+                } else {
+                        this.commandType = lastCommand;
+                }
+                
+                //extract the argument position for wrapping commands and cut that part
+                if (this.commandType.equals("w") || this.commandType.equals("ph")) {
+                        int beforeNumber = lastCommand.lastIndexOf(' ');
+                        int protoarg;
+                        try {
+                                String argumentAsString = lastCommand.substring(beforeNumber + 1);
+                                protoarg = Integer.parseInt(argumentAsString);
+                        } catch (Exception e) {
+                                protoarg = -1;
+                        }
+                        this.argument = protoarg;
+                } else {
+                        this.argument = -1;
+                }
+                
+                //extract the fun of the GF command
+                if (this.commandType.equals("w")) {
+                        int beforePos = lastCommand.indexOf(' ');
+                        int afterPos = lastCommand.lastIndexOf(' ');
+                        if (beforePos > -1 && afterPos > beforePos) {
+                                this.funName = lastCommand.substring(beforePos + 1, afterPos);
+                        } else {
+                                this.funName = null;
+                        }
+                } else {
+                        int beforePos = lastCommand.indexOf(' ');
+                        if (beforePos > -1) {
+                                this.funName = lastCommand.substring(beforePos + 1);
+                        } else {
+                                this.funName = null;
+                        }
+                }
+                
+                //get corresponding Printname
+                if (this.commandType.equals("d")) {
+                        this.printname = Printname.delete;
+                } else if (this.commandType.equals("ac")) {
+                        this.printname = Printname.addclip;
+                } 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, false);
+                } else if  (this.commandType.equals("ph")) {
+                        this.printname = Printname.peelHead(this.argument);
+                } else if (mlAbstract) {
+                        //create a new Printname
+                        this.printname = new Printname(funName, myShowText, null, null);
+                } else { //standard case
+                        if (printnameFun == null) {
+                                this.printname = manager.getPrintname(funName);
+                        } else {
+                                //overwrite mode. Until now, only for properties of self.
+                                this.printname = manager.getPrintname(printnameFun);
+                        }
+                }
+                
+                if (this.getSubcat() != null) {
+                        if (processedSubcats.contains(this.getSubcat())) {
+                                newSubcat = false;
+                        } else {
+                                newSubcat = true;
+                                processedSubcats.add(this.getSubcat());
+                        }
+                } else {
+                        newSubcat = false;
+                }
+                
+                //now append toAppend before it is too late.
+                //Only now, since it must not interfere with the things above.
+                if (toAppend != null) {
+                        this.command += toAppend;
+                }
+        }
+
+        /** 
+         * the text that is to be displayed in the refinement lists 
+         */
+        public String getDisplayText() {
+                String 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);
+                        result = result + insertion;
+                }
+                if (this.printname.type != null) {
+                        result = result + " : " + this.printname.type;
+                }
+                return result;
+        }
+
+        /**
+         * the text that is to be displayed as the tooltip 
+         */
+        public String getTooltipText() {
+                String result;
+                result = this.printname.getTooltipText();
+                if (this.commandType.equals("w")) {
+                        String insertion = "<br>The selected sub-tree will be the " + (this.argument + 1) + ". argument of this refinement.";
+                        result = Printname.htmlAppend(result, insertion);
+                }
+                return result;
+        }
+
+        /**
+         * returns the subcat of this command
+         */
+        public String getSubcat() {
+                if (this.subcat == null) {
+                        return this.printname.getSubcat();
+                } else {
+                        //special case, only for properties of self so far
+                        return this.subcat;
+                }
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinedAstNodeData.java

@@ -0,0 +1,68 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+import java.util.logging.*;
+/**
+ * @author daniels
+ * An object of this class represents a line in the GF abstract syntax tree
+ * in the graphical form. Well, not really, but how this line appears there
+ * and what its tooltip is is stored here.
+ * RefinedAstNodeData has its tooltip from the function it represents, not
+ * from its parent node.
+ */
+class RefinedAstNodeData extends AstNodeData {
+
+        protected final Printname printname;
+
+        /**
+         * all we have to know about an already refined node is its Printname
+         * and the GF line representing it 
+         * @param pname the suiting Printname, may be null if the line could 
+         * not be parsed
+         * @param node the GfAstNode for the current line
+         * @param pos The position in the GF AST of this node in Haskell notation
+         * @param selected if this is the selected node in the GF AST
+         * @param constraint A constraint from a parent node, that also
+         * applies for this node.
+         */
+        public RefinedAstNodeData(Printname pname, GfAstNode node, String pos, boolean selected, String constraint) {
+                super(node, pos, selected, constraint);
+                this.printname = pname;
+                if (logger.isLoggable(Level.FINEST)) {
+                        logger.finest(this.toString() + " - " + position);
+                }
+        }
+        
+        /**
+         * @return the printname associated with this object
+         */
+        public Printname getPrintname() {
+                return this.printname;
+        }
+
+        /**
+         * @return displays the tooltip of the registered Printname,
+         * which may be null
+         */
+        public String getParamTooltip() {
+                if (getPrintname() != null) {
+                        return getPrintname().getTooltipText();
+                } else {
+                        return null;
+                }
+        }
+        
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinementMenu.java

@@ -0,0 +1,518 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this applicationpackage de.uka.ilkd.key.ocl.gf;
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.awt.Color;
+import java.awt.Font;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
+import java.awt.event.KeyEvent;
+import java.awt.event.KeyListener;
+import java.awt.event.MouseAdapter;
+import java.awt.event.MouseEvent;
+import java.awt.event.MouseListener;
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.Hashtable;
+import java.util.Iterator;
+import java.util.Vector;
+import java.util.logging.Level;
+import java.util.logging.Logger;
+
+import javax.swing.DefaultListModel;
+import javax.swing.JList;
+import javax.swing.JMenu;
+import javax.swing.JMenuItem;
+import javax.swing.JPopupMenu;
+import javax.swing.JScrollPane;
+import javax.swing.JSplitPane;
+import javax.swing.ListSelectionModel;
+
+/**
+ * Takes care of managing the commands, that GF sent,
+ * including subcategories and their menus.
+ * Manages the graphical lists. To display them, they are reachable
+ * via getRefinementListsContainer().
+ * @author hdaniels
+  */
+class RefinementMenu {
+        /** 
+         * logs things like selections and key events 
+         */
+        private static Logger logger = Logger.getLogger(RefinementMenu.class.getName());
+       
+        /**
+         * the editor of which this menu is part of
+         */
+        final private GFEditor2 editor;
+        /** 
+         * the content of the refinementMenu 
+         */
+        public DefaultListModel listModel= new DefaultListModel();
+        /** 
+         * The list of current refinement options 
+         */       
+        private JList refinementList = new JList(this.listModel);
+        /**
+         * to store the Vectors which contain the display names for the
+         * ListModel for refinementSubcatList for the different 
+         * subcategory menus.
+         * The key is the shortname String, the value the Vector with the
+         * display Strings
+         */
+        private Hashtable subcatListModelHashtable = new Hashtable(); 
+        /** 
+         * this ListModel gets refilled every time a %WHATEVER command, 
+         * which stands for a shortname for a subcategory of commands
+         * in the ListModel of refinementList, is selected there
+         */
+        private DefaultListModel refinementSubcatListModel = new DefaultListModel();
+        /** 
+         * The list of current refinement options in the subcategory menu
+         */       
+        private JList refinementSubcatList = new JList(this.refinementSubcatListModel);
+        /** 
+         * the scrollpane containing the refinement subcategory
+         */
+        private JScrollPane refinementSubcatPanel = new JScrollPane(this.refinementSubcatList);
+        /** 
+         * store what the shorthand name for the current subcat is 
+         */
+        private String whichSubcat;
+        /** 
+         * stores the two refinement JLists 
+         */
+        private JSplitPane refinementListsContainer;
+        /**
+         * the scrollpane containing the refinements 
+         */
+        private JScrollPane refinementPanel = new JScrollPane(this.refinementList);
+        /** 
+         * here the GFCommand objects are stored
+         */
+        private Vector gfcommands = new Vector();
+        /**
+         * The cached popup menu containing the same stuff as the refinement list
+         */
+        public JPopupMenu popup2 = new JPopupMenu();
+
+        /**
+         * Creates the panels for the refinement (subcat) menu
+         * @param editor the editor, that the refinement menu is part of
+         */
+        protected RefinementMenu(GFEditor2 editor) {
+                this.editor = editor;
+                refinementListsContainer = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT,refinementPanel, refinementSubcatPanel);
+                refinementList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
+                
+                final MouseListener mlRefinementList = new MouseAdapter() {
+                        public void mouseClicked(MouseEvent e) {
+                                refinementList.setSelectionBackground(refinementSubcatList.getSelectionBackground());
+                                boolean doubleClick = (e.getClickCount() == 2); 
+                                listAction(refinementList, refinementList.locationToIndex(e.getPoint()), doubleClick);
+                        }
+                };
+                refinementList.addMouseListener(mlRefinementList);
+                refinementList.addKeyListener(new KeyListener() {
+                        /** Handle the key pressed event for the refinement list. */
+                        public void keyPressed(KeyEvent e) {
+                                int keyCode = e.getKeyCode();   
+                                if (logger.isLoggable(Level.FINER)) {
+                                        logger.finer("Key pressed: " + e.toString());
+                                }
+
+                                int index = refinementList.getSelectedIndex();                        
+                                if (index == -1) {
+                                        //nothing selected, so nothing to be seen here, please move along
+                                } else if (keyCode == KeyEvent.VK_ENTER) { 
+                                        listAction(refinementList, refinementList.getSelectedIndex(), true);
+                                } else if (keyCode == KeyEvent.VK_DOWN && index < listModel.getSize() - 1) {
+                                        listAction(refinementList, index + 1, false);
+                                } else if (keyCode == KeyEvent.VK_UP && index > 0) {
+                                        listAction(refinementList, index - 1, false);
+                                } else if (keyCode == KeyEvent.VK_RIGHT) {
+                                        if (refinementSubcatList.getModel().getSize() > 0) {
+                                                refinementSubcatList.requestFocusInWindow();
+                                                refinementSubcatList.setSelectedIndex(0);
+                                                refinementList.setSelectionBackground(Color.GRAY);
+                                        }
+                                }
+                        }
+
+                        /** 
+                         * Handle the key typed event.
+                         * We are not really interested in typed characters, thus empty
+                         */
+                        public void keyTyped(KeyEvent e) {
+                                //needed for KeyListener, but not used                
+                        }
+
+                        /** Handle the key released event. */
+                        public void keyReleased(KeyEvent e) {
+                                //needed for KeyListener, but not used
+                        }
+                });
+
+                refinementSubcatList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
+                
+                final MouseListener mlRefinementSubcatList = new MouseAdapter() {
+                        public void mouseClicked(MouseEvent e) {
+                                boolean doubleClick = (e.getClickCount() == 2);
+                                listAction(refinementSubcatList, refinementSubcatList.locationToIndex(e.getPoint()), doubleClick);
+                                refinementList.setSelectionBackground(Color.GRAY);
+                        }
+                };
+                refinementSubcatList.addMouseListener(mlRefinementSubcatList);
+                refinementSubcatList.addKeyListener(new KeyListener() {
+                        /** Handle the key pressed event. */
+                        public void keyPressed(KeyEvent e) {
+                                int keyCode = e.getKeyCode();   
+                                if (logger.isLoggable(Level.FINER)) {
+                                        logger.finer("Key pressed: " + e.toString());
+                                }
+                                if (keyCode == KeyEvent.VK_ENTER) {
+                                        listAction(refinementSubcatList, refinementSubcatList.getSelectedIndex(), true);
+                                } else if (keyCode == KeyEvent.VK_LEFT) {
+                                        refinementList.requestFocusInWindow();
+                                        refinementSubcatList.clearSelection();
+                                        refinementList.setSelectionBackground(refinementSubcatList.getSelectionBackground());
+                                }
+                        }
+
+                        /** 
+                         * Handle the key typed event.
+                         * We are not really interested in typed characters, thus empty
+                         */
+                        public void keyTyped(KeyEvent e) {
+                                //needed for KeyListener, but not used                
+                        }
+
+                        /** Handle the key released event. */
+                        public void keyReleased(KeyEvent e) {
+                                //needed for KeyListener, but not used
+                        }
+                });
+                refinementList.setToolTipText("The list of current refinement options");
+                refinementList.setCellRenderer(new ToolTipCellRenderer());
+                refinementSubcatList.setToolTipText("The list of current refinement options");
+                refinementSubcatList.setCellRenderer(new ToolTipCellRenderer());
+
+        }
+        
+        /**
+         * @return Returns the refinementListsContainer,
+         * which will contain both JLists.
+         */
+        protected JSplitPane getRefinementListsContainer() {
+                return refinementListsContainer;
+        }
+
+        /**
+         * handling the event of choosing the action at index from the list.
+         * That is either giving commands to GF or displaying the subcat menus
+         * @param list The list that generated this action
+         * @param index the index of the selected element in list
+         * @param doubleClick true iff a command should be sent to GF, 
+         * false if only a new subcat menu should be opened. 
+         */
+        private void listAction(JList list, int index, boolean doubleClick) {
+                if (index == -1) {
+                        if (logger.isLoggable(Level.FINER)) logger.finer("no selection");
+                } else {
+                        Object o;
+                        if (list == refinementList) {
+                                o = listModel.elementAt(index); 
+                        } else {
+                                if (whichSubcat == null) {
+                                        //this is probably the case when no fitting properties of self
+                                        //are available and only a string is displayed in the submenu.
+                                        //clicking that string should do exactly nothing.
+                                        return;
+                                }
+                                Vector cmdvector = (Vector)this.subcatListModelHashtable.get(this.whichSubcat);
+                                o = (cmdvector.get(index));
+                        }
+                        GFCommand command = null;
+                        if (o instanceof GFCommand) {
+                                command = (GFCommand)o;
+                        } else {
+                                return;
+                        }
+                        if (command instanceof SelfPropertiesCommand) {
+                               SelfPropertiesCommand  spc = (SelfPropertiesCommand)command;
+                               Vector selfs = spc.produceSubmenu();
+                               if (selfs.size() == 0) {
+                                       listModel.remove(index);
+                                       refinementSubcatListModel.clear();
+                                       refinementSubcatListModel.addElement("No properties fit here");
+                                       return;
+                               } else {
+                                       this.subcatListModelHashtable.put(command.getSubcat(), selfs);
+                                       listModel.remove(index);
+                                       LinkCommand newLink = new LinkCommand(PrintnameManager.SELF_SUBCAT, editor.getPrintnameManager());
+                                       listModel.add(index, newLink);
+                                       command = newLink;
+                               }
+                        } 
+                        if (command instanceof LinkCommand) { //includes SelfPropertiesCommand, which is intended
+                                this.whichSubcat = command.getSubcat();
+                                refinementSubcatListModel.clear();
+                                Vector currentCommands = (Vector)this.subcatListModelHashtable.get(this.whichSubcat);
+                                for (Iterator it = currentCommands.iterator(); it.hasNext();) {
+                                        this.refinementSubcatListModel.addElement(it.next());
+                                }
+                        } else if (doubleClick && command instanceof InputCommand) {
+                                InputCommand ic = (InputCommand)command;
+                                editor.executeInputCommand(ic);
+                                
+                        } else if (doubleClick){
+                                refinementSubcatListModel.clear();
+                                if (command instanceof RealCommand) {
+                                        editor.send("[t] " + command.getCommand(), true, ((RealCommand)command).undoSteps);
+                                } else {
+                                        //that shouldn't be the case ...
+                                        editor.send("[t] " + command.getCommand());
+                                }
+                        } else if (list == refinementList){
+                                refinementSubcatListModel.clear();
+                        }
+                }
+        }
+        /**
+         * Produces the popup menu that represents the current refinements.
+         * An alternative to the refinement list.
+         * @return s.a.
+         */
+        protected JPopupMenu producePopup() {
+                if (popup2.getComponentCount() > 0) {
+                        return popup2;
+                }
+                for (int i = 0; i < this.listModel.size(); i++) {
+                        GFCommand gfcmd = (GFCommand)this.listModel.get(i);
+                        if (gfcmd instanceof LinkCommand) {
+                                LinkCommand lc = (LinkCommand)gfcmd;
+                                Vector subcatMenu = (Vector)this.subcatListModelHashtable.get(lc.getSubcat());
+                                JMenu tempMenu = new JMenu(lc.getDisplayText());
+                                tempMenu.setToolTipText(lc.getTooltipText());
+                                tempMenu.setFont(popup2.getFont());
+                                JMenuItem tempMenuItem;
+                                for (Iterator it = subcatMenu.iterator(); it.hasNext();) {
+                                        GFCommand subgfcmd = (GFCommand)it.next();
+                                        tempMenuItem = menuForCommand(subgfcmd);
+                                        if (tempMenuItem != null) {
+                                                tempMenu.add(tempMenuItem);
+                                        }
+                                }
+                                popup2.add(tempMenu);
+                        } else { 
+                                JMenuItem tempMenu = menuForCommand(gfcmd);
+                                if (tempMenu != null) {
+                                        popup2.add(tempMenu);
+                                }
+                        }
+                }
+                return popup2;
+        }
+        
+        /**
+         * takes a GFCommand and "transforms" it in a JMenuItem.
+         * These JMenuItems have their own listeners that take care of
+         * doing what is right ...
+         * @param gfcmd a RealCommand or an InputCommand
+         * (LinkCommand is ignored and produces null as the result)
+         * @return either the correspondend JMenuItem or null.
+         */
+        private JMenuItem menuForCommand(GFCommand gfcmd) {
+                JMenuItem tempMenu = null;
+                if (gfcmd instanceof RealCommand){
+                        tempMenu = new JMenuItem(gfcmd.getDisplayText());
+                        tempMenu.setFont(popup2.getFont());
+                        tempMenu.setActionCommand(gfcmd.getCommand());
+                        tempMenu.setToolTipText(gfcmd.getTooltipText());
+                        tempMenu.addActionListener(new ActionListener() {
+                                public void actionPerformed(ActionEvent ae) {
+                                        JMenuItem mi = (JMenuItem)ae.getSource();
+                                        refinementSubcatListModel.clear();
+                                        String command = "[t] " + mi.getActionCommand();
+                                        editor.send(command);
+                                }
+                        });
+                } else if (gfcmd instanceof InputCommand) {
+                        tempMenu = new JMenuItem(gfcmd.getDisplayText());
+                        tempMenu.setFont(popup2.getFont());
+                        tempMenu.setActionCommand(gfcmd.getCommand());
+                        tempMenu.setToolTipText(gfcmd.getTooltipText());
+                        tempMenu.addActionListener(new ActionListener() {
+                                public void actionPerformed(ActionEvent ae) {
+                                        JMenuItem mi = (JMenuItem)ae.getSource();
+                                        String command = mi.getActionCommand();
+                                        InputCommand ic = InputCommand.forTypeName(command);
+                                        if (ic != null) {
+                                                editor.executeInputCommand(ic);
+                                        }
+                                }
+                        });
+                        
+                }
+                return tempMenu;
+        }
+        /**
+         * Takes the StringTuples in gfCommandVector, creates the RealCommand
+         * objects for them.
+         * Goes through this list and groups the RealCommands
+         * according to their subcategory tag (which starts with %)
+         * If there is a "(" afterwards, everything until the before last
+         * character in the printname will be used as the display name
+         * for this subcategory. If this displayname is defined a second time,
+         * it will get overwritten.
+         * Sorting is also done here.
+         * Adding additional special commands like InputCommand happens here too.
+         * @param gfCommandVector contains all RealCommands, that are available
+         * at the moment
+         * @param toAppend will be appended to every command, that is sent to GF.
+         * Normally, toAppend will be the empty String "". 
+         * But it can be a chain command's second part. 
+         * @param isAbstract If the selected menu language is abstract or not
+         * @param easyAttributes if true, attributes of self will be added.
+         * @param focusPosition The current position of the focus in the AST. 
+         * Needed for easy access to properties of self. 
+         * @param gfCapsule The read/write encapsulation of the GF process.
+         * Needed for easy access to properties of self.
+         */
+        protected void formRefinementMenu(final Vector gfCommandVector, final String toAppend, GfAstNode currentNode, final boolean isAbstract, boolean easyAttributes, LinPosition focusPosition, GfCapsule gfCapsule) {
+                this.listModel.clear();
+                this.refinementSubcatListModel.clear();
+                this.gfcommands.clear();
+                this.subcatListModelHashtable.clear();
+                this.whichSubcat = null;
+                this.popup2.removeAll();
+                Vector prelListModel = new Vector();
+                /** to keep track of subcats and their names */
+                HashSet processedSubcats = new HashSet();
+                //at the moment, we don't know yet, which subcats are
+                //nearly empty
+                for (Iterator it = gfCommandVector.iterator(); it.hasNext();) {
+                        final StringTuple st = (StringTuple)it.next();
+                        GFCommand gfcommand;
+                        if (st instanceof ChainCommandTuple) {
+                                ChainCommandTuple cct = (ChainCommandTuple)st;
+                                gfcommand = new RealCommand(st.first, processedSubcats, editor.getPrintnameManager(), st.second, isAbstract, toAppend, cct.undoSteps, cct.fun, cct.subcat);
+                        } else {
+                                gfcommand = new RealCommand(st.first, processedSubcats, editor.getPrintnameManager(), st.second, isAbstract, toAppend);
+                        }   
+                        if ((!editor.isGroupSubcat()) || (gfcommand.getSubcat() == null)) {
+                                prelListModel.addElement(gfcommand);
+                        } else {
+                                //put stuff in the correct Vector for the refinementSubcatListModel
+                                Vector lm;
+                                if (subcatListModelHashtable.containsKey(gfcommand.getSubcat())) {
+                                        lm = (Vector)this.subcatListModelHashtable.get(gfcommand.getSubcat());
+                                } else {
+                                        lm = new Vector();
+                                        this.subcatListModelHashtable.put(gfcommand.getSubcat(), lm);
+                                }
+                                lm.addElement(gfcommand);
+                                if (gfcommand.isNewSubcat()) {
+                                        GFCommand linkCmd = new LinkCommand(gfcommand.getSubcat(), editor.getPrintnameManager());
+                                        prelListModel.addElement(linkCmd);
+                                }
+                        }
+                }
+                
+                //so we remove empty subcats now and replace them by their RealCommand
+                for (int i = 0; i < prelListModel.size(); i++) {
+                        if (prelListModel.get(i) instanceof LinkCommand) {
+                                LinkCommand lc = (LinkCommand) prelListModel.get(i);
+                                Vector subcatMenu = (Vector)this.subcatListModelHashtable.get(lc.getSubcat());
+                                if (subcatMenu.size() == 1) {
+                                        RealCommand rc = (RealCommand)subcatMenu.get(0);
+                                        prelListModel.set(i, rc);
+                                }
+                        }
+                }
+                
+                
+                // Some types invite special treatment, like Int and String 
+                // which can be read from the user.
+                if (currentNode.isMeta()) {
+                        InputCommand usedInputCommand = null;
+                        if (currentNode.getType().equals("Int")) {
+                                usedInputCommand = InputCommand.intInputCommand;
+                                prelListModel.addElement(usedInputCommand);
+                        } if (currentNode.getType().equals("String")) {
+                                usedInputCommand = InputCommand.stringInputCommand;
+                                prelListModel.addElement(usedInputCommand);
+                        }
+                        if (usedInputCommand != null) {
+                                for (Iterator it = usedInputCommand.enteredValues.iterator(); it.hasNext();) {
+                                        Object o = it.next();
+                                        //for GF it seems to make no difference, 
+                                        //if we use 'g' or 'r' as the command to send 
+                                        //Int and String. 'r' is already supported
+                                        //by RealCommand, so I chose that.
+                                        RealCommand rc = new RealCommand("r " + o, processedSubcats, editor.getPrintnameManager(), "r " + o, isAbstract, toAppend);
+                                        prelListModel.addElement(rc);
+                                }
+                        }
+                }
+                
+                //add the special entry for the properties of self
+                if (easyAttributes) {
+                        final SelfPropertiesCommand spc = new SelfPropertiesCommand(editor.getPrintnameManager(), gfCapsule, focusPosition, isAbstract, toAppend, processedSubcats);
+                        prelListModel.add(spc);
+                }
+                
+                //now sort the preliminary listmodels
+                if (editor.isSortRefinements()) {
+                        Collections.sort(prelListModel);
+                        for (Iterator it = subcatListModelHashtable.values().iterator(); it.hasNext();) {
+                                Vector slm = (Vector)it.next();
+                                Collections.sort(slm);
+                        }
+                }
+                //now fill this.listModel
+                for (Iterator it = prelListModel.iterator(); it.hasNext();) {
+                        Object next = it.next();
+                        this.listModel.addElement(next);
+                }
+                //select the first command in the refinement menu, if available
+                if (this.listModel.size() > 0) {
+                        this.refinementList.setSelectedIndex(0);
+                } else {
+                        this.refinementList.setSelectedIndex(-1);
+                }
+                this.refinementList.setSelectionBackground(refinementSubcatList.getSelectionBackground());
+        }
+
+        /**
+         * Requests the focus for the refinement list
+         */
+        protected void requestFocus() {
+                refinementList.requestFocusInWindow();
+        }
+        
+        /**
+         * clears the list model
+         */
+        protected void reset() {
+                listModel.clear();
+        }
+        
+        /**
+         * Applies newFont to the visible elements
+         * @param newFont The new font, what else?
+         */
+        protected void setFont(Font newFont) {
+                refinementList.setFont(newFont);
+                refinementSubcatList.setFont(newFont);
+                popup2.setFont(newFont);  
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinementMenuCollector.java

@@ -0,0 +1,51 @@
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.Vector;
+
+/**
+ * Asks GF the Vector of RefinementMenu entries.
+ * 
+ * This class can be reused.
+ * @author daniels
+ */
+class RefinementMenuCollector extends AbstractProber {
+        /**
+         * here the result of this run is saved
+         */
+        Vector refinementMenuContent = null;
+        /**
+         * Standard fill-in-the-parameters constructor
+         * @param gfCapsule The reader/writer to GF
+         */
+        public RefinementMenuCollector(GfCapsule gfCapsule) {
+                super(gfCapsule);
+        }
+        
+        /**
+         * Asks GF (the same GF as the one editor has) to execute a command
+         * and returns the read refinement menu that is offered then.
+         * Uses the readRefinementMenu method from GFEditor2 which does not
+         * change any global variable besides GF itself. So that is safe.
+         * 
+         * Note: This method does not do undo automatically, since it is 
+         * intended to run several times in a row, so the u should be part of
+         * next command.
+         * @param command The command that is sent to GF. Should contain a mp
+         * to make sure that the command at the right position in the AST
+         * is read
+         * @return a Vector of StringTuple like readRefinementMenu does it.
+         */
+        public Vector readRefinementMenu(String command) {
+                send(command);
+                readGfedit();
+                return this.refinementMenuContent;
+        }
+        
+        /**
+         * parses the refinement menu part and stores it in this.refinementMenuContent
+         */
+        protected void readMenu() {
+                this.refinementMenuContent = gfCapsule.readRefinementMenu();
+        }
+        
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinementMenuTransformer.java

@@ -0,0 +1,223 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.Vector;
+import java.util.logging.Level;
+import java.util.logging.Logger;
+
+/**
+ * This class is completely static and cannot be instantiated. 
+ * @see #transformRefinementMenu(de.uka.ilkd.key.ocl.gf.TreeAnalysisResult, java.util.Vector, de.uka.ilkd.key.ocl.gf.GfCapsule)
+ * @author hdaniels
+ */
+class RefinementMenuTransformer {
+        /**
+         * if things are added to or removed from the refinement menu 
+         */
+        protected static Logger logger = Logger.getLogger(RefinementMenuTransformer.class.getName()); 
+        
+        private RefinementMenuTransformer() {
+                //A private constructor enforces the noninstantiability 
+                //of "RefinementMenuTransformer". 
+                //(See item 3 of "Effective Java".)
+        }
+        
+        /**
+         * Depending on tar, the refinement menu given in raw form in oldMenu
+         * is transformed.
+         * That includes:
+         *  - adding properties of self
+         *  - producing a reduced version for subtyping below a coerce 
+         *    where only Instances of subtypes are listed
+         *  - probes, if self and result are really applicable
+         *  - changes the delete command, when an unrefined Instance
+         *    argument of coerce is clicked on, to first delete the
+         *    whole coerce to avoid sticking with wrong type arguments.
+         * @param tar TreeAnalyser has decided what to do here. That is followed.
+         * @param oldMenu The original content of the refinement menu.
+         * Is a Vector of StringTuple
+         * @param gfCapsule The encapsulation of GF regarding read/write access
+         * @return The refinement menu in its new form
+         */
+        protected static Vector transformRefinementMenu(TreeAnalysisResult tar, Vector oldMenu, GfCapsule gfCapsule) {
+                //now do fill (or partially empty) the offered commands list
+                final Vector usedCommandVector;
+                if (tar.reduceCoerce) {
+                        //is only true if switched on globally.
+                        //And if conditions are right.
+                        usedCommandVector = produceReducedCoerceRefinementMenu(tar.focusPosition.position, gfCapsule);
+                } else {
+                        usedCommandVector = oldMenu;
+                }
+                if (tar.deleteAlsoAbove) {
+                        String newPos = tar.focusPosition.parentPosition();
+                        StringTuple newDelete = new StringTuple("mp " + newPos + " ;; d", "delete current subtree\\$also delete the encompassing coercion ");
+                        exchangeCommand(usedCommandVector, "d", newDelete);
+                }
+                if (tar.probeSelfResult) {
+                        probeCompletability(usedCommandVector, tar.focusPosition, gfCapsule);
+                }
+                if (tar.easyAttributes && !tar.reduceCoerce) {
+                        addSelfProperties(usedCommandVector, tar.focusPosition, gfCapsule);
+                }                
+                return usedCommandVector;
+        }
+        
+        /**
+         * Looks at the subtyping witness of the same coerce as currentPos
+         * and collects the possible refinements for all offered subtypes.
+         * It assumes that argument 0 of coerce is automatically filled in.
+         * 
+         * This method is surely <b>slow</b> since a lot of calls to GF is made
+         * here.
+         * @param currentPos musst point to a child of a coerce.
+         * @param gfCapsule The encapsulation of GF regarding read/write access
+         * @return a Vector of StringTuple as readRefinementMenu does.
+         * This Vector can be fed into formRefinementMenu.
+         */
+        private static Vector produceReducedCoerceRefinementMenu(String currentPos, GfCapsule gfCapsule) {
+                final HashSet commands = new HashSet();
+                RefinementMenuCollector rmc = new RefinementMenuCollector(gfCapsule);
+                //move to the subtype witness argument
+                final String collectSubtypesCommand = "mp " + LinPosition.calculateBrethrenPosition(currentPos, 2); 
+                Vector possibleSubtypes = rmc.readRefinementMenu(collectSubtypesCommand);
+                String undoString = "";
+                final String undoTemplate = "u 2 ;; ";
+                for (Iterator it = possibleSubtypes.iterator(); it.hasNext(); ) {
+                        StringTuple nextCommand = (StringTuple)it.next();
+//                        if (!nextCommand.first.trim().startsWith("r")) {
+//                                //no ac, d, rc or whatever wanted here. Only refine.
+//                                continue;
+//                        }
+                        final String collectRefinementsCommand = undoString  + nextCommand.first + " ;; mp " + currentPos;
+                        undoString = undoTemplate; //for all following runs we want an undo before it
+                        Vector nextRefinements = rmc.readRefinementMenu(collectRefinementsCommand);
+                        commands.addAll(nextRefinements);
+                }
+                final String cleanupCommand = "u 3"; //undo the last command and also the first mp
+                rmc.readRefinementMenu(cleanupCommand); //no harm done here, collector won't get reused
+                Vector result = new Vector(commands);
+                return result;
+        }
+        
+        /**
+         * checks if result and self make sense in the current context.
+         * if not, they are removed from oldMenu
+         * @param oldMenu A Vector of StringTuple that represents the 
+         * commands for the refinement menu
+         * @param focusPos The current position in the AST
+         * @param gfCapsule The encapsulation of GF regarding read/write access
+         */
+        private static void probeCompletability(Vector oldMenu, LinPosition focusPos, GfCapsule gfCapsule) {
+                /**
+                 * self and result both take two arguments.
+                 * The first is the type, which is fixed
+                 * if the second argument is refineable.
+                 * Important is the second. 
+                 * This only is refineable for the real type of self/result 
+                 */
+                if (focusPos == null) {
+                        //sadly, we can't do much
+                        return;
+                }
+                final String childPos = focusPos.childPosition(1);
+                final SelfResultProber cp = new SelfResultProber(gfCapsule);
+                for (int i = 0; i < oldMenu.size(); i++) {
+                        String cmd = ((StringTuple)oldMenu.elementAt(i)).first;
+                        if ((cmd != null) && ((cmd.indexOf("r core.self") > -1) || (cmd.indexOf("r core.result") > -1))) {
+                                //the first mp is necessary for the second of self/result.
+                                //without, GF will jump to a stupid position
+                                String newCommand = "mp " + focusPos.position + " ;; " + cmd + " ;; mp " + childPos;
+                                if (!cp.isAutoCompletable(newCommand, 3)) {
+                                        oldMenu.remove(i);
+                                        i -=1;
+                                }
+                        }
+                }
+        }
+
+        /**
+         * Probes for the properties of self, that could be filled in at
+         * the current focus position.
+         * If it finds any, these are added to oldMenu
+         * This method will add all offered commands to the refinement menu,
+         * not only for suiting subtypes due to speed reasons.
+         * @param oldMenu A Vector of StringTuple. The menu with the commands
+         * and show texts as given by GF. Gets modified.
+         * @param focusPos The position of the GF focus in the AST
+         * @param gfCapsule The encapsulation of GF regarding read/write access
+         */
+        private static void addSelfProperties(Vector oldMenu, LinPosition focusPos, GfCapsule gfCapsule) {
+                //solve in between to avoid some typing errors by closing some type arguments
+                final String probeCommand = "r core.implPropCall ;; mp " + focusPos.childPosition(2) + " ;; r core.self ;; solve ;; mp " + focusPos.childPosition(3);
+                final String deleteAppendix = " ;; d";
+                final RefinementMenuCollector rmc = new RefinementMenuCollector(gfCapsule);
+                Vector futureRefinements = rmc.readRefinementMenu(probeCommand + deleteAppendix);
+                final int undos = 5;
+                final boolean singleRefinement;
+                if (futureRefinements.size() == 1) {
+                        singleRefinement = true;
+                } else {
+                        singleRefinement = false;
+                }
+                final String cleanupCommand = "u " + undos;
+                rmc.readRefinementMenu(cleanupCommand); //no harm done here
+                for (Iterator it = futureRefinements.iterator(); it.hasNext();) {
+                        StringTuple st = (StringTuple)it.next();
+                        if (st.first.startsWith("r")) { //is a refinement, no ac or d
+                                String newCommand;
+                                //add the command that came before
+                                final int cmdUndos;
+                                if (singleRefinement) {
+                                        //that is an exceptional case, but might happen.
+                                        //Here we don't have to refine the final property
+                                        //at all, since GF does that automatically
+                                        newCommand = probeCommand + " ;; c solve";
+                                        cmdUndos = 5;
+                                } else {
+                                        //here the 'd' is not needed, since we know,
+                                        //that nothing is refined automatically
+                                        newCommand = probeCommand + " ;; " + st.first + " ;; c solve";
+                                        cmdUndos = 6;
+                                }
+                                // now extract the fun of the property
+                                String fun = st.first.substring(1).trim();
+                                ChainCommandTuple cct = new ChainCommandTuple(newCommand, st.second, fun, PrintnameManager.SELF_SUBCAT, cmdUndos);
+                                if (logger.isLoggable(Level.FINER)) {
+                                        logger.finer("added " + cct);
+                                }
+                                oldMenu.add(cct);
+                        }
+                }
+        }        
+        
+        /**
+         * Goes through oldMenu and if it finds a command in there, where
+         * first.equals(oldCommand), this command is replaced by newCommand.
+         * oldMenu's content thus gets modified.
+         * @param oldMenu a Vector of StringTuple
+         * @param oldCommand a GF command string (what is sent, not the show text)
+         * @param newCommand a StringTuple representing what could be a pait from GF
+         */
+        private static void exchangeCommand(Vector oldMenu, String oldCommand, StringTuple newCommand) {
+                for (int i = 0; i < oldMenu.size(); i++) {
+                        StringTuple next = (StringTuple)oldMenu.get(i);
+                        if (next.first.equals(oldCommand)) {
+                                oldMenu.remove(i);
+                                oldMenu.insertElementAt(newCommand, i);
+                        }
+                }
+        }
+        
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/SelfPropertiesCommand.java

@@ -0,0 +1,175 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this applicationpackage de.uka.ilkd.key.ocl.gf;
+
+package de.uka.ilkd.key.ocl.gf;
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.Vector;
+import java.util.logging.Level;
+import java.util.logging.Logger;
+
+/**
+ * This class is an unclean hack.
+ * The whole refinement menu architecture expected, that everything is probed,
+ * when the refinement menu is getting created.
+ * But for getting only subtype correct properties of self needs a number of
+ * calls to GF, which could be deferred to not make things slower than they
+ * already are.
+ * This deferred probing is done in this class.
+ * @author daniels
+ *
+ */
+class SelfPropertiesCommand extends LinkCommand {
+        private final static Logger logger = Logger.getLogger(SelfPropertiesCommand.class.getName());
+        private final GfCapsule gfCapsule;
+        private final LinPosition focusPos;
+        private final String toAppend;
+        private final boolean isAbstract;
+        private final HashSet processedSubcats;
+        private final PrintnameManager printnameManager;
+
+        /**
+         * A simple setter constructor, no calculation done here.
+         * @param manager The printname manager, that knows, how the properties
+         * of self should be listed in the refinement menu
+         * @param gfCapsule The reader/writer abstraction from GF
+         * @param focusPos The position of the GF focus
+         * @param isAbstract if Abstract is the current menu language
+         * @param toAppend If something should be appended to the command
+         * @param processedSubcats Here, the subcat for self is put into
+         */
+        public SelfPropertiesCommand(final PrintnameManager manager, GfCapsule gfCapsule, LinPosition focusPos, boolean isAbstract, String toAppend, HashSet processedSubcats) {
+                super(PrintnameManager.SELF_SUBCAT, manager);
+                this.gfCapsule = gfCapsule;
+                this.printnameManager = manager;
+                this.focusPos = focusPos;
+                this.processedSubcats = processedSubcats;
+                this.toAppend = toAppend;
+                this.isAbstract = isAbstract;
+        }
+
+        /**
+         * @return a Vector of RealCommand containing the suitable properties
+         * of self at the current focus position.
+         * Subtyping is taken into account, so only properties with a subtype
+         * of the supertype of the coerce above (at other places this method
+         * is not applicable) show up in this menu.
+         * The method used is similiar to the one for Instances below a coerce.
+         */
+        Vector produceSubmenu() {
+                logger.fine("SelfPropertiesCommand asked to produce a menu");
+                //HashSet to prevent duplicates
+                final HashSet commands = new HashSet();
+                RefinementMenuCollector rmc = new RefinementMenuCollector(gfCapsule);
+                //move to the subtype witness argument
+                final String collectSubtypesCommand = "mp " + LinPosition.calculateBrethrenPosition(focusPos.position, 2); 
+                final Vector possibleSubtypes = rmc.readRefinementMenu(collectSubtypesCommand);
+                String undoString = "";
+                int undos = 0;
+                //for the case, that there is only one possible refinement at all
+                //which gets automatically filled in
+                final StringBuffer singleReplacement = new StringBuffer();
+                //loop through the offered Subtype refinements
+                for (Iterator it = possibleSubtypes.iterator(); it.hasNext(); ) {
+                        StringTuple nextCommand = (StringTuple)it.next();
+                        if (!nextCommand.first.trim().startsWith("r")) {
+                                //no ac, d, rc or whatever wanted here. Only refine.
+                                continue;
+                        }
+                        final String commandPrefix = undoString + nextCommand.first + " ;; mp " + focusPos.position + " ;; ";
+                        logger.finer("commandPrefix: " + commandPrefix);
+                        Vector futureRefinements = new Vector();
+                        undos = addSelfProperties(futureRefinements, commandPrefix, singleReplacement);
+                        undos += 2; // to undo commandPrefix
+                        undoString = "u " + undos + " ;; "; //for all following runs we want an undo before it
+//                        Vector nextRefinements = rmc.readRefinementMenu(collectRefinementsCommand);
+                        commands.addAll(futureRefinements);
+                }
+                final String cleanupCommand = "u " + (undos + 1); //undo the last command and also the first mp
+                rmc.readRefinementMenu(cleanupCommand); //no harm done here, collector won't get reused
+                Vector result = new Vector();
+                for (Iterator it = commands.iterator(); it.hasNext();) {
+                        StringTuple st = (StringTuple)it.next();
+                        if ((commands.size() == 1) && (st instanceof ChainCommandTuple)) {
+                                //the case when only one property is available at all.
+                                //Then this will automatically be selected
+                                //To compensate for that, singleRefinement is used.
+                                //This will be just one refinement, otherwise, we
+                                //wouldn't be in this branch.
+                                //This refinement does not contain the actual r 
+                                //command and therefore needs one undo step less
+                                ChainCommandTuple cct = (ChainCommandTuple)st;
+                                st = new ChainCommandTuple(singleReplacement.toString(), cct.second, cct.fun, cct.subcat, cct.undoSteps - 1);
+                        }
+                        GFCommand gfcommand;
+                        if (st instanceof ChainCommandTuple) {
+                                ChainCommandTuple cct = (ChainCommandTuple)st;
+                                gfcommand = new RealCommand(st.first, processedSubcats, printnameManager, st.second, isAbstract, toAppend, cct.undoSteps, cct.fun, cct.subcat);
+                        } else {
+                                gfcommand = new RealCommand(st.first, processedSubcats, printnameManager, st.second, isAbstract, toAppend);
+                        }
+                        result.add(gfcommand);
+                }
+                Collections.sort(result);
+                return result;
+        }
+        
+        /**
+         * Probes for the properties of self, that could be filled in at
+         * the current focus position.
+         * If it finds any, these are added to result.
+         * @param result The Vector, that will get filled with the collected 
+         * chain commands
+         * @param commandPrefix The prefix, that is to be prepended to the 
+         * probing command. Used for refining with a Subtype witness and a
+         * mp to the Instance position, where this method expects to start.
+         * @param singleReplacement This is a hack for cases, when GF refines
+         * an refinement automatically. If that happens only for one subtype,
+         * then GF would fill that in automatically even when the supertype is
+         * open. Therefore, it must be omitted in the actual command.
+         * But this situation can only be checked after all subtypes have been
+         * probed.
+         * @return the number of undo steps needed to undo the probing command
+         * (without prefix, that is handled by the caller)
+         */
+        private int addSelfProperties(final Vector result, final String commandPrefix, final StringBuffer singleReplacement) {
+                //solve in between to avoid some typing errors by closing some type arguments
+                final String probeCommand = "r core.implPropCall ;; mp " + focusPos.childPosition(2) + " ;; r core.self ;; solve ;; mp " + focusPos.childPosition(3);
+                final String deleteAppendix = " ;; d";
+                final RefinementMenuCollector rmc = new RefinementMenuCollector(gfCapsule);
+                final String actualProbeCommand = commandPrefix + probeCommand + deleteAppendix;
+                logger.finer("&&& actual probe command:: " + actualProbeCommand);
+                Vector futureRefinements = rmc.readRefinementMenu(actualProbeCommand);
+                final int undos = 5;
+                for (Iterator it = futureRefinements.iterator(); it.hasNext();) {
+                        StringTuple st = (StringTuple)it.next();
+                        if (st.first.startsWith("r")) { //is a refinement, no ac or d
+                                String newCommand;
+                                //add the command that came before
+                                final int cmdUndos;
+                                if (futureRefinements.size() == 1) {
+                                        //the case, when only one property is defined in the grammar:
+                                        singleReplacement.append(probeCommand + " ;; c solve");
+                                }
+                                newCommand = probeCommand + " ;; " + st.first + " ;; c solve";
+                                cmdUndos = 6;
+                                // now extract the fun of the property
+                                String fun = st.first.substring(1).trim();
+                                ChainCommandTuple cct = new ChainCommandTuple(newCommand, st.second, fun, PrintnameManager.SELF_SUBCAT, cmdUndos);
+                                if (logger.isLoggable(Level.FINE)) {
+                                        logger.finer("added " + cct);
+                                }
+                                result.add(cct);
+                        }
+                }
+                return undos;
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/SelfResultProber.java

@@ -0,0 +1,84 @@
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.logging.*;
+
+/**
+ * asks GF if the given commands leads to a situation, where
+ * something could be filled in automatically.
+ * This class is meant for self and result.
+ * @author daniels
+ */
+class SelfResultProber extends AbstractProber {
+        /**
+         * This field is true in the beginning of each run, and 
+         * set to false, if the focus position when checking is found
+         * to be open.
+         */
+        protected boolean autocompleted = true;
+       
+        protected static Logger nogger = Logger.getLogger(SelfResultProber.class.getName());
+        /**
+         * A constructor which sets some fields
+         * @param gfCapsule The encapsulation of the running GF process
+         */
+        public SelfResultProber(GfCapsule gfCapsule) {
+                super(gfCapsule);
+        }
+        
+        /**
+         * asks GF if the given commands leads to a situation, where
+         * something could be filled in automatically.
+         * This function is meant for self and result.
+         * IMPORTANT: Must be called <b>after</b> &lt;/gfedit&gt; 
+         * when no other method reads sth. from GF. 
+         * It uses the same GF as everything else, since it tests if
+         * sth. is possible there. 
+         * @param gfCommand the command to be tested.
+         * One has to chain a mp command to make GF go to the right place afterwards
+         * @param chainCount The number of chained commands in gfCommand.
+         * So many undos are done to clean up afterwards. 
+         * @return true iff sth. could be filled in automatically
+         */
+        public boolean isAutoCompletable(String gfCommand, int chainCount) {
+                this.autocompleted = true;
+                send(gfCommand);
+                readGfedit();
+                final boolean result = this.autocompleted;
+                this.autocompleted = true;
+                //clean up and undo
+                send("u " + chainCount);
+                readAndIgnore();
+                if (nogger.isLoggable(Level.FINE)) {
+                        nogger.fine(result + " is the result for: '" + gfCommand +"'");
+                }
+                return result;
+        }
+        
+        /** 
+         * Reads the tree child of the XML from beginning to end.
+         * Sets autocompleted to false, if the focus position is open.
+         */
+        protected void readTree() {
+                String treeString = gfCapsule.readTree();
+                String[] treeArray = treeString.split("\\n");
+                for (int i = 0; i < treeArray.length; i++) {
+                        String result = treeArray[i].trim();
+                        if (result.startsWith("*")) {
+                                result = result.substring(1).trim();
+                                if (result.startsWith("?")) {
+                                        //the normal case, focus position open
+                                        this.autocompleted = false;
+                                } else if ((i >= 6) //that we could be at the instance argument at all
+                                                && (treeArray[i - 6].indexOf("coerce") > -1) //we are below a coerce
+                                                && (treeArray[i - 3].trim().startsWith("?")) //the Subtype argument is not filled in
+                                                // The super argument cannot be OclAnyC or even unrefined, because then this 
+                                                // method wouldn't have been called. Thus, the Subtype argument is unique.
+                                                ){
+                                        //we are below a coerce, but self would have a non-suiting subtype
+                                        this.autocompleted = false;
+                                }
+                        }
+
+                }
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/StringTuple.java

@@ -0,0 +1,54 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * Small tuple class for two Strings.
+ * The main use is grouping command and showname for GF commands before 
+ * they are processed.
+ * This class is mutable.
+ * Equality is bound to the first argument.
+ * @author daniels
+ */
+class StringTuple {
+        String first;
+        String second;
+
+        /**
+         * Just sets both values. 
+         * @param f Well, the first String
+         * @param s Well, the second String 
+         * (if it is used at all)
+         */
+        public StringTuple(String f, String s) {
+                this.first = f;
+                this.second = s;
+        }
+        
+        public int hashCode() {
+                return this.first.hashCode();
+        }
+        public boolean equals(Object o) {
+                if (o instanceof StringTuple) {
+                        return this.first.equals(((StringTuple)o).first);
+                } else {
+                        return false;
+                }
+        }
+        public String toString() {
+                return this.first;
+        }
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/SubtypingProber.java

@@ -0,0 +1,107 @@
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.logging.Logger;
+import java.util.*;
+
+/**
+ * This class goes through the tree and tries to close all open Subtype lines.
+ *
+ * Makes heavy use of instance fields instead of parameters and return values.
+ * I justify that with the rather small size of this class.
+ * Because of this this class has to be reinitialized for each run. 
+ * @author daniels
+ */
+class SubtypingProber extends RefinementMenuCollector {
+        private static Logger nogger = Logger.getLogger(SubtypingProber.class.getName());
+        /**
+         * how many undos are needed to clean up behind this probing
+         */
+        protected int undoSteps = 0;
+        /**
+         * the GF AST line by line
+         */
+        protected String[] treeArray = new String[0];
+        /**
+         * the pointer to the line, that has been read last
+         */
+        protected int currentLine;
+
+        /**
+         * Standard fill-in-the-parameters constructor
+         * @param gfCapsule The encapsulation of GF
+         */
+        public SubtypingProber(GfCapsule gfCapsule) {
+                super(gfCapsule);
+                this.currentLine = 0;
+        }
+
+        /**
+         * stores the read GF AST in treeArray
+         */
+        protected void readTree() {
+                String treeString = gfCapsule.readTree();
+                this.treeArray = treeString.split("\\n");
+        }
+        
+        /**
+         * looks at the refinement menu for node number lineNumber in the AST
+         * and if there is only one refinement command offered, does
+         * execute this.
+         * @param lineNumber
+         */
+        protected void checkLine(int lineNumber) {
+                String command = "mp [] ;; > " + lineNumber;
+                this.undoSteps += 2;
+                send(command);
+                readGfedit();
+                Vector commands = new Vector();
+                for (Iterator it = this.refinementMenuContent.iterator(); it.hasNext(); ) {
+                        StringTuple next = (StringTuple)it.next();
+                        if (next.first.startsWith("r")) {
+                                commands.add(next);
+                        }
+                }
+                if (commands.size() == 0) {
+                        //nothing can be done
+                        nogger.fine("no refinement for '" + this.treeArray[lineNumber] + "'");
+                } else if (commands.size() == 1) {
+                        StringTuple nextCommand = (StringTuple)commands.lastElement();
+                        nogger.fine("one refinement for '" + this.treeArray[lineNumber] + "'");
+                        send(nextCommand.first);
+                        this.undoSteps += 1;
+                        // now new things are in the state, 
+                        // but since we assume that nothing above lineNumber changes,
+                        // that is wanted.
+                        readGfedit();
+                } else {
+                        nogger.fine(commands.size() + " refinements for '" + this.treeArray[lineNumber] + "'");
+                }
+        }
+        
+        /**
+         * Asks GF for the AST and tries to hunt down all unrefined 
+         * Subtype witnesses.
+         * @return the number of undo steps this run needed
+         */
+        public int checkSubtyping() {
+                //solve to try to eliminate many unrefined places
+                send("c solve ;; mp []"); //focus at the top where '*' does not disturb
+                readGfedit();
+                this.undoSteps += 2;
+                for (int i = 3; i < this.treeArray.length; i++) { 
+                        //the condition gets rechecked every run, and length will only grow
+                        //We start at 3 since the witness is the third argument of coerce,
+                        //before nothing can happen 
+                        //(sth. like "n core.Subtype" does not count! 
+                        //(starting with new category Subtype) )
+                        if (this.treeArray[i].indexOf(": Subtype") > -1) {
+                                if (!this.treeArray[i - 2].startsWith("?") //both Class arguments refined
+                                                && !this.treeArray[i - 1].startsWith("?")) {
+                                        checkLine(i);
+                                }
+                        }
+                }
+                nogger.fine(this.undoSteps + " individual commands sent");
+                return this.undoSteps;
+        }
+}

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

@@ -0,0 +1,71 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.awt.Component;
+import javax.swing.JLabel;
+import javax.swing.JList;
+import javax.swing.ListCellRenderer;
+
+/**
+ * A cell renderer, that returns JLables, that put everything after the first
+ * '$' character into their tooltip
+ * @author daniels
+ */
+public class ToolTipCellRenderer extends JLabel implements ListCellRenderer {
+        
+        /**
+         * 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
+         * @param isSelected is the cell selected
+         * @param cellHasFocus the list and the cell have the focus
+         * @return a suiting JLabel
+         */
+        public Component getListCellRendererComponent(JList list, Object value, int index, boolean isSelected, boolean cellHasFocus) {
+                if (isSelected) {
+                        setBackground(list.getSelectionBackground());
+                        setForeground(list.getSelectionForeground());
+                }
+                else {
+                        setBackground(list.getBackground());
+                        setForeground(list.getForeground());
+                }
+                setEnabled(list.isEnabled());
+                setFont(list.getFont());
+                setOpaque(true);
+
+                
+                if (value == null) {
+                        setText("Null-Value!!! Something went terribly wrong here!");
+                } else if (value instanceof GFCommand){
+                        GFCommand gfc = (GFCommand)value;
+                        String disText = gfc.getDisplayText();
+                        if (gfc instanceof LinkCommand) {
+                                //italic font could be an alternative
+                                disText = "-> " + disText;
+                        }
+                        setText(disText);
+                        setToolTipText(gfc.getTooltipText());
+                } else {
+                        setText(value.toString());
+                        setToolTipText("Strange thing of class '" + value.getClass() + "'");
+                }
+                return this;
+        }
+        
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/TreeAnalyser.java

@@ -0,0 +1,387 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.Enumeration;
+import java.util.logging.Level;
+import java.util.logging.Logger;
+
+import javax.swing.tree.DefaultMutableTreeNode;
+
+/**
+ * Goes through the AST and:
+ *   Labels node according to the following:
+ *     hidden, if they are a coerce without a constraint
+ *     colored, if they are a coerce with a constraint
+ *   Saves a reference to the currently selected node
+ *   Finds out 
+ *     if attributes of self should be given an easy access,
+ *     if the refinement menu below a coerce should be reduces,
+ *     if it should be probed, if self and result are superfluous
+ *       in the refinement menu.
+ *     if a coerce should be introduced automatically.
+ * Takes a tree and hides the nodes labelled as hidden in another stage.
+ * @author hdaniels
+ */
+class TreeAnalyser {
+        /** 
+         * debug stuff for the tree 
+         */
+        private static Logger treeLogger = Logger.getLogger(TreeAnalyser.class.getName());
+        /** 
+         * dealing with coerce, when it is inserted and so on 
+         */
+        private static Logger coerceLogger = Logger.getLogger(TreeAnalyser.class.getName() + ".coerce");
+
+        /**
+         * if coerce should get hidden, if all their arguments are refined
+         */
+        private boolean hideCoerce;
+        /**
+         * if coerce should always be hidden,
+         */
+        private boolean hideCoerceAggressive;
+        /**
+         *  if the refinement menu should get condensed at all
+         */
+        private boolean coerceReduceRM;
+        /**
+         * if coerce should get introduced automatically at all
+         */
+        private boolean autoCoerce;
+        /**
+         * if result and self should be shown always
+         */
+        private boolean showSelfResult;
+        /**
+         * if properties of self should be probed for
+         */
+        private boolean easyAttributes;
+        /**
+         * If coerces whith both Class arguments
+         */
+        private boolean highlightSubtypingErrors;
+        
+        /**
+         * @param autoCoerce if coerce should get introduced automatically at all
+         * @param coerceReduceRM if the refinement menu should get condensed at all
+         * @param easyAttributes if properties of self should be probed for
+         * @param hideCoerce if coerce should get hidden, if all their arguments are refined
+         * @param hideCoerceAggressive if coerce should always be hidden, 
+         * unless there is a GF constraint
+         * @param highlightSubtypingErrors If coerces whith both Class arguments 
+         * refined, but not with the Subtype argument should get marked
+         * @param showSelfResult if result and self should be shown always
+         */
+        public TreeAnalyser(boolean autoCoerce, boolean coerceReduceRM, boolean easyAttributes, boolean hideCoerce, boolean hideCoerceAggressive, boolean highlightSubtypingErrors, boolean showSelfResult) {
+                this.autoCoerce = autoCoerce;
+                this.coerceReduceRM = coerceReduceRM;
+                this.easyAttributes = easyAttributes;
+                this.hideCoerce = hideCoerce;
+                this.hideCoerceAggressive = hideCoerceAggressive;
+                this.highlightSubtypingErrors = highlightSubtypingErrors;
+                this.showSelfResult = showSelfResult;
+        }
+
+        
+        /**
+         * Takes the rootNode of the AST and does some small analysis on it:
+         *   Check for missing Subtype witnesses, 
+         *   check if the Instance menu of a Coerce can be reduced
+         * @param topNode The root or top node of the AST
+         * @return an object that contains the result of this analysis.
+         * Currently this applies only to the selected node. 
+         * @see TreeAnalysisResult 
+         */
+        TreeAnalysisResult analyseTree(DefaultMutableTreeNode topNode) {
+                //just the initial values
+                String resultCommand = null;
+                int resultUndoSteps = -1;
+                boolean resultReduceCoerce = false;
+                boolean resultProbeSelfResult = false;
+                boolean resultDeleteAlsoAbove = false;
+                boolean resultEasyAttributes = false;
+                TreeAnalysisResult tar = new TreeAnalysisResult(resultCommand, resultUndoSteps, resultReduceCoerce, resultProbeSelfResult, resultDeleteAlsoAbove, resultEasyAttributes, null, null);
+
+                //doing it depth first, because we have to know the subtypingStatus
+                //of the children of coerce before we analyze coerce itself
+                for (Enumeration e = topNode.depthFirstEnumeration() ; e.hasMoreElements() ;) {
+                        DefaultMutableTreeNode currNode = (DefaultMutableTreeNode)e.nextElement();
+                        analyseTreeNode(currNode, tar);
+                }
+                AstNodeData and = (AstNodeData)tar.selectedNode.getUserObject();
+                if ((and.showInstead != -1) && (tar.command == null)) {
+                        //if the current node is hidden, move up in the tree,
+                        //until a visible node is found
+                        DefaultMutableTreeNode tn = (DefaultMutableTreeNode)tar.selectedNode.getParent();
+                        AstNodeData dand = null;
+                        while (tn != null) {
+                                dand = (AstNodeData)tn.getUserObject();
+                                if (dand.showInstead == -1) {
+                                        //found a visible node
+                                        break;
+                                }
+                                tn = (DefaultMutableTreeNode)tn.getParent();
+                        }
+                        if (dand != null) {
+                                tar.command = "[tr] mp " + dand.position;
+                                tar.undoSteps = 1;
+                        } //otherwise give up, can only occur, if coerce is the top node.
+                        //And for that, one would have to do a "n Instance" first,
+                        //which GF does not even offer.
+                }
+                return tar;
+        }
+        
+        /**
+         * Takes the rootNode of the AST and does some small analysis on it:
+         *   Check for missing Subtype witnesses, 
+         *   check if the Instance menu of a Coerce can be reduced
+         * @param nodeToCheck The node that is to be analysed
+         * @param tar The result, that gets modified
+         * @see TreeAnalysisResult
+         */
+        private void analyseTreeNode(DefaultMutableTreeNode nodeToCheck, TreeAnalysisResult tar) {
+                AstNodeData and = (AstNodeData)nodeToCheck.getUserObject();
+                DefaultMutableTreeNode parent = (DefaultMutableTreeNode)nodeToCheck.getParent();
+                Printname parentPrintname = null;
+                if ((parent != null) && (parent.getUserObject() != null) && (parent.getUserObject() instanceof AstNodeData)) {
+                        AstNodeData parentAnd = (AstNodeData)parent.getUserObject();
+                        parentPrintname = parentAnd.getPrintname();
+                }
+
+                if (and.selected) {
+                        tar.selectedNode = nodeToCheck;
+                        tar.currentNode = and.node;
+                        //set the focusPosition to a preliminary value
+                        tar.focusPosition = new LinPosition(and.position, true);
+                        //rather check too much for null
+                        if (this.autoCoerce
+                                        && (and.node != null)
+                                        && and.node.isMeta()
+                                        && (parent != null)
+                                        && (parent.getUserObject() != null)
+                                        && (and.node.getType() != null)
+                                        && (and.node.getType().startsWith("Instance"))) {
+                                //check, if a coerce is needed                                
+                                GfAstNode parentNode = ((AstNodeData)parent.getUserObject()).node;
+                                if (parentPrintname.getParamAutoCoerce(parent.getIndex(nodeToCheck))) {
+                                        coerceLogger.fine("Coerceable fun found: " + and.node + " + " + parentNode);
+                                        //refine with coerce. Do not allow another GF run, so [r]
+                                        tar.command = "[tr] r core.coerce ;; mp " + LinPosition.calculateChildPosition(and.position, 3);
+                                        tar.undoSteps = 2; //move there is also sth. to be undone
+                                } else if ((parentNode.getFun().indexOf("coerce") > -1)
+                                                //to avoid getting stuck below a coerce with wrong type arguments
+                                                //the coerce above is deleted and rerefined.
+                                                
+                                                //coerce below a coerce is never done automatically, so the else if is justified,
+                                                //meaning, that introduced a coerce, we do not have to delete it right a away 
+                                                && parent.getParent() != null 
+                                                && (parent.getParent() instanceof DefaultMutableTreeNode)) {
+                                        DefaultMutableTreeNode grandParent = (DefaultMutableTreeNode)parent.getParent();
+                                                if (grandParent != null) {
+                                                AstNodeData grandParentAnd = (AstNodeData)grandParent.getUserObject();
+                                                Printname grandParentPrintname = grandParentAnd.getPrintname();
+        
+                                                if (grandParentPrintname.getParamAutoCoerce(grandParent.getIndex(parent))) {
+                                                        coerceLogger.fine("Auto-Coerce to be un- and redone: " 
+                                                                        + and.node + " + " + parentNode 
+                                                                        + " -- " + tar.focusPosition.position);
+                                                        tar.command = "[tr] mp " + tar.focusPosition.parentPosition() 
+                                                                + " ;; d ;; mp " + tar.focusPosition.parentPosition() 
+                                                                + " ;; r core.coerce ;; mp " + tar.focusPosition.position;
+                                                        tar.undoSteps = 6;
+                                                }
+                                        }
+                                }
+                        }
+                        
+                        if (coerceReduceRM
+                                        && (and.node != null)
+                                        && (and.node.getType() != null)
+                                        && (parent != null)
+                                        && (parent.getUserObject() != null)
+                                        && (((AstNodeData)parent.getUserObject()).getPrintname() != null)
+                                        && (((AstNodeData)parent.getUserObject()).getPrintname().fun.endsWith("coerce"))
+                                        && (and.node.getType().startsWith("Instance")) //if coerce, than we are the Instance argument
+                                        && (((DefaultMutableTreeNode)(parent.getChildAt(2))).getUserObject() != null)
+                                        && (parent.getChildAt(2) != null)
+                                        && ((AstNodeData)((DefaultMutableTreeNode)(parent.getChildAt(2))).getUserObject()).node.isMeta()) {
+                                AstNodeData superTypeAnd = ((AstNodeData)((DefaultMutableTreeNode)(parent.getChildAt(1))).getUserObject());
+                                if (!superTypeAnd.node.isMeta() && (superTypeAnd.node.getFun().indexOf("OclAnyC") == -1)) {
+                                        //in these cases, everything goes. No sense in dozends of expensive GF runs then.
+                                        tar.reduceCoerce = true;
+                                }
+                                coerceLogger.fine("candidate for coerce reduction found: " + and.node + " + " + parent);
+                        }
+                        
+                        if (showSelfResult
+                                        && (and.node != null)
+                                        && (and.node.getType() != null)
+                                        && (and.node.getType().startsWith("Instance"))
+                                        && (tar.reduceCoerce //not everything is allowed here
+                                                      // if not below a coerce (covered above) and no constraints
+                                                        || (and.node.getType().indexOf("{") == -1)) 
+                                        ){
+                                //if there are constraints present, there is no point in probing, since
+                                //then either no or every instance is offered.
+                                //We do not have to probe then.
+                                tar.probeSelfResult = true;
+                        }
+                        
+                        if (easyAttributes
+                                        && (and.node != null)
+                                        && (and.node.getType() != null)
+                                        && (and.node.isMeta())
+                                        && (and.node.getType().startsWith("Instance"))
+                                ) {
+                                //not much to check here
+                                tar.easyAttributes = true;
+                        }
+                }
+                
+                //check for subtyping errors
+                if (highlightSubtypingErrors
+                                && (and.node != null)
+                                && (and.node.getType() != null)
+                                && (parent != null)
+                                && (and.node.isMeta()) //otherwise GF would complain
+                                && (and.node.getType().startsWith("Subtype")) //if coerce, than we are the Subtype argument
+                                ) {
+                        AstNodeData subtypeAnd = (AstNodeData)(((DefaultMutableTreeNode)(parent.getChildAt(0))).getUserObject());
+                        AstNodeData supertypeAnd = (AstNodeData)(((DefaultMutableTreeNode)(parent.getChildAt(1))).getUserObject());
+                        if ((subtypeAnd != null) && (supertypeAnd != null)) {
+                                if (!supertypeAnd.node.isMeta() && !subtypeAnd.node.isMeta()) {
+                                        //if one of them is meta, then the situation is not fixed yet,
+                                        //so don't complain.
+                                        and.subtypingStatus = false;
+                                } 
+                        }
+                }
+                //hide coerce if possible
+                //if coere is completely filled in (all children not meta),
+                //it will be replaced by child 3.
+                if (hideCoerce
+                                && (and.node != null)
+                                && (and.node.getType() != null)
+                                && (and.node.getFun().endsWith("coerce"))
+                                ) {
+                        /** 
+                         * if true, then something is unfinished or constrained.
+                         * So don't hide that node.
+                         */
+                        boolean metaChild = false;
+                        //check if constraints hold for this node
+                        if ((and.constraint != null) && (and.constraint.length() > 0)) {
+                                //some constraint holds here. 
+                                //We must not shroud a possible source for that.
+                                metaChild = true;
+                        }
+                        //This search will only be run once for each coerce:
+                        for (int i = 0; i < 3 && !metaChild; i++) {
+                                //This is for the more complicated collection
+                                //subtyping witnesses.
+                                //we do a depthFirst search to find meta nodes.
+                                //If they exist, we know that we shouldn't hide this node.
+                                for (Enumeration e = ((DefaultMutableTreeNode)nodeToCheck.getChildAt(i)).depthFirstEnumeration() ; e.hasMoreElements() ;) {
+                                        DefaultMutableTreeNode currNode = (DefaultMutableTreeNode)e.nextElement();
+                                        AstNodeData dand = (AstNodeData)currNode.getUserObject();
+                                        if (!dand.subtypingStatus
+                                                        //hideCoerceAggressive means that just incomplete type arguments are no reason to not hide the node
+                                                        //only subtypingStatus is one because then surely there is an error
+                                                        || (!hideCoerceAggressive && dand.node.isMeta())) {
+                                                metaChild = true;
+                                                break; //no need to go further
+                                        }
+                                }
+                                if (metaChild) {
+                                        break;
+                                }
+                        }
+                        //For the Instance argument, we do not have do to a deep search 
+                        AstNodeData childAnd = (AstNodeData)(((DefaultMutableTreeNode)(nodeToCheck.getChildAt(3))).getUserObject());
+                        if (!hideCoerceAggressive && childAnd.node.isMeta()) {
+                                //see reasons for hideCoerceAggressive above
+                                metaChild = true;
+                        }
+
+                        if (!metaChild) {
+                                and.showInstead = 3;
+                                //now label the type nodes as hidden
+                                for (int i = 0; i < 3 && !metaChild; i++) {
+                                        //This is for the more complicated collection
+                                        //subtyping witnesses.
+                                        for (Enumeration e = ((DefaultMutableTreeNode)nodeToCheck.getChildAt(i)).depthFirstEnumeration() ; e.hasMoreElements() ;) {
+                                                DefaultMutableTreeNode currNode = (DefaultMutableTreeNode)e.nextElement();
+                                                AstNodeData dand = (AstNodeData)currNode.getUserObject();
+                                                dand.showInstead = -2; // tag for hidden without replacement
+                                        }
+                                }
+
+                        }
+                        
+                        //if we are at a coerce above the selected Instance node,
+                        //we want to mark that, so that the d command can be modified
+                        if ((and.node != null)
+                                        && (and.node.getFun().endsWith("coerce"))
+                                        && (and.showInstead > -1) //only hidden coerce
+                                        && (((AstNodeData)((DefaultMutableTreeNode)nodeToCheck.getChildAt(3)).getUserObject()).selected)
+                                        ) {
+                                tar.deleteAlsoAbove = true;
+                        }
+                }
+        }
+        /**
+         * Removes nodes from the tree that has topNode as its root.
+         * Affected are nodes in which the field showInstead in their
+         * AstNodeData is greater than -1
+         * @param topNode The root of the tree from which nodes should
+         * be removed.
+         * @return The root of the transformed tree. 
+         * This might not be topNode, since that node might as well be 
+         * removed. 
+         */
+        protected static DefaultMutableTreeNode transformTree(DefaultMutableTreeNode topNode) {
+                DefaultMutableTreeNode nextNode = topNode;
+                while (nextNode != null) {
+                        AstNodeData and = (AstNodeData)nextNode.getUserObject();
+                        if (and.showInstead > -1) {
+                               DefaultMutableTreeNode parent = (DefaultMutableTreeNode)nextNode.getParent();
+                               if (parent == null) {
+                                       topNode = (DefaultMutableTreeNode)nextNode.getChildAt(and.showInstead);
+                                       if (treeLogger.isLoggable(Level.FINE)) {
+                                               //yeah, I know, variable naming is messed up here because of the assignment above
+                                               treeLogger.fine("hiding topNode ###" + nextNode + "###, showing instead ###" + topNode + "###");
+                                       }
+                                       nextNode = topNode;
+                               } else {
+                                       final int index = parent.getIndex(nextNode);
+                                       parent.remove(index);
+                                       DefaultMutableTreeNode instead = (DefaultMutableTreeNode)nextNode.getChildAt(and.showInstead);
+                                       parent.insert(instead, index);
+                                       if (treeLogger.isLoggable(Level.FINE)) {
+                                               treeLogger.fine("hiding node ###" + nextNode + "###, showing instead ###" + instead + "###");
+                                       }
+                                       nextNode = instead;
+                               }
+                        } else {
+                                nextNode = nextNode.getNextNode();
+                        }
+                }
+                return topNode;
+        }
+
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/TreeAnalysisResult.java

@@ -0,0 +1,92 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import javax.swing.tree.DefaultMutableTreeNode;
+
+/**
+ * A class to store the result of the tree analysis done in formTree
+ * @author daniels
+ */
+class TreeAnalysisResult {
+        /**
+         * The command, that is to be executed next automatically
+         */
+        String command;
+        /**
+         * the number of undo steps needed to undo command
+         */
+        int undoSteps;
+        /**
+         * reduceCoerce Whether the mechanism to produce a reduced
+         * refinement menu for coerce's 4th argument should kick in or not.
+         */
+        boolean reduceCoerce;
+        /**
+         * If the editor should ask GF if self an result are applicable here or not
+         */
+        boolean probeSelfResult;
+        /**
+         * If we at the the Instance Argument of a hidden
+         * coerce, we mark that (to change the d command)
+         */
+        boolean deleteAlsoAbove;
+        /**
+         * if the attributes of self should be added to the refinement menu.
+         */
+        boolean easyAttributes;
+        DefaultMutableTreeNode selectedNode = null;
+        /**
+         * The currently selected node
+         */
+        GfAstNode currentNode;
+        /**
+         * Where the cursor in GF is. 
+         * Correct is not yet known and thus always true.
+         */
+        LinPosition focusPosition;
+        
+        /**
+         * Just sets both values. 
+         * @param command The command, that is to be executed next automatically
+         * @param undoSteps the number of undo steps needed to undo command 
+         * @param reduceCoerce Whether the mechanism to produce a reduced
+         * refinement menu for coerce's 4th argument should kick in or not.
+         * @param probeSelfResult If the editor should ask GF if self an result
+         * are applicable here or not
+         * @param deleteAlsoAbove If we at the the Instance Argument of a hidden
+         * coerce, we mark that (to change the d command)
+         * @param easyAttributes if the attributes of self should be added to the
+         * refinement menu.
+         * @param currentNode The currently selected node
+         * @param focusPosition Where the cursor in GF is. 
+         * Correct is not yet known and thus always true.
+         */
+        public TreeAnalysisResult(String command, int undoSteps, boolean reduceCoerce, boolean probeSelfResult, boolean deleteAlsoAbove, boolean easyAttributes, GfAstNode currentNode, LinPosition focusPosition) {
+                this.command = command;
+                this.undoSteps = undoSteps;
+                this.reduceCoerce = reduceCoerce;
+                this.probeSelfResult = probeSelfResult;
+                this.deleteAlsoAbove = deleteAlsoAbove;
+                this.currentNode = currentNode;
+                this.easyAttributes = easyAttributes;
+                this.focusPosition = focusPosition;
+        }
+        
+        public String toString() {
+                return this.command + "|" + this.reduceCoerce + "|" + this.undoSteps + "|" + this.probeSelfResult;
+        }
+}

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

@@ -0,0 +1,120 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.io.IOException;
+import java.util.Hashtable;
+import java.util.logging.*;
+
+/**
+ * @author daniels
+ * If the entries of the refinement menu should have to appear there with
+ * type information appended to them, then the printnames have to get this
+ * knowledge at the time of their creation.
+ * When the entries are displayed, the display text line of GF is *not* looked
+ * at. And even if it would be, it would mess up the architecture, that the 
+ * printnames, and only they, are responsible for their linearization.
+ * Appending their type later on would break that architecture.
+ * So they have to be prepared.
+ */
+public class TypesLoader extends AbstractProber {
+        /**
+         * The hash in which the funs as keys and 
+         * types as values get saved. Both are Strings.
+         */
+        protected final Hashtable hashtable;
+        private static Logger nogger = Logger.getLogger(TypesLoader.class.getName());
+        /**
+         * @param gfCapsule the read/write encapsulation of the running GF
+         * @param myHashMap The hash in which the funs as keys and 
+         * types as values get saved. Both are Strings.
+         */
+        public TypesLoader(GfCapsule gfCapsule, Hashtable myHashMap) {
+                super(gfCapsule);
+                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 = gfCapsule.fromProc.readLine();
+                        if (nogger.isLoggable(Level.FINER)) {
+                                nogger.finer("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 = gfCapsule.fromProc.readLine();
+                                if (nogger.isLoggable(Level.FINER)) {
+                                        nogger.finer("7 " + result);
+                                }
+                        }
+                        if (nogger.isLoggable(Level.FINER)) {
+                                nogger.finer("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";
+                if (nogger.isLoggable(Level.FINE)) {
+                        nogger.fine("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());
+                }
+        }
+
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/UnrefinedAstNodeData.java

@@ -0,0 +1,64 @@
+//Copyright (c) Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.logging.*;
+
+/**
+ * @author daniels
+ *
+ * represents an open, unrefined node in the AST.
+ * It knows, how it is called and described (tooltip).
+ */
+public class UnrefinedAstNodeData extends AstNodeData {
+        /**
+         * The tooltip that this node as a parameter should get
+         */
+        protected final String paramTooltip;
+        
+        /**
+         * For a child we have to know its name, its type and the tooltip
+         * @param pTooltip The tooltip that this node as a parameter should get
+         * @param node The GfAstNode for the current AST node, for which
+         * this AstNodeData is the data for.
+         * @param pos The position in the GF AST of this node in Haskell notation
+         * @param selected if this is the selected node in the GF AST
+         * @param constraint A constraint from a parent node, that also
+         * applies for this node.
+         */
+        public UnrefinedAstNodeData(String pTooltip, GfAstNode node, String pos, boolean selected, String constraint) {
+                super(node, pos, selected, constraint);
+                this.paramTooltip = pTooltip;
+                if (logger.isLoggable(Level.FINEST)) {
+                        logger.finest(this.toString() + " - " + position);
+                }
+        }
+        /**
+         * @return no refinement, no printname, thus null
+         */
+        public Printname getPrintname() {
+                return null;
+        }
+
+        /**
+         * @return the parameter tooltip that this node has as a child
+         * of its parent (who gave it to it depending on its position)
+         */
+        public String getParamTooltip() {
+                return this.paramTooltip;
+        }
+
+}

src-2.9/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java

@@ -0,0 +1,243 @@
+//Copyright (c) Kristofer Johanisson 2005, Hans-Joachim Daniels 2005
+//
+//This program is free software; you can redistribute it and/or modify
+//it under the terms of the GNU General Public License as published by
+//the Free Software Foundation; either version 2 of the License, or
+//(at your option) any later version.
+//
+//This program is distributed in the hope that it will be useful,
+//but WITHOUT ANY WARRANTY; without even the implied warranty of
+//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//GNU General Public License for more details.
+//
+//You can either finde the file LICENSE or LICENSE.TXT in the source 
+//distribution or in the .jar file of this application
+
+
+package de.uka.ilkd.key.ocl.gf;
+
+
+import java.io.File;
+import java.util.logging.*;
+import javax.swing.ProgressMonitor;
+import java.util.Vector;
+
+/**
+ * consists of a bunch of static methods, mostly for String
+ * @author daniels
+ *
+ */
+public class Utils {
+        private static Logger timeLogger = Logger.getLogger(Utils.class.getName() + ".timer");
+        private static Logger deleteLogger = Logger.getLogger(Utils.class.getName() + ".delete");
+        private static Logger stringLogger = Logger.getLogger(Utils.class.getName() + ".string");
+        
+        private Utils() {
+                //non-instantiability enforced
+        }
+        
+        public static final String gf = "gf";
+        public static final String gfcm = "gfcm";
+        
+        /**
+         * Get the extension of a file.
+         */
+        public static String getExtension(File f) {
+                String ext = null;
+                String s = f.getName();
+                int i = s.lastIndexOf('.');
+                
+                if (i > 0 &&  i < s.length() - 1) {
+                        ext = s.substring(i+1).toLowerCase();
+                }
+                return ext;
+        }
+        /**
+         * Sets the progress on the given ProgressMonitor and logs the current time.
+         * @param pm the monitor which is to be updated. If null, only logging is done
+         * @param progress The progress in absolute ticks
+         * @param note The note that is to be displayed above the progress monitor
+         */
+        public static void tickProgress(ProgressMonitor pm, int progress, String note) {
+                if (note != null) {
+                        if (timeLogger.isLoggable(Level.FINER)) {
+                                timeLogger.finer(System.currentTimeMillis() + " : " + note);
+                        }
+                }
+                if (pm == null) {
+                        return;
+                }
+                pm.setProgress(progress);
+                if (note != null) {
+                        pm.setNote(note);
+                }
+        }
+        
+        /**
+         * schedules all Eng, OCL and Ger grammar files for deletion.
+         * @param grammarsDir The directory where those files are
+         */
+        public static void cleanupFromUMLTypes(String grammarsDir) {
+                String[] endings = {"Eng.gf", "Eng.gfc", "Ger.gf", "Ger.gfc", "OCL.gf", "OCL.gfc", ".gf", ".gfc"};
+                for (int i = 0; i < endings.length; i++) {
+                        String filename = grammarsDir + File.separator + GFEditor2.modelModulName + endings[i];
+                        File file = new File(filename);
+                        file.deleteOnExit();
+                        if (deleteLogger.isLoggable(Level.FINER)) {
+                                deleteLogger.fine("scheduled for deletion: " + filename);
+                        }
+                }
+                File file = new File(grammarsDir);
+                file.deleteOnExit();
+                file = file.getParentFile();
+                file.deleteOnExit();
+        }
+        
+        /**
+         * Searches for the first occurace not escaped with '\' of toBeFound in s.
+         * Works like String::indexOf otherwise
+         * @param s the String to search in
+         * @param toBeFound the String to search for
+         * @return the index of toBeFound, -1 if not found (or only escaped)
+         */
+        public static int indexOfNotEscaped(String s, String toBeFound) {
+                return indexOfNotEscaped(s, toBeFound, 0);
+        }
+        
+        /**
+         * Searches for the first occurace not escaped with '\' of toBeFound in s.
+         * Works like String::indexOf otherwise
+         * @param s the String to search in
+         * @param toBeFound the String to search for
+         * @param startIndex the index in s, from which the search starts
+         * @return the index of toBeFound, -1 if not found (or only escaped)
+         */
+        public static int indexOfNotEscaped(String s, String toBeFound, int startIndex) {
+                for (int from = startIndex; from < s.length();) {
+                        int i = s.indexOf(toBeFound, from);
+                        if (i <= 0) {
+                                //-1 is not found at all, 0 can't have a '\' before
+                                return i;
+                        } else if (s.charAt(i-1) != '\\') {
+                                return i;
+                        } else {
+                                from = i + 1;
+                        }
+                }
+                return -1;
+        }
+        
+        /**
+         * a simple replaceAll replacement, that uses NO regexps 
+         * and thus needs no freaking amount of backslashes
+         * @param original The String in which the replacements should take place
+         * @param toReplace the String literal that is to be replaced
+         * @param replacement the replacement string
+         * @return original, but with replacements
+         */
+        public static String replaceAll(String original, String toReplace, String replacement) {
+                StringBuffer sb = new StringBuffer(original);
+                for (int i = sb.indexOf(toReplace); i >= 0; i = sb.indexOf(toReplace, i + replacement.length())) {
+                        sb.replace(i, i + toReplace.length(), replacement);
+                }
+                return sb.toString();
+        }
+        
+        /**
+         * Removes all parts, that are inside "quotation marks" from s.
+         * Assumes no nesting of those, like in Java.
+         * " escaped with \ like \" do not count as quotation marks
+         * @param s The String, that possibly contains quotations
+         * @return a String described above, s without quotations.
+         */
+        public static String removeQuotations(String s) {
+                if (s.indexOf('"') == -1) {
+                        return s;
+                }
+                for (int begin = indexOfNotEscaped(s, "\""); begin > -1 ;  begin = indexOfNotEscaped(s, "\"", begin)) {//yes, I want an unescaped '"'!
+                        int end = indexOfNotEscaped(s, "\"", begin + 1);
+                        if (end > -1) {
+                                s = s.substring(0, begin) + s.substring(end + 1);
+                        } else {
+                                stringLogger.info("Strange String given: '" + s + "'");
+                                s = s.substring(0, begin);
+                        }
+                }
+                return s;
+        }
+        
+        /**
+         * counts the occurances of toSearch in s
+         * @param s The String in which the search shall take place
+         * @param toSearch The String that should be counted
+         * @return the number of occurances, 0 if s is null
+         */
+        public static int countOccurances(String s, String toSearch) {
+                if (s == null) {
+                        return 0;
+                }
+                int result = 0;
+                for (int i = s.indexOf(toSearch); i > -1; i = s.indexOf(toSearch, i)) {
+                        result++;
+                        i += toSearch.length();
+                }
+                return result;
+        }
+        
+        /**
+         * Takes an arbitrary Vector and executes toString on each element and
+         * puts these into a String[] of the same size as the Vector
+         * @param strings A Vector of Object, preferably String
+         * @return The Vector as a String[]
+         */
+        public static String[] vector2Array(Vector strings) {
+                String[] result = new String[strings.size()];
+                for (int i = 0; i < strings.size(); i++) {
+                        result[i] = strings.get(i).toString();
+                }
+                return result;
+        }
+        /**
+         * just replace sequences of spaces with one space
+         * @param s The string to be compacted
+         * @return the compacted result
+         */
+        static String compactSpaces(String s) {
+                String localResult = new String();
+                boolean spaceIncluded = false;
+                
+                for (int i = 0; i < s.length(); i++) {
+                        char c = s.charAt(i);
+                        if (c != ' ') { // include all non-spaces
+                                localResult += String.valueOf(c);
+                                spaceIncluded = false;
+                        } else {// we have a space
+                                if (!spaceIncluded) {
+                                        localResult += " ";
+                                        spaceIncluded = true;
+                                } // else just skip
+                        }
+                }
+                return localResult;
+        }
+        /**
+         * Replaces all occurances of toBeReplaced, that are not escaped by '\'
+         * with replacement
+         * @param working the String in which substrings should be replaced
+         * @param toBeReplaced The substring, that should be replaced by replacement
+         * @param replacement well, the replacement string
+         * @return The String with the replaced parts
+         */
+        public static String replaceNotEscaped(String working, String toBeReplaced, String replacement) {
+        		StringBuffer w = new StringBuffer(working);
+                        for (int i = w.indexOf(toBeReplaced); i > -1 && i < w.length(); i = w.indexOf(toBeReplaced, i)) {
+                                if (i == 0 || w.charAt(i - 1) != '\\') {
+        				w.replace(i, i + toBeReplaced.length(), replacement);
+        				i += replacement.length();
+        			} else {
+        				i += 1;
+        			}
+                        }
+        		return w.toString();
+        }
+}