Navigating in the tree now works (using absolute positions), what it not always did before.

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

@@ -15,13 +15,16 @@
 
 package de.uka.ilkd.key.ocl.gf;
 
+import java.util.logging.*;
+
 /**
  * @author hdaniels
  * An object of this type knows how it self should be rendered,
  * via Printname how its children should be rendered.
  * This means the tooltip information it got from there.
  */
-interface AstNodeData {
+abstract class AstNodeData {
+        protected static Logger logger = Logger.getLogger(DynamicTree2.class.getName());
         /**
          * @return the printname associated with this object
          */
@@ -38,4 +41,15 @@ interface AstNodeData {
          * @return true iff this node represents an open leaf
          */
         public abstract boolean isMeta();
+        /**
+         * keeps track of the number of children of this node.
+         * It has to be increased whenever a new child of this node is
+         * added.
+         */
+        public int childNum = 0;
+        /**
+         * @return The position String in the GF AST for this node
+         * in Haskell notation.
+         */
+        public abstract String getPosition();
 }

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

@@ -67,11 +67,9 @@ ActionListener{
                 
                 tree.addTreeSelectionListener(new TreeSelectionListener() {
                         /**
+                         * Moves to the position of the selected node in GF.
                          * the following is assumed:
-                         * in GF we can only switch to the last or the next editing position.
+                         * gfeditor.nodeTable contains the positions for all selectionPathes.
-                         * 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) {
@@ -93,13 +91,13 @@ ActionListener{
                                                         GFEditor2.treeLogger.finer("selected path" + tree.getSelectionPath());
                                                 }
                                         }
-                                        int i = ((Integer) gfeditor.nodeTable.get(tree.getSelectionPath())).intValue();
+                                        String pos = (String)gfeditor.nodeTable.get(tree.getSelectionPath());
-                                        int j = oldSelection;
+                                        if (pos == null || "".equals(pos)) {
+                                                //default to sth. sensible
+                                                pos = "[]";
+                                        }
                                         gfeditor.treeChanged = true;
-                                        if (i > j)
+                                        gfeditor.send("mp " + pos);
-                                                gfeditor.send("> " + String.valueOf(i - j));
-                                        else
-                                                gfeditor.send("< " + String.valueOf(j - i));
                                 }
                         }
                 });

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

@@ -141,11 +141,8 @@ public class GFEditor2 extends JFrame {
          */
         private String fileString = "";
         /**
-         * In GF the nodes in the AST are numbered in a linear fashion.
+         * The mapping between Java tree pathes and GF AST positions 
-         * When reading a from GF, we assign each tree node in the Java AST
+         * is stored here.
-         * the position in the 'flattened' GF tree.
-         * The mapping between Java tree pathes and GF node numbering is stored 
-         * here.
          */
         public Hashtable nodeTable = new Hashtable();
         /**this FileChooser gets enriched with the Term/Text option */
@@ -400,7 +397,13 @@ public class GFEditor2 extends JFrame {
          * 1 for text, 2 for HTML, 3 for both 
          */
         private int displayType = 1;
+        /**
+         * rbText, rbHtml and rbTextHtml are grouped here.
+         */
         private ButtonGroup bgDisplayType = new ButtonGroup();
+        /**
+         * The button that switches the linearization view to text only
+         */
         private JRadioButtonMenuItem rbText = new JRadioButtonMenuItem(new AbstractAction("pure text") {
                 public void actionPerformed(ActionEvent ae) {
                         int oldDisplayType = displayType;
@@ -414,6 +417,9 @@ public class GFEditor2 extends JFrame {
                         outputPanelUp.validate();
                 }
         });
+        /**
+         * The button that switches the linearization view to HTML only
+         */
         private JRadioButtonMenuItem rbHtml = new JRadioButtonMenuItem(new AbstractAction("HTML") {
                 public void actionPerformed(ActionEvent ae) {
                         int oldDisplayType = displayType;
@@ -427,6 +433,10 @@ public class GFEditor2 extends JFrame {
                         outputPanelUp.validate();
                 }
         });
+        /**
+         * The button that switches the linearization view to both text and 
+         * HTML separated with a JSplitpane
+         */
         private JRadioButtonMenuItem rbTextHtml = new JRadioButtonMenuItem(new AbstractAction("text and HTML") {
                 public void actionPerformed(ActionEvent ae) {
                         int oldDisplayType = displayType;
@@ -442,7 +452,16 @@ public class GFEditor2 extends JFrame {
                         outputPanelUp.validate();
                 }
         });
-        
+        /**
+         * Since the user will be able to send chain commands to GF,
+         * the editor has to keep track of them, sinve GF does not undo
+         * all parts with one undo, instead 'u n' with n as the number of
+         * individual commands, has to be sent.
+         * This array keeps track of the last 21 such chain commands.
+         * Farther back does the memory of the user probably not reach,
+         * after that only 'u 1' is offered.
+         */
+        final private int[] undoRecord = new int[21];
         
         /**
          * Initializes GF with the given command, sets up the GUI
@@ -1455,7 +1474,7 @@ public class GFEditor2 extends JFrame {
                 this.setSize(800,600);
                 outputPanelUp.setPreferredSize(new Dimension(400,230));
                 treePanel.setDividerLocation(0.3);
-                nodeTable.put(new TreePath(tree.rootNode.getPath()), new Integer(0));
+                nodeTable.put(new TreePath(tree.rootNode.getPath()), "");
                 
                 JRadioButton termButton = new JRadioButton("Term");
                 termButton.setActionCommand("term");
@@ -1505,7 +1524,7 @@ public class GFEditor2 extends JFrame {
                         toProc.write(text, 0, text.length());
                         toProc.newLine();
                         toProc.flush();
-                        //run();
+
                         if (andRead) {
                                 readAndDisplay();
                         }
@@ -2766,8 +2785,18 @@ public class GFEditor2 extends JFrame {
                                  * for the next child (the parent knows how many it has already)
                                  * and save it in an AstNodeData
                                  */
-                                
                                 DefaultMutableTreeNode parent = (DefaultMutableTreeNode)parentNodes.get(new Integer(shift));
+                                
+                                // compute the now childs position
+                                String newPos;
+                                if ((parent != null) && (parent.getUserObject() instanceof AstNodeData) && parent.getUserObject() != null) {
+                                        AstNodeData pand = (AstNodeData)parent.getUserObject();
+                                        newPos = LinPosition.calculateChildPosition(pand.getPosition(), pand.childNum++);
+                                } else {
+                                        //only the case for the root node
+                                        newPos = "[]";
+                                }
+                                
                                 //default case, if we can get more information, this is overwritten
                                 AstNodeData and;
                                 Printname childPrintname = null;
@@ -2777,7 +2806,7 @@ public class GFEditor2 extends JFrame {
                                 Printname parentPrintname = null;
                                 if (childPrintname != null) {
                                         //we know this one
-                                        and = new RefinedAstNodeData(childPrintname, node);
+                                        and = new RefinedAstNodeData(childPrintname, node, newPos);
                                 } else if (parent != null && node.isMeta()) {
                                         //new child without refinement
                                         AstNodeData parentAnd = (AstNodeData)parent.getUserObject();
@@ -2795,21 +2824,21 @@ public class GFEditor2 extends JFrame {
 //                                                if (logger.isLoggable(Level.FINER)) {
 //                                                        logger.finer("new node-parsing: '" + name + "', fun: '" + fun + "', type: '" + paramType + "'");
 //                                                }
-                                                and = new UnrefinedAstNodeData(paramTooltip, node);
+                                                and = new UnrefinedAstNodeData(paramTooltip, node, newPos);
 
                                         } else {
-                                                and = new RefinedAstNodeData(null, node);
+                                                and = new RefinedAstNodeData(null, node, newPos);
                                         }
                                 } else {
                                         //something unparsable, bad luck
                                         //or refined and not described
-                                        and = new RefinedAstNodeData(null, node);
+                                        and = new RefinedAstNodeData(null, node, newPos);
                                 }
                                 
                                 newChildNode = myTreePanel.addObject(parent, and);  
                                 parentNodes.put(new Integer(shift+1), newChildNode);
                                 path = new TreePath(newChildNode.getPath());
-                                nodeTable.put(path, new Integer(index));
+                                nodeTable.put(path, newPos);
 
                                 if (selected) {                        
                                         //show the selected as the 'selected' one in the JTree

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

@@ -49,7 +49,22 @@ class LinPosition {
          * @return the position string for the nrth child
          */
         public String childPosition(int nr) {
-                return this.position.substring(0, this.position.length() - 1) + "," + nr + "]";
+                return calculateChildPosition(this.position, nr);
+        }
+        
+        /**
+         * Creates a position string in Haskell notation for the argument 
+         * number nr for the position pos
+         * @param pos The position of the to be parent
+         * @param nr The number of the wanted argument
+         * @return the position string for the nrth child of pos
+         */
+        protected static String calculateChildPosition(String pos, int nr) {
+                if ("[]".equals(pos)) {
+                        return "[" + nr + "]";
+                } else {
+                        return pos.substring(0, pos.length() - 1) + "," + nr + "]";
+                }
         }
 
         /**

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

@@ -14,7 +14,7 @@
 //distribution or in the .jar file of this application
 
 package de.uka.ilkd.key.ocl.gf;
-
+import java.util.logging.*;
 /**
  * @author daniels
  * An object of this class represents a line in the GF abstract syntax tree
@@ -23,10 +23,11 @@ package de.uka.ilkd.key.ocl.gf;
  * RefinedAstNodeData has its tooltip from the function it represents, not
  * from its parent node.
  */
-class RefinedAstNodeData implements AstNodeData {
+class RefinedAstNodeData extends AstNodeData {
 
         protected final Printname printname;
         protected final GfAstNode node;
+        protected final String position;
 
         /**
          * all we have to know about an already refined node is its Printname
@@ -34,10 +35,15 @@ class RefinedAstNodeData implements AstNodeData {
          * @param pname the suiting Printname, may be null if the line could 
          * not be parsed
          * @param node the GfAstNode for the current line
+         * @param pos The position in the GF AST of this node in Haskell notation
          */
-        public RefinedAstNodeData(Printname pname, GfAstNode node) {
+        public RefinedAstNodeData(Printname pname, GfAstNode node, String pos) {
                 this.printname = pname;
                 this.node = node;
+                this.position = pos;
+                if (logger.isLoggable(Level.FINEST)) {
+                        logger.finest(this.toString() + " - " + getPosition());
+                }
         }
         
         /**
@@ -63,6 +69,11 @@ class RefinedAstNodeData implements AstNodeData {
                 return this.node.isMeta();
         }
         
+        public String getPosition() {
+                return this.position;
+        }
+
+        
         public String toString() {
                 return this.node.getLine();
         }

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

@@ -15,25 +15,33 @@
 
 package de.uka.ilkd.key.ocl.gf;
 
+import java.util.logging.*;
+
 /**
  * @author daniels
  *
  * represents an open, unrefined node in the AST.
  * It knows, how it is called and described (tooltip).
  */
-public class UnrefinedAstNodeData implements AstNodeData {
+public class UnrefinedAstNodeData extends AstNodeData {
         protected final GfAstNode node;
         protected final String paramTooltip;
+        protected final String position;
         
         /**
          * 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.
+         * @param pos The position in the GF AST of this node in Haskell notation
          */
-        public UnrefinedAstNodeData(String pTooltip, GfAstNode node) {
+        public UnrefinedAstNodeData(String pTooltip, GfAstNode node, String pos) {
                 this.node = node;
                 this.paramTooltip = pTooltip;
+                this.position = pos;
+                if (logger.isLoggable(Level.FINEST)) {
+                        logger.finest(this.toString() + " - " + getPosition());
+                }
         }
         /**
          * @return no refinement, no printname, thus null
@@ -53,6 +61,11 @@ public class UnrefinedAstNodeData implements AstNodeData {
         public boolean isMeta() {
                 return this.node.isMeta();
         }
+
+        public String getPosition() {
+                return this.position;
+        }
+        
         
         public String toString() {
                 return this.node.toString();

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

@@ -24,6 +24,7 @@ import javax.swing.ProgressMonitor;
 public class Utils {
         protected static Logger timeLogger = Logger.getLogger(Utils.class.getName() + ".timer");
         protected static Logger deleteLogger = Logger.getLogger(Utils.class.getName() + ".delete");
+        protected static Logger stringLogger = Logger.getLogger(Utils.class.getName() + ".string");
         
         private Utils() {
                 //non-instantiability enforced
@@ -135,4 +136,27 @@ public class Utils {
                 }
                 return sb.toString();
         }
+        
+        /**
+         * Removes all parts, that are inside "quotation marks" from s.
+         * Assumes no nesting of those, like in Java.
+         * " escaped with \ like \" do not count as quotation marks
+         * @param s The String, that possibly contains quotations
+         * @return a String described above, s without quotations.
+         */
+        public static String removeQuotations(String s) {
+                if (s.indexOf('"') == -1) {
+                        return s;
+                }
+                for (int begin = indexOfNotEscaped(s, "\""); begin > -1 ;  begin = indexOfNotEscaped(s, "\"", begin)) {//yes, I want an unescaped '"'!
+                        int end = indexOfNotEscaped(s, "\"", begin + 1);
+                        if (end > -1) {
+                                s = s.substring(0, begin) + s.substring(end + 1);
+                        } else {
+                                stringLogger.info("Strange String given: '" + s + "'");
+                                s = s.substring(0, begin);
+                        }
+                }
+                return s;
+        }
 }