From 8f785c8ed4dd935ca534d2314956f605f39c2bfc Mon Sep 17 00:00:00 2001 From: hdaniels Date: Fri, 1 Jul 2005 11:40:50 +0000 Subject: [PATCH] Append an additional newline before the message from GF. reordering of read and form methods. --- .../de/uka/ilkd/key/ocl/gf/GFEditor2.java | 75 +++++++++++++------ 1 file changed, 51 insertions(+), 24 deletions(-) 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 b93878478..b1b861b18 100644 --- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java @@ -161,9 +161,15 @@ public class GFEditor2 extends JFrame { * Avoids a time-consuming reconstruction and flickering. */ public boolean treeChanged = true; - /** The output from GF is in here */ + /** + * The output from GF is in here. + * Only the read methods, initializeGF and the prober objects access this. + */ private BufferedReader fromProc; - /** leave messages for GF here. */ + /** Used to leave messages for GF here. + * But only in send and special probers that clean up with undo + * after them (or don't change the state like PrintnameLoader). + */ private BufferedWriter toProc; /** Linearizations' display area */ private JTextArea linearizationArea = new JTextArea(); @@ -1665,16 +1671,18 @@ public class GFEditor2 extends JFrame { } readresult = next; readLin(); - readTree(); - readMessage(); + final String treeString = readTree(); + final String message = readMessage(); //read the menu stuff + Vector gfCommandVector; if (newObject) { - readRefinementMenu(); + gfCommandVector = readRefinementMenu(); } else { while(readresult.indexOf("" @@ -1683,6 +1691,25 @@ public class GFEditor2 extends JFrame { if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("11 " + readresult); } + //now the form methods are called: + if (treeChanged && (newObject)) { + formTree(tree, treeString); + } + if (gfCommandVector != null) { + formRefinementMenu(gfCommandVector); + } + if (newObject) { + //MUST come after readLin, but since formLin is called later too, + //this cannot be enforced with a local this.linearization + formLin(); + } + if (message != null && message.length()>1) { + this.display.addToStages("\n-------------\n" + message, "
" + message); + //in case no language is displayed + display(false, false); + } + + } catch (IOException e) { System.err.println("Could not read from external process:\n" + e); } @@ -1907,8 +1934,10 @@ public class GFEditor2 extends JFrame { * Parses the GF-output between and tags * and fills the corrsponding GUI list -"Select Action". * seems to expect the starting menu tag to be already read + * @return A Vector of GfCommand, that contains all commands, + * already parsed, but not grouped or otherwise treated. */ - protected void readRefinementMenu (){ + protected Vector readRefinementMenu (){ if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("list model changing! "); String s =""; Vector printnameVector = new Vector(); @@ -1968,7 +1997,7 @@ public class GFEditor2 extends JFrame { System.err.println(e.getMessage()); e.printStackTrace(); } - formRefinementMenu(gfCommandVector); + return gfCommandVector; } /** @@ -1978,6 +2007,8 @@ public class GFEditor2 extends JFrame { * character in the printname will be used as the display name * for this subcategory. If this displayname is defined a second time, * it will get overwritten. + * Sorting is also done here. + * Adding additional special commands like InputCommand happens here too. * @param gfCommandVector contains all RealCommands, that are available * at the moment */ @@ -2119,7 +2150,6 @@ public class GFEditor2 extends JFrame { readresult = fromProc.readLine(); if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult); } - if (newObject) formLin(); } catch(IOException e){ System.err.println(e.getMessage()); e.printStackTrace(); @@ -2129,8 +2159,9 @@ public class GFEditor2 extends JFrame { /** * reads in the tree and calls formTree without start end end tag of tree * expects the first starting XML tag tree to be already read + * @return the read tags for the tree or null if a read error occurs */ - protected void readTree(){ + protected String readTree(){ String treeString = ""; try { //read @@ -2143,23 +2174,20 @@ public class GFEditor2 extends JFrame { readresult = fromProc.readLine(); if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult); } - if (treeChanged && (newObject)) { - formTree(tree, treeString); - treeChanged = false; - } - treeString=""; + return treeString; } catch(IOException e){ System.err.println(e.getMessage()); e.printStackTrace(); + return null; } } /** * Parses the GF-output between tags - * and puts it in the linearization area. - * seems to expect the opening message tag to be already read + * and returns it. + * @return The read message. */ - protected void readMessage(){ + protected String readMessage(){ String s =""; try { // read @@ -2172,14 +2200,11 @@ public class GFEditor2 extends JFrame { readresult = fromProc.readLine(); if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 " + readresult); } - if (s.length()>1) { - this.display.addToStages("-------------\n" + s, "
" + s); - //in case no language is displayed - display(false, false); - } + return s; } catch(IOException e){ - System.err.println(e.getMessage()); + System.err.println(e.getLocalizedMessage()); e.printStackTrace(); + return e.getLocalizedMessage(); } } @@ -2188,6 +2213,7 @@ public class GFEditor2 extends JFrame { * the names of the languages and puts them into the language menu * Parses the GF-output between tags * and fill the New combobox in the GUI. + * Reading and forming is mixed, since forming is quite primitive. */ protected void formNewMenu () { boolean more = true; @@ -2730,7 +2756,7 @@ public class GFEditor2 extends JFrame { if (selected) { this.currentNode = node; } - + // use indentation to calculate the parent index++; s = s.substring(j+1); shift = (shift - star)/2; @@ -2821,6 +2847,7 @@ public class GFEditor2 extends JFrame { gui2.toFront(); index = 0; } + treeChanged = false; } /**