diff options
Diffstat (limited to 'src/JavaGUI2/de/uka')
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; + } } |