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

Lots of refactorings for gfeditor

Browse Source
This commit is contained in:
hdaniels
2005-09-10 09:15:54 +00:00
parent c39b31c74f
commit b3e111aa02
40 changed files with 5069 additions and 2552 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -15,8 +15,6 @@
package de.uka.ilkd.key.ocl.gf;
import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.IOException;
import java.util.logging.*;
@@ -27,18 +25,18 @@ import java.util.logging.*;
*
*/
abstract class AbstractProber {
protected final BufferedReader fromProc;
protected final BufferedWriter toProc;
/**
* reference to the editor whose readRefinementMenu method is used
*/
protected final GfCapsule gfCapsule;
protected static Logger logger = Logger.getLogger(AbstractProber.class.getName());
/**
* A constructor which sets some fields
* @param fromGf the stdout from the GF process
* @param toGf the stdin from the GF process
* @param gfCapsule The encapsulation of GF
*/
public AbstractProber(BufferedReader fromGf, BufferedWriter toGf) {
this.fromProc = fromGf;
this.toProc = toGf;
public AbstractProber(GfCapsule gfCapsule) {
this.gfCapsule = gfCapsule;
}
/**
@@ -49,9 +47,9 @@ abstract class AbstractProber {
*/
protected String readHmsg(String readresult) {
if (readresult.equals("<hmsg>")) {
skipChild("<hmsg>");
gfCapsule.skipChild("<hmsg>");
try {
String next = fromProc.readLine();
String next = gfCapsule.fromProc.readLine();
if (logger.isLoggable(Level.FINER)) {
logger.finer("2 " + next);
}
@@ -71,22 +69,28 @@ abstract class AbstractProber {
* @param readresult the first line with the opening tag
*/
protected void readLinearizations(String readresult) {
skipChild("<linearizations>");
gfCapsule.skipChild("<linearizations>");
}
/** Reads the tree child of the XML from beginning to end */
/**
* Reads the tree child of the XML from beginning to end
*/
protected void readTree() {
skipChild("<tree>");
gfCapsule.skipChild("<tree>");
}
/** Reads the message child of the XML from beginning to end */
/**
* Reads the message child of the XML from beginning to end
*/
protected void readMessage() {
skipChild("<message>");
gfCapsule.skipChild("<message>");
}
/** Reads the menu child of the XML from beginning to end */
/**
* Reads the menu child of the XML from beginning to end
*/
protected void readMenu() {
skipChild("<menu>");
gfCapsule.skipChild("<menu>");
}
/**
@@ -97,23 +101,24 @@ abstract class AbstractProber {
try {
String next = "";
//read <gfedit>
String readresult = fromProc.readLine();
String readresult = gfCapsule.fromProc.readLine();
if (logger.isLoggable(Level.FINER)) {
logger.finer("1 " + next);
}
//read either <hsmg> or <lineatization>
readresult = fromProc.readLine();
readresult = gfCapsule.fromProc.readLine();
if (logger.isLoggable(Level.FINER)) {
logger.finer("1 " + next);
}
next = readHmsg(readresult);
Hmsg hmsg = gfCapsule.readHmsg(readresult);
next = hmsg.lastline;
//in case there comes sth. unexpected before <linearizations>
//usually the while body is never entered
// %%%
while ((next!=null)&&((next.length()==0)||(!next.trim().equals("<linearizations>")))) {
next = fromProc.readLine();
next = gfCapsule.fromProc.readLine();
if (next!=null){
if (logger.isLoggable(Level.FINER)) {
logger.finer("1 " + next);
@@ -128,7 +133,7 @@ abstract class AbstractProber {
readMenu();
for (int i=0; i<3 && !next.equals(""); i++){
next = fromProc.readLine();
next = gfCapsule.fromProc.readLine();
if (logger.isLoggable(Level.FINER)) {
logger.finer("1 " + next);
}
@@ -140,31 +145,6 @@ abstract class AbstractProber {
}
/**
* Reads the output from GF until the ending tag corresponding to the
* given opening tag is read.
* @param opening tag in the format of &gt;gfinit&lt;
*/
protected void skipChild(String opening) {
String closing = (new StringBuffer(opening)).insert(1, '/').toString();
try {
String nextRead = fromProc.readLine();
if (logger.isLoggable(Level.FINER)) {
logger.finer("3 " + nextRead);
}
while (!nextRead.trim().equals(closing)) {
nextRead = fromProc.readLine();
if (logger.isLoggable(Level.FINER)) {
logger.finer("3 " + nextRead);
}
}
} catch (IOException e) {
System.err.println("Could not read from external process:\n" + e);
}
}
/**
* send a command to GF
* @param text the command, exactly the string that is going to be sent
@@ -173,29 +153,26 @@ abstract class AbstractProber {
if (logger.isLoggable(Level.FINE)) {
logger.fine("## send: '" + text + "'");
}
try {
toProc.write(text, 0, text.length());
toProc.newLine();
toProc.flush();
} catch (IOException e) {
System.err.println("Could not write to external process " + e);
}
gfCapsule.realSend(text);
}
/**
* 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();
protected void readAndIgnore() {
try {
StringBuffer debugCollector = new StringBuffer();
String readresult = gfCapsule.fromProc.readLine();
debugCollector.append(readresult).append('\n');
if (logger.isLoggable(Level.FINER)) logger.finer("14 "+readresult);
while (readresult.indexOf("</gfedit>") == -1) {
readresult = gfCapsule.fromProc.readLine();
debugCollector.append(readresult).append('\n');
if (logger.isLoggable(Level.FINER)) logger.finer("14 "+readresult);
}
}
//read trailing newline:
readresult = fromProc.readLine();
readresult = gfCapsule.fromProc.readLine();
debugCollector.append(readresult).append('\n');
if (logger.isLoggable(Level.FINER)) logger.finer("14 "+readresult);
} catch (IOException e) {

64
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AstNodeData.java
View File

@@ -22,6 +22,8 @@ import java.util.logging.*;
* An object of this type knows how it self should be rendered,
* via Printname how its children should be rendered.
* This means the tooltip information it got from there.
* Knows nothing directly of the type of the node, which an object of this class
* represents. That's whats GfAstNode is for.
*/
abstract class AstNodeData {
protected static Logger logger = Logger.getLogger(DynamicTree2.class.getName());
@@ -36,11 +38,6 @@ abstract class AstNodeData {
*/
public abstract String getParamTooltip();
/**
*
* @return true iff this node represents an open leaf
*/
public abstract boolean isMeta();
/**
* keeps track of the number of children of this node.
* It has to be increased whenever a new child of this node is
@@ -48,8 +45,61 @@ abstract class AstNodeData {
*/
public int childNum = 0;
/**
* @return The position String in the GF AST for this node
* The position String in the GF AST for this node
* in Haskell notation.
*/
public abstract String getPosition();
public final String position;
/**
* the GF node connected to this NodeData, not the JTree node
*/
public final GfAstNode node;
/**
* If a subtyping witness is missing, then this flag is false
*/
public boolean subtypingStatus = true;
/**
* if this is the active, selected, focused node
*/
public final boolean selected;
/**
* The constraint, that is valid on this node.
* If this node introduced a node itself and did not just inherit
* one, they are just concatenated.
* Until now, only the presence of a non-empty string here is used,
* so that is not important yet.
*/
public final String constraint;
/**
* some nodes like coerce should, if possible, be covered from the
* users eyes. If this variable is greater than -1, the child
* with that number is shown instead of this node.
* This node will not appear in the tree.
*/
public int showInstead = -1;
/**
* A simple setter constructor, that sets the fields of this class (except showInstead)
* @param node the GF node connected to this NodeData, not the JTree node
* @param pos The position String in the GF AST for this node
* in Haskell notation.
* @param selected if this is the active, selected, focused node
* @param constraint The GF constraint introduced in this node
*/
protected AstNodeData(GfAstNode node, String pos, boolean selected, String constraint) {
this.node = node;
this.position = pos;
this.selected = selected;
// I have no better idea, how to clutch them together, since
// I don't need the content of this field right now.
this.constraint = node.constraint + constraint;
}
public String toString() {
return this.node.getLine();
}
}

60
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ChainCommandTuple.java Normal file
View File

@@ -0,0 +1,60 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/**
* @author hdaniels
* For chain commands, it is not just enough, to save the command sent to GF
* and the respective show text.
* Then it would be unclear, which fun should determine the used printname.
* If none is given, the last one of a chain command is taken.
* But if a solve for example is to follow, this does not work.
* Thus, this class has some other fields to define the appearance of a
* chain command.
*/
class ChainCommandTuple extends StringTuple {
/**
* the fun, that selects the printname
*/
final public String fun;
/**
* Here the subcat of fun can be overwritten.
* Is used for the attributes of self.
*/
final public String subcat;
/**
* normally, the ';;' are counted. But if we know, how many commands we
* chain to each other, we can skip that step and use undoSteps instead
*/
final public int undoSteps;
/**
* A simple setter constructor
* @param command The command sent to GF
* @param showtext The text, that GF would display if no matching
* printname is found.
* @param fun The fun that selects the used printname
* @param subcat the subcategory for the refinement menu, overwrites
* the one defined in the printname
* @param undoSteps how many undos are needed to undo this command
*/
public ChainCommandTuple(String command, String showtext, String fun, String subcat, int undoSteps) {
super(command, showtext);
this.fun = fun;
this.subcat = subcat;
this.undoSteps = undoSteps;
}
}

15
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ConstraintCallback.java
View File

@@ -21,8 +21,7 @@ import java.util.logging.*;
* @author daniels
* Offers the interface that GFEditor2 uses to send back the constraint after editing.
* Has no dependancies on KeY or TogetherCC.
*
*/
*/
abstract class ConstraintCallback {
/**
@@ -30,6 +29,9 @@ abstract class ConstraintCallback {
*/
protected static Logger logger = Logger.getLogger(ConstraintCallback.class.getName());
/**
* The path name of the directory where the grammars reside
*/
String grammarsDir;
/**
* sets the directory where the grammars reside
@@ -38,6 +40,7 @@ abstract class ConstraintCallback {
void setGrammarsDir(final String grammarsDir) {
this.grammarsDir = grammarsDir;
}
/**
* gets the directory where the grammars reside
*/
@@ -51,5 +54,11 @@ abstract class ConstraintCallback {
* @param constraint The OCL constraint in question.
*/
abstract void sendConstraint(String constraint);
/**
* Sends the unfinished OCL constraint back to Together to save it
* as a GF tree as a JavaDoc comment.
* @param abs The GF tree in question
*/
abstract void sendAbstract(String abs);
}

79
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Display.java
View File

@@ -25,8 +25,14 @@ import javax.swing.JEditorPane;
* Takes care of collecting the linearized text and the length calculations
*/
class Display {
private final boolean doText;
private final boolean doHtml;
/**
* If the linearization should be displayed as pure text
*/
private boolean doText;
/**
* If the linearization should be displayed as HTML
*/
private boolean doHtml;
/**
* collects the linearization after each append.
* what's in here are Strings
@@ -46,33 +52,49 @@ class Display {
*/
private JEditorPane htmlLengthPane = new JEditorPane();
/** initializes this object, nothing special
/**
* initializes this object, nothing special
* @param dt 1 if only text is to be shown, 2 for only HTML, 3 for both.
* Other values are forbidden.
*/
public Display(int dt) {
switch (dt) {
case 1:
doText = true;
doHtml = false;
break;
case 2:
doText = false;
doHtml = true;
break;
case 3:
doText = true;
doHtml = true;
break;
default:
doText = true;
doHtml = true;
break;
}
setDisplayType(dt);
this.htmlLengthPane.setContentType("text/html");
this.htmlLengthPane.setEditable(false);
}
/**
* (de-)activates display of text and HTML according to dt
* @param dt 1 if only text is to be shown, 2 for only HTML, 3 for both.
*/
protected void setDisplayType(int dt) {
switch (dt) {
case 1:
doText = true;
doHtml = false;
break;
case 2:
doText = false;
doHtml = true;
break;
case 3:
doText = true;
doHtml = true;
break;
default:
doText = true;
doHtml = true;
break;
}
}
/**
* Resets the stored text, but leaves the scroll markers untouched.
*/
public void resetLin() {
linStagesHtml.clear();
linStagesText.clear();
htmlLengthPane.setText("");
}
/**
* @param font The Font, that is to be used. If null, the default of JTextPane is taken.
@@ -157,7 +179,7 @@ class Display {
* @return the HtmlMarkedArea object that represents the given information
* and knows about its beginning and end in the display areas.
*/
protected HtmlMarkedArea addAsMarked(String toAdd, LinPosition position, String language) {
protected MarkedArea addAsMarked(String toAdd, LinPosition position, String language) {
/** the length of the displayed HTML before the current append */
int oldLengthHtml = 0;
if (doHtml) {
@@ -187,7 +209,7 @@ class Display {
if (doHtml) {
final String newStageHtml = this.linStagesHtml.lastElement().toString();
final String newHtml = Printname.htmlPrepend(newStageHtml, "");
//yeah, daniels admits, this IS probably expensive
//yeah, daniels admits, this IS expensive
this.htmlLengthPane.setText(newHtml);
newLengthHtml = htmlLengthPane.getDocument().getLength();
if (newLengthHtml < oldLengthHtml) {
@@ -199,7 +221,7 @@ class Display {
if (doText) {
newLengthText = this.linStagesText.lastElement().toString().length();
}
final HtmlMarkedArea hma = new HtmlMarkedArea(oldLengthText, newLengthText, position, toAdd, oldLengthHtml, newLengthHtml, language);
final MarkedArea hma = new MarkedArea(oldLengthText, newLengthText, position, toAdd, oldLengthHtml, newLengthHtml, language);
return hma;
}
/**
@@ -210,6 +232,15 @@ class Display {
* To store the scroll state of the HTML linearization area
*/
Rectangle recHtml = new Rectangle();
/**
* To store the scroll state of the pure text linearization area
*/
int scrollText = 0;
/**
* To store the scroll state of the HTML linearization area
*/
int scrollHtml = 0;
public String toString() {

113
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/DynamicTree2.java
View File

@@ -29,21 +29,28 @@ import java.util.logging.*;
//import de.uka.ilkd.key.util.KeYResourceManager;
import java.awt.event.*;
//import java.net.URL;
public class DynamicTree2 extends JPanel implements KeyListener,
ActionListener{
/**
* A GUI class, does store the tree, but does not create it.
* The tree is created in GFEditor2.
* This class displays the tree and let the user interact with it via mouse clicks.
*/
public class DynamicTree2 extends JPanel implements KeyListener {
protected static Logger logger = Logger.getLogger(DynamicTree2.class.getName());
public DefaultMutableTreeNode rootNode;
protected DefaultTreeModel treeModel;
private DefaultTreeModel treeModel;
public JTree tree;
public int oldSelection = 0;
private Toolkit toolkit = Toolkit.getDefaultToolkit();
public JPopupMenu popup = new JPopupMenu();
JMenuItem menuItem;
private GFEditor2 gfeditor;
protected TreePath oldSelection = null;
/**
* Initializes the display state of the tree panel, sets up the
* event handlers.
* Does not initialize the tree.
* @param gfe The editor object this object belongs to.
*/
public DynamicTree2(GFEditor2 gfe) {
this.gfeditor = gfe;
@@ -54,12 +61,8 @@ ActionListener{
tree = new JTree(treeModel);
tree.setRootVisible(false);
tree.setEditable(false);
tree.getSelectionModel().setSelectionMode
(TreeSelectionModel.SINGLE_TREE_SELECTION);
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();
@@ -72,33 +75,29 @@ ActionListener{
* gfeditor.nodeTable contains the positions for all selectionPathes.
*/
public void valueChanged(TreeSelectionEvent e) {
if ((tree.getSelectionPath() != null) && tree.getSelectionPath().equals(oldSelection)) {
//nothing to be done here, probably
//triggered by showTree
return;
}
if (tree.getSelectionRows() != null) {
if (gfeditor.nodeTable == null) {
if (GFEditor2.treeLogger.isLoggable(Level.FINER)) {
GFEditor2.treeLogger.finer("null node table");
}
} else {
if (GFEditor2.treeLogger.isLoggable(Level.FINER)) {
GFEditor2.treeLogger.finer("node table: " + gfeditor.nodeTable.contains(new Integer(0)) + " " + gfeditor.nodeTable.keys().nextElement());
}
}
if (tree.getSelectionPath() == null) {
if (GFEditor2.treeLogger.isLoggable(Level.FINER)) {
GFEditor2.treeLogger.finer("null root path");
if (logger.isLoggable(Level.FINER)) {
logger.finer("null root path");
}
} else {
if (GFEditor2.treeLogger.isLoggable(Level.FINER)) {
GFEditor2.treeLogger.finer("selected path" + tree.getSelectionPath());
if (logger.isLoggable(Level.FINER)) {
logger.finer("selected path" + tree.getSelectionPath());
}
}
String pos = (String)gfeditor.nodeTable.get(tree.getSelectionPath());
String pos = gfeditor.getNodePosition(tree.getSelectionPath());
if (pos == null || "".equals(pos)) {
//default to sth. sensible
pos = "[]";
}
gfeditor.treeChanged = true;
gfeditor.send("mp " + pos);
gfeditor.send("[t] mp " + pos);
}
oldSelection = tree.getSelectionPath();
}
});
@@ -112,10 +111,20 @@ ActionListener{
add(scrollPane);
}
/**
* Remove all nodes in the tree and
* form a dummy tree in treePanel
*/
protected void resetTree() {
((DefaultTreeModel)(tree.getModel())).setRoot(new DefaultMutableTreeNode("Root"));
((DefaultTreeModel)(tree.getModel())).reload();
}
/** Remove all nodes except the root node. */
public void clear() {
rootNode.removeAllChildren();
treeModel.reload();
((DefaultTreeModel)(tree.getModel())).setRoot(null);
oldSelection = null;
//((DefaultTreeModel)(tree.getModel())).reload();
}
/** Remove the currently selected node. */
@@ -218,9 +227,9 @@ ActionListener{
exc.printStackTrace();
}
if (GFEditor2.treeLogger.isLoggable(Level.FINER)) {
GFEditor2.treeLogger.finer("The user has finished editing the node.");
GFEditor2.treeLogger.finer("New value: " + node.getUserObject());
if (logger.isLoggable(Level.FINER)) {
logger.finer("The user has finished editing the node.");
logger.finer("New value: " + node.getUserObject());
}
}
public void treeNodesInserted(TreeModelEvent e) {
@@ -234,6 +243,10 @@ ActionListener{
}
}
/**
* This tree cell renderer got overwritten to make it possible to show
* tooltips according to the user object
*/
private class MyRenderer extends DefaultTreeCellRenderer {
//int counter = 0;
//final ImageIcon iconFilled;
@@ -245,7 +258,11 @@ ActionListener{
// iconOpen = new ImageIcon(urlOpen);
// iconFilled = new ImageIcon(urlFilled);
// }
/**
* The heart of this class, sets display and tooltip text
* depending on the user data
*/
public Component getTreeCellRendererComponent(
JTree tree,
Object value,
@@ -264,6 +281,10 @@ ActionListener{
if (node.getUserObject() instanceof AstNodeData) {
AstNodeData and = (AstNodeData)node.getUserObject();
String ptt = and.getParamTooltip();
if (!and.subtypingStatus ) {
this.setForeground(Color.RED);
ptt = Printname.htmlAppend(ptt, "<p>Subtyping proof is missing. <br>If no refinements are offered here, then there is a subtyping error.");
}
this.setToolTipText(ptt);
this.setText(and.toString());
// if (and.isMeta()) {
@@ -309,12 +330,6 @@ ActionListener{
class PopupListener extends MouseAdapter {
public void mousePressed(MouseEvent e) {
int selRow = tree.getRowForLocation(e.getX(), e.getY());
tree.setSelectionRow(selRow);
if (GFEditor2.treeLogger.isLoggable(Level.FINER)) {
GFEditor2.treeLogger.finer("selection changed!");
}
//for the popup or parse field, do the same as for the linearization areas
gfeditor.maybeShowPopup(e);
}
@@ -323,11 +338,9 @@ ActionListener{
}
}
public void actionPerformed(ActionEvent ae) {
//nothing to be done here
}
/** Handle the key pressed event. */
/**
* Handle the key pressed event.
*/
public void keyPressed(KeyEvent e) {
int keyCode = e.getKeyCode();
switch (keyCode){
@@ -335,11 +348,15 @@ ActionListener{
case KeyEvent.VK_DELETE : gfeditor.send("d"); break;
}
}
/** Handle the key typed event. */
/**
* Handle the key typed event.
*/
public void keyTyped(KeyEvent e) {
//nothing to be done here
}
/** Handle the key released event. */
/**
* Handle the key released event.
*/
public void keyReleased(KeyEvent e) {
//nothing to be done here
}

67
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ExportFormatMenu.java Normal file
View File

@@ -0,0 +1,67 @@
// This file is part of KeY - Integrated Deductive Software Design
// Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
// Universitaet Koblenz-Landau, Germany
// Chalmers University of Technology, Sweden
//
// The KeY system is protected by the GNU General Public License.
// See LICENSE.TXT for details.
//
package de.uka.ilkd.key.ocl.gf;
import javax.swing.*;
import java.awt.*;
import java.awt.event.*;
/** Provide a choice of output formats: OCL or Natural Language. NL can be
* formatted using either HTML or LaTeX.
*/
public class ExportFormatMenu extends JPanel
{
public static int OCL = 0, HTML=1, LATEX=2;
private static String[] menuStrings = { "OCL",
"Natural Language/HTML (requires GF)",
"Natural Language/LaTeX (requires GF)"
};
private JComboBox formatMenu;
private int selection;
private ActionListener al = new ActionListener() {
public void actionPerformed(ActionEvent e) {
JComboBox cb = (JComboBox) e.getSource();
String s = (String) cb.getSelectedItem();
if (s.equals("OCL")) {
selection = OCL;
} else if (s.equals("Natural Language/HTML (requires GF)")) {
selection = HTML;
} else if (s.equals("Natural Language/LaTeX (requires GF)")) {
selection = LATEX;
} else { // should never occur
selection = OCL;
};
}
};
public ExportFormatMenu()
{
super();
this.setLayout(new BoxLayout(this,BoxLayout.Y_AXIS));
formatMenu = new JComboBox(menuStrings);
formatMenu.setSelectedIndex(0);
formatMenu.addActionListener(al);
this.add(Box.createVerticalGlue());
JLabel text = new JLabel("Choose output format:");
this.add(text);
text.setAlignmentX(Component.CENTER_ALIGNMENT);
this.add(formatMenu);
}
public int getSelection()
{
return selection;
}
}

63
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFCommand.java
View File

@@ -29,51 +29,78 @@ package de.uka.ilkd.key.ocl.gf;
*/
abstract class GFCommand implements Comparable{
/** the subcategory of this command */
/**
* the subcategory of this command
*/
public abstract String getSubcat();
/** the type of the command, r,w,ch,d,ac,... */
/**
* the type of the command, r,w,ch,d,ac,...
*/
protected String commandType;
/** the type of the command, r,w,ch,d,ac,... */
/**
* the type of the command, r,w,ch,d,ac,...
*/
public String getCommandType(){
return commandType;
}
/** for wrap, the number of the argument the current node should become */
/**
* for wrap, the number of the argument the current node should become
*/
protected int argument;
/**the actual command that this object should represent */
/**
* the actual command that this object should represent
*/
protected String command;
/**the actual command that this object should represent */
/**
* the actual command that this object should represent
*/
public String getCommand() {
return command;
}
/**the Printname corresponding to the GF fun of this command*/
/**
* the Printname corresponding to the GF fun of this command
*/
protected Printname printname;
/**the Printname corresponding to the GF fun of this command*/
/**
* the Printname corresponding to the GF fun of this command
*/
public Printname getPrintname(){
return printname;
}
/**the text that is to be displayed as the tooltip */
/**
* the text that is to be displayed as the tooltip
*/
public abstract String getTooltipText();
/** the text that is to be displayed in the refinement lists */
/**
* the text that is to be displayed in the refinement lists
*/
public abstract String getDisplayText();
/** the name of the fun that is used in this command */
/**
* the name of the fun that is used in this command
*/
protected String funName;
/** if this is the first occurence of the current subcat */
/**
* if this is the first occurence of the current subcat
*/
protected boolean newSubcat;
/** if this is the first occurence of the current subcat */
/**
* if this is the first occurence of the current subcat
*/
public boolean isNewSubcat() {
return newSubcat;
}
/**
* Compares two GFCommands.
* LinkCommands are the least. InputCommands the greatest. If that does not decide,
* the display name as a String does.
* LinkCommands are the least. Then the InputCommand (more than one
* does not happen). If that does not decide, the display name as a String does.
* @param o the other command.
* @return see above.
*/
@@ -87,11 +114,12 @@ abstract class GFCommand implements Comparable{
if (!(this instanceof LinkCommand) && (o instanceof LinkCommand)) {
return 1;
}
//LinkCommands are dealt with, so from now on, they don't occur
if (this instanceof InputCommand && !(o instanceof InputCommand)) {
return 1;
return -1;
}
if (!(this instanceof InputCommand) && (o instanceof InputCommand)) {
return -1;
return 1;
}
if (! (o instanceof GFCommand)) {
//This should never occur!
@@ -100,7 +128,6 @@ abstract class GFCommand implements Comparable{
GFCommand ocmd = (GFCommand)o;
return this.getDisplayText().compareTo(ocmd.getDisplayText());
}
}
public String toString() {

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

File diff suppressed because it is too large Load Diff

79
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GfAstNode.java
View File

@@ -18,11 +18,21 @@ package de.uka.ilkd.key.ocl.gf;
/**
* @author daniels
* This Class represents a parsed node in the GF AST.
* It knows about types, bound variables, funs.
* But nothing about printnames. That's what AstNodeData is for.
*/
class GfAstNode {
/**
* contains the types of the bound variables in the order of their occurence
*/
protected final String[] boundTypes;
/**
* contains the names of the bound variables in the order of their occurence
*/
protected final String[] boundNames;
/** The type of this AST node */
/**
* The type of this AST node
*/
private final String type;
/**
* @return The type of this AST node
@@ -30,8 +40,11 @@ class GfAstNode {
protected String getType() {
return type;
}
/** the fun represented in this AST node */
/**
* the fun represented in this AST node
*/
private final String fun;
/**
* @return the fun represented in this AST node.
* Can be a metavariable like "?1"
@@ -39,6 +52,7 @@ class GfAstNode {
protected String getFun() {
return fun;
}
/**
* @return true iff the node is a metavariable, i.e. open and not
* yet refined.
@@ -46,7 +60,9 @@ class GfAstNode {
protected boolean isMeta() {
return fun.startsWith("?");
}
/** the line that was used to build this node */
/**
* the line that was used to build this node
*/
private final String line;
/**
* @return the line that was used to build this node
@@ -54,6 +70,11 @@ class GfAstNode {
protected String getLine() {
return line;
}
/**
* The constraint attached to this node
*/
public final String constraint;
/**
* feed this constructor the line that appears in the GF AST and
@@ -63,7 +84,15 @@ class GfAstNode {
protected GfAstNode(final String line) {
this.line = line.trim();
final int index = this.line.lastIndexOf(" : ");
this.type = this.line.substring(index + 3);
String typeString = this.line.substring(index + 3);
final int constraintIndex = typeString.indexOf(" {");
if (constraintIndex > -1) {
this.constraint = typeString.substring(constraintIndex + 1).trim();
this.type = typeString.substring(0, constraintIndex).trim();
} else {
this.constraint = "";
this.type = typeString;
}
String myFun = this.line.substring(0, index);
if (myFun.startsWith("\\(")) {
final int end = myFun.lastIndexOf(") -> ");
@@ -89,46 +118,4 @@ class GfAstNode {
public String toString() {
return this.line;
}
public static void main(String[] args) {
String[] lines = {"?1 : Sent",
"Two : Instance Integer",
"?3 : Instance (Collection (?{this:=this{-0-}}))",
"NOPACKAGEP_StartC_Constr : Constraint {Constraint<>NOPACKAGEP_StartC_Constr (\\this -> invCt ?)}",
"\\(this : VarSelf NOPACKAGEP_StartC) -> invCt : ClassConstraintBody",
"\\(x_0 : Instance Integer) -> ?6 : Sent",
"\\(selfGF : VarSelf NOPACKAGEP_PayCardC),(amount : Instance Integer) -> preC : OperConstraintBody",
"\\(selfGF : VarSelf NOPACKAGEP_PayCardC),(amount : Instance Integer) -> ?0 : OperConstraintBody"
};
String[] funs = {"?1",
"Two",
"?3",
"NOPACKAGEP_StartC_Constr",
"invCt",
"?6",
"preC",
"?0"
};
String[] types = {"Sent",
"Instance Integer",
"Instance (Collection (?{this:=this{-0-}}))",
"Constraint {Constraint<>NOPACKAGEP_StartC_Constr (\\this -> invCt ?)}",
"ClassConstraintBody",
"Sent",
"OperConstraintBody",
"OperConstraintBody"
};
for (int i = 0; i < lines.length; i++) {
System.out.println("* " + lines[i]);
GfAstNode gfa = new GfAstNode(lines[i]);
if (!gfa.getFun().equals(funs[i])) {
System.out.println(" fun mismatch: expected '" + funs[i] + "', got '" + gfa.getFun() + "'");
}
if (!gfa.getType().equals(types[i])) {
System.out.println(" type mismatch: expected '" + types[i] + "', got '" + gfa.getType() + "'");
}
}
}
}

621
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GfCapsule.java Normal file
View File

@@ -0,0 +1,621 @@
//Copyright (c) Janna Khegai 2004, 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.File;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.OutputStreamWriter;
import java.util.Vector;
import java.util.logging.Level;
import java.util.logging.Logger;
import javax.swing.JFrame;
import javax.swing.JOptionPane;
import javax.swing.ProgressMonitor;
class GfCapsule {
/**
* XML parsing debug messages
*/
private static Logger xmlLogger = Logger.getLogger(GfCapsule.class.getName() + ".xml");
/**
* generic logging of this class
*/
private static Logger logger = Logger.getLogger(GfCapsule.class.getName());
/**
* The output from GF is in here.
* Only the read methods, initializeGF and the prober objects access this.
*/
BufferedReader fromProc;
/**
* Used to leave messages for GF here.
* But <b>only</b> in send and special probers that clean up with undo
* after them (or don't change the state like PrintnameLoader).
*/
BufferedWriter toProc;
/**
* Starts GF with the given command gfcmd in another process.
* Sets up the reader and writer to that process.
* Does in it self not read anything from GF.
* @param gfcmd The complete command to start GF, including 'gf' itself.
*/
public GfCapsule(String gfcmd){
try {
Process extProc = Runtime.getRuntime().exec(gfcmd);
InputStreamReader isr = new InputStreamReader(
extProc.getInputStream(),"UTF8");
this.fromProc = new BufferedReader (isr);
String defaultEncoding = isr.getEncoding();
if (logger.isLoggable(Level.FINER)) {
logger.finer("encoding "+defaultEncoding);
}
this.toProc = new BufferedWriter(new OutputStreamWriter(extProc.getOutputStream(),"UTF8"));
} catch (IOException e) {
JOptionPane.showMessageDialog(new JFrame(), "Could not start " + gfcmd+
"\nCheck your $PATH", "Error",
JOptionPane.ERROR_MESSAGE);
throw new RuntimeException("Could not start " + gfcmd+
"\nCheck your $PATH");
}
}
/**
* Does the actual writing of command to the GF process via STDIN
* @param command exactly the string that is going to be sent
*/
protected void realSend(String command) {
try {
toProc.write(command, 0, command.length());
toProc.newLine();
toProc.flush();
} catch (IOException e) {
System.err.println("Could not write to external process " + e);
}
}
/**
* reads the part between &gt;gfinit&lt; and &gt;/gfinit&lt;
* @return the data for the new category menu
*/
protected NewCategoryMenuResult readGfinit() {
try {
//read <hmsg> or <newcat> or <topic> (in case of no grammar loaded)
String readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("12 "+readresult);
//when old grammars are loaded, the first line looks like
//"reading grammar of old format letter.Abs.gfreading old file letter.Abs.gf<gfinit>"
if (readresult.indexOf("<gfinit>") > -1) {
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("12 "+readresult);
}
//no command appendix expected or applicable here, so appendix is discarded
Hmsg hmsg = readHmsg(readresult);
String next = hmsg.lastline;
//no hmsg supported here. Wouldn't be applicable.
//the reading above is to silently ignore it intead of failing.
//formHmsg(hmsg);
if ((next!=null) && ((next.indexOf("newcat") > -1)
|| (next.indexOf("topic") > -1))) {
NewCategoryMenuResult ncmr = readNewMenu();
return ncmr;
}
} catch (IOException e) {
System.err.println("Could not read from external process:\n" + e);
}
return null;
}
/**
* reads the greeting text from GF
* @return S tuple with first = the last read GF line,
* which should be the first loading line
* and second = The greetings string
*/
protected StringTuple readGfGreetings() {
try {
String readresult = "";
StringBuffer outputStringBuffer = new StringBuffer();
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("1 "+readresult);
while ((readresult.indexOf("gf")==-1) && (readresult.trim().indexOf("<") < 0)){
outputStringBuffer.append(readresult).append("\n");
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("1 "+readresult);
}
return new StringTuple(readresult, outputStringBuffer.toString());
} catch (IOException e) {
System.err.println("Could not read from external process:\n" + e);
return new StringTuple("", e.getLocalizedMessage());
}
}
/**
* reads the loading and compiling messages from GF
* @param readresult the first loading line
* @param pm to monitor the loading progress. May be null
* @return A tuple with first = the first line from &gt;gfinit&lt; or &gt;gfedit&lt;
* and second = the loading message as pure text
*/
protected StringTuple readGfLoading(String readresult, ProgressMonitor pm) {
try {
// in case nothing has been loaded first, the that has to be done now
if (readresult == null) {
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("1 " + readresult);
}
StringBuffer textPure = new StringBuffer();
int progress = 5300;
while (!(readresult.indexOf("<gfinit>") > -1 || (readresult.indexOf("<gfmenu>") > -1))){
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("1 "+readresult);
textPure.append(readresult).append("\n");
progress += 12;
Utils.tickProgress(pm, progress, null);
}
//when old grammars are loaded, the first line looks like
//"reading grammar of old format letter.Abs.gfreading old file letter.Abs.gf<gfinit>"
//without newlines
final int beginInit = readresult.indexOf("<gfinit>");
if (beginInit > 0) {
textPure.append(readresult.substring(0, beginInit)).append("\n");
//that is the expected result
readresult = "<gfinit>";
}
return new StringTuple(readresult, textPure.toString());
} catch (IOException e) {
System.err.println("Could not read from external process:\n" + e);
return new StringTuple("", e.getLocalizedMessage());
}
}
/**
* Reads the &lt;gfedit&gt; part from GF's XML output.
* The different subtags are put into the result
* @param newObj If a new object in the editor has been started.
* If the to-be-read hmsg contains the newObject flag,
* that overwrites this parameter
* @return the read tags, partially halfy parsed, partially raw.
* The way the different form methods expect it.
*/
protected GfeditResult readGfedit(boolean newObj) {
try {
String next = "";
//read <gfedit>
String readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("11 "+readresult);
//read either <hsmg> or <lineatization>
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("11 "+readresult);
//hmsg stuff
final Hmsg hmsg = readHmsg(readresult);
next = hmsg.lastline;
//reading <linearizations>
//seems to be the only line read here
//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);
} else {
System.exit(0);
}
}
readresult = next;
String lin = readLin();
final String treeString = readTree();
final String message = readMessage();
//read the menu stuff
Vector gfCommandVector;
if (newObj || hmsg.newObject) {
gfCommandVector = readRefinementMenu();
} else {
while(readresult.indexOf("</menu")==-1) {
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("12 " + readresult);
}
gfCommandVector = null;
}
// "" 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);
}
//all well, return the read stuff
return new GfeditResult(gfCommandVector, hmsg, lin, message, treeString);
} catch (IOException e) {
System.err.println("Could not read from external process:\n" + e);
}
//nothing well, return bogus stuff
return new GfeditResult(new Vector(), new Hmsg("", "", false, false, false, false, true), "", "", "");
}
/**
* reads the linearizations in all language.
* seems to expect the first line of the XML structure
* (< lin) already to be read
* Accumulates the GF-output between <linearization> </linearization> tags
*/
protected String readLin(){
StringBuffer lins = new StringBuffer();
try {
//read <linearizations>
String readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 " + readresult);
lins.append(readresult).append('\n');
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);
while ((readresult != null) && (readresult.indexOf("/linearization") == -1)){
lins.append(readresult).append('\n');
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("6 " + readresult);
}
} catch(IOException e){
System.err.println(e.getMessage());
e.printStackTrace();
}
return lins.toString();
}
/**
* 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 String readTree(){
String treeString = "";
try {
//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);
}
return treeString;
} catch(IOException e){
System.err.println(e.getMessage());
e.printStackTrace();
return null;
}
}
/**
* Parses the GF-output between <message> </message> tags
* and returns it.
* @return The read message.
*/
protected String readMessage(){
String s ="";
try {
// 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);
}
return s;
} catch(IOException e){
System.err.println(e.getLocalizedMessage());
e.printStackTrace();
return e.getLocalizedMessage();
}
}
/**
* reads the cat entries and puts them into result.menuContent,
* after that reads
* the names of the languages and puts them into the result.languages
* The loaded grammar files are put into result.paths,
* a guessed grammar name into result.grammarName
* Parses the GF-output between <gfinit> tags
*/
protected NewCategoryMenuResult readNewMenu () {
//here the read stuff is sorted into
String grammarName = "";
final Vector languages = new Vector();
final Vector menuContent = new Vector();
final Vector paths = new Vector();
boolean more = true;
try {
//read first cat
String readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) {
xmlLogger.finer("2 " + readresult);
}
if (readresult.indexOf("(none)") > -1) {
//no topics present
more = false;
}
while (more){
//adds new cat s to the menu
if (readresult.indexOf("topic") == -1) {
final String toAdd = readresult.substring(6);
menuContent.add(toAdd);
} else {
more = false;
}
//read </newcat
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("2 " + readresult);
//read <newcat (normally)
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
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("4 " + readresult);
}
//set topic
grammarName = readresult.substring(4) + " ";
//read </topic>
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("2 " + readresult);
//read <language>
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("3 " + readresult);
//read actual language
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 ((readresult.indexOf("/gfinit") == -1)
&& (readresult.indexOf("lin") == -1)) {
//form lang and Menu menu:
final String langName = readresult.substring(4);
languages.add(langName);
} else {
more = false;
}
// read </language>
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("2 " + readresult);
// read <language> or </gfinit...>
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("3 " + readresult);
if ((readresult.indexOf("/gfinit") != -1)
|| (readresult.indexOf("lin") != -1)) {
more = false;
}
// registering the file name:
if (readresult.indexOf("language") != -1) {
String path = readresult.substring(readresult.indexOf('=') + 1,
readresult.indexOf('>'));
path = path.substring(path.lastIndexOf(File.separatorChar) + 1);
if (xmlLogger.isLoggable(Level.FINE)) xmlLogger.fine("language: " + path);
paths.add(path);
}
// 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){
xmlLogger.warning(e.getMessage());
}
String[] menuContentArray = Utils.vector2Array(menuContent);
String[] languagesArray = Utils.vector2Array(languages);
String[] pathsArray = Utils.vector2Array(paths);
NewCategoryMenuResult result = new NewCategoryMenuResult(grammarName, menuContentArray, languagesArray, pathsArray);
return result;
}
/**
* Reads the hmsg part of the XML that is put out from GF.
* Everything in [] given in front of a GF command will be rewritten here.
* This method does nothing when no hmsg part is present.
*
* If a '$' appears in this string, everything that comes after it
* will be in result.second.
* ;; and [] don't work in the [] for the hmsg,
* therfore the following replacements are done:
* %% for ;;
* ( for [
* ) for ]
*
* If one of the characters c,t,n comes before, the following is done:
* c The output will be cleared before the linearization (TODO: done anyway?)
* t The treeChanged flag will be set to true
* n The newObject flag will be set to true
* p No other probing run should be done (avoid cycles)
* r To prevent the execution of automatically triggered commands to prevent recursion
*
* @param prevreadresult The last line read from GF
* @return first: the last line this method has read;
* second: the string after $, null if that is not present
*/
protected Hmsg readHmsg(String prevreadresult){
if ((prevreadresult!=null)&&(prevreadresult.indexOf("<hmsg>") > -1)) {
StringBuffer s =new StringBuffer("");
String commandAppendix = null;
try {
boolean onceAgain = true;
boolean recurse = true;
boolean newObj = false;
boolean treeCh = false;
boolean clear = false;
String readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 "+readresult);
while (readresult.indexOf("/hmsg")==-1){
s.append(readresult).append('\n');
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 "+readresult);
}
int commandAppendixStart = s.indexOf("$");
if (commandAppendixStart > -1 && commandAppendixStart < s.length() - 1) { //present, but not the last character
commandAppendix = s.substring(commandAppendixStart + 1, s.indexOf("\n")); //two \n trail the hmsg
//;; and [] don't work in the [] for the hmsg
commandAppendix = Utils.replaceAll(commandAppendix, "%%", ";;");
commandAppendix = Utils.replaceAll(commandAppendix, "(", "[");
commandAppendix = Utils.replaceAll(commandAppendix, ")", "]");
} else {
commandAppendixStart = s.length();
}
if (s.indexOf("c") > -1 && s.indexOf("c") < commandAppendixStart) {
//clear output before linearization
clear = true;
}
if (s.indexOf("t") > -1 && s.indexOf("t") < commandAppendixStart) {
//tree has changed
treeCh = true;
}
if (s.indexOf("p") > -1 && s.indexOf("p") < commandAppendixStart) {
//we must not probe again
onceAgain = false;
}
if (s.indexOf("r") > -1 && s.indexOf("r") < commandAppendixStart) {
//we must not probe again
recurse = false;
}
if (s.indexOf("n") > -1 && s.indexOf("n") < commandAppendixStart) {
//a new object has been created
newObj = true;
}
if (logger.isLoggable(Level.FINE)) {
if (commandAppendix != null) {
logger.fine("command appendix read: '" + commandAppendix + "'");
}
}
return new Hmsg(readresult, commandAppendix, onceAgain, recurse, newObj, treeCh, clear);
} catch(IOException e){
System.err.println(e.getMessage());
e.printStackTrace();
return new Hmsg("", null, false, true, false, true, false);
}
} else {
return new Hmsg(prevreadresult, null, true, true, false, true, false);
}
}
/**
* Parses the GF-output between <menu> and </menu> tags
* and puts a StringTuple for each show/send pair into the
* return vector.
* @return A Vector of StringTuple as described above
*/
protected Vector readRefinementMenu (){
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("list model changing! ");
String s ="";
Vector printnameVector = new Vector();
Vector commandVector = new Vector();
Vector gfCommandVector = new Vector();
try {
//read <menu>
String readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("7 " + readresult);
//read item
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
while (readresult.indexOf("/menu")==-1){
//read show
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 += readresult;
}
}
// if (s.charAt(0)!='d')
// listModel.addElement("Refine " + s);
// else
String showText = s;
printnameVector.addElement(s);
s = "";
//read /show
//read send
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)
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
// read /item
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
readresult = fromProc.readLine();
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("8 " + readresult);
StringTuple st = new StringTuple(myCommand.trim(), showText);
gfCommandVector.addElement(st);
}
} catch(IOException e){
System.err.println(e.getMessage());
e.printStackTrace();
}
return gfCommandVector;
}
/**
* Reads the output from GF until the ending tag corresponding to the
* given opening tag is read.
* @param opening tag in the format of &gt;gfinit&lt;
*/
protected void skipChild(String opening) {
String closing = (new StringBuffer(opening)).insert(1, '/').toString();
try {
String nextRead = fromProc.readLine();
if (logger.isLoggable(Level.FINER)) {
logger.finer("3 " + nextRead);
}
while (!nextRead.trim().equals(closing)) {
nextRead = fromProc.readLine();
if (logger.isLoggable(Level.FINER)) {
logger.finer("3 " + nextRead);
}
}
} catch (IOException e) {
System.err.println("Could not read from external process:\n" + e);
}
}
}

61
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GfeditResult.java Normal file
View File

@@ -0,0 +1,61 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.Vector;
/**
* Encapsulates the &lt;gfedit&gt; XML tree from GF.
* @author hdaniels
*/
class GfeditResult {
/**
* The fully parsed &lt;hmsg&gt; subtree
*/
final Hmsg hmsg;
/**
* A Vector of StringTuple where first is the command for GF
* and second is the show text
*/
final Vector gfCommands;
/**
* The tree from GF isn't XML anyway, so here it is in all its raw glory
*/
final String treeString;
/**
* if GF had something extra to tell, it can be found here
*/
final String message;
/**
* The XML for the linearizations in all languages
*/
final String linearizations;
/**
* A simple setter constructor
* @param gfCommands A Vector of StringTuple where first is the command for GF
* and second is the show text
* @param hmsg The fully parsed &lt;hmsg&gt; subtree
* @param linearizations The XML for the linearizations in all languages
* @param message the GF message
* @param treeString The tree from GF
*/
public GfeditResult(Vector gfCommands, Hmsg hmsg, String linearizations, String message, String treeString) {
this.gfCommands = gfCommands;
this.hmsg = hmsg;
this.linearizations = linearizations;
this.message = message;
this.treeString = treeString;
}
}

77
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Hmsg.java Normal file
View File

@@ -0,0 +1,77 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/**
* The parsed format of the hmsg, that GF sents, if a command in java mode
* was prefixed with [something].
* And that something gets parsed and stored in this representation.
* @author daniels
*/
class Hmsg {
/**
* The last read line
*/
String lastline = "";
/**
* the String that should be appended to all commands of the
* next refinement menu
*/
String appendix = null;
/**
* If the editor shall probe once again for missing subtyping witnesses.
* Unused.
*/
boolean onceAgain = false;
/**
* If false, no commands are executed automatically
* in the next GF reading run
*/
boolean recurse = false;
/**
* if the newObject flag should be set
*/
boolean newObject = false;
/**
* if the command changed the tree, so that it has to be rebuilt
*/
boolean treeChanged = false;
/**
* if the display should be cleared
*/
boolean clear = false;
/**
* A simple setter constructor
* @param lastRead The last read line
* @param appendix the String that should be appended to all commands of the
* next refinement menu
* @param onceAgain
* @param recurse If false, no commands are executed automatically
* in the next GF reading run
* @param newObject if the newObject flag should be set
* @param treeChanged if the command changed the tree, so that it has to be rebuilt
* @param clear if the display should get cleared
*/
public Hmsg(String lastRead, String appendix, boolean onceAgain, boolean recurse, boolean newObject, boolean treeChanged, boolean clear) {
this.lastline = lastRead;
this.appendix = appendix;
this.onceAgain = onceAgain;
this.recurse = recurse;
this.newObject = newObject;
this.treeChanged = treeChanged;
this.clear = clear;
}
}

63
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/HtmlMarkedArea.java
View File

@@ -1,63 +0,0 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/**
* @author daniels
*
* An extender of MarkedArea that adds additional fields for the click-in
* functionality for HTML
*/
class HtmlMarkedArea extends MarkedArea {
/** the start index in the HTML area */
final public int htmlBegin;
/** the end index in the HTML area */
final public int htmlEnd;
/**
* A stand-alone constuctor which takes all values as arguments
* @param b The starting position of the stored words
* @param e The ending position of the stored words
* @param p The position in the AST
* @param w The actual text of this area
* @param hb the start index in the HTML area
* @param he the end index in the HTML area
* @param lang the language of the current linearization
*/
public HtmlMarkedArea(int b, int e, LinPosition p, String w, int hb, int he, String lang) {
super(b, e, p, w, lang);
this.htmlBegin = hb;
this.htmlEnd = he;
}
/**
* Creates a copy of orig, but with additional fields for the click-
* in functionality for HTML
* @param orig the original MarkedArea that should be extended
* @param hb the start index in the HTML area
* @param he the end index in the HTML area
*/
HtmlMarkedArea(final MarkedArea orig, final int hb, final int he) {
super(orig.begin, orig.end, orig.position, orig.words, orig.language);
this.htmlBegin = hb;
this.htmlEnd = he;
}
public String toString() {
return begin + " - " + end + " : " + position + " = '" + words + "' ; HTML: " + htmlBegin + " - " + htmlEnd;
}
}

47
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/InputCommand.java
View File

@@ -14,13 +14,14 @@
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.HashSet;
/**
* @author daniels
*
* This class represents a fake command, i.e. nothing is send to GF here.
* Instead this class acts more like a placeholder for the input dialog.
* This dialog is handled in GFEditor2 when a InputCommand is executed.
* This class represents a fake command, i.e. nothing is send to GF here.
* Instead this class acts more like a placeholder for the input dialog.
* This dialog is handled in GFEditor2 when a InputCommand is executed.
* Reason: No GUI stuff in the command.
*/
class InputCommand extends GFCommand {
@@ -43,35 +44,56 @@ class InputCommand extends GFCommand {
protected Class type;
/**the text that is to be displayed as the title in the input window */
/**
* the text that is to be displayed as the title in the input window
*/
protected final String titleText;
/**the text that is to be displayed as the title in the input window */
/**
* the text that is to be displayed as the title in the input window
*/
public String getTitleText() {
return titleText;
}
/**
* stores the entered values, so they can be offered to the user
* the next time, in case, he wants them again.
*/
protected final HashSet enteredValues = new HashSet();
/**the text that is to be displayed as the tooltip */
/**
* the text that is to be displayed as the tooltip
*/
protected final String tooltipText;
/**the text that is to be displayed as the tooltip */
/**
* the text that is to be displayed as the tooltip
*/
public String getTooltipText() {
return tooltipText;
}
/** the text that is to be displayed in the refinement lists */
/**
* the text that is to be displayed in the refinement lists
*/
protected final String displayText;
/** the text that is to be displayed in the refinement lists */
/**
* the text that is to be displayed in the refinement lists
*/
public String getDisplayText() {
return displayText;
}
/** the subcategory of this command */
/**
* the subcategory of this command
*/
public String getSubcat() {
return null;
}
/**
* Checks if the given String can be converted into
* the Type of this InputCommand (int or String)
* the Type of this InputCommand (int or String).
* If that is possible, the converted object is saved
* in enteredValues for later redisplay for the user.
* @param o The String the user has typed
* @param reason If the entered String is not parseable as the expected
* type, an error message is appended to this StringBuffer, so better
@@ -95,6 +117,9 @@ class InputCommand extends GFCommand {
result = "\"" + o.toString() + "\"";
}
}
if (result != null) {
this.enteredValues.add(result);
}
return result;
}

39
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LanguageManager.java Normal file
View File

@@ -0,0 +1,39 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/**
* Sadly, this class is a hack.
* It serves as the pointer type to an inner class of GFEditor2.
* Two of its methods are needed outside after refactoring.
* @author daniels
*
*/
interface LanguageManager {
/**
* @param myLang The language in question
* @return true iff the language is present and set to active,
* false otherwise.
*/
public boolean isLangActive(String myLang);
/**
* Checks if myLang is already present, and if not,
* adds it. In that case, myActive is ignored.
* @param myLang The name of the language
* @param myActive whether the language is displayed or not
*/
public void add(String myLang, boolean myActive);
}

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

@@ -63,10 +63,30 @@ class LinPosition {
if ("[]".equals(pos)) {
return "[" + nr + "]";
} else {
return pos.substring(0, pos.length() - 1) + "," + nr + "]";
return pos.trim().substring(0, pos.length() - 1) + "," + nr + "]";
}
}
/**
* Creates a position string in Haskell notation for the argument
* number nr for the position pos' parent, i.e. brethren number nr.
* Example: calculateBrethrenPosition("[0,0,1]", 3).equals("[0,0,3]")
* @param pos The position of a brethren of the wanted
* @param nr The number of the wanted brethren
* @return the position string for the nrth brother of pos
*/
protected static String calculateBrethrenPosition(String pos, int nr) {
if ("[]".equals(pos)) {
return "[]"; //no brethren possible here
} else if (pos.lastIndexOf(',') == -1) {
return "[" + nr + "]"; //one below top
} else {
final String newPos = pos.substring(0, pos.lastIndexOf(',') + 1) + nr + "]";
return newPos;
}
}
/**
* compares two position strings and returns true, if superPosition is
* a prefix of subPosition, that is, if subPosition is in a subtree of
@@ -115,6 +135,21 @@ class LinPosition {
}
}
/**
* @return The Haskell position string for the parent of this position.
* If self is already the top node, [] is returned.
*/
public String parentPosition() {
if (this.position.equals("[]")) {
return this.position;
} else if (this.position.lastIndexOf(',') == -1) {
return "[]"; //one below top
} else {
final String newPos = this.position.substring(0, this.position.lastIndexOf(',')) + "]";
return newPos;
}
}
public String toString() {
return position + (correctPosition ? " correct" : " incorrect");
}

760
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Linearization.java Normal file
View File

@@ -0,0 +1,760 @@
//Copyright (c) Janna Khegai 2004, 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Vector;
import java.util.logging.Level;
import java.util.logging.Logger;
/**
* Encapsulates everything that has to do with the linearization.
* It is parsed here, and also the indices for click-in for pure text and HTML
* are managed here. They get calculated in GfCapsule.
* The result can be directly displayed, and this class has methods to translate
* the indices back to the respective tree positions.
* @author daniels
*/
class Linearization {
/**
* linearization marking debug messages
*/
protected static Logger logger = Logger.getLogger(Linearization.class.getName());
/**
* contains all the linearization pieces as HtmlMarkedArea
* Needed to know to which node in the AST a word in the linHtmlPane
* area belongs.
*/
private Vector htmlOutputVector = new Vector();
/**
* the GF-output between <linearization> </linearization> tags is stored here.
* Must be saved in case the displayed languages are changed.
* Only written in readLin
*/
private String linearization = "";
/**
* stack for storing the current position:
* When displaying, we start with the root of the AST.
* Whenever we start to display a node, it is pushed, and when it is completely displayed, we pop it.
* Only LinPositions are stored in here
* local in formLin?
* */
private Vector currentPosition = new Vector();
/**
* Must be the same Display as GFEditor2 uses
*/
private Display display;
/**
* to collect the linearization strings
*/
private HashMap linearizations = new HashMap();
/**
* Initializes this object and binds it to the given Display
* @param display The display, that the editor uses
*/
public Linearization(Display display) {
this.display = display;
}
/**
* @return Returns the linearizations.
*/
HashMap getLinearizations() {
return linearizations;
}
/**
* @param linearization The linearization to set.
*/
void setLinearization(String linearization) {
this.linearization = linearization;
}
/**
* resets the output mechanism.
*/
void reset() {
htmlOutputVector = new Vector();
}
/**
* Returns the widest position (see comments to comparePositions)
* covered in the string from begin to end in the
* 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 = LinPosition.maxPosition(max,(((MarkedArea)this.htmlOutputVector.elementAt(i)).position).position);
return max;
}
/**
* Appends the string restString to display.
* It parses the subtree tags and registers them.
* The focus tag is expected to be replaced by subtree.
* @param restString string to append, with tags in it.
* @param clickable if true, the text is appended and the subtree tags are
* parsed. If false, the text is appended, but the subtree tags are ignored.
* @param doDisplay true iff the output is to be displayed.
* Implies, if false, that clickable is treated as false.
* @param language the current linearization language
*/
private String appendMarked(String restString, final boolean clickable, boolean doDisplay, String language) {
String appendedPureText = "";
if (restString.length()>0) {
/**
* the length of what is already displayed of the linearization.
* Alternatively: What has been processed in restString since
* subtreeBegin
*/
int currentLength = 0;
/** position of &lt;subtree */
int subtreeBegin;
/** position of &lt;/subtree */
int subtreeEnd;
if (clickable && doDisplay) {
subtreeBegin = Utils.indexOfNotEscaped(restString, "<subtree");
subtreeEnd = Utils.indexOfNotEscaped(restString, "</subtree");
// cutting subtree-tags:
while ((subtreeEnd>-1)||(subtreeBegin>-1)) {
/**
* length of the portion that is to be displayed
* in the current run of appendMarked.
* For HTML this would have to be calculated
* in another way.
*/
final int newLength;
if ((subtreeEnd==-1)||((subtreeBegin<subtreeEnd)&&(subtreeBegin>-1))) {
final int subtreeTagEnd = Utils.indexOfNotEscaped(restString, ">",subtreeBegin);
final int nextOpeningTagBegin = Utils.indexOfNotEscaped(restString, "<", subtreeTagEnd);
//getting position:
final int posStringBegin = Utils.indexOfNotEscaped(restString, "[",subtreeBegin);
final int posStringEnd = Utils.indexOfNotEscaped(restString, "]",subtreeBegin);
final LinPosition position = new LinPosition(restString.substring(posStringBegin,posStringEnd+1),
restString.substring(subtreeBegin,subtreeTagEnd).indexOf("incorrect")==-1);
// is something before the tag?
// is the case in the first run
if (subtreeBegin-currentLength>1) {
if (logger.isLoggable(Level.FINER)) {
logger.finer("SOMETHING BEFORE THE TAG");
}
if (this.currentPosition.size()>0)
newLength = register(currentLength, subtreeBegin, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString, language);
else
newLength = register(currentLength, subtreeBegin, new LinPosition("[]",
restString.substring(subtreeBegin,subtreeTagEnd).indexOf("incorrect")==-1), restString, language);
} else { // nothing before the tag:
//the case in the beginning
if (logger.isLoggable(Level.FINER)) {
logger.finer("NOTHING BEFORE THE TAG");
}
if (nextOpeningTagBegin>0) {
newLength = register(subtreeTagEnd+2, nextOpeningTagBegin, position, restString, language);
} else {
newLength = register(subtreeTagEnd+2, restString.length(), position, restString, language);
}
restString = removeSubTreeTag(restString,subtreeBegin, subtreeTagEnd+1);
}
currentLength += newLength ;
} else {
// something before the </subtree> tag:
if (subtreeEnd-currentLength>1) {
if (logger.isLoggable(Level.FINER)) {
logger.finer("SOMETHING BEFORE THE </subtree> TAG");
}
if (this.currentPosition.size()>0)
newLength = register(currentLength, subtreeEnd, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString, language);
else
newLength = register(currentLength, subtreeEnd, new LinPosition("[]",
restString.substring(subtreeBegin,subtreeEnd).indexOf("incorrect")==-1), restString, language);
currentLength += newLength ;
}
// nothing before the tag:
else
// punctuation after the </subtree> tag:
if (restString.substring(subtreeEnd+10,subtreeEnd+11).trim().length()>0)
{
if (logger.isLoggable(Level.FINER)) {
logger.finer("PUNCTUATION AFTER THE </subtree> TAG"
+ "/n" + "STRING: " + restString);
}
//cutting the tag first!:
if (subtreeEnd>0) {
restString = removeSubTreeTag(restString,subtreeEnd-1, subtreeEnd+9);
} else {
restString = removeSubTreeTag(restString,subtreeEnd, subtreeEnd+9);
}
if (logger.isLoggable(Level.FINER)) {
logger.finer("STRING after cutting the </subtree> tag: "+restString);
}
// cutting the space in the last registered component:
if (this.htmlOutputVector.size()>0) {
((MarkedArea)this.htmlOutputVector.elementAt(this.htmlOutputVector.size()-1)).end -=1;
if (currentLength>0) {
currentLength -=1;
}
}
if (logger.isLoggable(Level.FINER)) {
logger.finer("currentLength: " + currentLength);
}
// register the punctuation:
if (this.currentPosition.size()>0) {
newLength = register(currentLength, currentLength+2, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString, language);
} else {
newLength = register(currentLength, currentLength+2, new LinPosition("[]",
true), restString, language);
}
currentLength += newLength ;
} else {
// just cutting the </subtree> tag:
restString = removeSubTreeTag(restString,subtreeEnd, subtreeEnd+10);
}
}
subtreeEnd = Utils.indexOfNotEscaped(restString, "</subtree");
subtreeBegin = Utils.indexOfNotEscaped(restString, "<subtree");
// if (debug2)
// System.out.println("/subtree index: "+l2 + "<subtree"+l);
if (logger.isLoggable(Level.FINER)) {
logger.finer("<-POSITION: "+subtreeBegin+" CURRLENGTH: "+currentLength
+ "\n STRING: "+restString.substring(currentLength));
}
} //while
} else { //no focus, no selection enabled (why ever)
//that means, that all subtree tags are removed here.
if (logger.isLoggable(Level.FINER)) {
logger.finer("NO SELECTION IN THE TEXT TO BE APPENDED!");
}
//cutting tags from previous focuses if any:
int r = Utils.indexOfNotEscaped(restString, "</subtree>");
while (r>-1) {
// check if punktualtion marks like . ! ? are at the end of a sentence:
if (restString.charAt(r+10)==' ')
restString = restString.substring(0,r)+restString.substring(r+11);
else
restString = restString.substring(0,r)+restString.substring(r+10);
r = Utils.indexOfNotEscaped(restString, "</subtree>");
}
r = Utils.indexOfNotEscaped(restString, "<subtree");
while (r>-1) {
int t = Utils.indexOfNotEscaped(restString, ">", r);
if (t<restString.length()-2)
restString = restString.substring(0,r)+restString.substring(t+2);
else
restString = restString.substring(0,r);
r = Utils.indexOfNotEscaped(restString, "<subtree");
}
}
// appending:
restString = unescapeTextFromGF(restString);
if (logger.isLoggable(Level.FINER)) {
logger.finer(restString);
}
appendedPureText = restString.replaceAll("&-","\n ");
//display the text if not already done in case of clickable
if (!clickable && doDisplay) {
// the text has only been pruned from markup, but still needs
// to be displayed
this.display.addToStages(appendedPureText, appendedPureText);
}
} // else: nothing to append
return appendedPureText;
}
/**
* Replaces a number of escaped characters by an unescaped version
* of the same length
* @param string The String with '\' as the escape character
* @return the same String, but with escaped characters removed
*
*/
static String unescapeTextFromGF(String string) {
final String more = "\\"+">";
final String less = "\\"+"<";
//%% by daniels, linearization output will be changed drastically
//(or probably will), so for now some hacks for -> and >=
string = Utils.replaceAll(string, "-" + more, "-> ");
string = Utils.replaceAll(string, "-" + more,"-> ");
string = Utils.replaceAll(string, more," >");
string = Utils.replaceAll(string, less," <");
//an escaped \ becomes a single \
string = Utils.replaceAll(string, "\\\\"," \\");
return string;
}
/**
* The substring from start to end in workingString, together with
* position is saved as a MarkedArea in this.htmlOutputVector.
* The information from where to where the to be created MarkedArea
* extends, is calculated in this method.
* @param start The position of the first character in workingString
* of the part, that is to be registered.
* @param end The position of the last character in workingString
* of the part, that is to be registered.
* @param position the position in the tree that corresponds to
* the to be registered text
* @param workingString the String from which the displayed
* characters are taken from
* @param language the current linearization language
* @return newLength, the difference between end and start
*/
private int register(int start, int end, LinPosition position, String workingString, String language) {
/**
* the length of the piece of text that is to be appended now
*/
final int newLength = end-start;
// the tag has some words to register:
if (newLength>0) {
final String stringToAppend = workingString.substring(start,end);
//if (stringToAppend.trim().length()>0) {
//get oldLength and add the new text
String toAdd = unescapeTextFromGF(stringToAppend);
final MarkedArea hma = this.display.addAsMarked(toAdd, position, language);
this.htmlOutputVector.add(hma);
if (logger.isLoggable(Level.FINER)) {
logger.finer("HTML added : " + hma);
}
} //some words to register
return newLength;
}
/**
* removing subtree-tag in the interval start-end
* and updating the coordinates after that
* basically part of appendMarked
* No subtree is removed, just the tag.
* @param s The String in which the subtree tag should be removed
* @param start position in restString
* @param end position in restString
* @return the String without the subtree-tags in the given interval
*/
private String removeSubTreeTag (final String s, final int start, final int end) {
String restString = s;
if (logger.isLoggable(Level.FINER)) {
logger.finer("removing: "+ start +" to "+ end);
}
int difference =end-start+1;
int positionStart, positionEnd;
if (difference>20) {
positionStart = Utils.indexOfNotEscaped(restString, "[", start);
positionEnd = Utils.indexOfNotEscaped(restString, "]", start);
currentPosition.addElement(new LinPosition(
restString.substring(positionStart, positionEnd+1),
restString.substring(start,end).indexOf("incorrect")==-1));
} else if (currentPosition.size()>0) {
currentPosition.removeElementAt(currentPosition.size()-1);
}
if (start>0) {
restString = restString.substring(0,start)+restString.substring(end+1);
} else{
restString = restString.substring(end+1);
}
return restString;
}
/**
* Goes through the list of MarkedAreas and creates MarkedAreaHighlightingStatus
* objects for them, which contain fields for incorrect constraints
* and if they belong to the selected subtree.
* @param focusPosition The AST position of the selected node
* @return a Vector of MarkedAreaHighlightingStatus
*/
Vector calculateHighlights(LinPosition focusPosition) {
Vector result = new Vector();
final HashSet incorrectMA = new HashSet();
for (int i = 0; i<htmlOutputVector.size(); i++) {
final MarkedArea ma = (MarkedArea)this.htmlOutputVector.elementAt(i);
//check, if and how ma should be highlighted
boolean incorrect = false;
boolean focused = false;
if (logger.isLoggable(Level.FINER)) {
logger.finer("Highlighting: " + ma);
}
if (!ma.position.correctPosition) {
incorrectMA.add(ma);
incorrect = true;
} else {
//This could be quadratic, but normally on very
//few nodes constraints are introduced, so
//incorrectMA should not contain many elements.
MarkedArea incMA;
for (Iterator it = incorrectMA.iterator(); !incorrect && it.hasNext();) {
incMA = (MarkedArea)it.next();
if (LinPosition.isSubtreePosition(incMA.position, ma.position)) {
incorrect = true;
}
}
}
if (LinPosition.isSubtreePosition(focusPosition, ma.position)) {
focused = true;
}
MarkedAreaHighlightingStatus mahs = new MarkedAreaHighlightingStatus(focused, incorrect, ma);
result.add(mahs);
}
return result;
}
/**
* Parses the linearization XML and calls outputAppend
* @param langMan The LangMenuModel, but that is an inner class and only
* the methods in the Interface LanguageManager are used here.
*/
void parseLin(LanguageManager langMan) {
linearizations.clear();
boolean firstLin=true;
//read first line like ' <lin lang=Abstract>'
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 readResult
int ind = Utils.indexOfNotEscaped(readResult, "=");
int ind2 = Utils.indexOfNotEscaped(readResult, ">");
/** The language of the linearization */
String language = readResult.substring(ind+1,ind2);
//the first direct linearization
readResult = lin.substring(0,lin.indexOf("</lin>"));
//the rest
lin = lin.substring(lin.indexOf("</lin>"));
while (readResult.length()>1) {
langMan.add(language,true);
// selected?
boolean visible = langMan.isLangActive(language);
if (visible && !firstLin) {
// appending sth. linearizationArea
this.display.addToStages("\n************\n", "<br><hr><br>");
}
if (logger.isLoggable(Level.FINER)) {
logger.finer("linearization for the language: "+readResult);
}
// change the focus tag into a subtree tag.
// focus handling now happens in GFEditor2::formTree
String readLin = readResult;
readLin = Utils.replaceNotEscaped(readLin, "<focus", "<subtree");
readLin = Utils.replaceNotEscaped(readLin, "</focus", "</subtree");
final boolean isAbstract = "Abstract".equals(language);
// now do appending and registering
String linResult = appendMarked(readLin + '\n', !isAbstract, visible, language);
if (visible) {
firstLin = false;
}
linearizations.put(language, linResult);
// read </lin>
lin = lin.substring(lin.indexOf('\n')+1);
// read lin or 'end'
if (lin.length()<1) {
break;
}
readResult = lin.substring(0,lin.indexOf('\n'));
lin = lin.substring(lin.indexOf('\n')+1);
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>"));
}
}
}
/**
*
* @param language The concrete language of choice
* @return The linearization of the subtree starting with the currently
* selected node in the given language.
*/
String getSelectedLinearization(final String language, final LinPosition focusPosition) {
StringBuffer sel = new StringBuffer();
for (int i = 0; i<htmlOutputVector.size(); i++) {
final MarkedArea ma = (MarkedArea)htmlOutputVector.elementAt(i);
if (language.equals(ma.language) && LinPosition.isSubtreePosition(focusPosition, ma.position)) {
sel.append(ma.words);
}
}
return sel.toString();
}
/**
* Takes the index of a caret position in the linearization area
* and returns the language of the clicked linearization.
* GF lists the different concrete languages one after the other,
* and this method looks at the linearization snipplets to get
* the language.
* If somehow no language can be found out, 'Abstract' is returned
* @param pos The index of the caret position
* @param htmlClicked If the HTML JTextPane has been clicked,
* false for the JTextArea
* @return the name of the concrete grammar (language) or Abstract
* (see above).
*/
String getLanguageForPos(int pos, final boolean htmlClicked) {
final String language;
MarkedArea ma = null;
if (htmlClicked) {
//HTML
for (int i = 0; i < htmlOutputVector.size(); i++) {
if ((pos >= ((MarkedArea)htmlOutputVector.get(i)).htmlBegin) && (pos <= ((MarkedArea)htmlOutputVector.get(i)).htmlEnd)) {
ma = (MarkedArea)htmlOutputVector.get(i);
break;
}
}
} else {
//assumably pure text
for (int i = 0; i < htmlOutputVector.size(); i++) {
if ((pos >= ((MarkedArea)htmlOutputVector.get(i)).begin) && (pos <= ((MarkedArea)htmlOutputVector.get(i)).end)) {
ma = (MarkedArea)htmlOutputVector.get(i);
break;
}
}
}
if (ma != null && ma.language != null) {
language = ma.language;
} else {
language = "Abstract";
}
return language;
}
/**
* The user has either just clicked in the linearization area,
* which means start == end, or he has selected a text, so that
* start < end.
* This method figures out the smallest subtree whose linearization
* completely encompasses the area from start to end.
* This method is for the HTML linearization area.
* @param start The index of the caret position at the begin of the selection
* @param end The index of the caret position at the end of the selection
* @return The 'root' of the subtree described above
*/
String markedAreaForPosHtml(int start, int end) {
if (htmlOutputVector.isEmpty()) {
return null;
}
String position = null; //the result
String jPosition ="", iPosition="";
MarkedArea jElement = null;
MarkedArea iElement = null;
int j = 0;
int i = htmlOutputVector.size()-1;
if (logger.isLoggable(Level.FINER))
for (int k=0; k < htmlOutputVector.size(); k++) {
logger.finer("element: "+k+" begin "+((MarkedArea)htmlOutputVector.elementAt(k)).htmlBegin+" "
+ "\n-> end: "+((MarkedArea)htmlOutputVector.elementAt(k)).htmlEnd+" "
+ "\n-> position: "+(((MarkedArea)htmlOutputVector.elementAt(k)).position).position+" "
+ "\n-> words: "+((MarkedArea)htmlOutputVector.elementAt(k)).words);
}
// localizing end:
while ((j < htmlOutputVector.size()) && (((MarkedArea)htmlOutputVector.elementAt(j)).htmlEnd < end)) {
j++;
}
// localising start:
while ((i >= 0) && (((MarkedArea)htmlOutputVector.elementAt(i)).htmlBegin > start)) {
i--;
}
if (logger.isLoggable(Level.FINER)) {
logger.finer("i: "+i+" j: "+j);
}
if ((j < htmlOutputVector.size())) {
jElement = (MarkedArea)htmlOutputVector.elementAt(j);
jPosition = jElement.position.position;
// less & before:
if (i == -1) { // less:
if (end>=jElement.htmlBegin) {
iElement = (MarkedArea)htmlOutputVector.elementAt(0);
iPosition = iElement.position.position;
if (logger.isLoggable(Level.FINER)) {
logger.finer("Less: "+jPosition+" and "+iPosition);
}
position = findMax(0,j);
if (logger.isLoggable(Level.FINER)) {
logger.finer("SELECTEDTEXT: "+position+"\n");
}
} else { // before:
if (logger.isLoggable(Level.FINER)) {
logger.finer("BEFORE vector of size: "+htmlOutputVector.size());
}
}
} else { // just:
iElement = (MarkedArea)htmlOutputVector.elementAt(i);
iPosition = iElement.position.position;
if (logger.isLoggable(Level.FINER)) {
logger.finer("SELECTED TEXT Just: "+iPosition +" and "+jPosition+"\n");
}
position = findMax(i,j);
if (logger.isLoggable(Level.FINER)) {
logger.finer("SELECTEDTEXT: "+position+"\n");
}
}
} else if (i>=0) { // more && after:
iElement = (MarkedArea)htmlOutputVector.elementAt(i);
iPosition = iElement.position.position;
// more
if (start<=iElement.htmlEnd) {
jElement = (MarkedArea)htmlOutputVector.elementAt(htmlOutputVector.size()-1);
jPosition = jElement.position.position;
if (logger.isLoggable(Level.FINER)) {
logger.finer("MORE: "+iPosition+ " and "+jPosition);
}
position = findMax(i,htmlOutputVector.size()-1);
if (logger.isLoggable(Level.FINER)) {
logger.finer("SELECTEDTEXT: "+position+"\n");
}
// after:
} else if (logger.isLoggable(Level.FINER)) {
logger.finer("AFTER vector of size: "+htmlOutputVector.size());
}
} else { // bigger:
iElement = (MarkedArea)htmlOutputVector.elementAt(0);
iPosition = iElement.position.position;
jElement = (MarkedArea)htmlOutputVector.elementAt(htmlOutputVector.size()-1);
jPosition = jElement.position.position;
if (logger.isLoggable(Level.FINER)) {
logger.finer("BIGGER: "+iPosition +" and "+jPosition+"\n"
+ "\n-> SELECTEDTEXT: []\n");
}
position = "[]";
}
return position;
}
/**
* The user has either just clicked in the linearization area,
* which means start == end, or he has selected a text, so that
* start < end.
* This method figures out the smallest subtree whose linearization
* completely encompasses the area from start to end.
* This method is for the pure text linearization area.
* @param start The index of the caret position at the begin of the selection
* @param end The index of the caret position at the end of the selection
* @return The 'root' of the subtree described above
*/
String markedAreaForPosPureText(int start, int end) {
if (htmlOutputVector.isEmpty()) {
return null;
}
//the result
String position = null;
//variables for confining the searched MarkedArea from
//start and end (somehow ...)
int j = 0;
int i = htmlOutputVector.size() - 1;
String jPosition ="", iPosition="";
MarkedArea jElement = null;
MarkedArea iElement = null;
if (logger.isLoggable(Level.FINER))
for (int k = 0; k < htmlOutputVector.size(); k++) {
logger.finer("element: " + k + " begin " + ((MarkedArea)htmlOutputVector.elementAt(k)).begin + " "
+ "\n-> end: " + ((MarkedArea)htmlOutputVector.elementAt(k)).end+" "
+ "\n-> position: " + (((MarkedArea)htmlOutputVector.elementAt(k)).position).position+" "
+ "\n-> words: " + ((MarkedArea)htmlOutputVector.elementAt(k)).words);
}
// localizing end:
while ((j < htmlOutputVector.size()) && (((MarkedArea)htmlOutputVector.elementAt(j)).end < end)) {
j++;
}
// localising start:
while ((i >= 0) && (((MarkedArea)htmlOutputVector.elementAt(i)).begin > start))
i--;
if (logger.isLoggable(Level.FINER)) {
logger.finer("i: " + i + " j: " + j);
}
if ((j < htmlOutputVector.size())) {
jElement = (MarkedArea)htmlOutputVector.elementAt(j);
jPosition = jElement.position.position;
// less & before:
if (i==-1) { // less:
if (end>=jElement.begin) {
iElement = (MarkedArea)htmlOutputVector.elementAt(0);
iPosition = iElement.position.position;
if (logger.isLoggable(Level.FINER)) {
logger.finer("Less: "+jPosition+" and "+iPosition);
}
position = findMax(0,j);
if (logger.isLoggable(Level.FINER)) {
logger.finer("SELECTEDTEXT: "+position+"\n");
}
} else if (logger.isLoggable(Level.FINER)) { // before:
logger.finer("BEFORE vector of size: " + htmlOutputVector.size());
}
} else { // just:
iElement = (MarkedArea)htmlOutputVector.elementAt(i);
iPosition = iElement.position.position;
if (logger.isLoggable(Level.FINER)) {
logger.finer("SELECTED TEXT Just: "+iPosition +" and "+jPosition+"\n");
}
position = findMax(i,j);
if (logger.isLoggable(Level.FINER)) {
logger.finer("SELECTEDTEXT: "+position+"\n");
}
}
} else if (i>=0) { // more && after:
iElement = (MarkedArea)htmlOutputVector.elementAt(i);
iPosition = iElement.position.position;
// more
if (start<=iElement.end) {
jElement = (MarkedArea)htmlOutputVector.elementAt(htmlOutputVector.size() - 1);
jPosition = jElement.position.position;
if (logger.isLoggable(Level.FINER)) {
logger.finer("MORE: "+iPosition+ " and "+jPosition);
}
position = findMax(i, htmlOutputVector.size()-1);
if (logger.isLoggable(Level.FINER)) {
logger.finer("SELECTEDTEXT: "+position+"\n");
}
} else if (logger.isLoggable(Level.FINER)) { // after:
logger.finer("AFTER vector of size: " + htmlOutputVector.size());
}
} else {
// bigger:
iElement = (MarkedArea)htmlOutputVector.elementAt(0);
iPosition = iElement.position.position;
jElement = (MarkedArea)htmlOutputVector.elementAt(htmlOutputVector.size()-1);
jPosition = jElement.position.position;
if (logger.isLoggable(Level.FINER)) {
logger.finer("BIGGER: "+iPosition +" and "+jPosition+"\n"
+ "\n-> SELECTEDTEXT: []\n");
}
position = "[]";
}
return position;
}
}

28
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinkCommand.java
View File

@@ -23,6 +23,14 @@ package de.uka.ilkd.key.ocl.gf;
*/
public class LinkCommand extends GFCommand {
/**
* Since LinkCommand is not a real command, that is sent to GF,
* most fields are given dummy values here.
* The subcat is assigned its full display name and tooltip
* @param subcat The subcategory of the menu behind this command
* @param manager The PrintnameManager, that can map subcat to its
* full name
*/
public LinkCommand(final String subcat, final PrintnameManager manager) {
this.command = subcat;
this.newSubcat = false;
@@ -46,20 +54,30 @@ public class LinkCommand extends GFCommand {
}
/**the text that is to be displayed as the tooltip */
/**
* the text that is to be displayed as the tooltip
*/
protected final String tooltipText;
/**the text that is to be displayed as the tooltip */
/**
* the text that is to be displayed as the tooltip
*/
public String getTooltipText() {
return tooltipText;
}
/** the text that is to be displayed in the refinement lists */
/**
* the text that is to be displayed in the refinement lists
*/
protected final String displayText;
/** the text that is to be displayed in the refinement lists */
/**
* the text that is to be displayed in the refinement lists
*/
public String getDisplayText() {
return displayText;
}
/** the subcategory of this command */
/**
* the subcategory of this command
*/
public String getSubcat() {
return this.command;
}

45
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/MarkedArea.java
View File

@@ -20,7 +20,7 @@ package de.uka.ilkd.key.ocl.gf;
* and an end in the linearization area and a position in the AST. It is used
* for clicking in the text
*
* @author janna
* @author janna, daniels
*/
class MarkedArea {
/**
@@ -46,24 +46,39 @@ class MarkedArea {
* this MarkedArea belongs to
*/
final public String language;
/**
* Creates a new MarkedArea and initializes the fields with the parameters
* @param b The starting position of the stored words
* @param e The ending position of the stored words
* @param p The position in the AST
* @param w The actual text of this area
* @param lang the language of the current linearization
/**
* the start index in the HTML area
*/
MarkedArea(int b, int e, LinPosition p, String w, String lang) {
begin = b;
end = e;
position = p;
words = w;
language = lang;
final public int htmlBegin;
/**
* the end index in the HTML area
*/
final public int htmlEnd;
/**
* A stand-alone constuctor which takes all values as arguments
* @param begin The starting position of the stored words
* @param end The ending position of the stored words
* @param position The position in the AST
* @param words The actual text of this area
* @param htmlBegin the start index in the HTML area
* @param htmlEnd the end index in the HTML area
* @param language the language of the current linearization
*/
public MarkedArea(int begin, int end, LinPosition position, String words, int htmlBegin, int htmlEnd, String language) {
this.begin = begin;
this.end = end;
this.position = position;
this.words = words;
this.language = language;
this.htmlBegin = htmlBegin;
this.htmlEnd = htmlEnd;
}
public String toString() {
return begin + " - " + end + " : " + position + " = '" + words + "'";
return begin + " - " + end + " : " + position + " = '" + words + "' ; HTML: " + htmlBegin + " - " + htmlEnd;
}
}

48
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/MarkedAreaHighlightingStatus.java Normal file
View File

@@ -0,0 +1,48 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/**
* Stores a MarkedArea together with some status fields, which tell
* how it should get highlighted.
* No direct highlighting stuff in here, that's done in GFEditor2
* @author daniels
*/
class MarkedAreaHighlightingStatus {
/**
* The MarkedArea, which contains the highlighting information
*/
final MarkedArea ma;
/**
* whether this MarkedArea is a subnode of the currently focused node
*/
final boolean focused;
/**
* whether this MarkedArea has (inherited) a GF constraint
*/
final boolean incorrect;
/**
* Initializes this immutable record class
* @param focused whether this MarkedArea is a subnode of the currently focused node
* @param incorrect whether this MarkedArea has (inherited) a GF constraint
* @param ma The MarkedArea, which contains the highlighting information
*/
public MarkedAreaHighlightingStatus(boolean focused, boolean incorrect, MarkedArea ma) {
this.focused = focused;
this.incorrect = incorrect;
this.ma = ma;
}
}

57
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/NewCategoryMenuResult.java Normal file
View File

@@ -0,0 +1,57 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/**
* GF sends the new menu as XML.
* After this has been parsed by GfCapsule, it is sent in this representation
* to GFEditor2.
* @author daniels
*
*/
class NewCategoryMenuResult {
/**
* The actual entries of the newMenu
*/
final String[] menuContent;
/**
* The languages, that GF sent
*/
final String[] languages;
/**
* the constituents of the import path?
*/
final String[] paths;
/**
* the name of the abstract grammar, also called topic
*/
final String grammarName;
/**
* Just sets the attributes of this class
* @param grammarName the name of the abstract grammar, also called topic
* @param menuContent The actual entries of the newMenu
* @param languages The languages, that GF sent
* @param paths the constituents of the import path?
*/
public NewCategoryMenuResult(String grammarName, String[] menuContent, String[] languages, String paths[]) {
this.grammarName = grammarName;
this.menuContent = menuContent;
this.languages = languages;
this.paths = paths;
}
}

217
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java
View File

@@ -34,12 +34,31 @@ import java.util.logging.*;
* HTML can be used inside the descriptions and the tooltip text
*/
class Printname {
protected static Logger subcatLogger = Logger.getLogger(Printname.class.getName());
private static Logger subcatLogger = Logger.getLogger(Printname.class.getName());
public static final Printname delete = new Printname("d", "delete current sub-tree");
public static final Printname addclip = new Printname("ac", "add to clipboard\\$<html>adds the current subtree to the clipboard.<br>It is offered in the refinement menu if the expected type fits to the one of the current sub-tree.</html>");
public static final Printname printhistory = new Printname("ph", "peel head\\$removes this fun and moves its first argument at its place instead");
/**
* delete is always the same and only consists of one letter, therefore static.
*/
public static final Printname delete = new Printname("d", "delete current sub-tree", false);
/**
* The ac command i always the same, therefore static
*/
public static final Printname addclip = new Printname("ac", "add to clipboard\\$<html>adds the current subtree to the clipboard.<br>It is offered in the refinement menu if the expected type fits to the one of the current sub-tree.</html>", false);
/**
* @param arg The number of the argument,
* that will take the place of the selected fun
* @return a Printname for the 'ph arg' command
*/
public static Printname peelHead(int arg) {
final String cmd = "ph " + arg;
final String show = "peel head " + arg + "\\$removes this fun and moves its " + (arg + 1) + ". argument at its place instead";
return new Printname(cmd, show, true);
}
/**
* the type of the fun behind that printname (if applicable)
*/
protected final String type;
/**
@@ -61,18 +80,26 @@ class Printname {
* The string that is followed by a new parameter to the GF function
*/
public final static String PARAM = "\\#";
/**
* If that follows "\#" in the parameter descriptions, then do an
* auto-coerce when this param is meta and selected
*/
public final static String AUTO_COERCE = "!";
/** the name of the fun that is used in this command */
/**
* the name of the fun that is used in this command
*/
protected final String fun;
/** the printname of this function */
/**
* the printname of this function
*/
protected final String printname;
/** to cache the printname, once it is constructed */
/**
* to cache the printname, once it is constructed
*/
protected String displayedPrintname = null;
/**
* the name of the module the fun belongs to
* null means that the function is saved without module information,
@@ -100,9 +127,13 @@ class Printname {
}
*/
/** the subcategory of this command */
/**
* the subcategory of this command
*/
protected final String subcat;
/** the subcategory of this command */
/**
* the subcategory of this command
*/
public String getSubcat() {
return subcat;
}
@@ -131,7 +162,7 @@ class Printname {
public String getParamName(int n) {
String name = null;
try {
name = (String)this.paramNames.get(n);
name = (String)this.paramNames.get(n);
} catch (ArrayIndexOutOfBoundsException e) {
subcatLogger.fine(e.getLocalizedMessage());
}
@@ -143,6 +174,26 @@ class Printname {
*/
protected final Vector paramTexts = new Vector();
/**
* tells, whether the nth parameter should be auto-coerced
* @param n the number of the parameter in question
* @return whether the nth parameter should be auto-coerced
*/
public boolean getParamAutoCoerce(int n) {
boolean result = false;
try {
result = ((Boolean)this.paramAutoCoerce.get(n)).booleanValue();
} catch (ArrayIndexOutOfBoundsException e) {
subcatLogger.fine(e.getLocalizedMessage());
}
return result;
}
/**
* stores for the parameters whether they should be auto-coerced or not.
* parallel with paramNames
*/
protected final Vector paramAutoCoerce = new Vector();
/**
* Creates a Printname for a normal GF function
@@ -166,81 +217,88 @@ class Printname {
} else {
this.funPresent = false;
}
//parse the fun name
{
int index = myFun.indexOf('.');
if (index > -1) {
//a valid fun name must not be empty
this.fun = myFun.substring(index + 1);
this.module = myFun.substring(0, index);
} else {
this.fun = myFun;
this.module = null;
}
int index = myFun.indexOf('.');
if (index > -1) {
//a valid fun name must not be empty
this.fun = myFun.substring(index + 1);
this.module = myFun.substring(0, index);
} else {
this.fun = myFun;
this.module = null;
}
}
//parse the parameters and cut that part
{
int index = Utils.indexOfNotEscaped(myPrintname, PARAM);
if (index > -1) {
String paramPart = myPrintname.substring(index);
String splitString;
//split takes a regexp as an argument. So we have to escape the '\' again.
if (PARAM.startsWith("\\")) {
splitString = "\\" + PARAM;
} else {
splitString = PARAM;
}
String[] params = paramPart.split(splitString);
//don't use the first split part, since it's empty
for (int i = 1; i < params.length; i++) {
String current = params[i];
int nameEnd = current.indexOf(' ');
int nameEnd2 = Utils.indexOfNotEscaped(current, PARAM);
if (nameEnd == -1) {
nameEnd = current.length();
}
String name = current.substring(0, nameEnd);
String description;
if (nameEnd < current.length() - 1) {
description = current.substring(nameEnd + 1).trim();
int index = Utils.indexOfNotEscaped(myPrintname, PARAM);
if (index > -1) {
String paramPart = myPrintname.substring(index);
String splitString;
//split takes a regexp as an argument. So we have to escape the '\' again.
if (PARAM.startsWith("\\")) {
splitString = "\\" + PARAM;
} else {
description = "";
splitString = PARAM;
}
this.paramNames.addElement(name);
this.paramTexts.addElement(description);
String[] params = paramPart.split(splitString);
//don't use the first split part, since it's empty
for (int i = 1; i < params.length; i++) {
String current = params[i];
boolean autocoerce = false;
if (AUTO_COERCE.equals(current.substring(0,1))) {
autocoerce = true;
//cut the !
current = current.substring(1);
}
int nameEnd = current.indexOf(' ');
int nameEnd2 = Utils.indexOfNotEscaped(current, PARAM);
if (nameEnd == -1) {
nameEnd = current.length();
}
String name = current.substring(0, nameEnd);
String description;
if (nameEnd < current.length() - 1) {
description = current.substring(nameEnd + 1).trim();
} else {
description = "";
}
this.paramNames.addElement(name);
this.paramTexts.addElement(description);
this.paramAutoCoerce.addElement(new Boolean(autocoerce));
}
myPrintname = myPrintname.substring(0, index);
}
myPrintname = myPrintname.substring(0, index);
}
}
//extract the subcategory part and cut that part
{
int index = Utils.indexOfNotEscaped(myPrintname, SUBCAT);
if (index > -1) {
String subcatPart = myPrintname.substring(index);
myPrintname = myPrintname.substring(0, index);
int indFull = subcatPart.indexOf('{');
if (indFull > -1) {
int indFullEnd = subcatPart.indexOf('}', indFull + 1);
if (indFullEnd == -1) {
indFullEnd = subcatPart.length();
}
String fullName = subcatPart.substring(indFull + 1, indFullEnd);
this.subcat = subcatPart.substring(0, indFull).trim();
this.subcatNameHashtable.put(this.subcat, fullName);
if (subcatLogger.isLoggable(Level.FINER)) {
subcatLogger.finer("new fullname '" + fullName + "' for category (shortname) '" + this.subcat + "'");
int index = Utils.indexOfNotEscaped(myPrintname, SUBCAT);
if (index > -1) {
String subcatPart = myPrintname.substring(index);
myPrintname = myPrintname.substring(0, index);
int indFull = subcatPart.indexOf('{');
if (indFull > -1) {
int indFullEnd = subcatPart.indexOf('}', indFull + 1);
if (indFullEnd == -1) {
indFullEnd = subcatPart.length();
}
String fullName = subcatPart.substring(indFull + 1, indFullEnd);
this.subcat = subcatPart.substring(0, indFull).trim();
this.subcatNameHashtable.put(this.subcat, fullName);
if (subcatLogger.isLoggable(Level.FINER)) {
subcatLogger.finer("new fullname '" + fullName + "' for category (shortname) '" + this.subcat + "'");
}
} else {
subcat = subcatPart.trim();
}
} else {
subcat = subcatPart.trim();
this.subcat = null;
}
} else {
this.subcat = null;
}
}
}
@@ -249,15 +307,17 @@ class Printname {
* like d, ph, ac
* @param command the GF command
* @param explanation an explanatory text what this command does
* @param funPresent If explanation already contains the fun.
* If true, the fun won't be printed in the refinement menu.
*/
protected Printname(String command, String explanation) {
protected Printname(String command, String explanation, boolean funPresent) {
this.fun = command;
this.subcatNameHashtable = null;
this.subcat = null;
this.module = "";
this.printname = explanation;
this.type = null;
this.funPresent = false;
this.funPresent = funPresent;
}
/**
@@ -276,7 +336,9 @@ class Printname {
this.funPresent = false;
}
/** the text that is to be displayed in the refinement lists */
/**
* the text that is to be displayed in the refinement lists
*/
public String getDisplayText() {
String result;
result = extractDisplayText(this.printname);
@@ -376,7 +438,12 @@ class Printname {
* @return the aforementioned result.
*/
public static String htmlAppend(String original, String insertion) {
StringBuffer result = new StringBuffer(original);
StringBuffer result;
if (original != null) {
result = new StringBuffer(original);
} else {
result = new StringBuffer();
}
int htmlindex = result.indexOf("</html>");
if (htmlindex > -1) {

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

@@ -15,8 +15,6 @@
package de.uka.ilkd.key.ocl.gf;
import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.IOException;
import java.util.Hashtable;
import java.util.logging.*;
@@ -26,20 +24,30 @@ import java.util.logging.*;
* the suiting Printname objects.
*/
public class PrintnameLoader extends AbstractProber {
protected final PrintnameManager printnameManager;
protected final static Logger nogger = Logger.getLogger(Printname.class.getName());
protected final Hashtable funTypes = new Hashtable();
protected final boolean loadTypes;
private final static Logger nogger = Logger.getLogger(Printname.class.getName());
/**
* @param fromGf The GF process
* @param toGf The GF process
* The PrintnameManager on which the read Printnames
* will be registered with their fun name.
*/
private final PrintnameManager printnameManager;
/**
* Here, the funs with their types get stored
*/
private final Hashtable funTypes = new Hashtable();
/**
* if the Printnames should have their type appended to their display names
*/
private final boolean loadTypes;
/**
* an initializing constructor, does nothing except setting fields
* @param gfCapsule the read/write encapsulation of GF
* @param pm The PrintnameManager on which the read Printnames
* will be registered with their fun name.
* @param withTypes true iff the Printnames should have their type
* appended to their display names
*/
public PrintnameLoader(BufferedReader fromGf, BufferedWriter toGf, PrintnameManager pm, boolean withTypes) {
super(fromGf, toGf);
public PrintnameLoader(GfCapsule gfCapsule, PrintnameManager pm, boolean withTypes) {
super(gfCapsule);
this.printnameManager = pm;
this.loadTypes = withTypes;
}
@@ -50,7 +58,7 @@ public class PrintnameLoader extends AbstractProber {
*/
protected void readMessage() {
try {
String result = this.fromProc.readLine();
String result = gfCapsule.fromProc.readLine();
if (nogger.isLoggable(Level.FINER)) {
nogger.finer("1 " + result);
}
@@ -59,11 +67,11 @@ public class PrintnameLoader extends AbstractProber {
result = result.trim();
if (result.startsWith("printname fun ")) {
//unescape backslashes. Probably there are more
result = GFEditor2.unescapeTextFromGF(result);
result = Linearization.unescapeTextFromGF(result);
this.printnameManager.addNewPrintnameLine(result, this.funTypes);
}
result = this.fromProc.readLine();
result = gfCapsule.fromProc.readLine();
if (nogger.isLoggable(Level.FINER)) {
nogger.finer("1 " + result);
}
@@ -84,10 +92,10 @@ public class PrintnameLoader extends AbstractProber {
* @param lang The module for which the grammars should be printed.
* If lang is "" or null, the last read grammar module is used.
*/
public void readPrintnames(String lang) {
protected void readPrintnames(String lang) {
//before, we want the types to be read.
if (this.loadTypes) {
TypesLoader tl = new TypesLoader(fromProc, toProc, this.funTypes);
TypesLoader tl = new TypesLoader(gfCapsule, this.funTypes);
tl.readTypes();
}
//prints the printnames of the last loaded grammar,

23
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameManager.java
View File

@@ -25,7 +25,24 @@ import java.util.logging.*;
* counterpart is done here.
*/
class PrintnameManager {
protected static Logger logger = Logger.getLogger(Printname.class.getName());
/**
* This constructor is a bit of a hack.
* It puts the \%SELF subcat into this.printnames.
* This subcat does not appear in the grammars and thus is
* introduced here. If it is defined there although, this
* definition is used. So it does not hurt.
*/
public PrintnameManager() {
this.subcatNames.put(SELF_SUBCAT, "properties of self\\$shortcuts to the properties of self, that have a fitting type");
}
/**
* The name of the subcat, that is used for the easy property access
* of self.
*/
static final String SELF_SUBCAT = "\\%SELF";
private static Logger logger = Logger.getLogger(Printname.class.getName());
protected final static String frontMatter = "printname fun ";
@@ -39,7 +56,9 @@ class PrintnameManager {
*/
protected final Hashtable subcatNames = new Hashtable();
/** contains all the Printnames with the fun names as keys */
/**
* contains all the Printnames with the fun names as keys
*/
protected final Hashtable printnames = new Hashtable();
/**

20
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ReadDialog.java
View File

@@ -41,11 +41,11 @@ import java.util.logging.*;
*/
class ReadDialog implements ActionListener{
/** XML parsing debug messages */
protected static Logger xmlLogger = Logger.getLogger(GFEditor2.class.getName() + "_XML");
private static Logger xmlLogger = Logger.getLogger(GFEditor2.class.getName() + "_XML");
/** The window to which this class belongs */
protected final GFEditor2 owner;
private final GFEditor2 owner;
/** is the main thing of this class */
protected final JDialog readDialog;
private final JDialog readDialog;
/** main area of the Read dialog (content pane)*/
private final JPanel inputPanel = new JPanel();
/** OK, Cancel, Browse in the Read dialog */
@@ -69,7 +69,7 @@ class ReadDialog implements ActionListener{
/** to select to input a String in the Read dialog */
private final JRadioButton stringReadButton = new JRadioButton("String");
/** used for new Topic, Import and Browse (readDialog) */
protected final JFileChooser fc = new JFileChooser("./");
private final JFileChooser fc = new JFileChooser("./");
/**
* if a user sends a custom command to GF, he might want to do this
* again with the same command.
@@ -170,15 +170,13 @@ class ReadDialog implements ActionListener{
}
if ( obj == ok ) {
owner.treeChanged = true;
if (termReadButton.isSelected()) {
termInput = inputField.getText();
if (termInput.indexOf(File.separatorChar)==-1){
owner.send("g "+termInput);
owner.send("[t] g "+termInput);
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("sending term string");
}
else {
owner.send("tfile "+termInput);
} else {
owner.send("[t] tfile "+termInput);
if (xmlLogger.isLoggable(Level.FINER)) {
xmlLogger.finer("sending file term: "+termInput);
}
@@ -186,11 +184,11 @@ class ReadDialog implements ActionListener{
} else { //String selected
parseInput = inputField.getText();
if (parseInput.indexOf(File.separatorChar)==-1){
owner.send("p "+parseInput);
owner.send("[t] p "+parseInput);
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("sending parse string: "+parseInput);
}
else {
owner.send("pfile "+parseInput);
owner.send("[t] pfile "+parseInput);
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("sending file parse string: "+parseInput);
}
}

142
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RealCommand.java
View File

@@ -21,13 +21,29 @@ import java.util.logging.*;
/**
* @author daniels
* This class represents a command, that is sent to GF
* This class represents a command, that is sent to GF.
* TODO Refactor the chain command stuff out of this class and make it a subclass
*/
class RealCommand extends GFCommand {
/**
* maps shorthands to fullnames
*/
private final static HashMap fullnames = new HashMap();
protected final static Logger logger = Logger.getLogger(Printname.class.getName());
private final static Logger logger = Logger.getLogger(Printname.class.getName());
/**
* The number of undo steps that is needed to undo this fun call
*/
public final int undoSteps;
/**
* The text that GF sent to describe the command
*/
protected final String showText;
protected final String subcat;
/**
* Creates a Command that stands for a GF command, no link command
@@ -40,33 +56,85 @@ class RealCommand extends GFCommand {
* which should be the command followed by the printname
* @param mlAbstract is true, iff the menu language is set to Abstract
* Then no preloaded printnames are used.
* @param toAppend will be appended to the command, that is sent to GF.
* Normally, toAppend will be the empty String "".
* But it can be a chain command's second part.
* It will not be shown to the user.
*/
public RealCommand(final String myCommand, final HashSet processedSubcats, final PrintnameManager manager, final String myShowText, final boolean mlAbstract) {
public RealCommand(final String myCommand, final HashSet processedSubcats, final PrintnameManager manager, final String myShowText, final boolean mlAbstract, final String toAppend) {
this(myCommand, processedSubcats, manager, myShowText, mlAbstract, toAppend, 1, null, null);
}
/**
* Creates a Command that stands for a GF command, no link command
* sets all the attributes of this semi-immutable class.
* @param myCommand the actual GF command
* @param processedSubcats
* @param manager maps funs to previously read Printnames.
* Thus needs to be the same object.
* @param myShowText The text GF prints in the show part of the XML
* which should be the command followed by the printname
* @param mlAbstract is true, iff the menu language is set to Abstract
* Then no preloaded printnames are used.
* @param toAppend will be appended to the command, that is sent to GF.
* Normally, toAppend will be the empty String "".
* But it can be a chain command's second part.
* It will not be shown to the user.
* @param undoSteps The number of undo steps that is needed to undo this fun call
* @param printnameFun If the fun, that selects the printname, should not be read from
* myCommand. For single commands, this is the only fun. For chain command, the last is
* taken. With this parameter, this behaviour can be overwritten
* @param subcat Normally, every fun has its own Printname, which has a fixed
* category. Sometimes, for the properies of self for example,
* this should be overwritten. If null, the subcat from the printname is used.
*/
public RealCommand(final String myCommand, final HashSet processedSubcats, final PrintnameManager manager, final String myShowText, final boolean mlAbstract, String toAppend, int undoSteps, String printnameFun, String subcat) {
if (fullnames.isEmpty()) {
fullnames.put("w", "wrap");
fullnames.put("r", "refine");
fullnames.put("ch", "change head");
fullnames.put("rc", "refine from history:");
fullnames.put("ph", "peel head");
}
if (logger.isLoggable(Level.FINEST)) {
logger.finest("new RealCommand: " + myCommand);
}
//if we have a ChainCommand, but undoSteps is just 1, count the undoSteps.
if ((undoSteps == 1) && (myCommand.indexOf(";;") > -1)) {
int occ = Utils.countOccurances(Utils.removeQuotations(myCommand), ";;") + 1;
this.undoSteps = occ;
} else {
this.undoSteps = undoSteps;
}
this.command = myCommand.trim();
this.showText = myShowText;
//extract command type
int ind = this.command.indexOf(' ');
if (ind > -1) {
this.commandType = this.command.substring(0, ind);
this.subcat = subcat;
//handle chain commands.
//Only the last command counts for the printname selection
final String lastCommand;
if (this.undoSteps > 1) {
//TODO: sth. like refine " f ;;d" ;; mp [2] will break here.
final int chainIndex = this.command.lastIndexOf(";;");
lastCommand = this.command.substring(chainIndex + 2).trim();
} else {
this.commandType = this.command;
lastCommand = this.command;
}
//extract command type
int ind = lastCommand.indexOf(' ');
if (ind > -1) {
this.commandType = lastCommand.substring(0, ind);
} else {
this.commandType = lastCommand;
}
//extract the argument position for wrapping commands and cut that part
if (this.commandType.equals("w")) {
int beforeNumber = this.command.lastIndexOf(' ');
if (this.commandType.equals("w") || this.commandType.equals("ph")) {
int beforeNumber = lastCommand.lastIndexOf(' ');
int protoarg;
try {
String argumentAsString = this.command.substring(beforeNumber + 1);
String argumentAsString = lastCommand.substring(beforeNumber + 1);
protoarg = Integer.parseInt(argumentAsString);
} catch (Exception e) {
protoarg = -1;
@@ -78,17 +146,17 @@ class RealCommand extends GFCommand {
//extract the fun of the GF command
if (this.commandType.equals("w")) {
int beforePos = this.command.indexOf(' ');
int afterPos = this.command.lastIndexOf(' ');
int beforePos = lastCommand.indexOf(' ');
int afterPos = lastCommand.lastIndexOf(' ');
if (beforePos > -1 && afterPos > beforePos) {
this.funName = this.command.substring(beforePos + 1, afterPos);
this.funName = lastCommand.substring(beforePos + 1, afterPos);
} else {
this.funName = null;
}
} else {
int beforePos = this.command.indexOf(' ');
int beforePos = lastCommand.indexOf(' ');
if (beforePos > -1) {
this.funName = this.command.substring(beforePos + 1);
this.funName = lastCommand.substring(beforePos + 1);
} else {
this.funName = null;
}
@@ -99,17 +167,23 @@ class RealCommand extends GFCommand {
this.printname = Printname.delete;
} else if (this.commandType.equals("ac")) {
this.printname = Printname.addclip;
} else if (this.commandType.equals("ph")) {
this.printname = Printname.printhistory;
} else if (this.commandType.equals("rc")) {
String subtree = this.showText.substring(3);
this.printname = new Printname(this.getCommand(), subtree + "\\$paste the previously copied subtree here<br>" + subtree);
this.printname = new Printname(this.getCommand(), subtree + "\\$paste the previously copied subtree here<br>" + subtree, false);
} else if (this.commandType.equals("ph")) {
this.printname = Printname.peelHead(this.argument);
} else if (mlAbstract) {
//create a new Printname
this.printname = new Printname(funName, myShowText, null, null);
} else {
this.printname = manager.getPrintname(funName);
} else { //standard case
if (printnameFun == null) {
this.printname = manager.getPrintname(funName);
} else {
//overwrite mode. Until now, only for properties of self.
this.printname = manager.getPrintname(printnameFun);
}
}
if (this.getSubcat() != null) {
if (processedSubcats.contains(this.getSubcat())) {
newSubcat = false;
@@ -120,9 +194,17 @@ class RealCommand extends GFCommand {
} else {
newSubcat = false;
}
//now append toAppend before it is too late.
//Only now, since it must not interfere with the things above.
if (toAppend != null) {
this.command += toAppend;
}
}
/** the text that is to be displayed in the refinement lists */
/**
* the text that is to be displayed in the refinement lists
*/
public String getDisplayText() {
String result = "";
if (this.printname.funPresent) {
@@ -146,7 +228,9 @@ class RealCommand extends GFCommand {
return result;
}
/**the text that is to be displayed as the tooltip */
/**
* the text that is to be displayed as the tooltip
*/
public String getTooltipText() {
String result;
result = this.printname.getTooltipText();
@@ -157,9 +241,15 @@ class RealCommand extends GFCommand {
return result;
}
/**
* returns the subcat of this command
*/
public String getSubcat() {
return this.printname.getSubcat();
if (this.subcat == null) {
return this.printname.getSubcat();
} else {
//special case, only for properties of self so far
return this.subcat;
}
}
protected final String showText;
}

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

@@ -26,8 +26,6 @@ import java.util.logging.*;
class RefinedAstNodeData extends AstNodeData {
protected final Printname printname;
protected final GfAstNode node;
protected final String position;
/**
* all we have to know about an already refined node is its Printname
@@ -36,13 +34,15 @@ class RefinedAstNodeData extends AstNodeData {
* not be parsed
* @param node the GfAstNode for the current line
* @param pos The position in the GF AST of this node in Haskell notation
* @param selected if this is the selected node in the GF AST
* @param constraint A constraint from a parent node, that also
* applies for this node.
*/
public RefinedAstNodeData(Printname pname, GfAstNode node, String pos) {
public RefinedAstNodeData(Printname pname, GfAstNode node, String pos, boolean selected, String constraint) {
super(node, pos, selected, constraint);
this.printname = pname;
this.node = node;
this.position = pos;
if (logger.isLoggable(Level.FINEST)) {
logger.finest(this.toString() + " - " + getPosition());
logger.finest(this.toString() + " - " + position);
}
}
@@ -65,17 +65,4 @@ class RefinedAstNodeData extends AstNodeData {
}
}
public boolean isMeta() {
return this.node.isMeta();
}
public String getPosition() {
return this.position;
}
public String toString() {
return this.node.getLine();
}
}

518
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinementMenu.java Normal file
View File

@@ -0,0 +1,518 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this applicationpackage de.uka.ilkd.key.ocl.gf;
package de.uka.ilkd.key.ocl.gf;
import java.awt.Color;
import java.awt.Font;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.awt.event.KeyEvent;
import java.awt.event.KeyListener;
import java.awt.event.MouseAdapter;
import java.awt.event.MouseEvent;
import java.awt.event.MouseListener;
import java.util.Collections;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
import java.util.Vector;
import java.util.logging.Level;
import java.util.logging.Logger;
import javax.swing.DefaultListModel;
import javax.swing.JList;
import javax.swing.JMenu;
import javax.swing.JMenuItem;
import javax.swing.JPopupMenu;
import javax.swing.JScrollPane;
import javax.swing.JSplitPane;
import javax.swing.ListSelectionModel;
/**
* Takes care of managing the commands, that GF sent,
* including subcategories and their menus.
* Manages the graphical lists. To display them, they are reachable
* via getRefinementListsContainer().
* @author hdaniels
*/
class RefinementMenu {
/**
* logs things like selections and key events
*/
private static Logger logger = Logger.getLogger(RefinementMenu.class.getName());
/**
* the editor of which this menu is part of
*/
final private GFEditor2 editor;
/**
* the content of the refinementMenu
*/
public DefaultListModel listModel= new DefaultListModel();
/**
* The list of current refinement options
*/
private JList refinementList = new JList(this.listModel);
/**
* to store the Vectors which contain the display names for the
* ListModel for refinementSubcatList for the different
* subcategory menus.
* The key is the shortname String, the value the Vector with the
* display Strings
*/
private Hashtable subcatListModelHashtable = new Hashtable();
/**
* this ListModel gets refilled every time a %WHATEVER command,
* which stands for a shortname for a subcategory of commands
* in the ListModel of refinementList, is selected there
*/
private DefaultListModel refinementSubcatListModel = new DefaultListModel();
/**
* The list of current refinement options in the subcategory menu
*/
private JList refinementSubcatList = new JList(this.refinementSubcatListModel);
/**
* the scrollpane containing the refinement subcategory
*/
private JScrollPane refinementSubcatPanel = new JScrollPane(this.refinementSubcatList);
/**
* store what the shorthand name for the current subcat is
*/
private String whichSubcat;
/**
* stores the two refinement JLists
*/
private JSplitPane refinementListsContainer;
/**
* the scrollpane containing the refinements
*/
private JScrollPane refinementPanel = new JScrollPane(this.refinementList);
/**
* here the GFCommand objects are stored
*/
private Vector gfcommands = new Vector();
/**
* The cached popup menu containing the same stuff as the refinement list
*/
public JPopupMenu popup2 = new JPopupMenu();
/**
* Creates the panels for the refinement (subcat) menu
* @param editor the editor, that the refinement menu is part of
*/
protected RefinementMenu(GFEditor2 editor) {
this.editor = editor;
refinementListsContainer = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT,refinementPanel, refinementSubcatPanel);
refinementList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
final MouseListener mlRefinementList = new MouseAdapter() {
public void mouseClicked(MouseEvent e) {
refinementList.setSelectionBackground(refinementSubcatList.getSelectionBackground());
boolean doubleClick = (e.getClickCount() == 2);
listAction(refinementList, refinementList.locationToIndex(e.getPoint()), doubleClick);
}
};
refinementList.addMouseListener(mlRefinementList);
refinementList.addKeyListener(new KeyListener() {
/** Handle the key pressed event for the refinement list. */
public void keyPressed(KeyEvent e) {
int keyCode = e.getKeyCode();
if (logger.isLoggable(Level.FINER)) {
logger.finer("Key pressed: " + e.toString());
}
int index = refinementList.getSelectedIndex();
if (index == -1) {
//nothing selected, so nothing to be seen here, please move along
} else if (keyCode == KeyEvent.VK_ENTER) {
listAction(refinementList, refinementList.getSelectedIndex(), true);
} else if (keyCode == KeyEvent.VK_DOWN && index < listModel.getSize() - 1) {
listAction(refinementList, index + 1, false);
} else if (keyCode == KeyEvent.VK_UP && index > 0) {
listAction(refinementList, index - 1, false);
} else if (keyCode == KeyEvent.VK_RIGHT) {
if (refinementSubcatList.getModel().getSize() > 0) {
refinementSubcatList.requestFocusInWindow();
refinementSubcatList.setSelectedIndex(0);
refinementList.setSelectionBackground(Color.GRAY);
}
}
}
/**
* Handle the key typed event.
* We are not really interested in typed characters, thus empty
*/
public void keyTyped(KeyEvent e) {
//needed for KeyListener, but not used
}
/** Handle the key released event. */
public void keyReleased(KeyEvent e) {
//needed for KeyListener, but not used
}
});
refinementSubcatList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
final MouseListener mlRefinementSubcatList = new MouseAdapter() {
public void mouseClicked(MouseEvent e) {
boolean doubleClick = (e.getClickCount() == 2);
listAction(refinementSubcatList, refinementSubcatList.locationToIndex(e.getPoint()), doubleClick);
refinementList.setSelectionBackground(Color.GRAY);
}
};
refinementSubcatList.addMouseListener(mlRefinementSubcatList);
refinementSubcatList.addKeyListener(new KeyListener() {
/** Handle the key pressed event. */
public void keyPressed(KeyEvent e) {
int keyCode = e.getKeyCode();
if (logger.isLoggable(Level.FINER)) {
logger.finer("Key pressed: " + e.toString());
}
if (keyCode == KeyEvent.VK_ENTER) {
listAction(refinementSubcatList, refinementSubcatList.getSelectedIndex(), true);
} else if (keyCode == KeyEvent.VK_LEFT) {
refinementList.requestFocusInWindow();
refinementSubcatList.clearSelection();
refinementList.setSelectionBackground(refinementSubcatList.getSelectionBackground());
}
}
/**
* Handle the key typed event.
* We are not really interested in typed characters, thus empty
*/
public void keyTyped(KeyEvent e) {
//needed for KeyListener, but not used
}
/** Handle the key released event. */
public void keyReleased(KeyEvent e) {
//needed for KeyListener, but not used
}
});
refinementList.setToolTipText("The list of current refinement options");
refinementList.setCellRenderer(new ToolTipCellRenderer());
refinementSubcatList.setToolTipText("The list of current refinement options");
refinementSubcatList.setCellRenderer(new ToolTipCellRenderer());
}
/**
* @return Returns the refinementListsContainer,
* which will contain both JLists.
*/
protected JSplitPane getRefinementListsContainer() {
return refinementListsContainer;
}
/**
* handling the event of choosing the action at index from the list.
* That is either giving commands to GF or displaying the subcat menus
* @param list The list that generated this action
* @param index the index of the selected element in list
* @param doubleClick true iff a command should be sent to GF,
* false if only a new subcat menu should be opened.
*/
private void listAction(JList list, int index, boolean doubleClick) {
if (index == -1) {
if (logger.isLoggable(Level.FINER)) logger.finer("no selection");
} else {
Object o;
if (list == refinementList) {
o = listModel.elementAt(index);
} else {
if (whichSubcat == null) {
//this is probably the case when no fitting properties of self
//are available and only a string is displayed in the submenu.
//clicking that string should do exactly nothing.
return;
}
Vector cmdvector = (Vector)this.subcatListModelHashtable.get(this.whichSubcat);
o = (cmdvector.get(index));
}
GFCommand command = null;
if (o instanceof GFCommand) {
command = (GFCommand)o;
} else {
return;
}
if (command instanceof SelfPropertiesCommand) {
SelfPropertiesCommand spc = (SelfPropertiesCommand)command;
Vector selfs = spc.produceSubmenu();
if (selfs.size() == 0) {
listModel.remove(index);
refinementSubcatListModel.clear();
refinementSubcatListModel.addElement("No properties fit here");
return;
} else {
this.subcatListModelHashtable.put(command.getSubcat(), selfs);
listModel.remove(index);
LinkCommand newLink = new LinkCommand(PrintnameManager.SELF_SUBCAT, editor.getPrintnameManager());
listModel.add(index, newLink);
command = newLink;
}
}
if (command instanceof LinkCommand) { //includes SelfPropertiesCommand, which is intended
this.whichSubcat = command.getSubcat();
refinementSubcatListModel.clear();
Vector currentCommands = (Vector)this.subcatListModelHashtable.get(this.whichSubcat);
for (Iterator it = currentCommands.iterator(); it.hasNext();) {
this.refinementSubcatListModel.addElement(it.next());
}
} else if (doubleClick && command instanceof InputCommand) {
InputCommand ic = (InputCommand)command;
editor.executeInputCommand(ic);
} else if (doubleClick){
refinementSubcatListModel.clear();
if (command instanceof RealCommand) {
editor.send("[t] " + command.getCommand(), true, ((RealCommand)command).undoSteps);
} else {
//that shouldn't be the case ...
editor.send("[t] " + command.getCommand());
}
} else if (list == refinementList){
refinementSubcatListModel.clear();
}
}
}
/**
* Produces the popup menu that represents the current refinements.
* An alternative to the refinement list.
* @return s.a.
*/
protected JPopupMenu producePopup() {
if (popup2.getComponentCount() > 0) {
return popup2;
}
for (int i = 0; i < this.listModel.size(); i++) {
GFCommand gfcmd = (GFCommand)this.listModel.get(i);
if (gfcmd instanceof LinkCommand) {
LinkCommand lc = (LinkCommand)gfcmd;
Vector subcatMenu = (Vector)this.subcatListModelHashtable.get(lc.getSubcat());
JMenu tempMenu = new JMenu(lc.getDisplayText());
tempMenu.setToolTipText(lc.getTooltipText());
tempMenu.setFont(popup2.getFont());
JMenuItem tempMenuItem;
for (Iterator it = subcatMenu.iterator(); it.hasNext();) {
GFCommand subgfcmd = (GFCommand)it.next();
tempMenuItem = menuForCommand(subgfcmd);
if (tempMenuItem != null) {
tempMenu.add(tempMenuItem);
}
}
popup2.add(tempMenu);
} else {
JMenuItem tempMenu = menuForCommand(gfcmd);
if (tempMenu != null) {
popup2.add(tempMenu);
}
}
}
return popup2;
}
/**
* takes a GFCommand and "transforms" it in a JMenuItem.
* These JMenuItems have their own listeners that take care of
* doing what is right ...
* @param gfcmd a RealCommand or an InputCommand
* (LinkCommand is ignored and produces null as the result)
* @return either the correspondend JMenuItem or null.
*/
private JMenuItem menuForCommand(GFCommand gfcmd) {
JMenuItem tempMenu = null;
if (gfcmd instanceof RealCommand){
tempMenu = new JMenuItem(gfcmd.getDisplayText());
tempMenu.setFont(popup2.getFont());
tempMenu.setActionCommand(gfcmd.getCommand());
tempMenu.setToolTipText(gfcmd.getTooltipText());
tempMenu.addActionListener(new ActionListener() {
public void actionPerformed(ActionEvent ae) {
JMenuItem mi = (JMenuItem)ae.getSource();
refinementSubcatListModel.clear();
String command = "[t] " + mi.getActionCommand();
editor.send(command);
}
});
} else if (gfcmd instanceof InputCommand) {
tempMenu = new JMenuItem(gfcmd.getDisplayText());
tempMenu.setFont(popup2.getFont());
tempMenu.setActionCommand(gfcmd.getCommand());
tempMenu.setToolTipText(gfcmd.getTooltipText());
tempMenu.addActionListener(new ActionListener() {
public void actionPerformed(ActionEvent ae) {
JMenuItem mi = (JMenuItem)ae.getSource();
String command = mi.getActionCommand();
InputCommand ic = InputCommand.forTypeName(command);
if (ic != null) {
editor.executeInputCommand(ic);
}
}
});
}
return tempMenu;
}
/**
* Takes the StringTuples in gfCommandVector, creates the RealCommand
* objects for them.
* Goes through this list and groups the RealCommands
* according to their subcategory tag (which starts with %)
* If there is a "(" afterwards, everything until the before last
* 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
* @param toAppend will be appended to every command, that is sent to GF.
* Normally, toAppend will be the empty String "".
* But it can be a chain command's second part.
* @param isAbstract If the selected menu language is abstract or not
* @param easyAttributes if true, attributes of self will be added.
* @param focusPosition The current position of the focus in the AST.
* Needed for easy access to properties of self.
* @param gfCapsule The read/write encapsulation of the GF process.
* Needed for easy access to properties of self.
*/
protected void formRefinementMenu(final Vector gfCommandVector, final String toAppend, GfAstNode currentNode, final boolean isAbstract, boolean easyAttributes, LinPosition focusPosition, GfCapsule gfCapsule) {
this.listModel.clear();
this.refinementSubcatListModel.clear();
this.gfcommands.clear();
this.subcatListModelHashtable.clear();
this.whichSubcat = null;
this.popup2.removeAll();
Vector prelListModel = new Vector();
/** to keep track of subcats and their names */
HashSet processedSubcats = new HashSet();
//at the moment, we don't know yet, which subcats are
//nearly empty
for (Iterator it = gfCommandVector.iterator(); it.hasNext();) {
final StringTuple st = (StringTuple)it.next();
GFCommand gfcommand;
if (st instanceof ChainCommandTuple) {
ChainCommandTuple cct = (ChainCommandTuple)st;
gfcommand = new RealCommand(st.first, processedSubcats, editor.getPrintnameManager(), st.second, isAbstract, toAppend, cct.undoSteps, cct.fun, cct.subcat);
} else {
gfcommand = new RealCommand(st.first, processedSubcats, editor.getPrintnameManager(), st.second, isAbstract, toAppend);
}
if ((!editor.isGroupSubcat()) || (gfcommand.getSubcat() == null)) {
prelListModel.addElement(gfcommand);
} else {
//put stuff in the correct Vector for the refinementSubcatListModel
Vector lm;
if (subcatListModelHashtable.containsKey(gfcommand.getSubcat())) {
lm = (Vector)this.subcatListModelHashtable.get(gfcommand.getSubcat());
} else {
lm = new Vector();
this.subcatListModelHashtable.put(gfcommand.getSubcat(), lm);
}
lm.addElement(gfcommand);
if (gfcommand.isNewSubcat()) {
GFCommand linkCmd = new LinkCommand(gfcommand.getSubcat(), editor.getPrintnameManager());
prelListModel.addElement(linkCmd);
}
}
}
//so we remove empty subcats now and replace them by their RealCommand
for (int i = 0; i < prelListModel.size(); i++) {
if (prelListModel.get(i) instanceof LinkCommand) {
LinkCommand lc = (LinkCommand) prelListModel.get(i);
Vector subcatMenu = (Vector)this.subcatListModelHashtable.get(lc.getSubcat());
if (subcatMenu.size() == 1) {
RealCommand rc = (RealCommand)subcatMenu.get(0);
prelListModel.set(i, rc);
}
}
}
// Some types invite special treatment, like Int and String
// which can be read from the user.
if (currentNode.isMeta()) {
InputCommand usedInputCommand = null;
if (currentNode.getType().equals("Int")) {
usedInputCommand = InputCommand.intInputCommand;
prelListModel.addElement(usedInputCommand);
} if (currentNode.getType().equals("String")) {
usedInputCommand = InputCommand.stringInputCommand;
prelListModel.addElement(usedInputCommand);
}
if (usedInputCommand != null) {
for (Iterator it = usedInputCommand.enteredValues.iterator(); it.hasNext();) {
Object o = it.next();
//for GF it seems to make no difference,
//if we use 'g' or 'r' as the command to send
//Int and String. 'r' is already supported
//by RealCommand, so I chose that.
RealCommand rc = new RealCommand("r " + o, processedSubcats, editor.getPrintnameManager(), "r " + o, isAbstract, toAppend);
prelListModel.addElement(rc);
}
}
}
//add the special entry for the properties of self
if (easyAttributes) {
final SelfPropertiesCommand spc = new SelfPropertiesCommand(editor.getPrintnameManager(), gfCapsule, focusPosition, isAbstract, toAppend, processedSubcats);
prelListModel.add(spc);
}
//now sort the preliminary listmodels
if (editor.isSortRefinements()) {
Collections.sort(prelListModel);
for (Iterator it = subcatListModelHashtable.values().iterator(); it.hasNext();) {
Vector slm = (Vector)it.next();
Collections.sort(slm);
}
}
//now fill this.listModel
for (Iterator it = prelListModel.iterator(); it.hasNext();) {
Object next = it.next();
this.listModel.addElement(next);
}
//select the first command in the refinement menu, if available
if (this.listModel.size() > 0) {
this.refinementList.setSelectedIndex(0);
} else {
this.refinementList.setSelectedIndex(-1);
}
this.refinementList.setSelectionBackground(refinementSubcatList.getSelectionBackground());
}
/**
* Requests the focus for the refinement list
*/
protected void requestFocus() {
refinementList.requestFocusInWindow();
}
/**
* clears the list model
*/
protected void reset() {
listModel.clear();
}
/**
* Applies newFont to the visible elements
* @param newFont The new font, what else?
*/
protected void setFont(Font newFont) {
refinementList.setFont(newFont);
refinementSubcatList.setFont(newFont);
popup2.setFont(newFont);
}
}

51
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinementMenuCollector.java Normal file
View File

@@ -0,0 +1,51 @@
package de.uka.ilkd.key.ocl.gf;
import java.util.Vector;
/**
* Asks GF the Vector of RefinementMenu entries.
*
* This class can be reused.
* @author daniels
*/
class RefinementMenuCollector extends AbstractProber {
/**
* here the result of this run is saved
*/
Vector refinementMenuContent = null;
/**
* Standard fill-in-the-parameters constructor
* @param gfCapsule The reader/writer to GF
*/
public RefinementMenuCollector(GfCapsule gfCapsule) {
super(gfCapsule);
}
/**
* Asks GF (the same GF as the one editor has) to execute a command
* and returns the read refinement menu that is offered then.
* Uses the readRefinementMenu method from GFEditor2 which does not
* change any global variable besides GF itself. So that is safe.
*
* Note: This method does not do undo automatically, since it is
* intended to run several times in a row, so the u should be part of
* next command.
* @param command The command that is sent to GF. Should contain a mp
* to make sure that the command at the right position in the AST
* is read
* @return a Vector of StringTuple like readRefinementMenu does it.
*/
public Vector readRefinementMenu(String command) {
send(command);
readGfedit();
return this.refinementMenuContent;
}
/**
* parses the refinement menu part and stores it in this.refinementMenuContent
*/
protected void readMenu() {
this.refinementMenuContent = gfCapsule.readRefinementMenu();
}
}

223
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinementMenuTransformer.java Normal file
View File

@@ -0,0 +1,223 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Vector;
import java.util.logging.Level;
import java.util.logging.Logger;
/**
* This class is completely static and cannot be instantiated.
* @see #transformRefinementMenu(de.uka.ilkd.key.ocl.gf.TreeAnalysisResult, java.util.Vector, de.uka.ilkd.key.ocl.gf.GfCapsule)
* @author hdaniels
*/
class RefinementMenuTransformer {
/**
* if things are added to or removed from the refinement menu
*/
protected static Logger logger = Logger.getLogger(RefinementMenuTransformer.class.getName());
private RefinementMenuTransformer() {
//A private constructor enforces the noninstantiability
//of "RefinementMenuTransformer".
//(See item 3 of "Effective Java".)
}
/**
* Depending on tar, the refinement menu given in raw form in oldMenu
* is transformed.
* That includes:
* - adding properties of self
* - producing a reduced version for subtyping below a coerce
* where only Instances of subtypes are listed
* - probes, if self and result are really applicable
* - changes the delete command, when an unrefined Instance
* argument of coerce is clicked on, to first delete the
* whole coerce to avoid sticking with wrong type arguments.
* @param tar TreeAnalyser has decided what to do here. That is followed.
* @param oldMenu The original content of the refinement menu.
* Is a Vector of StringTuple
* @param gfCapsule The encapsulation of GF regarding read/write access
* @return The refinement menu in its new form
*/
protected static Vector transformRefinementMenu(TreeAnalysisResult tar, Vector oldMenu, GfCapsule gfCapsule) {
//now do fill (or partially empty) the offered commands list
final Vector usedCommandVector;
if (tar.reduceCoerce) {
//is only true if switched on globally.
//And if conditions are right.
usedCommandVector = produceReducedCoerceRefinementMenu(tar.focusPosition.position, gfCapsule);
} else {
usedCommandVector = oldMenu;
}
if (tar.deleteAlsoAbove) {
String newPos = tar.focusPosition.parentPosition();
StringTuple newDelete = new StringTuple("mp " + newPos + " ;; d", "delete current subtree\\$also delete the encompassing coercion ");
exchangeCommand(usedCommandVector, "d", newDelete);
}
if (tar.probeSelfResult) {
probeCompletability(usedCommandVector, tar.focusPosition, gfCapsule);
}
if (tar.easyAttributes && !tar.reduceCoerce) {
addSelfProperties(usedCommandVector, tar.focusPosition, gfCapsule);
}
return usedCommandVector;
}
/**
* Looks at the subtyping witness of the same coerce as currentPos
* and collects the possible refinements for all offered subtypes.
* It assumes that argument 0 of coerce is automatically filled in.
*
* This method is surely <b>slow</b> since a lot of calls to GF is made
* here.
* @param currentPos musst point to a child of a coerce.
* @param gfCapsule The encapsulation of GF regarding read/write access
* @return a Vector of StringTuple as readRefinementMenu does.
* This Vector can be fed into formRefinementMenu.
*/
private static Vector produceReducedCoerceRefinementMenu(String currentPos, GfCapsule gfCapsule) {
final HashSet commands = new HashSet();
RefinementMenuCollector rmc = new RefinementMenuCollector(gfCapsule);
//move to the subtype witness argument
final String collectSubtypesCommand = "mp " + LinPosition.calculateBrethrenPosition(currentPos, 2);
Vector possibleSubtypes = rmc.readRefinementMenu(collectSubtypesCommand);
String undoString = "";
final String undoTemplate = "u 2 ;; ";
for (Iterator it = possibleSubtypes.iterator(); it.hasNext(); ) {
StringTuple nextCommand = (StringTuple)it.next();
// if (!nextCommand.first.trim().startsWith("r")) {
// //no ac, d, rc or whatever wanted here. Only refine.
// continue;
// }
final String collectRefinementsCommand = undoString + nextCommand.first + " ;; mp " + currentPos;
undoString = undoTemplate; //for all following runs we want an undo before it
Vector nextRefinements = rmc.readRefinementMenu(collectRefinementsCommand);
commands.addAll(nextRefinements);
}
final String cleanupCommand = "u 3"; //undo the last command and also the first mp
rmc.readRefinementMenu(cleanupCommand); //no harm done here, collector won't get reused
Vector result = new Vector(commands);
return result;
}
/**
* checks if result and self make sense in the current context.
* if not, they are removed from oldMenu
* @param oldMenu A Vector of StringTuple that represents the
* commands for the refinement menu
* @param focusPos The current position in the AST
* @param gfCapsule The encapsulation of GF regarding read/write access
*/
private static void probeCompletability(Vector oldMenu, LinPosition focusPos, GfCapsule gfCapsule) {
/**
* 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
*/
if (focusPos == null) {
//sadly, we can't do much
return;
}
final String childPos = focusPos.childPosition(1);
final SelfResultProber cp = new SelfResultProber(gfCapsule);
for (int i = 0; i < oldMenu.size(); i++) {
String cmd = ((StringTuple)oldMenu.elementAt(i)).first;
if ((cmd != null) && ((cmd.indexOf("r core.self") > -1) || (cmd.indexOf("r core.result") > -1))) {
//the first mp is necessary for the second of self/result.
//without, GF will jump to a stupid position
String newCommand = "mp " + focusPos.position + " ;; " + cmd + " ;; mp " + childPos;
if (!cp.isAutoCompletable(newCommand, 3)) {
oldMenu.remove(i);
i -=1;
}
}
}
}
/**
* Probes for the properties of self, that could be filled in at
* the current focus position.
* If it finds any, these are added to oldMenu
* This method will add all offered commands to the refinement menu,
* not only for suiting subtypes due to speed reasons.
* @param oldMenu A Vector of StringTuple. The menu with the commands
* and show texts as given by GF. Gets modified.
* @param focusPos The position of the GF focus in the AST
* @param gfCapsule The encapsulation of GF regarding read/write access
*/
private static void addSelfProperties(Vector oldMenu, LinPosition focusPos, GfCapsule gfCapsule) {
//solve in between to avoid some typing errors by closing some type arguments
final String probeCommand = "r core.implPropCall ;; mp " + focusPos.childPosition(2) + " ;; r core.self ;; solve ;; mp " + focusPos.childPosition(3);
final String deleteAppendix = " ;; d";
final RefinementMenuCollector rmc = new RefinementMenuCollector(gfCapsule);
Vector futureRefinements = rmc.readRefinementMenu(probeCommand + deleteAppendix);
final int undos = 5;
final boolean singleRefinement;
if (futureRefinements.size() == 1) {
singleRefinement = true;
} else {
singleRefinement = false;
}
final String cleanupCommand = "u " + undos;
rmc.readRefinementMenu(cleanupCommand); //no harm done here
for (Iterator it = futureRefinements.iterator(); it.hasNext();) {
StringTuple st = (StringTuple)it.next();
if (st.first.startsWith("r")) { //is a refinement, no ac or d
String newCommand;
//add the command that came before
final int cmdUndos;
if (singleRefinement) {
//that is an exceptional case, but might happen.
//Here we don't have to refine the final property
//at all, since GF does that automatically
newCommand = probeCommand + " ;; c solve";
cmdUndos = 5;
} else {
//here the 'd' is not needed, since we know,
//that nothing is refined automatically
newCommand = probeCommand + " ;; " + st.first + " ;; c solve";
cmdUndos = 6;
}
// now extract the fun of the property
String fun = st.first.substring(1).trim();
ChainCommandTuple cct = new ChainCommandTuple(newCommand, st.second, fun, PrintnameManager.SELF_SUBCAT, cmdUndos);
if (logger.isLoggable(Level.FINER)) {
logger.finer("added " + cct);
}
oldMenu.add(cct);
}
}
}
/**
* Goes through oldMenu and if it finds a command in there, where
* first.equals(oldCommand), this command is replaced by newCommand.
* oldMenu's content thus gets modified.
* @param oldMenu a Vector of StringTuple
* @param oldCommand a GF command string (what is sent, not the show text)
* @param newCommand a StringTuple representing what could be a pait from GF
*/
private static void exchangeCommand(Vector oldMenu, String oldCommand, StringTuple newCommand) {
for (int i = 0; i < oldMenu.size(); i++) {
StringTuple next = (StringTuple)oldMenu.get(i);
if (next.first.equals(oldCommand)) {
oldMenu.remove(i);
oldMenu.insertElementAt(newCommand, i);
}
}
}
}

175
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/SelfPropertiesCommand.java Normal file
View File

@@ -0,0 +1,175 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this applicationpackage de.uka.ilkd.key.ocl.gf;
package de.uka.ilkd.key.ocl.gf;
import java.util.Collections;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Vector;
import java.util.logging.Level;
import java.util.logging.Logger;
/**
* This class is an unclean hack.
* The whole refinement menu architecture expected, that everything is probed,
* when the refinement menu is getting created.
* But for getting only subtype correct properties of self needs a number of
* calls to GF, which could be deferred to not make things slower than they
* already are.
* This deferred probing is done in this class.
* @author daniels
*
*/
class SelfPropertiesCommand extends LinkCommand {
private final static Logger logger = Logger.getLogger(SelfPropertiesCommand.class.getName());
private final GfCapsule gfCapsule;
private final LinPosition focusPos;
private final String toAppend;
private final boolean isAbstract;
private final HashSet processedSubcats;
private final PrintnameManager printnameManager;
/**
* A simple setter constructor, no calculation done here.
* @param manager The printname manager, that knows, how the properties
* of self should be listed in the refinement menu
* @param gfCapsule The reader/writer abstraction from GF
* @param focusPos The position of the GF focus
* @param isAbstract if Abstract is the current menu language
* @param toAppend If something should be appended to the command
* @param processedSubcats Here, the subcat for self is put into
*/
public SelfPropertiesCommand(final PrintnameManager manager, GfCapsule gfCapsule, LinPosition focusPos, boolean isAbstract, String toAppend, HashSet processedSubcats) {
super(PrintnameManager.SELF_SUBCAT, manager);
this.gfCapsule = gfCapsule;
this.printnameManager = manager;
this.focusPos = focusPos;
this.processedSubcats = processedSubcats;
this.toAppend = toAppend;
this.isAbstract = isAbstract;
}
/**
* @return a Vector of RealCommand containing the suitable properties
* of self at the current focus position.
* Subtyping is taken into account, so only properties with a subtype
* of the supertype of the coerce above (at other places this method
* is not applicable) show up in this menu.
* The method used is similiar to the one for Instances below a coerce.
*/
Vector produceSubmenu() {
logger.fine("SelfPropertiesCommand asked to produce a menu");
//HashSet to prevent duplicates
final HashSet commands = new HashSet();
RefinementMenuCollector rmc = new RefinementMenuCollector(gfCapsule);
//move to the subtype witness argument
final String collectSubtypesCommand = "mp " + LinPosition.calculateBrethrenPosition(focusPos.position, 2);
final Vector possibleSubtypes = rmc.readRefinementMenu(collectSubtypesCommand);
String undoString = "";
int undos = 0;
//for the case, that there is only one possible refinement at all
//which gets automatically filled in
final StringBuffer singleReplacement = new StringBuffer();
//loop through the offered Subtype refinements
for (Iterator it = possibleSubtypes.iterator(); it.hasNext(); ) {
StringTuple nextCommand = (StringTuple)it.next();
if (!nextCommand.first.trim().startsWith("r")) {
//no ac, d, rc or whatever wanted here. Only refine.
continue;
}
final String commandPrefix = undoString + nextCommand.first + " ;; mp " + focusPos.position + " ;; ";
logger.finer("commandPrefix: " + commandPrefix);
Vector futureRefinements = new Vector();
undos = addSelfProperties(futureRefinements, commandPrefix, singleReplacement);
undos += 2; // to undo commandPrefix
undoString = "u " + undos + " ;; "; //for all following runs we want an undo before it
// Vector nextRefinements = rmc.readRefinementMenu(collectRefinementsCommand);
commands.addAll(futureRefinements);
}
final String cleanupCommand = "u " + (undos + 1); //undo the last command and also the first mp
rmc.readRefinementMenu(cleanupCommand); //no harm done here, collector won't get reused
Vector result = new Vector();
for (Iterator it = commands.iterator(); it.hasNext();) {
StringTuple st = (StringTuple)it.next();
if ((commands.size() == 1) && (st instanceof ChainCommandTuple)) {
//the case when only one property is available at all.
//Then this will automatically be selected
//To compensate for that, singleRefinement is used.
//This will be just one refinement, otherwise, we
//wouldn't be in this branch.
//This refinement does not contain the actual r
//command and therefore needs one undo step less
ChainCommandTuple cct = (ChainCommandTuple)st;
st = new ChainCommandTuple(singleReplacement.toString(), cct.second, cct.fun, cct.subcat, cct.undoSteps - 1);
}
GFCommand gfcommand;
if (st instanceof ChainCommandTuple) {
ChainCommandTuple cct = (ChainCommandTuple)st;
gfcommand = new RealCommand(st.first, processedSubcats, printnameManager, st.second, isAbstract, toAppend, cct.undoSteps, cct.fun, cct.subcat);
} else {
gfcommand = new RealCommand(st.first, processedSubcats, printnameManager, st.second, isAbstract, toAppend);
}
result.add(gfcommand);
}
Collections.sort(result);
return result;
}
/**
* Probes for the properties of self, that could be filled in at
* the current focus position.
* If it finds any, these are added to result.
* @param result The Vector, that will get filled with the collected
* chain commands
* @param commandPrefix The prefix, that is to be prepended to the
* probing command. Used for refining with a Subtype witness and a
* mp to the Instance position, where this method expects to start.
* @param singleReplacement This is a hack for cases, when GF refines
* an refinement automatically. If that happens only for one subtype,
* then GF would fill that in automatically even when the supertype is
* open. Therefore, it must be omitted in the actual command.
* But this situation can only be checked after all subtypes have been
* probed.
* @return the number of undo steps needed to undo the probing command
* (without prefix, that is handled by the caller)
*/
private int addSelfProperties(final Vector result, final String commandPrefix, final StringBuffer singleReplacement) {
//solve in between to avoid some typing errors by closing some type arguments
final String probeCommand = "r core.implPropCall ;; mp " + focusPos.childPosition(2) + " ;; r core.self ;; solve ;; mp " + focusPos.childPosition(3);
final String deleteAppendix = " ;; d";
final RefinementMenuCollector rmc = new RefinementMenuCollector(gfCapsule);
final String actualProbeCommand = commandPrefix + probeCommand + deleteAppendix;
logger.finer("&&& actual probe command:: " + actualProbeCommand);
Vector futureRefinements = rmc.readRefinementMenu(actualProbeCommand);
final int undos = 5;
for (Iterator it = futureRefinements.iterator(); it.hasNext();) {
StringTuple st = (StringTuple)it.next();
if (st.first.startsWith("r")) { //is a refinement, no ac or d
String newCommand;
//add the command that came before
final int cmdUndos;
if (futureRefinements.size() == 1) {
//the case, when only one property is defined in the grammar:
singleReplacement.append(probeCommand + " ;; c solve");
}
newCommand = probeCommand + " ;; " + st.first + " ;; c solve";
cmdUndos = 6;
// now extract the fun of the property
String fun = st.first.substring(1).trim();
ChainCommandTuple cct = new ChainCommandTuple(newCommand, st.second, fun, PrintnameManager.SELF_SUBCAT, cmdUndos);
if (logger.isLoggable(Level.FINE)) {
logger.finer("added " + cct);
}
result.add(cct);
}
}
return undos;
}
}

59
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/CompletableProber.java → src/JavaGUI2/de/uka/ilkd/key/ocl/gf/SelfResultProber.java
View File

@@ -1,8 +1,5 @@
package de.uka.ilkd.key.ocl.gf;
import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.IOException;
import java.util.logging.*;
/**
@@ -11,22 +8,21 @@ import java.util.logging.*;
* This class is meant for self and result.
* @author daniels
*/
class AutoCompletableProber extends AbstractProber {
class SelfResultProber 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());
protected static Logger nogger = Logger.getLogger(SelfResultProber.class.getName());
/**
* A constructor which sets some fields
* @param fromGf the stdout from the GF process
* @param toGf the stdin from the GF process
* @param gfCapsule The encapsulation of the running GF process
*/
public AutoCompletableProber(BufferedReader fromGf, BufferedWriter toGf) {
super(fromGf, toGf);
public SelfResultProber(GfCapsule gfCapsule) {
super(gfCapsule);
}
/**
@@ -51,7 +47,7 @@ class AutoCompletableProber extends AbstractProber {
this.autocompleted = true;
//clean up and undo
send("u " + chainCount);
readAndIgnore(fromProc);
readAndIgnore();
if (nogger.isLoggable(Level.FINE)) {
nogger.fine(result + " is the result for: '" + gfCommand +"'");
}
@@ -63,31 +59,26 @@ class AutoCompletableProber extends AbstractProber {
* 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);
String treeString = gfCapsule.readTree();
String[] treeArray = treeString.split("\\n");
for (int i = 0; i < treeArray.length; i++) {
String result = treeArray[i].trim();
if (result.startsWith("*")) {
result = result.substring(1).trim();
if (result.startsWith("?")) {
//the normal case, focus position open
this.autocompleted = false;
} else if ((i >= 6) //that we could be at the instance argument at all
&& (treeArray[i - 6].indexOf("coerce") > -1) //we are below a coerce
&& (treeArray[i - 3].trim().startsWith("?")) //the Subtype argument is not filled in
// The super argument cannot be OclAnyC or even unrefined, because then this
// method wouldn't have been called. Thus, the Subtype argument is unique.
){
//we are below a coerce, but self would have a non-suiting subtype
this.autocompleted = false;
}
}
} catch(IOException e){
System.err.println(e.getMessage());
e.printStackTrace();
}
}
}

54
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/StringTuple.java Normal file
View File

@@ -0,0 +1,54 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/**
* Small tuple class for two Strings.
* The main use is grouping command and showname for GF commands before
* they are processed.
* This class is mutable.
* Equality is bound to the first argument.
* @author daniels
*/
class StringTuple {
String first;
String second;
/**
* Just sets both values.
* @param f Well, the first String
* @param s Well, the second String
* (if it is used at all)
*/
public StringTuple(String f, String s) {
this.first = f;
this.second = s;
}
public int hashCode() {
return this.first.hashCode();
}
public boolean equals(Object o) {
if (o instanceof StringTuple) {
return this.first.equals(((StringTuple)o).first);
} else {
return false;
}
}
public String toString() {
return this.first;
}
}

107
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/SubtypingProber.java Normal file
View File

@@ -0,0 +1,107 @@
package de.uka.ilkd.key.ocl.gf;
import java.util.logging.Logger;
import java.util.*;
/**
* This class goes through the tree and tries to close all open Subtype lines.
*
* Makes heavy use of instance fields instead of parameters and return values.
* I justify that with the rather small size of this class.
* Because of this this class has to be reinitialized for each run.
* @author daniels
*/
class SubtypingProber extends RefinementMenuCollector {
private static Logger nogger = Logger.getLogger(SubtypingProber.class.getName());
/**
* how many undos are needed to clean up behind this probing
*/
protected int undoSteps = 0;
/**
* the GF AST line by line
*/
protected String[] treeArray = new String[0];
/**
* the pointer to the line, that has been read last
*/
protected int currentLine;
/**
* Standard fill-in-the-parameters constructor
* @param gfCapsule The encapsulation of GF
*/
public SubtypingProber(GfCapsule gfCapsule) {
super(gfCapsule);
this.currentLine = 0;
}
/**
* stores the read GF AST in treeArray
*/
protected void readTree() {
String treeString = gfCapsule.readTree();
this.treeArray = treeString.split("\\n");
}
/**
* looks at the refinement menu for node number lineNumber in the AST
* and if there is only one refinement command offered, does
* execute this.
* @param lineNumber
*/
protected void checkLine(int lineNumber) {
String command = "mp [] ;; > " + lineNumber;
this.undoSteps += 2;
send(command);
readGfedit();
Vector commands = new Vector();
for (Iterator it = this.refinementMenuContent.iterator(); it.hasNext(); ) {
StringTuple next = (StringTuple)it.next();
if (next.first.startsWith("r")) {
commands.add(next);
}
}
if (commands.size() == 0) {
//nothing can be done
nogger.fine("no refinement for '" + this.treeArray[lineNumber] + "'");
} else if (commands.size() == 1) {
StringTuple nextCommand = (StringTuple)commands.lastElement();
nogger.fine("one refinement for '" + this.treeArray[lineNumber] + "'");
send(nextCommand.first);
this.undoSteps += 1;
// now new things are in the state,
// but since we assume that nothing above lineNumber changes,
// that is wanted.
readGfedit();
} else {
nogger.fine(commands.size() + " refinements for '" + this.treeArray[lineNumber] + "'");
}
}
/**
* Asks GF for the AST and tries to hunt down all unrefined
* Subtype witnesses.
* @return the number of undo steps this run needed
*/
public int checkSubtyping() {
//solve to try to eliminate many unrefined places
send("c solve ;; mp []"); //focus at the top where '*' does not disturb
readGfedit();
this.undoSteps += 2;
for (int i = 3; i < this.treeArray.length; i++) {
//the condition gets rechecked every run, and length will only grow
//We start at 3 since the witness is the third argument of coerce,
//before nothing can happen
//(sth. like "n core.Subtype" does not count!
//(starting with new category Subtype) )
if (this.treeArray[i].indexOf(": Subtype") > -1) {
if (!this.treeArray[i - 2].startsWith("?") //both Class arguments refined
&& !this.treeArray[i - 1].startsWith("?")) {
checkLine(i);
}
}
}
nogger.fine(this.undoSteps + " individual commands sent");
return this.undoSteps;
}
}

387
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/TreeAnalyser.java Normal file
View File

@@ -0,0 +1,387 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.Enumeration;
import java.util.logging.Level;
import java.util.logging.Logger;
import javax.swing.tree.DefaultMutableTreeNode;
/**
* Goes through the AST and:
* Labels node according to the following:
* hidden, if they are a coerce without a constraint
* colored, if they are a coerce with a constraint
* Saves a reference to the currently selected node
* Finds out
* if attributes of self should be given an easy access,
* if the refinement menu below a coerce should be reduces,
* if it should be probed, if self and result are superfluous
* in the refinement menu.
* if a coerce should be introduced automatically.
* Takes a tree and hides the nodes labelled as hidden in another stage.
* @author hdaniels
*/
class TreeAnalyser {
/**
* debug stuff for the tree
*/
private static Logger treeLogger = Logger.getLogger(TreeAnalyser.class.getName());
/**
* dealing with coerce, when it is inserted and so on
*/
private static Logger coerceLogger = Logger.getLogger(TreeAnalyser.class.getName() + ".coerce");
/**
* if coerce should get hidden, if all their arguments are refined
*/
private boolean hideCoerce;
/**
* if coerce should always be hidden,
*/
private boolean hideCoerceAggressive;
/**
* if the refinement menu should get condensed at all
*/
private boolean coerceReduceRM;
/**
* if coerce should get introduced automatically at all
*/
private boolean autoCoerce;
/**
* if result and self should be shown always
*/
private boolean showSelfResult;
/**
* if properties of self should be probed for
*/
private boolean easyAttributes;
/**
* If coerces whith both Class arguments
*/
private boolean highlightSubtypingErrors;
/**
* @param autoCoerce if coerce should get introduced automatically at all
* @param coerceReduceRM if the refinement menu should get condensed at all
* @param easyAttributes if properties of self should be probed for
* @param hideCoerce if coerce should get hidden, if all their arguments are refined
* @param hideCoerceAggressive if coerce should always be hidden,
* unless there is a GF constraint
* @param highlightSubtypingErrors If coerces whith both Class arguments
* refined, but not with the Subtype argument should get marked
* @param showSelfResult if result and self should be shown always
*/
public TreeAnalyser(boolean autoCoerce, boolean coerceReduceRM, boolean easyAttributes, boolean hideCoerce, boolean hideCoerceAggressive, boolean highlightSubtypingErrors, boolean showSelfResult) {
this.autoCoerce = autoCoerce;
this.coerceReduceRM = coerceReduceRM;
this.easyAttributes = easyAttributes;
this.hideCoerce = hideCoerce;
this.hideCoerceAggressive = hideCoerceAggressive;
this.highlightSubtypingErrors = highlightSubtypingErrors;
this.showSelfResult = showSelfResult;
}
/**
* Takes the rootNode of the AST and does some small analysis on it:
* Check for missing Subtype witnesses,
* check if the Instance menu of a Coerce can be reduced
* @param topNode The root or top node of the AST
* @return an object that contains the result of this analysis.
* Currently this applies only to the selected node.
* @see TreeAnalysisResult
*/
TreeAnalysisResult analyseTree(DefaultMutableTreeNode topNode) {
//just the initial values
String resultCommand = null;
int resultUndoSteps = -1;
boolean resultReduceCoerce = false;
boolean resultProbeSelfResult = false;
boolean resultDeleteAlsoAbove = false;
boolean resultEasyAttributes = false;
TreeAnalysisResult tar = new TreeAnalysisResult(resultCommand, resultUndoSteps, resultReduceCoerce, resultProbeSelfResult, resultDeleteAlsoAbove, resultEasyAttributes, null, null);
//doing it depth first, because we have to know the subtypingStatus
//of the children of coerce before we analyze coerce itself
for (Enumeration e = topNode.depthFirstEnumeration() ; e.hasMoreElements() ;) {
DefaultMutableTreeNode currNode = (DefaultMutableTreeNode)e.nextElement();
analyseTreeNode(currNode, tar);
}
AstNodeData and = (AstNodeData)tar.selectedNode.getUserObject();
if ((and.showInstead != -1) && (tar.command == null)) {
//if the current node is hidden, move up in the tree,
//until a visible node is found
DefaultMutableTreeNode tn = (DefaultMutableTreeNode)tar.selectedNode.getParent();
AstNodeData dand = null;
while (tn != null) {
dand = (AstNodeData)tn.getUserObject();
if (dand.showInstead == -1) {
//found a visible node
break;
}
tn = (DefaultMutableTreeNode)tn.getParent();
}
if (dand != null) {
tar.command = "[tr] mp " + dand.position;
tar.undoSteps = 1;
} //otherwise give up, can only occur, if coerce is the top node.
//And for that, one would have to do a "n Instance" first,
//which GF does not even offer.
}
return tar;
}
/**
* Takes the rootNode of the AST and does some small analysis on it:
* Check for missing Subtype witnesses,
* check if the Instance menu of a Coerce can be reduced
* @param nodeToCheck The node that is to be analysed
* @param tar The result, that gets modified
* @see TreeAnalysisResult
*/
private void analyseTreeNode(DefaultMutableTreeNode nodeToCheck, TreeAnalysisResult tar) {
AstNodeData and = (AstNodeData)nodeToCheck.getUserObject();
DefaultMutableTreeNode parent = (DefaultMutableTreeNode)nodeToCheck.getParent();
Printname parentPrintname = null;
if ((parent != null) && (parent.getUserObject() != null) && (parent.getUserObject() instanceof AstNodeData)) {
AstNodeData parentAnd = (AstNodeData)parent.getUserObject();
parentPrintname = parentAnd.getPrintname();
}
if (and.selected) {
tar.selectedNode = nodeToCheck;
tar.currentNode = and.node;
//set the focusPosition to a preliminary value
tar.focusPosition = new LinPosition(and.position, true);
//rather check too much for null
if (this.autoCoerce
&& (and.node != null)
&& and.node.isMeta()
&& (parent != null)
&& (parent.getUserObject() != null)
&& (and.node.getType() != null)
&& (and.node.getType().startsWith("Instance"))) {
//check, if a coerce is needed
GfAstNode parentNode = ((AstNodeData)parent.getUserObject()).node;
if (parentPrintname.getParamAutoCoerce(parent.getIndex(nodeToCheck))) {
coerceLogger.fine("Coerceable fun found: " + and.node + " + " + parentNode);
//refine with coerce. Do not allow another GF run, so [r]
tar.command = "[tr] r core.coerce ;; mp " + LinPosition.calculateChildPosition(and.position, 3);
tar.undoSteps = 2; //move there is also sth. to be undone
} else if ((parentNode.getFun().indexOf("coerce") > -1)
//to avoid getting stuck below a coerce with wrong type arguments
//the coerce above is deleted and rerefined.
//coerce below a coerce is never done automatically, so the else if is justified,
//meaning, that introduced a coerce, we do not have to delete it right a away
&& parent.getParent() != null
&& (parent.getParent() instanceof DefaultMutableTreeNode)) {
DefaultMutableTreeNode grandParent = (DefaultMutableTreeNode)parent.getParent();
if (grandParent != null) {
AstNodeData grandParentAnd = (AstNodeData)grandParent.getUserObject();
Printname grandParentPrintname = grandParentAnd.getPrintname();
if (grandParentPrintname.getParamAutoCoerce(grandParent.getIndex(parent))) {
coerceLogger.fine("Auto-Coerce to be un- and redone: "
+ and.node + " + " + parentNode
+ " -- " + tar.focusPosition.position);
tar.command = "[tr] mp " + tar.focusPosition.parentPosition()
+ " ;; d ;; mp " + tar.focusPosition.parentPosition()
+ " ;; r core.coerce ;; mp " + tar.focusPosition.position;
tar.undoSteps = 6;
}
}
}
}
if (coerceReduceRM
&& (and.node != null)
&& (and.node.getType() != null)
&& (parent != null)
&& (parent.getUserObject() != null)
&& (((AstNodeData)parent.getUserObject()).getPrintname() != null)
&& (((AstNodeData)parent.getUserObject()).getPrintname().fun.endsWith("coerce"))
&& (and.node.getType().startsWith("Instance")) //if coerce, than we are the Instance argument
&& (((DefaultMutableTreeNode)(parent.getChildAt(2))).getUserObject() != null)
&& (parent.getChildAt(2) != null)
&& ((AstNodeData)((DefaultMutableTreeNode)(parent.getChildAt(2))).getUserObject()).node.isMeta()) {
AstNodeData superTypeAnd = ((AstNodeData)((DefaultMutableTreeNode)(parent.getChildAt(1))).getUserObject());
if (!superTypeAnd.node.isMeta() && (superTypeAnd.node.getFun().indexOf("OclAnyC") == -1)) {
//in these cases, everything goes. No sense in dozends of expensive GF runs then.
tar.reduceCoerce = true;
}
coerceLogger.fine("candidate for coerce reduction found: " + and.node + " + " + parent);
}
if (showSelfResult
&& (and.node != null)
&& (and.node.getType() != null)
&& (and.node.getType().startsWith("Instance"))
&& (tar.reduceCoerce //not everything is allowed here
// if not below a coerce (covered above) and no constraints
|| (and.node.getType().indexOf("{") == -1))
){
//if there are constraints present, there is no point in probing, since
//then either no or every instance is offered.
//We do not have to probe then.
tar.probeSelfResult = true;
}
if (easyAttributes
&& (and.node != null)
&& (and.node.getType() != null)
&& (and.node.isMeta())
&& (and.node.getType().startsWith("Instance"))
) {
//not much to check here
tar.easyAttributes = true;
}
}
//check for subtyping errors
if (highlightSubtypingErrors
&& (and.node != null)
&& (and.node.getType() != null)
&& (parent != null)
&& (and.node.isMeta()) //otherwise GF would complain
&& (and.node.getType().startsWith("Subtype")) //if coerce, than we are the Subtype argument
) {
AstNodeData subtypeAnd = (AstNodeData)(((DefaultMutableTreeNode)(parent.getChildAt(0))).getUserObject());
AstNodeData supertypeAnd = (AstNodeData)(((DefaultMutableTreeNode)(parent.getChildAt(1))).getUserObject());
if ((subtypeAnd != null) && (supertypeAnd != null)) {
if (!supertypeAnd.node.isMeta() && !subtypeAnd.node.isMeta()) {
//if one of them is meta, then the situation is not fixed yet,
//so don't complain.
and.subtypingStatus = false;
}
}
}
//hide coerce if possible
//if coere is completely filled in (all children not meta),
//it will be replaced by child 3.
if (hideCoerce
&& (and.node != null)
&& (and.node.getType() != null)
&& (and.node.getFun().endsWith("coerce"))
) {
/**
* if true, then something is unfinished or constrained.
* So don't hide that node.
*/
boolean metaChild = false;
//check if constraints hold for this node
if ((and.constraint != null) && (and.constraint.length() > 0)) {
//some constraint holds here.
//We must not shroud a possible source for that.
metaChild = true;
}
//This search will only be run once for each coerce:
for (int i = 0; i < 3 && !metaChild; i++) {
//This is for the more complicated collection
//subtyping witnesses.
//we do a depthFirst search to find meta nodes.
//If they exist, we know that we shouldn't hide this node.
for (Enumeration e = ((DefaultMutableTreeNode)nodeToCheck.getChildAt(i)).depthFirstEnumeration() ; e.hasMoreElements() ;) {
DefaultMutableTreeNode currNode = (DefaultMutableTreeNode)e.nextElement();
AstNodeData dand = (AstNodeData)currNode.getUserObject();
if (!dand.subtypingStatus
//hideCoerceAggressive means that just incomplete type arguments are no reason to not hide the node
//only subtypingStatus is one because then surely there is an error
|| (!hideCoerceAggressive && dand.node.isMeta())) {
metaChild = true;
break; //no need to go further
}
}
if (metaChild) {
break;
}
}
//For the Instance argument, we do not have do to a deep search
AstNodeData childAnd = (AstNodeData)(((DefaultMutableTreeNode)(nodeToCheck.getChildAt(3))).getUserObject());
if (!hideCoerceAggressive && childAnd.node.isMeta()) {
//see reasons for hideCoerceAggressive above
metaChild = true;
}
if (!metaChild) {
and.showInstead = 3;
//now label the type nodes as hidden
for (int i = 0; i < 3 && !metaChild; i++) {
//This is for the more complicated collection
//subtyping witnesses.
for (Enumeration e = ((DefaultMutableTreeNode)nodeToCheck.getChildAt(i)).depthFirstEnumeration() ; e.hasMoreElements() ;) {
DefaultMutableTreeNode currNode = (DefaultMutableTreeNode)e.nextElement();
AstNodeData dand = (AstNodeData)currNode.getUserObject();
dand.showInstead = -2; // tag for hidden without replacement
}
}
}
//if we are at a coerce above the selected Instance node,
//we want to mark that, so that the d command can be modified
if ((and.node != null)
&& (and.node.getFun().endsWith("coerce"))
&& (and.showInstead > -1) //only hidden coerce
&& (((AstNodeData)((DefaultMutableTreeNode)nodeToCheck.getChildAt(3)).getUserObject()).selected)
) {
tar.deleteAlsoAbove = true;
}
}
}
/**
* Removes nodes from the tree that has topNode as its root.
* Affected are nodes in which the field showInstead in their
* AstNodeData is greater than -1
* @param topNode The root of the tree from which nodes should
* be removed.
* @return The root of the transformed tree.
* This might not be topNode, since that node might as well be
* removed.
*/
protected static DefaultMutableTreeNode transformTree(DefaultMutableTreeNode topNode) {
DefaultMutableTreeNode nextNode = topNode;
while (nextNode != null) {
AstNodeData and = (AstNodeData)nextNode.getUserObject();
if (and.showInstead > -1) {
DefaultMutableTreeNode parent = (DefaultMutableTreeNode)nextNode.getParent();
if (parent == null) {
topNode = (DefaultMutableTreeNode)nextNode.getChildAt(and.showInstead);
if (treeLogger.isLoggable(Level.FINE)) {
//yeah, I know, variable naming is messed up here because of the assignment above
treeLogger.fine("hiding topNode ###" + nextNode + "###, showing instead ###" + topNode + "###");
}
nextNode = topNode;
} else {
final int index = parent.getIndex(nextNode);
parent.remove(index);
DefaultMutableTreeNode instead = (DefaultMutableTreeNode)nextNode.getChildAt(and.showInstead);
parent.insert(instead, index);
if (treeLogger.isLoggable(Level.FINE)) {
treeLogger.fine("hiding node ###" + nextNode + "###, showing instead ###" + instead + "###");
}
nextNode = instead;
}
} else {
nextNode = nextNode.getNextNode();
}
}
return topNode;
}
}

92
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/TreeAnalysisResult.java Normal file
View File

@@ -0,0 +1,92 @@
//Copyright (c) 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
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import javax.swing.tree.DefaultMutableTreeNode;
/**
* A class to store the result of the tree analysis done in formTree
* @author daniels
*/
class TreeAnalysisResult {
/**
* The command, that is to be executed next automatically
*/
String command;
/**
* the number of undo steps needed to undo command
*/
int undoSteps;
/**
* reduceCoerce Whether the mechanism to produce a reduced
* refinement menu for coerce's 4th argument should kick in or not.
*/
boolean reduceCoerce;
/**
* If the editor should ask GF if self an result are applicable here or not
*/
boolean probeSelfResult;
/**
* If we at the the Instance Argument of a hidden
* coerce, we mark that (to change the d command)
*/
boolean deleteAlsoAbove;
/**
* if the attributes of self should be added to the refinement menu.
*/
boolean easyAttributes;
DefaultMutableTreeNode selectedNode = null;
/**
* The currently selected node
*/
GfAstNode currentNode;
/**
* Where the cursor in GF is.
* Correct is not yet known and thus always true.
*/
LinPosition focusPosition;
/**
* Just sets both values.
* @param command The command, that is to be executed next automatically
* @param undoSteps the number of undo steps needed to undo command
* @param reduceCoerce Whether the mechanism to produce a reduced
* refinement menu for coerce's 4th argument should kick in or not.
* @param probeSelfResult If the editor should ask GF if self an result
* are applicable here or not
* @param deleteAlsoAbove If we at the the Instance Argument of a hidden
* coerce, we mark that (to change the d command)
* @param easyAttributes if the attributes of self should be added to the
* refinement menu.
* @param currentNode The currently selected node
* @param focusPosition Where the cursor in GF is.
* Correct is not yet known and thus always true.
*/
public TreeAnalysisResult(String command, int undoSteps, boolean reduceCoerce, boolean probeSelfResult, boolean deleteAlsoAbove, boolean easyAttributes, GfAstNode currentNode, LinPosition focusPosition) {
this.command = command;
this.undoSteps = undoSteps;
this.reduceCoerce = reduceCoerce;
this.probeSelfResult = probeSelfResult;
this.deleteAlsoAbove = deleteAlsoAbove;
this.currentNode = currentNode;
this.easyAttributes = easyAttributes;
this.focusPosition = focusPosition;
}
public String toString() {
return this.command + "|" + this.reduceCoerce + "|" + this.undoSteps + "|" + this.probeSelfResult;
}
}

31
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/TypesLoader.java
View File

@@ -15,28 +15,35 @@
package de.uka.ilkd.key.ocl.gf;
import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.IOException;
import java.util.Hashtable;
import java.util.logging.*;
/**
* @author daniels
* asks GF to print all available printnames, parses that list and generates
* the suiting Printname objects.
* If the entries of the refinement menu should have to appear there with
* type information appended to them, then the printnames have to get this
* knowledge at the time of their creation.
* When the entries are displayed, the display text line of GF is *not* looked
* at. And even if it would be, it would mess up the architecture, that the
* printnames, and only they, are responsible for their linearization.
* Appending their type later on would break that architecture.
* So they have to be prepared.
*/
public class TypesLoader extends AbstractProber {
protected final Hashtable hashtable;
protected static Logger nogger = Logger.getLogger(TypesLoader.class.getName());
/**
* @param fromGf The GF process
* @param toGf The GF process
* The hash in which the funs as keys and
* types as values get saved. Both are Strings.
*/
protected final Hashtable hashtable;
private static Logger nogger = Logger.getLogger(TypesLoader.class.getName());
/**
* @param gfCapsule the read/write encapsulation of the running GF
* @param myHashMap The hash in which the funs as keys and
* types as values get saved. Both are Strings.
*/
public TypesLoader(BufferedReader fromGf, BufferedWriter toGf, Hashtable myHashMap) {
super(fromGf, toGf);
public TypesLoader(GfCapsule gfCapsule, Hashtable myHashMap) {
super(gfCapsule);
this.hashtable = myHashMap;
}
@@ -46,7 +53,7 @@ public class TypesLoader extends AbstractProber {
*/
protected void readMessage() {
try {
String result = this.fromProc.readLine();
String result = gfCapsule.fromProc.readLine();
if (nogger.isLoggable(Level.FINER)) {
nogger.finer("7 " + result);
}
@@ -58,7 +65,7 @@ public class TypesLoader extends AbstractProber {
readType(result);
}
result = this.fromProc.readLine();
result = gfCapsule.fromProc.readLine();
if (nogger.isLoggable(Level.FINER)) {
nogger.finer("7 " + result);
}

30
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/UnrefinedAstNodeData.java
View File

@@ -24,23 +24,26 @@ import java.util.logging.*;
* It knows, how it is called and described (tooltip).
*/
public class UnrefinedAstNodeData extends AstNodeData {
protected final GfAstNode node;
/**
* The tooltip that this node as a parameter should get
*/
protected final String paramTooltip;
protected final String position;
/**
* For a child we have to know its name, its type and the tooltip
* @param pTooltip
* @param pTooltip The tooltip that this node as a parameter should get
* @param node The GfAstNode for the current AST node, for which
* this AstNodeData is the data for.
* @param pos The position in the GF AST of this node in Haskell notation
* @param selected if this is the selected node in the GF AST
* @param constraint A constraint from a parent node, that also
* applies for this node.
*/
public UnrefinedAstNodeData(String pTooltip, GfAstNode node, String pos) {
this.node = node;
public UnrefinedAstNodeData(String pTooltip, GfAstNode node, String pos, boolean selected, String constraint) {
super(node, pos, selected, constraint);
this.paramTooltip = pTooltip;
this.position = pos;
if (logger.isLoggable(Level.FINEST)) {
logger.finest(this.toString() + " - " + getPosition());
logger.finest(this.toString() + " - " + position);
}
}
/**
@@ -57,18 +60,5 @@ public class UnrefinedAstNodeData extends AstNodeData {
public String getParamTooltip() {
return this.paramTooltip;
}
public boolean isMeta() {
return this.node.isMeta();
}
public String getPosition() {
return this.position;
}
public String toString() {
return this.node.toString();
}
}

91
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java
View File

@@ -20,11 +20,17 @@ package de.uka.ilkd.key.ocl.gf;
import java.io.File;
import java.util.logging.*;
import javax.swing.ProgressMonitor;
import java.util.Vector;
/**
* consists of a bunch of static methods, mostly for String
* @author daniels
*
*/
public class Utils {
protected static Logger timeLogger = Logger.getLogger(Utils.class.getName() + ".timer");
protected static Logger deleteLogger = Logger.getLogger(Utils.class.getName() + ".delete");
protected static Logger stringLogger = Logger.getLogger(Utils.class.getName() + ".string");
private static Logger timeLogger = Logger.getLogger(Utils.class.getName() + ".timer");
private static Logger deleteLogger = Logger.getLogger(Utils.class.getName() + ".delete");
private static Logger stringLogger = Logger.getLogger(Utils.class.getName() + ".string");
private Utils() {
//non-instantiability enforced
@@ -33,7 +39,7 @@ public class Utils {
public static final String gf = "gf";
public static final String gfcm = "gfcm";
/*
/**
* Get the extension of a file.
*/
public static String getExtension(File f) {
@@ -131,7 +137,7 @@ public class Utils {
*/
public static String replaceAll(String original, String toReplace, String replacement) {
StringBuffer sb = new StringBuffer(original);
for (int i = sb.indexOf(toReplace); i >= 0; i = sb.indexOf(toReplace)) {
for (int i = sb.indexOf(toReplace); i >= 0; i = sb.indexOf(toReplace, i + replacement.length())) {
sb.replace(i, i + toReplace.length(), replacement);
}
return sb.toString();
@@ -159,4 +165,79 @@ public class Utils {
}
return s;
}
/**
* counts the occurances of toSearch in s
* @param s The String in which the search shall take place
* @param toSearch The String that should be counted
* @return the number of occurances, 0 if s is null
*/
public static int countOccurances(String s, String toSearch) {
if (s == null) {
return 0;
}
int result = 0;
for (int i = s.indexOf(toSearch); i > -1; i = s.indexOf(toSearch, i)) {
result++;
i += toSearch.length();
}
return result;
}
/**
* Takes an arbitrary Vector and executes toString on each element and
* puts these into a String[] of the same size as the Vector
* @param strings A Vector of Object, preferably String
* @return The Vector as a String[]
*/
public static String[] vector2Array(Vector strings) {
String[] result = new String[strings.size()];
for (int i = 0; i < strings.size(); i++) {
result[i] = strings.get(i).toString();
}
return result;
}
/**
* just replace sequences of spaces with one space
* @param s The string to be compacted
* @return the compacted result
*/
static String compactSpaces(String s) {
String localResult = new String();
boolean spaceIncluded = false;
for (int i = 0; i < s.length(); i++) {
char c = s.charAt(i);
if (c != ' ') { // include all non-spaces
localResult += String.valueOf(c);
spaceIncluded = false;
} else {// we have a space
if (!spaceIncluded) {
localResult += " ";
spaceIncluded = true;
} // else just skip
}
}
return localResult;
}
/**
* Replaces all occurances of toBeReplaced, that are not escaped by '\'
* with replacement
* @param working the String in which substrings should be replaced
* @param toBeReplaced The substring, that should be replaced by replacement
* @param replacement well, the replacement string
* @return The String with the replaced parts
*/
public static String replaceNotEscaped(String working, String toBeReplaced, String replacement) {
StringBuffer w = new StringBuffer(working);
for (int i = w.indexOf(toBeReplaced); i > -1 && i < w.length(); i = w.indexOf(toBeReplaced, i)) {
if (i == 0 || w.charAt(i - 1) != '\\') {
w.replace(i, i + toBeReplaced.length(), replacement);
i += replacement.length();
} else {
i += 1;
}
}
return w.toString();
}
}