diff --git a/src/GF/Shell/Commands.hs b/src/GF/Shell/Commands.hs index 4fb3048ee..b5bd28e3c 100644 --- a/src/GF/Shell/Commands.hs +++ b/src/GF/Shell/Commands.hs @@ -432,7 +432,7 @@ displaySStateJavaX isNew env state = unlines $ tagXML "gfedit" $ concat [ zipper = stateSState state linAll = map lin lgrs gr = firstStateGrammar env - mark = if isNew then markOptXML else markOptJava + mark = markOptXML -- markOptJava langAbstract = language "Abstract" langXML = language "XML" diff --git a/src/JavaGUI/DynamicTree2.java b/src/JavaGUI/DynamicTree2.java new file mode 100644 index 000000000..9abd9671d --- /dev/null +++ b/src/JavaGUI/DynamicTree2.java @@ -0,0 +1,272 @@ + +/* + * 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 java.util.Vector; +import java.awt.event.*; + +public class DynamicTree2 extends JPanel implements KeyListener, + ActionListener{ + public static DefaultMutableTreeNode rootNode; + protected DefaultTreeModel treeModel; + public JTree tree; + public int oldSelection = 0; + private Toolkit toolkit = Toolkit.getDefaultToolkit(); + JPopupMenu popup = new JPopupMenu(); + JMenuItem menuItem; + Timer timer = new Timer(500, this); + MouseEvent m; + + public DynamicTree2() { + timer.setRepeats(false); + 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() { + public void valueChanged(TreeSelectionEvent e) { + if (tree.getSelectionRows()!=null) { + if (GFEditor2.nodeTable == null) + {if (GFEditor2.debug) System.out.println("null node table");} + else + {if (GFEditor2.debug) System.out.println("node table: "+ + GFEditor2.nodeTable.contains(new Integer(0)) +" "+ + GFEditor2.nodeTable.keys().nextElement()); } + if (tree.getSelectionPath() == null) + {if (GFEditor2.debug) System.out.println("null root path"); } + else + {if (GFEditor2.debug) System.out.println("selected path"+ + tree.getSelectionPath());} + int i = ((Integer)GFEditor2.nodeTable.get( + tree.getSelectionPath())).intValue(); + int j = oldSelection; + GFEditor2.treeChanged = true; + if (i>j) GFEditor2.send("> "+String.valueOf(i-j)); + else GFEditor2.send("< "+String.valueOf(j-i)); + } + } + }); + + tree.setCellRenderer(new MyRenderer()); + tree.setShowsRootHandles(true); + 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 currently selected node. */ + 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); + } + + public DefaultMutableTreeNode addObject(DefaultMutableTreeNode parent, + Object child) { + return addObject(parent, child, false); + } + + public DefaultMutableTreeNode addObject(DefaultMutableTreeNode parent, + Object child, + boolean shouldBeVisible) { + 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) {} + + if (GFEditor2.debug) System.out.println + ("The user has finished editing the node."); + if (GFEditor2.debug) System.out.println( + "New value: " + node.getUserObject()); + } + public void treeNodesInserted(TreeModelEvent e) { + } + public void treeNodesRemoved(TreeModelEvent e) { + } + public void treeStructureChanged(TreeModelEvent e) { + } + } + + private class MyRenderer extends DefaultTreeCellRenderer { + ImageIcon tutorialIcon; + + public MyRenderer() { + tutorialIcon = new ImageIcon("images/middle.gif"); + } + + 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 (leaf && isTutorialBook(value)) + setIcon(tutorialIcon); + + return this; + } + protected boolean isTutorialBook(Object value) { + DefaultMutableTreeNode node = + (DefaultMutableTreeNode)value; + String nodeInfo = + (String)(node.getUserObject()); + + if (nodeInfo.indexOf("?") >= 0) { + return true; + } + + 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.debug) System.out.println("selection changed!"); + maybeShowPopup(e); + } + + public void mouseReleased(MouseEvent e) { + if (GFEditor2.debug) System.out.println("mouse released!"); + maybeShowPopup(e); + } + } + void maybeShowPopup(MouseEvent e) { + if (GFEditor2.debug) System.out.println("may be!"); + if (e.isPopupTrigger()) { + m=e; + timer.start(); + } + } + void addMenuItem(String name){ + menuItem = new JMenuItem(name); + menuItem.addActionListener(this); + popup.add(menuItem); + + } + + public void actionPerformed(ActionEvent ae) + { + if (ae.getSource()==timer){ + if (GFEditor2.debug) System.out.println("changing menu!"); + popup.removeAll(); + for (int i = 0; i',i); @@ -731,15 +743,15 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener, if (debug) System.out.println("'POSITION START: "+m); n=result.indexOf("]",m); if (debug) System.out.println("POSITION END: "+n); -// if (debug) + if (debug) System.out.println("form Lin1: "+result); - focusPosition = result.substring(m+9,n); + focusPosition = result.substring(m+9,n+1); statusLabel.setText(" "+result.substring(i+5,j)); //cutting result= result.substring(0,l)+result.substring(j+2); i=result.indexOf("/focus",l); selectionLength = i-l-1; -// if (debug) + if (debug2) System.out.println("selection length: "+selectionLength); j=result.indexOf('>',i); k=result.length()-j-1; @@ -761,13 +773,16 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener, // appending the resulting string // only one focus if (j==-1){ - System.out.println("ONE FOCUS"); - appendMarked(result+'\n',l,result.length()-k); + if (debug2) + System.out.println("ONE FOCUS"); + // last space is not included!: + appendMarked(result+'\n',l,l+selectionLength-2); } //several focuses else { - System.out.println("MANY FOCUSes"); - appendMarked(result.substring(0,j),l,l+selectionLength-1); + if (debug2) + System.out.println("MANY FOCUSes"); + appendMarked(result.substring(0,j),l,l+selectionLength-2); result = result.substring(j); outputAppend(); } @@ -1239,13 +1254,13 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener, "Document is empty!","Error", JOptionPane.ERROR_MESSAGE); } } - public static void populateTree(DynamicTree treePanel) { + public static void populateTree(DynamicTree2 treePanel) { String p1Name = new String("Root"); DefaultMutableTreeNode p1; p1 = treePanel.addObject(null, p1Name); } - public static void formTree(DynamicTree treePanel) { + public static void formTree(DynamicTree2 treePanel) { Hashtable table = new Hashtable(); TreePath path=null; boolean treeStarted = false, selected = false; @@ -1412,189 +1427,206 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener, /** Handle the key released event. */ public void keyReleased(KeyEvent e) { } + public String comparePositions(String first, String second) + { + String common ="[]"; + int i = 1; + while ((i0&&(end0&&(end=0)&&(((MarkedArea)outputVector.elementAt(i)).begin > start)) + i--; + + if ((j=jElement.begin) - { - position = jElement.position+"]"; - System.out.println("SELECTEDTEXT: "+position+"\n"); - treeChanged = true; - send("mp "+position); - } - } else - System.out.println("no position in vector of size: "+outputVector.size()); - } + jElement = (MarkedArea)outputVector.elementAt(j); + jPosition = jElement.position; + // less & before: + if (i==-1) + { // less: + if (end>=jElement.begin) + { + iElement = (MarkedArea)outputVector.elementAt(0); + iPosition = iElement.position; + if (debug2) + System.out.println("Less: "+jPosition+" and "+iPosition); + position = findMax(0,j); + if (debug2) + System.out.println("SELECTEDTEXT: "+position+"\n"); + treeChanged = true; + send("mp "+position); + } + // before: + else + if (debug2) + System.out.println("BEFORE vector of size: "+outputVector.size()); + } + // just: + else + { + iElement = (MarkedArea)outputVector.elementAt(i); + iPosition = iElement.position; + if (debug2) + System.out.println("SELECTEDTEXT: "+iPosition +" and "+jPosition+"\n"); + position = findMax(i,j); + if (debug2) + System.out.println("SELECTEDTEXT: "+position+"\n"); + treeChanged = true; + send("mp "+position); + } + } + else + // more && after: + if (i>=0) + { + iElement = (MarkedArea)outputVector.elementAt(i); + iPosition = iElement.position; + // more + if (start<=iElement.end) + { + jElement = (MarkedArea)outputVector.elementAt(outputVector.size()-1); + jPosition = jElement.position; + if (debug2) + System.out.println("MORE: "+iPosition+ " and "+jPosition); + position = findMax(i,outputVector.size()-1); + if (debug2) + System.out.println("SELECTEDTEXT: "+position+"\n"); + treeChanged = true; + send("mp "+position); + } + else + // after: + if (debug2) + System.out.println("AFTER vector of size: "+outputVector.size()); + } + else + // bigger: + { + iElement = (MarkedArea)outputVector.elementAt(0); + iPosition = iElement.position; + jElement = (MarkedArea)outputVector.elementAt(outputVector.size()-1); + jPosition = jElement.position; + if (debug2) + System.out.println("BIGGER: "+iPosition +" and "+jPosition+"\n"); + if (debug2) + System.out.println("SELECTEDTEXT: []\n"); + treeChanged = true; + send("mp []"); + } + }//not null selection } public static void appendMarked(String s, int selectionStart, int selectionEnd) { - System.out.println("STRING: "+s); - int oldLength = output.getText().length(); - int currentLength = 0; - int newLength=0; - int addedLength=0; - int resultCurrent=0; - int resultNew=0; - boolean selectionCheck ; - String position = ""; - int j, l, l2, n, m2, m1, pos, selStartTotal, selEndTotal; + if (debug2) + System.out.println("STRING: "+s); + currentLength = 0; + newLength=0; + oldLength = output.getText().length(); + int j, l, l2, n, pos, selStartTotal, selEndTotal, selEndT; restString = s; + int m2, m1; + String position = ""; if (selectionStart>-1) { selStart = selectionStart; selEnd = selectionEnd; - System.out.println("SELECTION: " + selStart + " "+selEnd+ "TOTAL: "+s.length()); + if (debug2) + System.out.println("SELECTION: " + selStart + " "+selEnd+ "TOTAL: "+s.length()); selectionCheck = (s.substring(selStart, selEnd).indexOf("<")==-1); l = restString.indexOf("-1)||(l>-1)) { - if ((l-1)) + if ((l2==-1)||((l-1))) { - m2 = restString.indexOf("]",l); - m1 = restString.indexOf("[",l); j = restString.indexOf(">",l); n = restString.indexOf("<",j); - // the tag has some words to register: - if ((n-j)>3) + m1 = restString.indexOf("[",l); + m2 = restString.indexOf("]",l); + //getting position: + position = restString.substring(m1,m2+1); + if (debug2) + System.out.println("<-POSITION: "+l+" CURRLENGTH: "+currentLength); + // something before the tag: + if (l-currentLength>1) { - //getting position: - - position = restString.substring(m1,m2); - - - newLength = n-j-3+l; - //focus has a separate position: - if (selectionCheck&&(selEnd tags: removeSubTreeTag(l2,l2+10); - l2 = restString.indexOf("0) { selStartTotal = selStart+oldLength; selEndTotal = selEnd+oldLength; + selEndT = selEndTotal+1; pos = ((MarkedArea)outputVector.elementAt(outputVector.size()-1)).end; - System.out.print("the last registered position: "+ pos); - System.out.println(" selStart: "+ selStartTotal+ " selEnd: "+selEndTotal); + if (debug2) + System.out.print("the last registered position: "+ pos); + if (debug2) + System.out.println(" selStart: "+ selStartTotal+ " selEnd: "+selEndTotal); if (selEnd+oldLength>pos) { - addedLength = selEnd-selStart+1; - outputVector.add(new MarkedArea(selStart+oldLength, selEnd+oldLength, focusPosition)); - System.out.println("APPENDNG Selection Last:"+restString.substring(selStart,selEnd+1)+ - "Length: "+addedLength+" POSITION: "+selStartTotal + " "+selEndTotal); + addedLength = selEnd-selStart+2; + outputVector.add(new MarkedArea(selStartTotal, selEndTotal+1, focusPosition)); + if (debug2) + System.out.println("APPENDNG Selection Last:"+restString.substring(selStart)+ + "Length: "+addedLength+" POSITION: "+selStartTotal + " "+selEndT); } } } //if selectionStart>-1 @@ -1602,15 +1634,114 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener, output.append(restString); if (selectionStart>-1) try { - output.getHighlighter().addHighlight(selStart+oldLength, selEnd+oldLength, new DefaultHighlighter.DefaultHighlightPainter(Color.green) ); -// output.getHighlighter().addHighlight(selStart+oldLength, selEnd+oldLength, new DefaultHighlighter.DefaultHighlightPainter(Color.white) ); + output.getHighlighter().addHighlight(selStart+oldLength, selEnd+oldLength+1, new DefaultHighlighter.DefaultHighlightPainter(Color.green) ); +// output.getHighlighter().addHighlight(selStart+oldLength, selEnd+oldLength+1, new DefaultHighlighter.DefaultHighlightPainter(Color.white) ); } catch (Exception e) {System.out.println("highlighting problem!");} } + + + public static void register(int start, int end, String position) + { + oldLength = output.getText().length(); + addedLength = 0; + int resultCurrent = 0; + int resultNew = 0; + newLength = end-start; + // the tag has some words to register: + if (newLength>0) + { + //focus has a separate position: + if (selectionCheck&&(selEnd0) + { + outputVector.add(new MarkedArea(resultCurrent, resultNew, position)); + if (debug2) + System.out.println("APPENDING ZONE:"+stringToAppend+ + "Length: "+newLength+" POSITION: "+resultCurrent + " "+resultNew); + } + else + if (debug2) + System.out.println("whiteSpaces: "+newLength); + } + } //some words to register + } + //updating: public static void removeSubTreeTag (int start, int end) { + if (debug2) + System.out.println("removing: "+ start +" to "+ end); int difference =end-start+1; + int positionStart, positionEnd; + if ((newLength==0)&&(difference>20)) + { + positionStart = restString.indexOf("[", start); + positionEnd = restString.indexOf("]", start); + currentPosition = restString.substring(positionStart, positionEnd+1); + } restString = restString.substring(0,start)+restString.substring(end+1); if (selStart > end) { selStart -=difference; diff --git a/src/Makefile b/src/Makefile index a2e1ee8dd..5f739e040 100644 --- a/src/Makefile +++ b/src/Makefile @@ -28,4 +28,4 @@ hugs: today: runhugs util/MkToday javac: - cd java ; javac GFEditor.java ; cd .. + cd java ; javac *.java ; cd ..