From f3d774c5f7fd8039f84365d875c0cedb02cbac18 Mon Sep 17 00:00:00 2001 From: hdaniels Date: Fri, 1 Jul 2005 14:29:38 +0000 Subject: [PATCH] Navigating in the tree now works (using absolute positions), what it not always did before. --- .../de/uka/ilkd/key/ocl/gf/AstNodeData.java | 16 +++++- .../de/uka/ilkd/key/ocl/gf/DynamicTree2.java | 18 +++--- .../de/uka/ilkd/key/ocl/gf/GFEditor2.java | 57 ++++++++++++++----- .../de/uka/ilkd/key/ocl/gf/LinPosition.java | 17 +++++- .../ilkd/key/ocl/gf/RefinedAstNodeData.java | 17 +++++- .../ilkd/key/ocl/gf/UnrefinedAstNodeData.java | 17 +++++- .../de/uka/ilkd/key/ocl/gf/Utils.java | 24 ++++++++ 7 files changed, 135 insertions(+), 31 deletions(-) diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AstNodeData.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AstNodeData.java index 329568654..df86fa936 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AstNodeData.java +++ b/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(); } diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/DynamicTree2.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/DynamicTree2.java index 890943262..59616034a 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/DynamicTree2.java +++ b/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. - * In the displayed tree, we can click everywhere. - * We navigate through the GF tree by giving the direction - * and the number of steps + * gfeditor.nodeTable contains the positions for all selectionPathes. */ 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(); - int j = oldSelection; + String pos = (String)gfeditor.nodeTable.get(tree.getSelectionPath()); + if (pos == null || "".equals(pos)) { + //default to sth. sensible + pos = "[]"; + } gfeditor.treeChanged = true; - if (i > j) - gfeditor.send("> " + String.valueOf(i - j)); - else - gfeditor.send("< " + String.valueOf(j - i)); + gfeditor.send("mp " + pos); } } }); diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java index b1b861b18..0e781ddaa 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java +++ b/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. - * When reading a from GF, we assign each tree node in the Java AST - * the position in the 'flattened' GF tree. - * The mapping between Java tree pathes and GF node numbering is stored - * here. + * The mapping between Java tree pathes and GF AST positions + * 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 diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinPosition.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinPosition.java index 46cf32558..0c2c51309 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinPosition.java +++ b/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 + "]"; + } } /** diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinedAstNodeData.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinedAstNodeData.java index 14663e085..a1bff105b 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinedAstNodeData.java +++ b/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(); } diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/UnrefinedAstNodeData.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/UnrefinedAstNodeData.java index 288b1fd2e..2f2819290 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/UnrefinedAstNodeData.java +++ b/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(); diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java index fc93852a2..0f7a9f724 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java +++ b/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; + } }