added daniels' version of the Java editor

src/JavaGUI2/LICENCE_jargs

@@ -0,0 +1,29 @@
+Copyright (c) 2001-2003 Steve Purcell.
+Copyright (c) 2002      Vidar Holen.
+Copyright (c) 2002      Michal Ceresna.
+Copyright (c) 2005      Ewan Mellor.
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met: Redistributions of source code must retain the above copyright notice,
+this list of conditions and the following disclaimer. Redistributions in
+binary form must reproduce the above copyright notice, this list of
+conditions and the following disclaimer in the documentation and/or other
+materials provided with the distribution. Neither the name of the copyright
+holder nor the names of its contributors may be used to endorse or promote
+products derived from this software without specific prior written
+permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE
+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.

src/JavaGUI2/ManifestMain.txt

@@ -0,0 +1,3 @@
+Manifest-Version: 1.0
+Main-Class: de.uka.ilkd.key.ocl.gf.GFEditor2
+Class-Path: log4j-1.2.8.jar jargs-1.0.jar

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

@@ -0,0 +1,172 @@
+package de.uka.ilkd.key.ocl.gf;
+
+import java.io.BufferedReader;
+import java.io.BufferedWriter;
+import java.io.IOException;
+
+import org.apache.log4j.Logger;
+
+/**
+ * A class that offers a basic readGfEdit method with a lot of
+ * hot spots where subclasses can plug in 
+ * @author daniels
+ *
+ */
+abstract class AbstractProber {
+        protected final BufferedReader fromProc;
+        protected final BufferedWriter toProc;
+        protected static Logger logger = Logger.getLogger(AbstractProber.class.getName());        
+        
+        /**
+         * A constructor which sets some fields
+         * @param fromGf the stdout from the GF process
+         * @param toGf the stdin from the GF process
+         */
+        public AbstractProber(BufferedReader fromGf, BufferedWriter toGf) {
+                this.fromProc = fromGf;
+                this.toProc = toGf;
+        }
+        
+        /**
+         * 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>")) {
+                        skipChild("<hmsg>");
+                        try {
+                                String next = fromProc.readLine();
+                                if (logger.isDebugEnabled()) {
+                                        logger.debug("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) {
+                skipChild("<linearizations>");
+        }
+
+        /** Reads the tree child of the XML from beginning to end */
+        protected void readTree() {
+                skipChild("<tree>");
+        }
+
+        /** Reads the message child of the XML from beginning to end */
+        protected void readMessage() {
+                skipChild("<message>");
+        }
+        
+        /** Reads the menu child of the XML from beginning to end */
+        protected void readMenu() {
+                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 = fromProc.readLine();
+                        if (logger.isDebugEnabled()) {
+                                logger.debug("1 " + next);
+                        }
+                        //read either <hsmg> or <lineatization>
+                        readresult = fromProc.readLine();
+                        if (logger.isDebugEnabled()) {
+                                logger.debug("1 " + next);
+                        }
+                        
+                        next = readHmsg(readresult);
+                        
+                        //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 = fromProc.readLine();
+                                if (next!=null){
+                                        if (logger.isDebugEnabled()) {
+                                                logger.debug("1 " + next);
+                                        }
+                                } else {
+                                        System.exit(0);
+                                }
+                        }
+                        readLinearizations(next);
+                        readTree();
+                        readMessage();
+                        readMenu();
+                        
+                        for (int i=0; i<3 && !next.equals(""); i++){ 
+                                next = fromProc.readLine();
+                                if (logger.isDebugEnabled()) {
+                                        logger.debug("1 " + next);
+                                }
+                        }
+                        
+                } catch (IOException e) {
+                        System.err.println("Could not read from external process:\n" + e);
+                }
+                
+        }
+        
+        /**
+         * 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.isDebugEnabled()) {
+                                logger.debug("3 " + nextRead);
+                        }
+                        while (!nextRead.trim().equals(closing)) {
+                                nextRead = fromProc.readLine();
+                                if (logger.isDebugEnabled()) {
+                                        logger.debug("3 " + nextRead);
+                                }
+                        }
+                } 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.isDebugEnabled()) {
+                        logger.debug("## send: '" + text + "'");
+                }
+                try {
+                        toProc.write(text, 0, text.length());
+                        toProc.newLine();
+                        toProc.flush();
+                } catch (IOException e) {
+                        System.err.println("Could not write to external process " + e);
+                }  
+        }
+
+        
+}

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

@@ -0,0 +1,30 @@
+/*
+ * Created on 27.04.2005
+ *
+ */
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * @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.
+ */
+interface AstNodeData {
+        /**
+         * @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();
+
+        /**
+         * 
+         * @return true iff this node represents an open leaf
+         */
+        public abstract boolean isMeta();
+}

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

