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

Eliminated result as a global variable

Browse Source
This commit is contained in:
hdaniels
2005-07-01 08:47:21 +00:00
parent c0026af3a7
commit 76d50368fb
6 changed files with 369 additions and 319 deletions
Download Patch File Download Diff File Expand all files Collapse all files

25
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AbstractProber.java
View File

@@ -170,8 +170,8 @@ abstract class AbstractProber {
* @param text the command, exactly the string that is going to be sent
*/
protected void send(String text) {
if (logger.isLoggable(Level.FINER)) {
logger.finer("## send: '" + text + "'");
if (logger.isLoggable(Level.FINE)) {
logger.fine("## send: '" + text + "'");
}
try {
toProc.write(text, 0, text.length());
@@ -182,5 +182,24 @@ abstract class AbstractProber {
}
}
/**
* Just reads the complete output of a GF run and ignores it.
* @param fromProc The process from which the GFEDIT should be read.
*/
static void readAndIgnore(BufferedReader fromProc) {
try {
String readresult = fromProc.readLine();
if (logger.isLoggable(Level.FINER)) logger.finer("14 "+readresult);
while (readresult.indexOf("</gfedit>") == -1) {
readresult = fromProc.readLine();
if (logger.isLoggable(Level.FINER)) logger.finer("14 "+readresult);
}
//read trailing newline:
readresult = fromProc.readLine();
if (logger.isLoggable(Level.FINER)) logger.finer("14 "+readresult);
} catch (IOException e) {
System.err.println("Could not read from external process:\n" + e);
}
}
}

93
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/CompletableProber.java Normal file
View File

@@ -0,0 +1,93 @@
package de.uka.ilkd.key.ocl.gf;
import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.IOException;
import java.util.logging.*;
/**
* asks GF if the given commands leads to a situation, where
* something could be filled in automatically.
* This class is meant for self and result.
* @author daniels
*/
class AutoCompletableProber extends AbstractProber {
/**
* This field is true in the beginning of each run, and
* set to false, if the focus position when checking is found
* to be open.
*/
protected boolean autocompleted = true;
protected static Logger nogger = Logger.getLogger(AutoCompletableProber.class.getName());
/**
* A constructor which sets some fields
* @param fromGf the stdout from the GF process
* @param toGf the stdin from the GF process
*/
public AutoCompletableProber(BufferedReader fromGf, BufferedWriter toGf) {
super(fromGf, toGf);
}
/**
* asks GF if the given commands leads to a situation, where
* something could be filled in automatically.
* This function is meant for self and result.
* IMPORTANT: Must be called <b>after</b> &lt;/gfedit&gt;
* when no other method reads sth. from GF.
* It uses the same GF as everything else, since it tests if
* sth. is possible there.
* @param gfCommand the command to be tested.
* One has to chain a mp command to make GF go to the right place afterwards
* @param chainCount The number of chained commands in gfCommand.
* So many undos are done to clean up afterwards.
* @return true iff sth. could be filled in automatically
*/
public boolean isAutoCompletable(String gfCommand, int chainCount) {
this.autocompleted = true;
send(gfCommand);
readGfedit();
final boolean result = this.autocompleted;
this.autocompleted = true;
//clean up and undo
send("u " + chainCount);
readAndIgnore(fromProc);
if (nogger.isLoggable(Level.FINE)) {
nogger.fine(result + " is the result for: '" + gfCommand +"'");
}
return result;
}
/**
* Reads the tree child of the XML from beginning to end.
* Sets autocompleted to false, if the focus position is open.
*/
protected void readTree() {
try {
String result = fromProc.readLine();
if (nogger.isLoggable(Level.FINER)) {
nogger.finer("14 " + result);
}
while (result.indexOf("/tree")==-1){
result = result.trim();
if (result.startsWith("*")) {
result = result.substring(1).trim();
if (result.startsWith("?")) {
this.autocompleted = false;
}
}
result = fromProc.readLine();
if (nogger.isLoggable(Level.FINER)) {
nogger.finer("14 " + result);
}
}
} catch(IOException e){
System.err.println(e.getMessage());
e.printStackTrace();
}
}
}

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

@@ -2,7 +2,7 @@
// Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//it under the terms of the GNU General Public License as publisrhed by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
@@ -131,7 +131,7 @@ public class GFEditor2 extends JFrame {
protected String selectedMenuLanguage = "Abstract";
/**
* the GF-output between <linearization> </linearization> tags is stored here.
* must be saved in case the displayed languages are changed.
* Must be saved in case the displayed languages are changed.
* Only written in readLin
*/
private String linearization = "";
@@ -161,14 +161,10 @@ public class GFEditor2 extends JFrame {
* Avoids a time-consuming reconstruction and flickering.
*/
public boolean treeChanged = true;
/** the most common use is to store here what is read from GF */
private String result;
/** The output from GF is in here */
private BufferedReader fromProc;
/** leave messages for GF here. */
private BufferedWriter toProc;
/** used to print error messages */
private final String commandPath;
/** Linearizations' display area */
private JTextArea linearizationArea = new JTextArea();
/** the content of the refinementMenu */
@@ -372,14 +368,6 @@ public class GFEditor2 extends JFrame {
* most often null, except for Int and String, which can be parsed.
*/
private GfAstNode currentNode = null;
/**
* Here the node is stored that introduces the bound variables
* self and possibly result.
* This knowledge is read in formTree and used in probeProbability,
* which is called by readAndDisplay which again is called by a
* number of functions. Thus a 'global' variable.
*/
private GfAstNode constraintNode = null;
/** stores the displayed parts of the linearization */
private Display display = new Display(3);
@@ -460,7 +448,6 @@ public class GFEditor2 extends JFrame {
*/
public GFEditor2(String gfcmd, boolean isHtml, URL baseURL) {
this.callback = null;
this.commandPath = gfcmd;
Image icon = null;
try {
final URL iconURL = ClassLoader.getSystemResource("gf-icon.gif");
@@ -485,7 +472,6 @@ public class GFEditor2 extends JFrame {
*/
public GFEditor2(String gfcmd, ConstraintCallback callback, String initAbs, ProgressMonitor pm) {
this.callback = callback;
this.commandPath = gfcmd;
Utils.tickProgress(pm, 5220, "Loading grammars");
initializeGF(gfcmd, pm);
@@ -1652,9 +1638,8 @@ public class GFEditor2 extends JFrame {
/**
* reads the output from GF starting with &gt;gfedit&lt; and last reads &gt;/gfedit&lt;.
* Feeds the editor with what was read.
* @return the last read line, should be ""
*/
protected String readGfedit() {
protected void readGfedit() {
try {
String next = "";
//read <gfedit>
@@ -1669,7 +1654,8 @@ public class GFEditor2 extends JFrame {
//reading <linearizations>
//seems to be the only line read here
while ((next!=null)&&((next.length()==0)||(next.indexOf("<lin ")==-1))) {
//this is here to give as some sort of catch clause.
while ((next!=null)&&((next.length()==0)||(next.indexOf("<linearizations>")==-1))) {
next = fromProc.readLine();
if (next!=null){
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("10 "+next);
@@ -1677,7 +1663,7 @@ public class GFEditor2 extends JFrame {
System.exit(0);
}
}
result = next;
readresult = next;
readLin();
readTree();
readMessage();
@@ -1685,20 +1671,20 @@ public class GFEditor2 extends JFrame {
if (newObject) {
readRefinementMenu();
} else {
while(result.indexOf("</menu")==-1) {
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("12 "+result);
while(readresult.indexOf("</menu")==-1) {
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("12 " + readresult);
}
}
for (int i=0; i<3 && !result.equals(""); i++){
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("11 "+result);
// "" should occur quite fast, but it has not already been read,
// since the last read line is "</menu>"
for (int i = 0; i < 3 && !readresult.equals(""); i++){
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("11 " + readresult);
}
return result;
} catch (IOException e) {
System.err.println("Could not read from external process:\n" + e);
return result;
}
}
@@ -1706,67 +1692,29 @@ public class GFEditor2 extends JFrame {
/**
* checks if result and self make sense in the current context.
* if not, they are removed from the list
*
*/
protected void probeCompletability() {
if (!showSelfResult) {
if (!showSelfResult || (this.focusPosition == null)) {
return;
}
final String varself = "VarSelf";
final String varresult = "VarResult";
/**
* self and result both take two arguments.
* The first is the type, which is fixed
* if the second argument is refineable.
* Important is the second.
* This only is refineable for the real type of self/result
*/
final String childPos = this.focusPosition.childPosition(1);
final AutoCompletableProber cp = new AutoCompletableProber(fromProc, toProc);
for (int i = 0; i < listModel.size(); i++) {
String cmd = ((GFCommand)listModel.elementAt(i)).getCommand();
//can we check the types at all?
if ((cmd != null) && (this.currentNode != null) && (this.constraintNode != null)) {
if ((cmd.indexOf("r core.self") > -1)) {
if (checkTypeSelfResult(i, varself) ){
i -=1;
}
}
if ((cmd.indexOf("r core.result") > -1)) {
if (checkTypeSelfResult(i, varresult)) {
i -= 1;
}
if ((cmd != null) && ((cmd.indexOf("r core.self") > -1) || (cmd.indexOf("r core.result") > -1))) {
String newCommand = cmd + " ;; mp " + childPos;
if (!cp.isAutoCompletable(newCommand, 2)) {
listModel.remove(i);
i -=1;
}
}
//(cmd.indexOf("r core.result") > -1)
}
}
/**
* Compares the type of the currently offered self or result and
* removes this command from the list, if it doesn't match
* the type of the on the top level introduced bound variable
* for self resp. result
* @param i The number of the current cmd in this.listModel
* @param boundVar indicates whether self or result is to be
* checked.
* if boundVar is "VarResult", result is checked, if boundVar is
* "VarSelf", self.
* Use nothing else!
* @return true iff a command was removed from listModel
*/
private boolean checkTypeSelfResult(int i, String boundVar) {
//assert "VarSelf".equals(boundVar) || "VarResult".equals(boundVar);
final String instance = "Instance";
String selfType = null;
//find the bound VarSelf variable
for (int j = 0; j < this.constraintNode.boundNames.length; j++) {
if (this.constraintNode.boundTypes[j].startsWith(boundVar)) {
selfType = this.constraintNode.boundTypes[j].substring(boundVar.length()).trim();
}
}
// check if the current node can be refined with sth
// of type Instance WhatEverClassSelfHas
if ((selfType == null) || (!(instance + " " + selfType).equals(this.currentNode.getType()))) {
//remove it from the list of offered commands
listModel.remove(i);
return true;
} else {
return false;
}
}
@@ -1968,22 +1916,24 @@ public class GFEditor2 extends JFrame {
Vector gfCommandVector = new Vector();
HashSet processedSubcats = new HashSet();
try {
//read <menu>
String readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 " + readresult);
//read item
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 "+result);
while (result.indexOf("/menu")==-1){
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
while (readresult.indexOf("/menu")==-1){
//read show
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 "+result);
while (result.indexOf("/show")==-1){
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("9 "+result);
if (result.indexOf("/show")==-1)
{
if (result.length()>8)
s+=result.trim();
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
while (readresult.indexOf("/show") == -1){
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("9 " + readresult);
if (readresult.indexOf("/show") == -1) {
if (readresult.length()>8)
s += readresult.trim();
else
s+=result;
s += readresult;
}
}
// if (s.charAt(0)!='d')
@@ -1991,24 +1941,24 @@ public class GFEditor2 extends JFrame {
// else
String showText = s;
printnameVector.addElement(s);
s="";
s = "";
//read /show
//read send
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 "+result);
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 "+result);
String myCommand = result;
commandVector.add(this.result);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
String myCommand = readresult;
commandVector.add(readresult);
//read /send (discarded)
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 "+result);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
// read /item
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 "+result);
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 "+result);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
final boolean isAbstract = "Abstract".equals(this.selectedMenuLanguage);
RealCommand gfc = new RealCommand(myCommand, processedSubcats, this.printnameManager, showText, isAbstract);
@@ -2137,9 +2087,7 @@ public class GFEditor2 extends JFrame {
//a new object has been created
this.newObject = true;
}
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 "+result);
return result;
return readresult;
} catch(IOException e){
System.err.println(e.getMessage());
e.printStackTrace();
@@ -2159,18 +2107,19 @@ public class GFEditor2 extends JFrame {
*/
protected void readLin(){
try {
linearization="";
linearization += result+"\n";
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 "+result);
while ((result!=null)&&(result.indexOf("/linearization")==-1)){
linearization += result+"\n";
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 "+result);
linearization="";
//read <linearizations>
String readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 " + readresult);
linearization += readresult + "\n";
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);
while ((readresult != null) && (readresult.indexOf("/linearization") == -1)){
linearization += readresult + "\n";
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);
}
if (newObject) formLin();
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 "+result);
if (newObject) formLin();
} catch(IOException e){
System.err.println(e.getMessage());
e.printStackTrace();
@@ -2184,20 +2133,21 @@ public class GFEditor2 extends JFrame {
protected void readTree(){
String treeString = "";
try {
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 "+result);
while (result.indexOf("/tree")==-1){
treeString += result+"\n";
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 "+result);
//read <tree>
String readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);
while (readresult.indexOf("/tree") == -1){
treeString += readresult + "\n";
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);
}
if (treeChanged && (newObject)) {
formTree(tree, treeString);
treeChanged = false;
}
treeString="";
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 "+result);
treeString="";
} catch(IOException e){
System.err.println(e.getMessage());
e.printStackTrace();
@@ -2212,20 +2162,21 @@ public class GFEditor2 extends JFrame {
protected void readMessage(){
String s ="";
try {
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 "+result);
while (result.indexOf("/message")==-1){
s += result+"\n";
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 "+result);
// read <message>
String readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 " + readresult);
while (readresult.indexOf("/message") == -1){
s += readresult + "\n";
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 " + readresult);
}
if (s.length()>1) {
this.display.addToStages("-------------\n" + s, "<hr>" + s);
//in case no language is displayed
display(false, false);
}
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 "+result);
} catch(IOException e){
System.err.println(e.getMessage());
e.printStackTrace();
@@ -2242,54 +2193,54 @@ public class GFEditor2 extends JFrame {
boolean more = true;
try {
//read first cat
result = fromProc.readLine();
String readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) {
xmlLogger.finer("2 "+result);
xmlLogger.finer("2 " + readresult);
}
if (result.indexOf("(none)") > -1) {
if (readresult.indexOf("(none)") > -1) {
//no topics present
more = false;
}
while (more){
//adds new cat s to the menu
if (result.indexOf("topic")==-1) {
newCategoryMenu.addItem(result.substring(6));
if (readresult.indexOf("topic") == -1) {
newCategoryMenu.addItem(readresult.substring(6));
}
else
more = false;
//read </newcat
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("2 "+result);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("2 " + readresult);
//read <newcat (normally)
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("3 "+result);
if (result.indexOf("topic")!=-1) {
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("3 " + readresult);
if (readresult.indexOf("topic") != -1) {
//no more categories
more = false;
}
//read next cat / topic
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("4 "+result);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("4 " + readresult);
}
//set topic
grammar.setText(result.substring(4)+" ");
grammar.setText(readresult.substring(4)+" ");
//read </topic>
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("2 "+result);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("2 " + readresult);
//read <language>
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("3 "+result);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("3 " + readresult);
//read actual language
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("4 "+result);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("4 " + readresult);
//read the languages and select the last non-abstract
more = true;
while (more){
if ((result.indexOf("/gfinit")==-1)&&(result.indexOf("lin")==-1)) {
if ((readresult.indexOf("/gfinit") == -1) && (readresult.indexOf("lin") == -1)) {
//form lang and Menu menu:
final String langName = result.substring(4);
final String langName = readresult.substring(4);
final boolean active;
if (langName.equals("Abstract")) {
active = false;
@@ -2308,29 +2259,30 @@ public class GFEditor2 extends JFrame {
more = false;
}
// read </language>
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("2 "+result);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("2 " + readresult);
// read <language> or </gfinit...>
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("3 "+result);
if ((result.indexOf("/gfinit")!=-1)||(result.indexOf("lin")!=-1))
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("3 " + readresult);
if ((readresult.indexOf("/gfinit") != -1) || (readresult.indexOf("lin") != -1))
more = false;
if (result.indexOf("/gfinit")!=-1)
if (readresult.indexOf("/gfinit") != -1)
finished = true;
// registering the file name:
if (result.indexOf("language")!=-1) {
String path = result.substring(result.indexOf('=')+1,
result.indexOf('>'));
path =path.substring(path.lastIndexOf('/')+1);
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("name: "+path);
if (readresult.indexOf("language") != -1) {
String path = readresult.substring(readresult.indexOf('=') + 1,
readresult.indexOf('>'));
path = path.substring(path.lastIndexOf('/') + 1);
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("name: " + path);
fileString +="--" + path +"\n";
if (path.lastIndexOf('.')!=path.indexOf('.'))
grammar.setText(path.substring(0,
path.indexOf('.')).toUpperCase()+" ");
}
//TODO in case of finished, read "", otherwise ...
result = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("4 "+result);
// in case of finished, read the final "" after </gfinit>,
// otherwise the name of the next language
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("4 " + readresult);
}
} catch(IOException e){
logger.warning(e.getMessage());
@@ -2342,57 +2294,56 @@ public class GFEditor2 extends JFrame {
* Sets the current focusPosition, then changes all &lt;focus&gt; tags
* into regular &lt;subtree&gt; tags.
*
* Expects its argument in this.result
*
* Then control is given to appendMarked, which does the display
* @param readLin The text between &lt;lin&gt; &lt;/lin&gt; tags.
* @param clickable true iff the correspondent display area should be clickable
* @param doDisplay true iff the linearization should be displayed.
* @param language the current linearization language
*/
protected StringBuffer outputAppend(boolean clickable, boolean doDisplay, String language){
protected StringBuffer outputAppend(String readLin, boolean clickable, boolean doDisplay, String language){
final StringBuffer linCollector = new StringBuffer();
//result=result.replace('\n',' ');
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("INPUT:"+result);
linMarkingLogger.finer("INPUT:" + readLin);
}
int focusTagBegin = this.result.indexOf("<focus");
int typeBegin=this.result.indexOf("type=",focusTagBegin);
int focusTagEnd = this.result.indexOf('>',typeBegin);
int focusTagBegin = readLin.indexOf("<focus");
int typeBegin=readLin.indexOf("type=",focusTagBegin);
int focusTagEnd = readLin.indexOf('>',typeBegin);
// status incorrect ?:
final int typeEnd;
if ((typeBegin > -1) && (this.result.substring(typeBegin,focusTagEnd).indexOf("incorrect")!=-1)) {
typeEnd = result.indexOf("status");
if ((typeBegin > -1) && (readLin.substring(typeBegin,focusTagEnd).indexOf("incorrect")!=-1)) {
typeEnd = readLin.indexOf("status");
} else {
typeEnd = focusTagEnd;
}
int focusTextBegin = this.result.indexOf("focus");
int focusTextBegin = readLin.indexOf("focus");
if (focusTagBegin!=-1){
// in case focus tag is cut into two lines:
if (focusTagBegin==-1){
focusTagBegin = focusTextBegin - 7;
}
final int positionBegin=this.result.indexOf("position",focusTagBegin);
final int positionEnd=this.result.indexOf("]",positionBegin);
final int positionBegin=readLin.indexOf("position",focusTagBegin);
final int positionEnd=readLin.indexOf("]",positionBegin);
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("POSITION START: "+positionBegin
+ "\n-> POSITION END: "+positionEnd);
}
if (xmlLogger.isLoggable(Level.FINER)) {
xmlLogger.finer("form Lin1: "+this.result);
xmlLogger.finer("form Lin1: " + readLin);
}
this.focusPosition = new LinPosition(result.substring(positionBegin+9,positionEnd+1),
this.result.substring(positionBegin,focusTagEnd).indexOf("incorrect")==-1);
statusLabel.setText(" "+result.substring(typeBegin+5,typeEnd));
this.focusPosition = new LinPosition(readLin.substring(positionBegin + 9, positionEnd+1),
readLin.substring(positionBegin, focusTagEnd).indexOf("incorrect") == -1);
statusLabel.setText(" " + readLin.substring(typeBegin + 5, typeEnd));
//changing <focus> to <subtree>
this.result = replaceNotEscaped(this.result, "<focus", "<subtree");
this.result = replaceNotEscaped(this.result, "</focus", "</subtree");
readLin = replaceNotEscaped(readLin, "<focus", "<subtree");
readLin = replaceNotEscaped(readLin, "</focus", "</subtree");
String appended = appendMarked(this.result + '\n', clickable, doDisplay, language);
String appended = appendMarked(readLin + '\n', clickable, doDisplay, language);
linCollector.append(appended);
} else {//no focus at all (message?):
this.focusPosition = null;
// beware the side-effects! They are, what counts
linCollector.append(appendMarked(this.result + '\n', clickable, doDisplay, language));
linCollector.append(appendMarked(readLin + '\n', clickable, doDisplay, language));
}
// if (logger.isLoggable(Level.FINER)) {
// logger.finer("collected appended linearizations:\n" + linCollector.toString());
@@ -2426,7 +2377,9 @@ public class GFEditor2 extends JFrame {
* Parses the GF-output between <linearization> </linearization> tags
*
* pseudo-parses the XML lins and fills the output text area
* with the lin in all enabled languages
* with the lin in all enabled languages.
*
* Expects the linearization string to be in this.linearization.
*/
protected void formLin(){
//reset previous output
@@ -2435,19 +2388,19 @@ public class GFEditor2 extends JFrame {
boolean firstLin=true;
//read first line like ' <lin lang=Abstract>'
result = linearization.substring(0,linearization.indexOf('\n'));
String readResult = linearization.substring(0,linearization.indexOf('\n'));
//the rest of the linearizations
String lin = linearization.substring(linearization.indexOf('\n')+1);
//extract the language from result
int ind = Utils.indexOfNotEscaped(result, "=");
int ind2 = Utils.indexOfNotEscaped(result, ">");
//extract the language from readResult
int ind = Utils.indexOfNotEscaped(readResult, "=");
int ind2 = Utils.indexOfNotEscaped(readResult, ">");
/** The language of the linearization */
String language = result.substring(ind+1,ind2);
String language = readResult.substring(ind+1,ind2);
//the first direct linearization
result = lin.substring(0,lin.indexOf("</lin>"));
readResult = lin.substring(0,lin.indexOf("</lin>"));
//the rest
lin = lin.substring(lin.indexOf("</lin>"));
while (result.length()>1) {
while (readResult.length()>1) {
this.langMenuModel.add(language,true);
// selected?
boolean visible = this.langMenuModel.isLangActive(language);
@@ -2456,11 +2409,11 @@ public class GFEditor2 extends JFrame {
this.display.addToStages("\n************\n", "<br><hr><br>");
}
if (xmlLogger.isLoggable(Level.FINER)) {
xmlLogger.finer("linearization for the language: "+result);
xmlLogger.finer("linearization for the language: "+readResult);
}
// we want the side-effects of outputAppend
final boolean isAbstract = "Abstract".equals(language);
String linResult = outputAppend(!isAbstract, visible, language).toString();
String linResult = outputAppend(readResult, !isAbstract, visible, language).toString();
if (visible) {
firstLin = false;
}
@@ -2472,14 +2425,14 @@ public class GFEditor2 extends JFrame {
break;
}
result = lin.substring(0,lin.indexOf('\n'));
readResult = lin.substring(0,lin.indexOf('\n'));
lin = lin.substring(lin.indexOf('\n')+1);
if (result.indexOf("<lin ")!=-1){
//extract the language from result
ind = result.indexOf('=');
ind2 = result.indexOf('>');
language = result.substring(ind+1,ind2);
result = lin.substring(0,lin.indexOf("</lin>"));
if (readResult.indexOf("<lin ")!=-1){
//extract the language from readResult
ind = readResult.indexOf('=');
ind2 = readResult.indexOf('>');
language = readResult.substring(ind+1,ind2);
readResult = lin.substring(0,lin.indexOf("</lin>"));
lin = lin.substring(lin.indexOf("</lin>"));
}
}
@@ -2507,12 +2460,12 @@ public class GFEditor2 extends JFrame {
HtmlMarkedArea incMA;
for (Iterator it = incorrectMA.iterator(); !incorrect && it.hasNext();) {
incMA = (HtmlMarkedArea)it.next();
if (isSubtreePosition(incMA.position, ma.position)) {
if (LinPosition.isSubtreePosition(incMA.position, ma.position)) {
incorrect = true;
}
}
}
if (isSubtreePosition(this.focusPosition, ma.position)) {
if (LinPosition.isSubtreePosition(this.focusPosition, ma.position)) {
focused = true;
}
@@ -2528,10 +2481,6 @@ public class GFEditor2 extends JFrame {
highlightHtml(ma, Color.RED);
}
}
// if (logger.isLoggable(Level.FINER)) {
// logger.finer("completeLin: \n" + completeLin);
// }
}
@@ -2611,31 +2560,6 @@ public class GFEditor2 extends JFrame {
}
/**
* compares two position strings and returns true, if superPosition is
* a prefix of subPosition, that is, if subPosition is in a subtree of
* superPosition
* @param superPosition the position String in Haskell notation
* ([0,1,0,4]) of the to-be super-branch of subPosition
* @param subPosition the position String in Haskell notation
* ([0,1,0,4]) of the to-be (grand-)child-branch of superPosition
* @return true iff superPosition denotes an ancestor of subPosition
*/
private static boolean isSubtreePosition(final LinPosition superPosition, final LinPosition subPosition) {
if (superPosition == null || subPosition == null) {
return false;
}
String superPos = superPosition.position;
String subPos = subPosition.position;
if (superPos.length() < 2 || subPos.length() < 2 ) {
return false;
}
superPos = superPos.substring(1, superPos.length() - 1);
subPos = subPos.substring(1, subPos.length() - 1);
boolean result = subPos.startsWith(superPos);
return result;
}
/**
* Sets the font on all the GUI-elements to font.
* @param newFont the font everything should have afterwards
@@ -2782,14 +2706,6 @@ public class GFEditor2 extends JFrame {
if (s.indexOf('*')!=-1) {
star = 1;
}
/**
* only the first node in the AST that introduces an oper
* constraint brings with it the bound variables for self
* and result.
* At least for single context constraints, but that is exactly
* that what the editor is for.
*/
boolean boundVarsEncountered = false;
while (s.length()>0) {
/**
* every two ' ' indicate one tree depth level
@@ -2814,11 +2730,6 @@ public class GFEditor2 extends JFrame {
if (selected) {
this.currentNode = node;
}
//get the node that introduces self and result
if ((!boundVarsEncountered) && ("OperConstraintBody".equals(node.getType()) || "ClassConstraintBody".equals(node.getType()))) {
this.constraintNode = node;
boundVarsEncountered = true;
}
index++;
s = s.substring(j+1);
@@ -2868,9 +2779,6 @@ public class GFEditor2 extends JFrame {
//or refined and not described
and = new RefinedAstNodeData(null, node);
}
newChildNode = myTreePanel.addObject(parent, and);
parentNodes.put(new Integer(shift+1), newChildNode);
@@ -2885,7 +2793,7 @@ public class GFEditor2 extends JFrame {
treeLogger.finer("new selected index "+ index);
}
// set the description of the crrent parameter to a more
// set the description of the current parameter to a more
// prominent place
String paramName = null;
int paramPosition = -1;
@@ -2915,48 +2823,21 @@ public class GFEditor2 extends JFrame {
}
}
/**
* Returns the biggest position of first and second.
* Each word in the linearization area has the corresponding
* position in the tree. The position-notion is taken from
* GF-Haskell, where empty position ("[]")
* represents tree-root, "[0]" represents first child of the root,
* "[0,0]" represents the first grandchild of the root etc.
* So comparePositions("[0]","[0,0]")="[0]"
*/
private String comparePositions(String first, String second) {
String common ="[]";
int i = 1;
while ((i<Math.min(first.length()-1,second.length()-1))&&(first.substring(0,i+1).equals(second.substring(0,i+1))))
{
common=first.substring(0,i+1);
i+=2;
}
if (common.charAt(common.length()-1)==']') {
return common;
} else {
return common+"]";
}
}
/**
* Returns the widest position (see comments to comparePositions)
* covered in the string from begin to end in the
* linearization area
* @param begin
* @param end
* linearization area.
* @param begin The index in htmlOutputVector of the first MarkedArea, that is possibly the max
* @param end The index in htmlOutputVector of the last MarkedArea, that is possibly the max
* @return the position in GF Haskell notation (hdaniels guesses)
*/
private String findMax(int begin, int end) {
String max = (((MarkedArea)this.htmlOutputVector.elementAt(begin)).position).position;
for (int i = begin+1; i <= end; i++)
max = comparePositions(max,(((MarkedArea)this.htmlOutputVector.elementAt(i)).position).position);
max = LinPosition.maxPosition(max,(((MarkedArea)this.htmlOutputVector.elementAt(i)).position).position);
return max;
}
/**
* Appends the string s to the text in the linearization area
* on the screen. It parses the subtree tags and registers them.
@@ -3156,29 +3037,6 @@ public class GFEditor2 extends JFrame {
/**
* Finding position of the searchString not starting with escape symbol (\\)
* in the string s from position.
* @param s the String that is to be checked.
* @param searchString
* @param position
* @return the position of the first such a char after position
*/
private int getCharacter(String s, String searchString, int position) {
int t = s.indexOf(searchString, position);
int i = t-1;
int k = 0;
while ((i>-1)&&(s.charAt(i)=='\\')) {
k++;
i--;
}
if (k % 2 == 0) {
return t;
} else {
return getCharacter(s, searchString, t+1);
}
}
/**
* The substring from start to end in workingString, together with
* position is saved as a MarkedArea in this.htmlOutputVector.
@@ -3428,7 +3286,6 @@ public class GFEditor2 extends JFrame {
popup2.show(e.getComponent(), e.getX(), e.getY());
}
// middle click
//TODO parsing via middle click
if (e.getButton() == MouseEvent.BUTTON2) {
// selection Exists:
if (popUpLogger.isLoggable(Level.FINER)) {
@@ -3475,7 +3332,7 @@ public class GFEditor2 extends JFrame {
StringBuffer sel = new StringBuffer();
for (int i = 0; i<htmlOutputVector.size(); i++) {
final HtmlMarkedArea ma = (HtmlMarkedArea)htmlOutputVector.elementAt(i);
if (language.equals(ma.language) && isSubtreePosition(focusPosition, ma.position)) {
if (language.equals(ma.language) && LinPosition.isSubtreePosition(focusPosition, ma.position)) {
sel.append(ma.words);
}
}

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

@@ -21,7 +21,7 @@ package de.uka.ilkd.key.ocl.gf;
* if all hold (correct/incorrect).
* Class is immutable.
*/
public class LinPosition {
class LinPosition {
/**
* a position in the AST in Haskell notation
*/
@@ -42,6 +42,64 @@ public class LinPosition {
correctPosition = cor;
}
/**
* Creates a position string in Haskell notation for the argument
* number nr of this node.
* @param nr The number of the wanted argument
* @return the position string for the nrth child
*/
public String childPosition(int nr) {
return this.position.substring(0, this.position.length() - 1) + "," + nr + "]";
}
/**
* compares two position strings and returns true, if superPosition is
* a prefix of subPosition, that is, if subPosition is in a subtree of
* superPosition
* @param superPosition the position String in Haskell notation
* ([0,1,0,4]) of the to-be super-branch of subPosition
* @param subPosition the position String in Haskell notation
* ([0,1,0,4]) of the to-be (grand-)child-branch of superPosition
* @return true iff superPosition denotes an ancestor of subPosition
*/
public static boolean isSubtreePosition(final LinPosition superPosition, final LinPosition subPosition) {
if (superPosition == null || subPosition == null) {
return false;
}
String superPos = superPosition.position;
String subPos = subPosition.position;
if (superPos.length() < 2 || subPos.length() < 2 ) {
return false;
}
superPos = superPos.substring(1, superPos.length() - 1);
subPos = subPos.substring(1, subPos.length() - 1);
boolean result = subPos.startsWith(superPos);
return result;
}
/**
* Returns the biggest position of first and second.
* Each word in the linearization area has the corresponding
* position in the tree. The position-notion is taken from
* GF-Haskell, where empty position ("[]")
* represents tree-root, "[0]" represents first child of the root,
* "[0,0]" represents the first grandchild of the root etc.
* So comparePositions("[0]","[0,0]")="[0]"
*/
public static String maxPosition(String first, String second) {
String common ="[]";
int i = 1;
while ((i<Math.min(first.length()-1,second.length()-1))&&(first.substring(0,i+1).equals(second.substring(0,i+1)))) {
common=first.substring(0,i+1);
i+=2;
}
if (common.charAt(common.length()-1)==']') {
return common;
} else {
return common+"]";
}
}
public String toString() {
return position + (correctPosition ? " correct" : " incorrect");
}

23
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/NoLineBreakFormatter.java Normal file
View File

@@ -0,0 +1,23 @@
package de.uka.ilkd.key.ocl.gf;
import java.util.logging.Formatter;
import java.util.logging.LogRecord;
/**
* @author daniels
* A simple Formatter class, that does not introduce linebreaks, so that
* continous lines can be read under each other.
*/
public class NoLineBreakFormatter extends Formatter {
/**
* @see java.util.logging.Formatter#format(java.util.logging.LogRecord)
*/
public String format(LogRecord record) {
final String shortLoggerName = record.getLoggerName().substring(record.getLoggerName().lastIndexOf('.') + 1);
return record.getLevel() + " : "
+ shortLoggerName + " "
+ record.getSourceMethodName() + " -:- "
+ record.getMessage() + "\n";
}
}

2
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameLoader.java
View File

@@ -95,7 +95,7 @@ public class PrintnameLoader extends AbstractProber {
if (lang != null && !("".equals(lang))) {
sendString = sendString + " -lang=" + lang;
}
nogger.info("collecting printnames :" + sendString);
nogger.fine("collecting printnames :" + sendString);
send(sendString);
readGfedit();
}