diff --git a/src/JavaGUI/GFEditor.java b/src/JavaGUI/GFEditor.java index 4fb7699ef..0ebf91e7e 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,15 +10,9 @@ import java.io.*; import java.util.*; //import gfWindow.GrammarFilter; -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 class GFEditor extends JFrame implements ActionListener, KeyListener { + public static boolean debug = true; public static boolean newObject = false; public static boolean finished = false; private String parseInput = ""; @@ -31,7 +25,6 @@ public class GFEditor extends JFrame implements ActionListener, CaretListener, 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("./"); @@ -48,6 +41,8 @@ public class GFEditor extends JFrame implements ActionListener, CaretListener, 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"); @@ -234,7 +229,6 @@ public class GFEditor extends JFrame implements ActionListener, CaretListener, cp = getContentPane(); cp.setLayout(new BorderLayout()); output.setToolTipText("Linearizations' display area"); - output.addCaretListener(this); output.setEditable(false); output.setLineWrap(true); output.setWrapStyleWord(true); @@ -439,7 +433,7 @@ public class GFEditor extends JFrame implements ActionListener, CaretListener, result = fromProc.readLine(); if (debug) System.out.println("1 "+result); } - appendMarked(outputString, -1,-1); + output.append(outputString); while ((result.indexOf("newcat")==-1)&&(result.indexOf("1) - appendMarked("-------------"+'\n'+s,-1,-1); + output.append("-------------"+'\n'+s); result = fromProc.readLine(); if (debug) System.out.println("7 "+result); } catch(IOException e){ } @@ -718,8 +711,8 @@ public class GFEditor extends JFrame implements ActionListener, CaretListener, } catch(IOException e){ } } - public void outputAppend(){ - int i, j, k, l, l2, m=0, n=0; + public void outputAppend(){ + int i, j, k, l, l2, m; l = result.indexOf("',i); @@ -728,51 +721,56 @@ public class GFEditor extends JFrame implements ActionListener, CaretListener, // 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+2); + result= result.substring(0,l)+result.substring(j+1); i=result.indexOf("/focus",l); if (debug) System.out.println("/ is at the position"+i); j=result.indexOf('>',i); - k=result.length()-j-1; + k=result.length()-j; if (debug) System.out.println("form Lin2: "+result); + m = output.getText().length(); - 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 (debug) + System.out.println("char at the previous position"+result.charAt(i-1)); if (result.charAt(i-1)!='<') - result= result.substring(0,i-8)+result.substring(j+2); + result= result.substring(0,i-8)+result.substring(j+1); else - result= result.substring(0,i-1)+result.substring(j+2); + result= result.substring(0,i-1)+result.substring(j+1); 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)