@@ -0,0 +1,40 @@
+package de.uka.ilkd.key.ocl.gf;
+
+import org.apache.log4j.Logger;
+
+/**
+ * @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());
+
+        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);
+
+}

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

@@ -0,0 +1,202 @@
+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 {
+        private final boolean doText;
+        private final 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) {
+                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;
+                }
+                this.htmlLengthPane.setContentType("text/html");
+                this.htmlLengthPane.setEditable(false);
+        }
+
+        
+        /**
+         * @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
+         * @return the HtmlMarkedArea object that represents the given information
+         * and knows about its beginning and end in the display areas.
+         */
+        protected HtmlMarkedArea addAsMarked(String toAdd, LinPosition position) {
+                /** 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 probably 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 HtmlMarkedArea hma = new HtmlMarkedArea(oldLengthText, newLengthText, position, toAdd, oldLengthHtml, newLengthHtml);
+                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();
+        
+        
+        public String toString() {
+                return getText();
+        }
+}

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

@@ -0,0 +1,347 @@
+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 org.apache.log4j.Logger;
+
+//import de.uka.ilkd.key.util.KeYResourceManager;
+
+import java.awt.event.*;
+//import java.net.URL;
+
+public class DynamicTree2 extends JPanel implements KeyListener,
+ActionListener{
+        protected static Logger logger = Logger.getLogger(DynamicTree2.class.getName());
+        
+        public DefaultMutableTreeNode rootNode;
+        protected DefaultTreeModel treeModel;
+        public JTree tree;
+        public int oldSelection = 0;
+        private Toolkit toolkit = Toolkit.getDefaultToolkit();
+        public JPopupMenu popup = new JPopupMenu();
+        JMenuItem menuItem;
+        private GFEditor2 gfeditor;
+        
+        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);
+                menuItem = new JMenuItem("Paste");
+                menuItem.addActionListener(this);
+                popup.add(menuItem);                         
+                
+                //Add listener to components that can bring up popup menus.
+                MouseListener popupListener = new PopupListener();
+                tree.addMouseListener(popupListener);
+                
+                tree.addTreeSelectionListener(new TreeSelectionListener() {
+                        /**
+                         * the following is assumed:
+                         * in GF we can only switch to the last or the next editing position.
+                         * In the displayed tree, we can click everywhere.
+                         * We navigate through the GF tree by giving the direction 
+                         * and the number of steps
+                         */
+                        public void valueChanged(TreeSelectionEvent e) {
+                                if (tree.getSelectionRows() != null) {
+                                        if (gfeditor.nodeTable == null) {
+                                                if (GFEditor2.treeLogger.isDebugEnabled()) {
+                                                        GFEditor2.treeLogger.debug("null node table");
+                                                }
+                                        } else {
+                                                if (GFEditor2.treeLogger.isDebugEnabled()) {
+                                                        GFEditor2.treeLogger.debug("node table: " + gfeditor.nodeTable.contains(new Integer(0)) + " " + gfeditor.nodeTable.keys().nextElement());
+                                                }
+                                        }
+                                        if (tree.getSelectionPath() == null) {
+                                                if (GFEditor2.treeLogger.isDebugEnabled()) {
+                                                        GFEditor2.treeLogger.debug("null root path");
+                                                }
+                                        } else {
+                                                if (GFEditor2.treeLogger.isDebugEnabled()) {
+                                                        GFEditor2.treeLogger.debug("selected path" + tree.getSelectionPath());
+                                                }
+                                        }
+                                        int i = ((Integer) gfeditor.nodeTable.get(tree.getSelectionPath())).intValue();
+                                        int j = oldSelection;
+                                        gfeditor.treeChanged = true;
+                                        if (i > j)
+                                                gfeditor.send("> " + String.valueOf(i - j));
+                                        else
+                                                gfeditor.send("< " + String.valueOf(j - i));
+                                }
+                        }
+                });
+                
+                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 except the root node. */
+        public void clear() {
+                rootNode.removeAllChildren();
+                treeModel.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.isDebugEnabled()) {
+                        logger.debug("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 (GFEditor2.treeLogger.isDebugEnabled()) {
+                                GFEditor2.treeLogger.debug("The user has finished editing the node.");
+                                GFEditor2.treeLogger.debug("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
+                }
+        }
+        
+        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);
+//                }
+               
+                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();
+				                        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) {
+                        int selRow = tree.getRowForLocation(e.getX(), e.getY());
+                        tree.setSelectionRow(selRow);
+                        if (GFEditor2.treeLogger.isDebugEnabled()) {
+                                GFEditor2.treeLogger.debug("selection changed!");
+                        }
+                        maybeShowPopup(e);
+                }
+                
+                public void mouseReleased(MouseEvent e) {
+                        //nothing to be done here
+                }
+                void maybeShowPopup(MouseEvent e) {
+                        if (GFEditor2.treeLogger.isDebugEnabled()) {
+                                GFEditor2.treeLogger.debug("may be show Popup!");        
+                        }
+                        if (e.isPopupTrigger()) {
+                                if (GFEditor2.treeLogger.isDebugEnabled()) {
+                                        GFEditor2.treeLogger.debug("changing menu!");
+                                }
+                                popup = gfeditor.producePopup();
+                                popup.show(e.getComponent(), e.getX(), e.getY());
+                        } 
+                }
+        }
+
+        public void actionPerformed(ActionEvent ae) {
+                //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/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFCommand.java

@@ -0,0 +1,104 @@
+/*
+ * Created on 20.04.2005
+ */
+package de.uka.ilkd.key.ocl.gf;
+
+
+import org.apache.log4j.Logger;
+
+/**
+ * @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{
+        
+        protected static Logger subcatLogger = Logger.getLogger(GFEditor2.class.getName() + "_subcat");
+        
+        /** 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. InputCommands the greatest. 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;
+                }
+                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/JavaGUI2/de/uka/ilkd/key/ocl/gf/GfAstNode.java

@@ -0,0 +1,123 @@
+/*
+ * Created on 06.05.2005
+ *
+ */
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * @author daniels
+ * This Class represents a parsed node in the GF AST.
+ */
+class GfAstNode {
+        protected final String[] boundTypes;
+        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;
+        }
+
+        /**
+         * 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(" : ");
+                this.type = this.line.substring(index + 3);
+                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;
+        }
+        
+        public static void main(String[] args) {
+               String[] lines = {"?1 : Sent",
+                               "Two : Instance Integer",
+                               "?3 : Instance (Collection (?{this:=this{-0-}}))",
+                               "NOPACKAGEP_StartC_Constr : Constraint {Constraint<>NOPACKAGEP_StartC_Constr (\\this -> invCt ?)}",
+                               "\\(this : VarSelf NOPACKAGEP_StartC) -> invCt : ClassConstraintBody",
+                               "\\(x_0 : Instance Integer) -> ?6 : Sent",
+                               "\\(selfGF : VarSelf NOPACKAGEP_PayCardC),(amount : Instance Integer) -> preC : OperConstraintBody",
+               				   "\\(selfGF : VarSelf NOPACKAGEP_PayCardC),(amount : Instance Integer) -> ?0 : OperConstraintBody"
+                               };
+               String[] funs = {"?1",
+                               	"Two",
+                               	"?3",
+                               	"NOPACKAGEP_StartC_Constr",
+                               	"invCt",
+                               	"?6",
+                               	"preC",
+                               	"?0" 
+                               	};
+               String[] types = {"Sent",
+                               "Instance Integer",
+                               "Instance (Collection (?{this:=this{-0-}}))",
+                               "Constraint {Constraint<>NOPACKAGEP_StartC_Constr (\\this -> invCt ?)}",
+                               "ClassConstraintBody",
+                               "Sent",
+                               "OperConstraintBody",
+                               "OperConstraintBody" 
+                               };
+               
+               for (int i = 0; i < lines.length; i++) {
+                       System.out.println("* " + lines[i]);
+                       GfAstNode gfa = new GfAstNode(lines[i]);
+                       if (!gfa.getFun().equals(funs[i])) {
+                               System.out.println("  fun mismatch: expected '" + funs[i] + "', got '" + gfa.getFun() + "'");
+                       }
+                       if (!gfa.getType().equals(types[i])) {
+                               System.out.println("  type mismatch: expected '" + types[i] + "', got '" + gfa.getType() + "'");
+                       }
+
+               }
+        }
+}

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

@@ -0,0 +1,40 @@
+// 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 java.io.File;
+import javax.swing.filechooser.*;
+
+public class GrammarFilter extends FileFilter {
+        
+        // Accept all directories and all gf, gfm 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.gfm)) {
+                                return true;
+                        } else {
+                                return false;
+                        }
+                }
+                
+                return false;
+        }
+        
+        // The description of this filter
+        public String getDescription() {
+                return "Just Grammars (*.gf, *.gfm)";
+        }
+}

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

@@ -0,0 +1,47 @@
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * @author daniels
+ *
+ * An extender of MarkedArea that adds additional fields for the click-in 
+ * functionality for HTML
+ */
+class HtmlMarkedArea extends MarkedArea {
+
+        /** 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 b The starting position of the stored words
+         * @param e The ending position of the stored words
+         * @param p The position in the AST
+         * @param w The actual text of this area
+         * @param hb the start index in the HTML area
+         * @param he the end index in the HTML area
+         */
+        public HtmlMarkedArea(int b, int e, LinPosition p, String w, int hb, int he) {
+                super(b, e, p, w);
+                this.htmlBegin = hb;
+                this.htmlEnd = he;
+        }
+        
+        /**
+         * Creates a copy of orig, but with additional fields for the click-
+         * in functionality for HTML
+         * @param orig the original MarkedArea that should be extended
+         * @param hb the start index in the HTML area
+         * @param he the end index in the HTML area
+         */
+        HtmlMarkedArea(final MarkedArea orig, final int hb, final int he) {
+                super(orig.begin, orig.end, orig.position, orig.words);
+                this.htmlBegin = hb;
+                this.htmlEnd = he;
+        }
+        
+        public String toString() {
+                return begin + " - " + end + " : " + position + " = '" + words + "' ; HTML: " + htmlBegin + " - " + htmlEnd;
+        }
+}

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

@@ -0,0 +1,104 @@
+package de.uka.ilkd.key.ocl.gf;
+
+import org.apache.log4j.Logger;
+
+/**
+ * @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 {
+        protected final static Logger logger = Logger.getLogger(Printname.class.getName());
+        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;
+        }
+        
+        
+        /**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)
+         * @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() + "\"";
+                        }
+                }
+                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/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinPosition.java

@@ -0,0 +1,34 @@
+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.
+ */
+public 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;
+        }
+        
+        public String toString() {
+                return position + (correctPosition ? " correct" : " incorrect");
+        }
+}
+

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

