GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-09 04:59:31 -06:00
Code Issues Packages Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
hdaniels
2005-07-01 14:29:38 +00:00
parent 8f785c8ed4
commit f3d774c5f7
7 changed files with 135 additions and 31 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -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();
}

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

@@ -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);
}
}
});

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

@@ -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

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

@@ -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 + "]";
}
}
/**

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

@@ -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();
}

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

@@ -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();

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

@@ -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;
}
}