diff --git a/src/GF/Shell/Commands.hs b/src/GF/Shell/Commands.hs index aac758ae7..42a4f013c 100644 --- a/src/GF/Shell/Commands.hs +++ b/src/GF/Shell/Commands.hs @@ -431,7 +431,7 @@ displaySStateJavaX env state = unlines $ tagXML "gfedit" $ concat [ zipper = stateSState state linAll = map lin lgrs gr = firstStateGrammar env - mark = markOptJava -- to be: markOptXML + mark = markOptJava --to be: markOptXML langAbstract = language "Abstract" langXML = language "XML" diff --git a/src/JavaGUI/GFEditor.java b/src/JavaGUI/GFEditor.java index 2625f2e3a..4fb7699ef 100644 --- a/src/JavaGUI/GFEditor.java +++ b/src/JavaGUI/GFEditor.java @@ -1,4 +1,4 @@ -//package javaGUI; +//package javaGUI; import java.awt.*; import java.awt.event.*; @@ -10,9 +10,15 @@ import java.io.*; import java.util.*; //import gfWindow.GrammarFilter; -public class GFEditor extends JFrame implements ActionListener, KeyListener { +public class GFEditor extends JFrame implements ActionListener, CaretListener, + KeyListener { public static boolean debug = false; + public static String focusPosition=""; + public static int selStart = -1; + public static int selEnd = -1; + public static String restString = ""; + public static boolean newObject = false; public static boolean finished = false; private String parseInput = ""; @@ -25,6 +31,7 @@ public class GFEditor extends JFrame implements ActionListener, KeyListener { private static String treeString = ""; private static String fileString = ""; public static Vector commands = new Vector(); + public static Vector outputVector = new Vector(); public static Hashtable nodeTable = new Hashtable(); JFileChooser fc1 = new JFileChooser("./"); JFileChooser fc = new JFileChooser("./"); @@ -41,8 +48,6 @@ public class GFEditor extends JFrame implements ActionListener, KeyListener { private static boolean waiting = false; public static boolean treeChanged = true; private static String result; - private static int selectionStart; - private static int selectionEnd; private static BufferedReader fromProc; private static BufferedWriter toProc; private static String commandPath = new String("GF"); @@ -229,6 +234,7 @@ public class GFEditor extends JFrame implements ActionListener, KeyListener { cp = getContentPane(); cp.setLayout(new BorderLayout()); output.setToolTipText("Linearizations' display area"); + output.addCaretListener(this); output.setEditable(false); output.setLineWrap(true); output.setWrapStyleWord(true); @@ -433,7 +439,7 @@ public class GFEditor extends JFrame implements ActionListener, KeyListener { result = fromProc.readLine(); if (debug) System.out.println("1 "+result); } - output.append(outputString); + appendMarked(outputString, -1,-1); while ((result.indexOf("newcat")==-1)&&(result.indexOf("1) - output.append("-------------"+'\n'+s); + appendMarked("-------------"+'\n'+s,-1,-1); result = fromProc.readLine(); if (debug) System.out.println("7 "+result); } catch(IOException e){ } @@ -712,65 +719,60 @@ public class GFEditor extends JFrame implements ActionListener, KeyListener { } public void outputAppend(){ - int i, j, k, l, l2, m; - i=result.indexOf("type="); - j=result.indexOf('>',i); + int i, j, k, l, l2, m=0, n=0; l = result.indexOf("',i); l2 = result.indexOf("focus"); if (l2!=-1){ // in case focus tag is cut into two lines: if (l==-1) l=l2-7; - + m=result.indexOf("position",l); + System.out.println("POSITION START: "+m); + n=result.indexOf("]",m); + System.out.println("POSITION END: "+n); + focusPosition = result.substring(m+9,n); if (debug) System.out.println("form Lin1: "+result); statusLabel.setText(" "+result.substring(i+5,j)); //cutting - result= result.substring(0,l)+result.substring(j+1); - i=result.indexOf("/f",l); -System.out.println("/ is at the position"+i); + result= result.substring(0,l)+result.substring(j+2); + i=result.indexOf("/focus",l); + if (debug) System.out.println("/ is at the position"+i); j=result.indexOf('>',i); - k=result.length()-j; + k=result.length()-j-1; if (debug) System.out.println("form Lin2: "+result); - m = output.getText().length(); - //cutting - // in case focus tag is cut into two lines: if (debug) System.out.println("char at the previous position"+result.charAt(i-1)); + //cutting + // in case focus tag is cut into two lines: if (result.charAt(i-1)!='<') - result= result.substring(0,i-8)+result.substring(j+1); + result= result.substring(0,i-8)+result.substring(j+2); else - result= result.substring(0,i-1)+result.substring(j+1); + result= result.substring(0,i-1)+result.substring(j+2); j= result.indexOf("0) System.out.println(output.getText().charAt(end)); + if (start=((MarkedArea)outputVector.elementAt(j)).begin) + System.out.println("SELECTEDTEXT: "+ + ((MarkedArea)outputVector.elementAt(j)).position+"\n"); + } else + System.out.println("no position in vector of size: "+outputVector.size()); + } + } + + 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; + restString = s; + if (selectionStart>-1) + { + selStart = selectionStart; + selEnd = selectionEnd; + selectionCheck = (s.substring(selectionStart, selectionEnd).indexOf("<")==-1); + l = restString.indexOf("-1)||(l>-1)) + { + if ((l-1)) + { + j = restString.indexOf(">",l); + n = restString.indexOf("<",j); + // the tag has some words to register: + if ((n-j)>3) + { + //getting position: + position = String.valueOf(outputVector.size()); + newLength = n-j-3+l; + //focus has a separate position: + if (selectionCheck&&(selEnd tags: + removeSubTreeTag(l2,l2+10); + l2 = restString.indexOf("-1 + // appending: + 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) ); + } catch (Exception e) {System.out.println("highlighting problem!");} + } + + //updating: + public static void removeSubTreeTag (int start, int end) + { + int difference =end-start+1; + restString = restString.substring(0,start)+restString.substring(end+1); + if (selStart > end) + { selStart -=difference; + selEnd -=difference; + } + else + if (selEnd < start) ; + else selEnd -=difference; + } public void listAction(int index) { if (index == -1)