@@ -0,0 +1,55 @@
+/*
+ * Created on 21.04.2005
+ */
+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 {
+        
+        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/JavaGUI2/de/uka/ilkd/key/ocl/gf/MarkedArea.java

@@ -0,0 +1,40 @@
+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
+ */
+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;
+        /**
+         * Creates a new MarkedArea and initializes the fields with the parameters
+         * @param b The starting position of the stored words
+         * @param e The ending position of the stored words
+         * @param p The position in the AST
+         * @param w The actual text of this area
+         */
+        MarkedArea(int b, int e, LinPosition p, String w) {
+                begin = b;
+                end = e;
+                position = p;
+                words = w;
+        }
+        
+        public String toString() {
+                return begin + " - " + end + " : " + position + " = '" + words + "'";
+        }
+}
+

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

@@ -0,0 +1,458 @@
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.Hashtable;
+import java.util.Vector;
+
+import org.apache.log4j.Logger;
+
+/**
+ * @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 {
+        protected static Logger subcatLogger = Logger.getLogger(Printname.class.getName());
+        
+        public static final Printname delete = new Printname("d", "delete current sub-tree");
+        public static final Printname addclip = new Printname("ac", "add to clipboard\\$<html>adds the current subtree to the clipboard.<br>It is offered in the refinement menu if the expected type fits to the one of the current sub-tree.</html>");
+        public static final Printname printhistory = new Printname("ph", "print history\\$prints all previous command in the linearization area");
+
+        /** 
+         * 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 = "\\#";
+        
+        
+        /** 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.warn(e.getLocalizedMessage());
+                }
+                return name;
+        }
+        /**
+         * contains the descriptions of the paramters of this function (String).
+         * Parallel with paramNames
+         */
+        protected final Vector paramTexts = 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
+         */
+        public Printname(String myFun, String myPrintname, Hashtable myFullnames) {
+                myFun = myFun.trim();
+                myPrintname = myPrintname.trim();
+                this.printname = myPrintname;
+                this.subcatNameHashtable = myFullnames;
+
+                //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];
+                                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);
+                        }
+                        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.isDebugEnabled()) {
+                                        subcatLogger.debug("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
+         */
+        protected Printname(String command, String explanation) {
+                this.fun = command;
+                this.subcatNameHashtable = null;
+                this.subcat = null;
+                this.module = "";
+                this.printname = explanation;
+        }
+        
+        /**
+         * 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 + "$insert the bound variable" + bound;
+        }
+        
+        /** 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 = new StringBuffer(original);
+                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.warn(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;
+        }
+        
+        /**
+         * 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);
+                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);
+                System.out.println("*" + pn.getTooltipText());
+        }
+        
+        public String toString() {
+                return getDisplayText() + "  \n  " + getTooltipText() + " (" + this.paramNames.size() + ")";
+        }
+
+}

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

@@ -0,0 +1,83 @@
+package de.uka.ilkd.key.ocl.gf;
+
+import java.io.BufferedReader;
+import java.io.BufferedWriter;
+import java.io.IOException;
+
+import org.apache.log4j.Logger;
+
+/**
+ * @author daniels
+ *
+ * TODO To change the template for this generated type comment go to
+ * Window - Preferences - Java - Code Style - Code Templates
+ */
+public class PrintnameLoader extends AbstractProber {
+        protected final PrintnameManager printnameManager;
+        protected static Logger nogger = Logger.getLogger(Printname.class.getName());
+        /**
+         * @param fromGf The GF process
+         * @param toGf The GF process
+         * @param pm The PrintnameManager on which the read Printnames
+         * will be registered with their fun name.
+         */
+        public PrintnameLoader(BufferedReader fromGf, BufferedWriter toGf, PrintnameManager pm) {
+                super(fromGf, toGf);
+                this.printnameManager = pm;
+        }
+        
+        /** 
+         * Reads the tree child of the XML from beginning to end.
+         * Sets autocompleted to false, if the focus position is open.
+         */
+        protected void readMessage() {
+                try {
+                        String result = this.fromProc.readLine();
+                        if (nogger.isDebugEnabled()) {
+                                nogger.debug("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 = GFEditor2.unescapeTextFromGF(result);
+                                        this.printnameManager.addNewPrintnameLine(result);
+                                }
+                                
+                                result = this.fromProc.readLine();
+                                if (nogger.isDebugEnabled()) {
+                                        nogger.debug("1 " + result);
+                                }
+                        }
+                        if (nogger.isDebugEnabled()) {
+                                nogger.debug("finished loading printnames");
+                        }
+                } catch(IOException e){
+                        System.err.println(e.getMessage());
+                        e.printStackTrace();
+                }
+
+        }
+        
+        /**
+         * asks GF to print a list of all available printnames and 
+         * calls the registered PrintnameManager to register those.
+         * @param lang The module for which the grammars should be printed. 
+         * If lang is "" or null, the last read grammar module is used. 
+         */
+        public void readPrintnames(String lang) {
+                //send("gf pg -lang=FromUMLTypesOCL -printer=printnames");
+                //prints the printnames of the last loaded grammar,
+                //which can be another one than FromUMLTypesOCL
+                String sendString = "gf pg -printer=printnames";
+                if (lang != null && !("".equals(lang))) {
+                        sendString = sendString + " -lang=" + lang;
+                }
+                nogger.info("collecting printnames :" + sendString);
+                send(sendString);
+                readGfedit();
+        }
+
+
+}

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

@@ -0,0 +1,139 @@
+package de.uka.ilkd.key.ocl.gf;
+import java.util.Hashtable;
+
+import org.apache.log4j.Logger;
+
+/**
+ * @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 {
+        protected 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"
+         */
+        public void addNewPrintnameLine(String line) {
+                line = removePluses(line);
+                
+            	//remove "printname fun " (the frontMatter)
+            	int index = line.indexOf(frontMatter);
+            	line = line.substring(index + frontMatter.length()).trim();
+
+            	//extract fun name
+            	int endFun = line.indexOf(' ');
+            	String fun = line.substring(0, endFun);
+            	//extract printname
+            	String printname = line.substring(line.indexOf('"') + 1, line.lastIndexOf('"'));
+
+            	addNewPrintname(fun, printname);
+        }
+        
+        /**
+         * 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) {
+                if (logger.isDebugEnabled()) {
+                        logger.debug("addNewPrintname, myFun = '" + myFun + "' , myPrintname = '" + myPrintname + "'");
+                }
+                Printname printname = new Printname(myFun, myPrintname, this.subcatNames);
+                if (logger.isDebugEnabled()) {
+                        logger.debug("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.warn("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/JavaGUI2/de/uka/ilkd/key/ocl/gf/ReadDialog.java

@@ -0,0 +1,193 @@
+/*
+ * Created on 13.05.2005
+ *
+ * TODO To change the template for this generated file go to
+ * Window - Preferences - Java - Code Style - Code Templates
+ */
+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 org.apache.log4j.Logger;
+
+/**
+ * Takes care of reading in Strings that are to be parsed and terms.
+ * @author daniels
+ *
+ */
+class ReadDialog implements ActionListener{
+        /** XML parsing debug messages  */
+        protected static Logger xmlLogger = Logger.getLogger(GFEditor2.class.getName() + "_XML");
+        /** The window to which this class belongs */
+        protected final GFEditor2 owner;
+        /** is the main thing of this class */
+        protected 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) */
+        protected 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 ) {
+                        owner.treeChanged = true; 
+                        if (termReadButton.isSelected()) { 
+                                termInput = inputField.getText();
+                                if (termInput.indexOf(File.separatorChar)==-1){
+                                        owner.send("g "+termInput); 
+                                        if (xmlLogger.isDebugEnabled()) xmlLogger.debug("sending term  string");
+                                }
+                                else {
+                                        owner.send("tfile "+termInput);                           
+                                        if (xmlLogger.isDebugEnabled()) {
+                                                xmlLogger.debug("sending file term: "+termInput);
+                                        }
+                                }
+                        } else { //String selected
+                                parseInput = inputField.getText();
+                                if (parseInput.indexOf(File.separatorChar)==-1){
+                                        owner.send("p "+parseInput);        
+                                        if (xmlLogger.isDebugEnabled()) xmlLogger.debug("sending parse string: "+parseInput);
+                                }   
+                                else {
+                                        owner.send("pfile "+parseInput);           
+                                        if (xmlLogger.isDebugEnabled()) xmlLogger.debug("sending file parse string: "+parseInput);        
+                                }
+                        }
+                        readDialog.setVisible(false);
+                }
+
+        }
+
+}

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

@@ -0,0 +1,146 @@
+/*
+ * Created on 21.04.2005
+ *
+ */
+package de.uka.ilkd.key.ocl.gf;
+
+import java.util.HashSet;
+import java.util.HashMap;
+import org.apache.log4j.Logger;
+
+/**
+ * @author daniels
+ * This class represents a command, that is sent to GF
+ */
+class RealCommand extends GFCommand {
+        
+        private final static HashMap fullnames = new HashMap();
+
+        protected final static Logger logger = Logger.getLogger(Printname.class.getName());
+        
+        /**
+         * 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.
+         */
+        public RealCommand(final String myCommand, HashSet processedSubcats, final PrintnameManager manager, final String myShowText, boolean mlAbstract) {
+                if (fullnames.isEmpty()) {
+                        fullnames.put("w", "wrap");
+                        fullnames.put("ch", "change head");
+                        fullnames.put("rc", "refine from history:");
+                }
+                if (logger.isDebugEnabled()) {
+                        logger.debug("new RealCommand: " + myCommand);                        
+                }
+                this.command = myCommand.trim();
+                this.showText = myShowText;
+                //extract command type
+                int ind = this.command.indexOf(' ');
+                if (ind > -1) {
+                        this.commandType = this.command.substring(0, ind);
+                } else {
+                        this.commandType = this.command;
+                }
+                
+                //extract the argument position for wrapping commands and cut that part
+                if (this.commandType.equals("w")) {
+                        int beforeNumber = this.command.lastIndexOf(' ');
+                        int protoarg;
+                        try {
+                                String argumentAsString = this.command.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 = this.command.indexOf(' ');
+                        int afterPos = this.command.lastIndexOf(' ');
+                        if (beforePos > -1 && afterPos > beforePos) {
+                                this.funName = this.command.substring(beforePos + 1, afterPos);
+                        } else {
+                                this.funName = null;
+                        }
+                } else {
+                        int beforePos = this.command.indexOf(' ');
+                        if (beforePos > -1) {
+                                this.funName = this.command.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("ph")) {
+                        this.printname = Printname.printhistory;
+                } else if (this.commandType.equals("rc")) {
+                        String subtree = this.showText.substring(3);
+                        this.printname = new Printname(this.getCommand(), subtree + "$paste the previously copied subtree here<br>" + subtree);
+                } else if (mlAbstract) {
+                        //create a new Printname
+                        this.printname = new Printname(funName, myShowText, null);
+                } else {
+                        this.printname = manager.getPrintname(funName);
+                }
+                if (this.getSubcat() != null) {
+                        if (processedSubcats.contains(this.getSubcat())) {
+                                newSubcat = false;
+                        } else {
+                                newSubcat = true;
+                                processedSubcats.add(this.getSubcat());
+                        }
+                } else {
+                        newSubcat = false;
+                }
+        }
+
+        /** the text that is to be displayed in the refinement lists */
+        public String getDisplayText() {
+                String result = "";
+                if (fullnames.containsKey(this.commandType)) {
+                        result = fullnames.get(this.commandType) + " '";
+                }
+                result = result + this.printname.getDisplayText();
+                if (fullnames.containsKey(this.commandType)) {
+                        result = result + "'";
+                }
+                if (this.commandType.equals("w")) {
+                        String insertion = " as argument " + (this.argument + 1);
+                        result = result + insertion;
+                }
+                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;
+        }
+
+        public String getSubcat() {
+                return this.printname.getSubcat();
+        }
+        
+        protected final String showText;
+}

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

@@ -0,0 +1,58 @@
+/*
+ * Created on 27.04.2005
+ */
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * @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 implements AstNodeData {
+
+        protected final Printname printname;
+        protected final GfAstNode node;
+
+        /**
+         * 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
+         */
+        public RefinedAstNodeData(Printname pname, GfAstNode node) {
+                this.printname = pname;
+                this.node = node;
+        }
+        
+        /**
+         * @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;
+                }
+        }
+        
+        public boolean isMeta() {
+                return this.node.isMeta();
+        }
+        
+        public String toString() {
+                return this.node.getLine();
+        }
+
+}

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

@@ -0,0 +1,66 @@
+/*
+ * Created on 13.04.2005
+ *
+ * TODO To change the template for this generated file go to
+ * Window - Preferences - Java - Code Style - Code Templates
+ */
+package de.uka.ilkd.key.ocl.gf;
+
+import java.awt.Component;
+import org.apache.log4j.Logger;
+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 {
+        
+        protected static Logger logger = Logger.getLogger(ToolTipCellRenderer.class.getName());
+        
+        /**
+         * Returns a JLabel with a tooltip in which everything after the 
+         * first '$' character is.
+         * @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/JavaGUI2/de/uka/ilkd/key/ocl/gf/UnrefinedAstNodeData.java

@@ -0,0 +1,50 @@
+/*
+ * Created on 27.04.2005
+ *
+ */
+package de.uka.ilkd.key.ocl.gf;
+
+/**
+ * @author daniels
+ *
+ * represents an open, unrefined node in the AST.
+ * It knows, how it is called and described (tooltip).
+ */
+public class UnrefinedAstNodeData implements AstNodeData {
+        protected final GfAstNode node;
+        protected final String paramTooltip;
+        
+        /**
+         * For a child we have to know its name, its type and the tooltip
+         * @param pTooltip
+         * @param node The GfAstNode for the current AST node, for which
+         * this AstNodeData is the data for.
+         */
+        public UnrefinedAstNodeData(String pTooltip, GfAstNode node) {
+                this.node = node;
+                this.paramTooltip = pTooltip;
+        }
+        /**
+         * @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;
+        }
+        
+        public boolean isMeta() {
+                return this.node.isMeta();
+        }
+        
+        public String toString() {
+                return this.node.toString();
+        }
+
+}

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

@@ -0,0 +1,156 @@
+// 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 java.io.File;
+
+import javax.swing.ProgressMonitor;
+
+import org.apache.log4j.Logger;
+
+public class Utils {
+        protected static Logger timeLogger = Logger.getLogger("de.uka.ilkd.key.ocl.gf.utils.timer");
+        protected static Logger deleteLogger = Logger.getLogger("de.uka.ilkd.key.ocl.gf.utils.delete");
+        
+        private Utils() {
+                //non-instantiability enforced
+        }
+        
+        public static final String gf = "gf";
+        public static final String gfm = "gfm";
+        
+        /*
+         * 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.isDebugEnabled()) {
+                                timeLogger.debug(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.isDebugEnabled()) {
+                                deleteLogger.debug("scheduled for deletion: " + filename);
+                        }
+                }
+                File file = new File(grammarsDir);
+                file.deleteOnExit();
+                file = file.getParentFile();
+                file.deleteOnExit();
+        }
+        
+        /** 
+         * shamelessly copied from de.uka.ilkd.key.gui.Main
+         * With that, the editor is compilable without changes.
+         */
+        private static final String LOGGER_CONFIGURATION = 
+            	System.getProperty("user.home")+
+            	 File.separator+".key"+File.separator+"logger.props";
+
+        /** 
+         * shamelessly copied from de.uka.ilkd.key.gui.Main
+         * With that, the editor is compilable without changes.
+         * Only gets called in stand-alone mode, not when run with KeY.
+         */
+        public static void configureLogger() {
+                if ((new File(LOGGER_CONFIGURATION)).exists())
+                        org.apache.log4j.PropertyConfigurator.configureAndWatch(
+                                        LOGGER_CONFIGURATION, 1500);
+                else {
+                        org.apache.log4j.BasicConfigurator.configure();
+                        Logger.getRootLogger().setLevel(org.apache.log4j.Level.ERROR);
+                }
+        }
+
+        /**
+         * 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)) {
+                        sb.replace(i, i + toReplace.length(), replacement);
+                }
+                return sb.toString();
+        }
+}

src/Makefile

@@ -7,6 +7,7 @@ GHCFLAGS+= -fglasgow-exts -package util
 GHCOPTFLAGS=-O2
 GHCFUDFLAG=
 JAVAFLAGS=-target 1.4 -source 1.4
+GFEDITOR=JavaGUI2
 
 DIST_DIR=GF-$(PACKAGE_VERSION)
 NOT_IN_DIST= \
@@ -93,10 +94,12 @@ shell:
 clean: 
 	find . '(' -name '*~' -o -name '*.hi' -o -name '*.ghi' -o -name '*.o' ')' -exec rm -f '{}' ';'
 	-rm -f JavaGUI/*.class
+	-rm -f $(GFEDITOR)/de/uka/ilkd/key/ocl/gf/*.class
 	-rm -f gf.wixobj
 
 distclean: clean
 	-rm -f JavaGUI/gf-java.jar jgf
+	-rm -f $(GFEDITOR)/gfeditor.jar jgf
 	-rm -f tools/$(GF_DOC_EXE)
 	-rm -f config.status config.mk config.log
 	-rm -f *.tgz *.zip
@@ -111,9 +114,12 @@ today:
 
 javac:
 	$(JAVAC) $(JAVAFLAGS) JavaGUI/*.java
+	$(JAVAC) $(JAVAFLAGS) -classpath $(GFEDITOR):$(GFEDITOR)/log4j-1.2.8.jar:$(GFEDITOR)/jargs-1.0.jar $(GFEDITOR)/de/uka/ilkd/key/ocl/gf/*.java
+	
 
 jar: javac
-	cd JavaGUI; $(JAR) -cmf manifest.txt gf-java.jar *.class
+	cd JavaGUI; $(JAR) -cmf manifest.txt gf-java.jar *.class ; cd ..
+	cd $(GFEDITOR) ; rm -rf jarcontents ; mkdir jarcontents ; cp -r de/ ManifestMain.txt jarcontents ; cat jargs-1.0.jar | (cd jarcontents; jar -x jargs) ; cat log4j-1.2.8.jar | (cd jarcontents; jar -x org) ; cd jarcontents ; $(JAR) -cmf ManifestMain.txt ../gfeditor.jar  de/uka/ilkd/key/ocl/gf/*.class org jargs ; cd .. ; rm -rf jarcontents ; cd ..
 
 showflags:
 	@echo $(GHCFLAGS)
@@ -187,6 +193,7 @@ binary-dist:
 	$(MAKE) all
 	$(INSTALL) ../bin/$(GF_EXE) tools/$(GF_DOC_EXE) $(BIN_DIST_DIR)
 	$(INSTALL) -m 0644 JavaGUI/gf-java.jar $(BIN_DIST_DIR)
+	$(INSTALL) -m 0644 $(GFEDITOR)/gfeditor.jar $(BIN_DIST_DIR)
 	$(INSTALL) configure config.guess config.sub install-sh $(BIN_DIST_DIR)
 	$(INSTALL) -m 0644 config.mk.in jgf.in $(BIN_DIST_DIR)
 	$(INSTALL) -m 0644 ../README ../LICENSE $(BIN_DIST_DIR)
@@ -229,8 +236,13 @@ install-editor:
 	$(INSTALL) -d $(datadir)/GF-$(PACKAGE_VERSION)
 	$(INSTALL) jgf $(bindir)
 	$(INSTALL) -m 0644 JavaGUI/gf-java.jar $(datadir)/GF-$(PACKAGE_VERSION)
+	$(INSTALL) gfeditor $(bindir)
+	$(INSTALL) -m 0644 $(GFEDITOR)/gfeditor.jar $(datadir)/GF-$(PACKAGE_VERSION)
 
 install-java: javac
 	-rm -f ../bin/JavaGUI
 	ln -s ../src/JavaGUI ../bin
 	@echo "PLEASE edit GFHOME in bin/jgf"
+	-rm -f ../bin/$(GFEDITOR)
+	ln -s ../src/$(GFEDITOR) ../bin
+

src/Makefile.binary

@@ -8,7 +8,9 @@ install:
 	$(INSTALL) gf$(EXEEXT) gfdoc$(EXEEXT) jgf $(bindir)
 	$(INSTALL) -d $(GF_DATA_DIR)
 	$(INSTALL) -m 0644 gf-java.jar $(GF_DATA_DIR)
+	$(INSTALL) -m 0644 gfeditor.jar $(GF_DATA_DIR)
 
 uninstall:
 	-rm -f $(bindir)/gf$(EXEEXT) $(bindir)/gfdoc$(EXEEXT) $(bindir)/jgf
 	-rm -f $(GF_DATA_DIR)/gf-java.jar
+	-rm -f $(GF_DATA_DIR)/gfeditor.jar

src/configure.ac

@@ -4,9 +4,9 @@ AC_INIT([GF],[2.2],[aarne@cs.chalmers.se],[GF])
 
 AC_PREREQ(2.53)
 
-AC_REVISION($Revision: 1.23 $)
+AC_REVISION($Revision: 1.24 $)
 
-AC_CONFIG_FILES([config.mk jgf])
+AC_CONFIG_FILES([config.mk jgf gfeditor])
 
 AC_CANONICAL_HOST
 

src/gfeditor.in

@@ -0,0 +1,39 @@
+#!/bin/sh
+
+prefix=@prefix@
+exec_prefix=@exec_prefix@
+GF_BIN_DIR=@bindir@
+GF_DATA_DIR=@datadir@/GF-@PACKAGE_VERSION@
+
+JAVA="@JAVA@"
+
+GF=$GF_BIN_DIR/gf
+JARFILE=$GF_DATA_DIR/gfeditor.jar
+
+if [ ! -x "${JAVA}" ]; then
+    JAVA=`which java`
+fi
+
+if [ ! -x "${JAVA}" ]; then
+    echo "No Java VM found"
+    exit 1
+fi
+
+if [ ! -f "${JARFILE}" ]; then
+   echo "JAR file ${JARFILE} not found"
+   exit 1
+fi
+
+if [ ! -x "${GF}" ]; then
+   GF=`which gf`
+fi
+
+if [ ! -x "${GF}" ]; then
+    echo "gf not found"
+    exit 1
+fi
+
+COMMAND= ${JAVA} -jar ${JARFILE} -g $GF $*
+
+echo ${COMMAND}
+exec ${COMMAND}