diff --git a/src/JavaGUI2/LICENCE_jargs b/src/JavaGUI2/LICENCE_jargs new file mode 100644 index 000000000..509c1b7cb --- /dev/null +++ b/src/JavaGUI2/LICENCE_jargs @@ -0,0 +1,29 @@ +Copyright (c) 2001-2003 Steve Purcell. +Copyright (c) 2002 Vidar Holen. +Copyright (c) 2002 Michal Ceresna. +Copyright (c) 2005 Ewan Mellor. + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: Redistributions of source code must retain the above copyright notice, +this list of conditions and the following disclaimer. Redistributions in +binary form must reproduce the above copyright notice, this list of +conditions and the following disclaimer in the documentation and/or other +materials provided with the distribution. Neither the name of the copyright +holder nor the names of its contributors may be used to endorse or promote +products derived from this software without specific prior written +permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE +LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR +CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF +SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS +INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN +CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) +ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGE. diff --git a/src/JavaGUI2/ManifestMain.txt b/src/JavaGUI2/ManifestMain.txt new file mode 100644 index 000000000..b398ff78d --- /dev/null +++ b/src/JavaGUI2/ManifestMain.txt @@ -0,0 +1,3 @@ +Manifest-Version: 1.0 +Main-Class: de.uka.ilkd.key.ocl.gf.GFEditor2 +Class-Path: log4j-1.2.8.jar jargs-1.0.jar diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AbstractProber.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AbstractProber.java new file mode 100644 index 000000000..73f4a5c1a --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AbstractProber.java @@ -0,0 +1,172 @@ +package de.uka.ilkd.key.ocl.gf; + +import java.io.BufferedReader; +import java.io.BufferedWriter; +import java.io.IOException; + +import org.apache.log4j.Logger; + +/** + * A class that offers a basic readGfEdit method with a lot of + * hot spots where subclasses can plug in + * @author daniels + * + */ +abstract class AbstractProber { + protected final BufferedReader fromProc; + protected final BufferedWriter toProc; + 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 + */ + public AbstractProber(BufferedReader fromGf, BufferedWriter toGf) { + this.fromProc = fromGf; + this.toProc = toGf; + } + + /** + * reads the hmsg part + * @param readresult the first line + * @return the first line of the next XML child. + * if no hmsg is present @see readresult is returned. + */ + protected String readHmsg(String readresult) { + if (readresult.equals("")) { + skipChild(""); + try { + String next = fromProc.readLine(); + if (logger.isDebugEnabled()) { + logger.debug("2 " + next); + } + return next; + } catch (IOException e) { + System.err.println("Could not read from external process:\n" + e); + return ""; + } + } else { + return readresult; + } + } + + /** + * reads the linearization subtree. + * The first line should be already read + * @param readresult the first line with the opening tag + */ + protected void readLinearizations(String readresult) { + skipChild(""); + } + + /** Reads the tree child of the XML from beginning to end */ + protected void readTree() { + skipChild(""); + } + + /** Reads the message child of the XML from beginning to end */ + protected void readMessage() { + skipChild(""); + } + + /** Reads the menu child of the XML from beginning to end */ + protected void readMenu() { + skipChild(""); + } + + /** + * reads the output from GF starting with >gfedit< + * and last reads >/gfedit<. + */ + protected void readGfedit() { + try { + String next = ""; + //read + String readresult = fromProc.readLine(); + if (logger.isDebugEnabled()) { + logger.debug("1 " + next); + } + //read either or + readresult = fromProc.readLine(); + if (logger.isDebugEnabled()) { + logger.debug("1 " + next); + } + + next = readHmsg(readresult); + + //in case there comes sth. unexpected before + //usually the while body is never entered + // %%% + while ((next!=null)&&((next.length()==0)||(!next.trim().equals("")))) { + next = fromProc.readLine(); + if (next!=null){ + if (logger.isDebugEnabled()) { + logger.debug("1 " + next); + } + } else { + System.exit(0); + } + } + readLinearizations(next); + readTree(); + readMessage(); + readMenu(); + + for (int i=0; i<3 && !next.equals(""); i++){ + next = fromProc.readLine(); + if (logger.isDebugEnabled()) { + logger.debug("1 " + next); + } + } + + } catch (IOException e) { + System.err.println("Could not read from external process:\n" + e); + } + + } + + /** + * Reads the output from GF until the ending tag corresponding to the + * given opening tag is read. + * @param opening tag in the format of >gfinit< + */ + protected void skipChild(String opening) { + String closing = (new StringBuffer(opening)).insert(1, '/').toString(); + try { + String nextRead = fromProc.readLine(); + if (logger.isDebugEnabled()) { + logger.debug("3 " + nextRead); + } + while (!nextRead.trim().equals(closing)) { + nextRead = fromProc.readLine(); + if (logger.isDebugEnabled()) { + logger.debug("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 + */ + protected void send(String text) { + if (logger.isDebugEnabled()) { + logger.debug("## 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); + } + } + + +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AstNodeData.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AstNodeData.java new file mode 100644 index 000000000..a37f0aa5b --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AstNodeData.java @@ -0,0 +1,30 @@ +/* + * Created on 27.04.2005 + * + */ +package de.uka.ilkd.key.ocl.gf; + +/** + * @author hdaniels + * 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. + */ +interface AstNodeData { + /** + * @return the printname associated with this object + */ + public abstract Printname getPrintname(); + + /** + * @return the parameter tooltip that this node has as a child + * of its parent (who gave it to it depending on its position) + */ + public abstract String getParamTooltip(); + + /** + * + * @return true iff this node represents an open leaf + */ + public abstract boolean isMeta(); +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ConstraintCallback.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ConstraintCallback.java new file mode 100644 index 000000000..f617fa719 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ConstraintCallback.java @@ -0,0 +1,40 @@ +package de.uka.ilkd.key.ocl.gf; + +import org.apache.log4j.Logger; + +/** + * @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 { + + /** + * Does the logging. What else should it do? + */ + protected static Logger logger = Logger.getLogger(ConstraintCallback.class.getName()); + + String grammarsDir; + /** + * sets the directory where the grammars reside + * @param grammarsDir + */ + void setGrammarsDir(final String grammarsDir) { + this.grammarsDir = grammarsDir; + } + /** + * gets the directory where the grammars reside + */ + String getGrammarsDir() { + return this.grammarsDir; + } + + /** + * Sends the finished OCL constraint back to Together to save it + * as a JavaDoc comment. + * @param constraint The OCL constraint in question. + */ + abstract void sendConstraint(String constraint); + +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Display.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Display.java new file mode 100644 index 000000000..fc07ff019 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Display.java @@ -0,0 +1,202 @@ +package de.uka.ilkd.key.ocl.gf; + +import java.awt.Font; +import java.awt.Rectangle; +import java.util.Vector; +import javax.swing.JEditorPane; + +/** + * @author daniels + * Takes care of collecting the linearized text and the length calculations + */ +class Display { + private final boolean doText; + private final boolean doHtml; + /** + * collects the linearization after each append. + * what's in here are Strings + */ + private Vector linStagesHtml = new Vector(); + /** + * collects the linearization after each append. + * what's in here are Strings + */ + private Vector linStagesText = new Vector(); + /** + * Is used to calculate the length of a HTML snipplet. + * This pane is not displayed in hope to avoid any actual renderings + * which would just slow the length calculation down. + * Perhaps that's an abuse ... + * And perhaps this pane is not needed + */ + private JEditorPane htmlLengthPane = new JEditorPane(); + + /** 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; + } + this.htmlLengthPane.setContentType("text/html"); + this.htmlLengthPane.setEditable(false); + } + + + /** + * @param font The Font, that is to be used. If null, the default of JTextPane is taken. + * @return the collected HTML text, that has been added to this object. + * <html> tags are wrapped around the result, if not already there. + */ + protected String getHtml(Font font) { + if (!doHtml) { + return ""; + } + String result; + if (this.linStagesHtml.size() > 0) { + String fontface; + if (font != null) { + //fontface = " style=\"font-size:" + font.getSize()+ "pt\""; + fontface = " style=\"font: " + font.getSize()+ "pt " + font.getName() + "\""; + } else { + fontface = ""; + } + result ="" + this.linStagesHtml.get(this.linStagesHtml.size() - 1).toString() + ""; + } else { + result = ""; + } + return result; + } + + /** + * @return The collected pure text, that has been added to this object. + */ + protected String getText() { + if (!doText) { + return ""; + } + String result; + if (this.linStagesText.size() > 0) { + result = this.linStagesText.lastElement().toString(); + } else { + result = ""; + } + return result; + } + + /** + * Appends the given text to the respective fields from + * where it can be displayed later + * @param text The pure text that is to be appended. + * @param html The HTML text that is to be appended. + * Most likely the same as text + */ + protected void addToStages(final String text, final String html) { + //add to HTML + if (doHtml) { + final String newStageHtml; + if (this.linStagesHtml.size() > 0) { + newStageHtml = this.linStagesHtml.get(this.linStagesHtml.size() - 1) + html; + } else { + newStageHtml = html; + } + this.linStagesHtml.add(newStageHtml); + } + + //add to Text + if (doText) { + final String newStageText; + if (this.linStagesText.size() > 0) { + newStageText = linStagesText.get(linStagesText.size() - 1) + text; + } else { + newStageText = text; + } + this.linStagesText.add(newStageText); + } + } + + /** + * Adds toAdd to both the pure text as the HTML fields, they are inherently the same, + * since they are mapped to the same position in the AST. + * On the way of adding, some length calculations are done, which are used to + * create an HtmlMarkedArea object, which is ready to be used in GFEditor2. + * @param toAdd The String that the to-be-produced MarkedArea should represent + * @param position The position String in Haskell notation + * @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) { + /** the length of the displayed HTML before the current append */ + int oldLengthHtml = 0; + if (doHtml) { + if (this.linStagesHtml.size() > 0) { + // is still in there. Does not absolutely need to be + // cached in a global variable + oldLengthHtml = this.htmlLengthPane.getDocument().getLength(); + } else { + oldLengthHtml = 0; + } + } + /** the length of the text before the current append */ + int oldLengthText = 0; + if (doText) { + if (this.linStagesText.size() > 0) { + // is still in there. Does not absolutely need to be + // cached in a global variable + oldLengthText = this.linStagesText.lastElement().toString().length(); + } else { + oldLengthText = 0; + } + } + addToStages(toAdd, toAdd); + //calculate beginning and end + //for HTML + int newLengthHtml = 0; + if (doHtml) { + final String newStageHtml = this.linStagesHtml.lastElement().toString(); + final String newHtml = Printname.htmlPrepend(newStageHtml, ""); + //yeah, daniels admits, this IS probably expensive + this.htmlLengthPane.setText(newHtml); + newLengthHtml = htmlLengthPane.getDocument().getLength(); + if (newLengthHtml < oldLengthHtml) { + newLengthHtml = oldLengthHtml; + } + } + //for text + int newLengthText = 0; + if (doText) { + newLengthText = this.linStagesText.lastElement().toString().length(); + } + final HtmlMarkedArea hma = new HtmlMarkedArea(oldLengthText, newLengthText, position, toAdd, oldLengthHtml, newLengthHtml); + return hma; + } + /** + * To store the scroll state of the pure text linearization area + */ + Rectangle recText = new Rectangle(); + /** + * To store the scroll state of the HTML linearization area + */ + Rectangle recHtml = new Rectangle(); + + + public String toString() { + return getText(); + } +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/DynamicTree2.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/DynamicTree2.java new file mode 100644 index 000000000..548395260 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/DynamicTree2.java @@ -0,0 +1,347 @@ +package de.uka.ilkd.key.ocl.gf; +/* + * This code is based on an example provided by Richard Stanford, + * a tutorial reader. + */ + +import java.awt.*; +import javax.swing.*; +import javax.swing.tree.*; +import javax.swing.event.*; + +import org.apache.log4j.Logger; + +//import de.uka.ilkd.key.util.KeYResourceManager; + +import java.awt.event.*; +//import java.net.URL; + +public class DynamicTree2 extends JPanel implements KeyListener, +ActionListener{ + protected static Logger logger = Logger.getLogger(DynamicTree2.class.getName()); + + public DefaultMutableTreeNode rootNode; + protected DefaultTreeModel treeModel; + public JTree tree; + public int oldSelection = 0; + private Toolkit toolkit = Toolkit.getDefaultToolkit(); + public JPopupMenu popup = new JPopupMenu(); + JMenuItem menuItem; + private GFEditor2 gfeditor; + + public DynamicTree2(GFEditor2 gfe) { + + this.gfeditor = gfe; + rootNode = new DefaultMutableTreeNode("Root Node"); + treeModel = new DefaultTreeModel(rootNode); + treeModel.addTreeModelListener(new MyTreeModelListener()); + + tree = new JTree(treeModel); + tree.setRootVisible(false); + tree.setEditable(false); + 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(); + tree.addMouseListener(popupListener); + + tree.addTreeSelectionListener(new TreeSelectionListener() { + /** + * the following is assumed: + * in GF we can only switch to the last or the next editing position. + * In the displayed tree, we can click everywhere. + * We navigate through the GF tree by giving the direction + * and the number of steps + */ + public void valueChanged(TreeSelectionEvent e) { + if (tree.getSelectionRows() != null) { + if (gfeditor.nodeTable == null) { + if (GFEditor2.treeLogger.isDebugEnabled()) { + GFEditor2.treeLogger.debug("null node table"); + } + } else { + if (GFEditor2.treeLogger.isDebugEnabled()) { + GFEditor2.treeLogger.debug("node table: " + gfeditor.nodeTable.contains(new Integer(0)) + " " + gfeditor.nodeTable.keys().nextElement()); + } + } + if (tree.getSelectionPath() == null) { + if (GFEditor2.treeLogger.isDebugEnabled()) { + GFEditor2.treeLogger.debug("null root path"); + } + } else { + if (GFEditor2.treeLogger.isDebugEnabled()) { + GFEditor2.treeLogger.debug("selected path" + tree.getSelectionPath()); + } + } + int i = ((Integer) gfeditor.nodeTable.get(tree.getSelectionPath())).intValue(); + int j = oldSelection; + gfeditor.treeChanged = true; + if (i > j) + gfeditor.send("> " + String.valueOf(i - j)); + else + gfeditor.send("< " + String.valueOf(j - i)); + } + } + }); + + tree.setCellRenderer(new MyRenderer()); + tree.setShowsRootHandles(true); + ToolTipManager.sharedInstance().registerComponent(tree); + ToolTipManager.sharedInstance().setDismissDelay(60000); + setPreferredSize(new Dimension(200, 100)); + JScrollPane scrollPane = new JScrollPane(tree); + setLayout(new GridLayout(1,0)); + add(scrollPane); + } + + /** Remove all nodes except the root node. */ + public void clear() { + rootNode.removeAllChildren(); + treeModel.reload(); + } + + /** Remove the currently selected node. */ + public void removeCurrentNode() { + TreePath currentSelection = tree.getSelectionPath(); + if (currentSelection != null) { + DefaultMutableTreeNode currentNode = (DefaultMutableTreeNode) + (currentSelection.getLastPathComponent()); + MutableTreeNode parent = (MutableTreeNode)(currentNode.getParent()); + if (parent != null) { + treeModel.removeNodeFromParent(currentNode); + return; + } + } + + // Either there was no selection, or the root was selected. + toolkit.beep(); + } + + /** + * Add child to the root node. + * It will come last in this node. + * @param child the payload of the new node + * @return the tree node having child as the node data + */ + public DefaultMutableTreeNode addObject(Object child) { + DefaultMutableTreeNode parentNode = null; + TreePath parentPath = tree.getSelectionPath(); + + if (parentPath == null) { + parentNode = rootNode; + } else { + parentNode = (DefaultMutableTreeNode) + (parentPath.getLastPathComponent()); + } + + return addObject(parentNode, child, true); + } + + /** + * Add a new node containing child to the node parent. + * It will come last in this node. + * This method gets actually called + * @param parent the parent node of the to be created node + * @param child the wannabe node data + * @return the tree node having child as the node data and parent as the parent + */ + public DefaultMutableTreeNode addObject(DefaultMutableTreeNode parent, + Object child) { + return addObject(parent, child, false); + } + + /** + * Add child to the currently selected node (parent?). + * It will come last in this node. + * @param parent the parent node of the to be created node + * @param child the wannabe node data + * @param shouldBeVisible true iff the viewport should show the + * new node afterwards + * @return the tree node having child as the node data and parent + * as the parent + */ + public DefaultMutableTreeNode addObject(DefaultMutableTreeNode parent, Object child, boolean shouldBeVisible) { + if (logger.isDebugEnabled()) { + logger.debug("node added: '" + child + "', parent: '" + parent + "'"); + } + DefaultMutableTreeNode childNode = new DefaultMutableTreeNode(child); + + if (parent == null) { + parent = rootNode; + } + + treeModel.insertNodeInto(childNode, parent, + parent.getChildCount()); + + // Make sure the user can see the lovely new node. + if (shouldBeVisible) { + tree.scrollPathToVisible(new TreePath(childNode.getPath())); + } + return childNode; + } + + class MyTreeModelListener implements TreeModelListener { + public void treeNodesChanged(TreeModelEvent e) { + DefaultMutableTreeNode node; + node = (DefaultMutableTreeNode) + (e.getTreePath().getLastPathComponent()); + + /* + * If the event lists children, then the changed + * node is the child of the node we've already + * gotten. Otherwise, the changed node and the + * specified node are the same. + */ + try { + int index = e.getChildIndices()[0]; + node = (DefaultMutableTreeNode)(node.getChildAt(index)); + } catch (NullPointerException exc) { + System.err.println(exc.getMessage()); + exc.printStackTrace(); + } + + if (GFEditor2.treeLogger.isDebugEnabled()) { + GFEditor2.treeLogger.debug("The user has finished editing the node."); + GFEditor2.treeLogger.debug("New value: " + node.getUserObject()); + } + } + public void treeNodesInserted(TreeModelEvent e) { + //nothing to be done here + } + public void treeNodesRemoved(TreeModelEvent e) { + //nothing to be done here + } + public void treeStructureChanged(TreeModelEvent e) { + //nothing to be done here + } + } + + private class MyRenderer extends DefaultTreeCellRenderer { + //int counter = 0; + //final ImageIcon iconFilled; + //final ImageIcon iconOpen; + +// public MyRenderer() { +// final URL urlOpen = KeYResourceManager.getManager().getResourceFile(DynamicTree2.class, "metal_leaf_open.png"); +// final URL urlFilled = KeYResourceManager.getManager().getResourceFile(DynamicTree2.class, "metal_leaf_filled.png"); +// iconOpen = new ImageIcon(urlOpen); +// iconFilled = new ImageIcon(urlFilled); +// } + + public Component getTreeCellRendererComponent( + JTree tree, + Object value, + boolean sel, + boolean expanded, + boolean leaf, + int row, + boolean hasFocus) { + + super.getTreeCellRendererComponent( + tree, value, sel, + expanded, leaf, row, + hasFocus); + if (value instanceof DefaultMutableTreeNode) { + DefaultMutableTreeNode node = (DefaultMutableTreeNode)value; + if (node.getUserObject() instanceof AstNodeData) { + AstNodeData and = (AstNodeData)node.getUserObject(); + String ptt = and.getParamTooltip(); + this.setToolTipText(ptt); + this.setText(and.toString()); +// if (and.isMeta()) { +// this.setLeafIcon(this.iconOpen); +// } else { +// this.setLeafIcon(this.iconFilled); +// } + } else { + this.setToolTipText(null); + this.setText(value.toString()); + } + } else { + this.setToolTipText(null); + this.setText(value.toString()); + } + return this; + } + + /** + * Checks if the current node represents an open metavariable + * or question mark + * @param value The payload of the node + * @return true iff value begins with a '?' + */ + protected boolean isMetavariable(Object value) { + try { + DefaultMutableTreeNode node = + (DefaultMutableTreeNode)value; + String nodeInfo = + (String)(node.getUserObject()); + if (nodeInfo.indexOf("?") == 0) { + return true; + } + } catch (Exception e) { + e.printStackTrace(); + return false; + } + + return false; + } + + }//class + + class PopupListener extends MouseAdapter { + public void mousePressed(MouseEvent e) { + int selRow = tree.getRowForLocation(e.getX(), e.getY()); + tree.setSelectionRow(selRow); + if (GFEditor2.treeLogger.isDebugEnabled()) { + GFEditor2.treeLogger.debug("selection changed!"); + } + maybeShowPopup(e); + } + + public void mouseReleased(MouseEvent e) { + //nothing to be done here + } + void maybeShowPopup(MouseEvent e) { + if (GFEditor2.treeLogger.isDebugEnabled()) { + GFEditor2.treeLogger.debug("may be show Popup!"); + } + if (e.isPopupTrigger()) { + if (GFEditor2.treeLogger.isDebugEnabled()) { + GFEditor2.treeLogger.debug("changing menu!"); + } + popup = gfeditor.producePopup(); + popup.show(e.getComponent(), e.getX(), e.getY()); + } + } + } + + public void actionPerformed(ActionEvent ae) { + //nothing to be done here + } + + /** Handle the key pressed event. */ + public void keyPressed(KeyEvent e) { + int keyCode = e.getKeyCode(); + switch (keyCode){ + case KeyEvent.VK_SPACE : gfeditor.send("'"); break; + case KeyEvent.VK_DELETE : gfeditor.send("d"); break; + } + } + /** Handle the key typed event. */ + public void keyTyped(KeyEvent e) { + //nothing to be done here + } + /** Handle the key released event. */ + public void keyReleased(KeyEvent e) { + //nothing to be done here + } + +} + + diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFCommand.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFCommand.java new file mode 100644 index 000000000..bbbf41618 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFCommand.java @@ -0,0 +1,104 @@ +/* + * Created on 20.04.2005 + */ +package de.uka.ilkd.key.ocl.gf; + + +import org.apache.log4j.Logger; + +/** + * @author daniels + * A class that represents a GF command together with its printname. + * It also gives easy access to all the abuses of the printname like + * the subcategory, the tooltip, it knows about wrapping and so on. + * + * The static stuff could produce problems if the editor is started + * several times without closing it first. It probably should be moved + * into a manager class. + * Or the instances that get generated during one run all share the same + * "pseudo-static" Hashtables. This is probably better. + * + */ +abstract class GFCommand implements Comparable{ + + protected static Logger subcatLogger = Logger.getLogger(GFEditor2.class.getName() + "_subcat"); + + /** the subcategory of this command */ + public abstract String getSubcat(); + /** the type of the command, r,w,ch,d,ac,... */ + protected String commandType; + /** 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 */ + protected int argument; + + /**the actual command that this object should represent */ + protected String command; + /**the actual command that this object should represent */ + public String getCommand() { + return command; + } + + /**the Printname corresponding to the GF fun of this command*/ + protected Printname printname; + /**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 */ + public abstract String getTooltipText(); + + /** 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 */ + protected String funName; + + /** if this is the first occurence of the current subcat */ + protected boolean newSubcat; + /** 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. + * @param o the other command. + * @return see above. + */ + public int compareTo(Object o) { + if (this.equals(o)) { + return 0; + } + if (this instanceof LinkCommand && !(o instanceof LinkCommand)) { + return -1; + } + if (!(this instanceof LinkCommand) && (o instanceof LinkCommand)) { + return 1; + } + if (this instanceof InputCommand && !(o instanceof InputCommand)) { + return 1; + } + if (!(this instanceof InputCommand) && (o instanceof InputCommand)) { + return -1; + } + if (! (o instanceof GFCommand)) { + //This should never occur! + return -1; + } else { + GFCommand ocmd = (GFCommand)o; + return this.getDisplayText().compareTo(ocmd.getDisplayText()); + } + + } + + public String toString() { + return getDisplayText() + " \n " + getTooltipText(); + } + +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java new file mode 100644 index 000000000..0e1da2828 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java @@ -0,0 +1,4033 @@ +package de.uka.ilkd.key.ocl.gf; + +import java.awt.*; +import java.awt.event.*; +import javax.swing.*; +import javax.swing.text.*; +import javax.swing.event.*; +import javax.swing.tree.*; +import java.io.*; +import java.util.*; +import java.net.URL; +import javax.swing.text.html.HTMLDocument; +import java.net.MalformedURLException; +import org.apache.log4j.Logger; +import jargs.gnu.CmdLineParser; + +public class GFEditor2 extends JFrame implements ActionListener, CaretListener, +KeyListener, FocusListener { + + /** the main logger for this class */ + protected static Logger logger = Logger.getLogger(GFEditor2.class.getName()); + /** + * logs the time at several stages when starting the editor. + * For calibrating the ProgressMonitor + */ + protected static Logger timeLogger = Logger.getLogger("de.uka.ilkd.key.ocl.gf.Timer"); + /** print MarkedAreas */ + protected static Logger markedAreaLogger = Logger.getLogger(GFEditor2.class.getName() + "_MarkedArea"); + /** print MarkedAreas */ + protected static Logger htmlLogger = Logger.getLogger(GFEditor2.class.getName() + "_HTML"); + /** debug stuff for the tree */ + public static Logger treeLogger = Logger.getLogger(GFEditor2.class.getName() + "_Tree"); + /** red mark-up && html debug messages */ + protected static Logger redLogger = Logger.getLogger(GFEditor2.class.getName() + "_Red"); + /** pop-up/mouse handling debug messages */ + protected static Logger popUpLogger = Logger.getLogger(GFEditor2.class.getName() + "_PopUp"); + /** linearization marking debug messages */ + protected static Logger linMarkingLogger = Logger.getLogger(GFEditor2.class.getName() + "_LinMarking"); + /** XML parsing debug messages */ + protected static Logger xmlLogger = Logger.getLogger(GFEditor2.class.getName() + "_XML"); + /** keyPressedEvents & Co. */ + protected static Logger keyLogger = Logger.getLogger(GFEditor2.class.getName() + "_key"); + /** keyPressedEvents & Co. */ + protected static Logger sendLogger = Logger.getLogger(GFEditor2.class.getName() + ".send"); + + public final static String modelModulName = "FromUMLTypes"; + /** + * Does the saving of constraints in Together. + * Or to be more precise, itself knows nothing about Together. + * Only its subclasses. That way it can be compiled without KeY. + */ + final private ConstraintCallback callback; + + /** to collect the linearization strings */ + private HashMap linearizations = new HashMap(); + /** current Font */ + private Font font; + /** contains the offered fonts by name */ + private JMenu fontMenu; + /** offers a list of font sizes */ + private JMenu sizeMenu; + + public JPopupMenu popup2 = new JPopupMenu(); + /** + * what is written here is parsed and the result inserted instead of tbe selection. + * No idea how this element is displayed + */ + public JTextField parseField = new JTextField("textField!"); + + /** + * to save the old selection before editing i field + * or the new selection? + */ + public String selectedText=""; + + /** + * The position of the focus, that is, the currently selected node in the AST + */ + public LinPosition focusPosition ; + /** + * 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? + * */ + public Vector currentPosition = new Vector(); + + /** + * When a new category is chosen, it is set to true. + * In the reset or a completely new state it is falsed. + * The structure of the GF output is different then and this must be taken + * care of. + */ + public boolean newObject = false; + /** + * the opposite of newObject + * is only true, when we don't have a chosen category. + * false: reading lins and tree + * true: reading categories from GF + */ + public boolean finished = false; + /** + * if the user enters text for the alpha conversion, he perhaps wants to input the same text again. + * Therefore it is saved. + */ + private String alphaInput = ""; + /** + * if a user sends a custom command to GF, he might want to do this + * again with the same command. + * Therefore it is saved. + */ + private String commandInput = ""; + + /** + * default status text, just status + */ + private final static String status = "status"; + /** + * the language the possible actions are displayed + */ + protected String selectedMenuLanguage = "Abstract"; + /** + * the GF-output between tags is stored here. + * must be saved in case the displayed languages are changed. + * Only written in readLin + */ + private String linearization = ""; + /** + * write-only variable, stores the current import paths + * reset after each reset. + */ + private String fileString = ""; + /** + * In GF the nodes in the AST are numbered in a linear fashion. + * When reading a from GF, we assign each tree node in the Java AST + * the position in the 'flattened' GF tree. + * The mapping between Java tree pathes and GF node numbering is stored + * here. + */ + public Hashtable nodeTable = new Hashtable(); + /**this FileChooser gets enriched with the Term/Text option */ + JFileChooser saveFc = new JFileChooser("./"); + /** used for new Topic, Import and Browse (readDialog) */ + JFileChooser fc = new JFileChooser("./"); + private final static String [] modifyMenu = {"Modify", "identity","transfer", + "compute", "paraphrase", "generate","typecheck", "solve", "context" }; + private static final String [] newMenu = {"New"}; + + /** + * if treeChanged is false, we don't have to rebuild it. + * Avoids a time-consuming reconstruction and flickering. + */ + public boolean treeChanged = true; + /** the most common use is to store here what is read from GF */ + private String result; + /** The output from GF is in here */ + private BufferedReader fromProc; + /** leave messages for GF here. */ + private BufferedWriter toProc; + /** used to print error messages */ + private final String commandPath; + /** Linearizations' display area */ + private JTextArea linearizationArea = new JTextArea(); + /** the content of the refinementMenu */ + public DefaultListModel listModel= new DefaultListModel(); + /** The list of current refinement options */ + private JList refinementList = new JList(this.listModel); + /** + * The abstract syntax tree representation of the current editing object + */ + private DynamicTree2 tree = new DynamicTree2(this); + + /** Current Topic */ + private JLabel grammar = new JLabel("No topic "); + /** + * Writing the current editing object to file in the term or text + * format + */ + private JButton save = new JButton("Save"); + /** + * Reading both a new environment and an editing object from file. + * Current editing will be discarded + */ + private JButton open = new JButton("Open"); + /** + * Reading a new environment from file. Current editing will be + * discarded. + */ + private JButton newTopic; + /** Sending a command to GF */ + private JButton gfCommand; + + /** Moving the focus to the previous metavariable */ + private JButton leftMeta = new JButton("?<"); + /** Moving the focus to the previous term */ + private JButton left = new JButton("<"); + /** Moving the focus to the top term */ + private JButton top = new JButton("Top"); + /** Moving the focus to the next term */ + private JButton right = new JButton(">"); + /** Moving the focus to the next metavariable */ + private JButton rightMeta = new JButton(">?"); + private JLabel actionOnSubterm = new JLabel("Select Action on Subterm"); + /** Refining with term or linearization from typed string or file */ + private JButton read = new JButton("Read"); + // private JButton parse = new JButton("Parse"); + // private JButton term = new JButton("Term"); + /** Performing alpha-conversion of bound variables */ + private JButton alpha; + /** Generating random refinement */ + private JButton random; + /** Going back to the previous state */ + private JButton undo; + /** The main panel on which the others are put */ + private JPanel coverPanel = new JPanel(); + /** the dialog to read in Strings or Terms */ + private ReadDialog readDialog; + + /** The list of available categories to start editing */ + private JComboBox newCategoryMenu = new JComboBox(newMenu); + /** Choosing a linearization method */ + private JComboBox modify = new JComboBox(modifyMenu); + // private JComboBox mode = new JComboBox(modeMenu); + /** the panel with the more general command buttons */ + private JPanel downPanel = new JPanel(); + /** the splitpane containing tree on the left and linearization area on the right*/ + private JSplitPane treePanel; + /** the upper button bar for New, Save */ + private JPanel upPanel = new JPanel(); + /** the panel that contains the navigation buttons and some explanatory text */ + private JPanel middlePanel = new JPanel(); + /** the panel that contains only the navigation buttons */ + private JPanel middlePanelUp = new JPanel(); + /** the panel that vontains the the explanatory text for the refinement menu */ + private JPanel middlePanelDown = new JPanel(); + /** splits between tree and lin above and nav buttons and refinements below */ + private JSplitPane centerPanel; + /** the window that contains the refinements when in split mode */ + private JFrame gui2 = new JFrame(); + /** the main window with tree, lin and buttons when in split mode */ + private JPanel centerPanel2= new JPanel(); + /** contains refinment list and navigation buttons */ + private JPanel centerPanelDown = new JPanel(); + /** the scrollpane containing the refinements */ + private JScrollPane refinementPanel = new JScrollPane(this.refinementList); + /** only contains the linearization area */ + private JScrollPane outputPanelText = new JScrollPane(this.linearizationArea); + /** HTML Linearizations' display area */ + private JTextPane htmlLinPane = new JTextPane(); + /** only contains the HTML linearization area */ + private JScrollPane outputPanelHtml = new JScrollPane(this.htmlLinPane); + /** contains both pure text and HTML areas */ + private JSplitPane linSplitPane; + /** contains the linSplitPane and the status field below it */ + private JPanel outputPanelUp = new JPanel(new BorderLayout()); + /** contains statusLabel */ + private JPanel statusPanel = new JPanel(); + /** The type the currently focused term has */ + private JLabel statusLabel = new JLabel(status); + /** the main menu in the top */ + private JMenuBar menuBar= new JMenuBar(); + //private ButtonGroup menuGroup = new ButtonGroup(); + /** View settings */ + private JMenu viewMenu= new JMenu("View"); + /** + * stores a list of all languages + abstract to select the language, + * in which the selectMenu will be filled. + */ + private JMenu mlMenu= new JMenu("language"); + /** Choosing the refinement options' representation */ + private JMenu modeMenu= new JMenu("Menus"); + /** Language settings */ + private JMenu langMenu= new JMenu("Languages"); + /** Main operations */ + private JMenu fileMenu= new JMenu("File"); + /** stores whether the refinement list should be in 'long' format */ + private JRadioButtonMenuItem rbMenuItemLong; + // private JRadioButtonMenuItem rbMenuItemAbs; + /** stores whether the refinement list should be in 'untyped' format */ + private JRadioButtonMenuItem rbMenuItemUnTyped; + /** stores whether the AST is visible or not */ + private JCheckBoxMenuItem treeCbMenuItem; + /** in the save dialog whether to save as a Term or as linearized Text */ + private ButtonGroup saveTypeGroup = new ButtonGroup(); + /** the entries of the filter menu */ + private final static String [] filterMenuContents = {"identity", + "erase", "take100", "text", "code", "latexfile", + "structured", "unstructured" }; + /** Choosing the linearization representation format */ + private JMenu filterMenu = new JMenu("Filter"); + /** for managing the filter menu entries*/ + private ButtonGroup filterButtonGroup = new ButtonGroup(); + //now for stuff that is more or less OCL specific + + /** Some usability things can be switched off here for testing */ + private JMenu usabilityMenu= new JMenu("Usability"); + /** + * stores whether self and result should only be made visible + * if applicable + */ + private JCheckBoxMenuItem selfresultCbMenuItem; + /** to switch grouping of entries in the refinement menu on and off */ + private JCheckBoxMenuItem subcatCbMenuItem; + /** to switch sorting of entries in the refinement menu on and off */ + private JCheckBoxMenuItem sortCbMenuItem; + + /** + * if true, self and result are only shown if applicable, + * tied to @see selfresultCbMenuItem + */ + private boolean showSelfResult = true; + /** + * if true, refinements are grouped by subcat + * tied to @see subcatCbMenuItem + */ + private boolean groupSubcat = true; + /** + * if true, refinements are grouped by subcat + * tied to @see subcatCbMenuItem + */ + private boolean sortRefinements = true; + /** + * 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; + + /** here the GFCommand objects are stored*/ + private Vector gfcommands = new Vector(); + + /** handles all the Printname naming a.s.o */ + private PrintnameManager printnameManager; + + /** + * stores the current type. Since the parsing often fails, this is + * most often null, except for Int and String, which can be parsed. + */ + private GfAstNode currentNode = null; + /** + * Here the node is stored that introduces the bound variables + * self and possibly result. + * This knowledge is read in formTree and used in probeProbability, + * which is called by readAndDisplay which again is called by a + * number of functions. Thus a 'global' variable. + */ + private GfAstNode constraintNode = null; + /** stores the displayed parts of the linearization */ + private Display display = new Display(3); + + /** + * contains all the linearization pieces as HtmlMarkedArea + * Needed to know to which node in the AST a word in the linHtmlPane + * area belongs. + */ + public Vector htmlOutputVector = new Vector(); + /** + * contains all the linearization pieces as MarkedArea + * Needed to know to which node in the AST a word in the linearization + * area belongs. + * At the moment, this is double effort, but the old way of generating + * MarkedAreas should go away. + */ + public Vector textOutputVector = new Vector(); + + /** takes care of the menus that display the available languages */ + private LangMenuModel langMenuModel = new LangMenuModel(); + + //Now the stuff for choosing the wanted output type (pure text or HTML) + /** + * 1 for text, 2 for HTML, 3 for both + */ + private int displayType = 1; + private ButtonGroup bgDisplayType = new ButtonGroup(); + private JRadioButtonMenuItem rbText = new JRadioButtonMenuItem(new AbstractAction("pure text") { + public void actionPerformed(ActionEvent ae) { + int oldDisplayType = displayType; + displayType = 1; + outputPanelUp.removeAll(); + outputPanelUp.add(outputPanelText, BorderLayout.CENTER); + outputPanelUp.add(statusPanel, BorderLayout.SOUTH); + if (ae != null && oldDisplayType == 2) { //not manually called in the beginning and only HTML + formLin(); + } + outputPanelUp.validate(); + } + }); + private JRadioButtonMenuItem rbHtml = new JRadioButtonMenuItem(new AbstractAction("HTML") { + public void actionPerformed(ActionEvent ae) { + int oldDisplayType = displayType; + displayType = 2; + outputPanelUp.removeAll(); + outputPanelUp.add(outputPanelHtml, BorderLayout.CENTER); + outputPanelUp.add(statusPanel, BorderLayout.SOUTH); + if (ae != null && oldDisplayType == 1) { //not manually called in the beginning and only text + formLin(); + } + outputPanelUp.validate(); + } + }); + private JRadioButtonMenuItem rbTextHtml = new JRadioButtonMenuItem(new AbstractAction("text and HTML") { + public void actionPerformed(ActionEvent ae) { + int oldDisplayType = displayType; + displayType = 3; + linSplitPane.setLeftComponent(outputPanelText); + linSplitPane.setRightComponent(outputPanelHtml); + outputPanelUp.removeAll(); + outputPanelUp.add(linSplitPane, BorderLayout.CENTER); + outputPanelUp.add(statusPanel, BorderLayout.SOUTH); + if (ae != null && oldDisplayType != 3) { //not manually called in the beginning and not both (the latter should always be true) + formLin(); + } + outputPanelUp.validate(); + } + }); + + + /** + * Initializes GF with the given command, sets up the GUI + * and reads the first GF output + * @param gfcmd The command with all parameters, including -java + * that is to be executed. Will set up the GF side of this session. + * @param isHtml true iff the editor should start in HTML mode. + * @param baseURL the URL that is the base for all relative links in HTML + */ + public GFEditor2(String gfcmd, boolean isHtml, URL baseURL) { + this.callback = null; + this.commandPath = gfcmd; + initializeGUI(baseURL, isHtml); + initializeGF(gfcmd, null); + //readAndDisplay(); + } + + /** + * a specialized constructor for OCL comstraints + * Starts with a new Constraint and an initial syntax tree + * @param gfcmd The command with all parameters, including -java + * that is to be executed. Will set up the GF side of this session. + * @param callback The class responsible for saving the OCL constraint + * as a JavaDoc comment + * @param initAbs the initial abstract syntax tree + * @param pm to monitor the loading progress. May be null + */ + public GFEditor2(String gfcmd, ConstraintCallback callback, String initAbs, ProgressMonitor pm) { + this.callback = callback; + this.commandPath = gfcmd; + + Utils.tickProgress(pm, 5220, "Loading grammars"); + initializeGF(gfcmd, pm); + Utils.tickProgress(pm, 9350, "Initializing GUI"); + initializeGUI(null, true); + + // send correct term (syntax tree) + //The initial GF constraint has until now always been + //automatically solvable. So don't startle the user + //with painting everything red. + send(initAbs + " ;; c solve ", false); + readAndDisplay(); + Utils.tickProgress(pm, 9700, "Loading finished"); + pm.close(); + logger.debug("GFEditor2 constructor finished"); + } + + /** + * Starts GF and sets up the reading facilities. + * Shouldn't be called twice. + * @param gfcmd The command for GF to be executed. + * expects the -java parameters and all grammar modules + * to be specified. Simply executes this command without any + * modifications. + * @param pm to monitor the loading progress. May be null + */ + private void initializeGF(String gfcmd, ProgressMonitor pm){ + try { + Utils.tickProgress(pm, 5250, "Starting GF"); + logger.debug("Trying: "+gfcmd); + Process extProc = Runtime.getRuntime().exec(gfcmd); + InputStreamReader isr = new InputStreamReader( + extProc.getInputStream(),"UTF8"); + this.fromProc = new BufferedReader (isr); + String defaultEncoding = isr.getEncoding(); + if (logger.isDebugEnabled()) { + logger.debug("encoding "+defaultEncoding); + } + this.toProc = new BufferedWriter(new OutputStreamWriter(extProc.getOutputStream(),"UTF8")); + + readInit(pm, true); + resetPrintnames(false); + } 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"); + } + + } + + /** + * (re-)initializes this.printnameManager and loads the printnames from + * GF. + * @param replayState If GF should be called to give the same state as before, + * but without the message. Is needed, when this function is started by the user. + * If sth. else is sent to GF automatically, this is not needed. + * + */ + private void resetPrintnames(boolean replayState) { + this.printnameManager = new PrintnameManager(); + PrintnameLoader pl = new PrintnameLoader(this.fromProc, this.toProc, this.printnameManager); + if (!selectedMenuLanguage.equals("Abstract")) { + String sendString = selectedMenuLanguage; + pl.readPrintnames(sendString); + //empty GF command, clears the message, so that the printnames + //are not printed again when for example a 'ml' command comes + //next + if (replayState) { + send("gf "); + } + } + } + /** + * reliefs the constructor from setting up the GUI stuff + * @param baseURL the base URL for relative links in the HTML view + * @param showHtml TODO + */ + private void initializeGUI(URL baseURL, boolean showHtml) { + this.setDefaultCloseOperation(DO_NOTHING_ON_CLOSE); + this.addWindowListener(new WindowAdapter() { + public void windowClosing(WindowEvent e) { + endProgram(); + } + }); + + this.readDialog = new ReadDialog(this); + + //Add listener to components that can bring up popup menus. + MouseListener popupListener2 = new PopupListener(); + linearizationArea.addMouseListener(popupListener2); + + //now for the menus + + setJMenuBar(menuBar); + setTitle("GF Syntax Editor"); + viewMenu.setToolTipText("View settings"); + fileMenu.setToolTipText("Main operations"); + langMenu.setToolTipText("Language settings"); + usabilityMenu.setToolTipText("Usability settings"); + menuBar.add(fileMenu); + menuBar.add(langMenu); + menuBar.add(viewMenu); + menuBar.add(modeMenu); + menuBar.add(usabilityMenu); + modeMenu.setToolTipText("Choosing the refinement options' representation"); + + /** + * listens to the showTree JCheckBoxMenuItem and + * switches displaying the AST on or off + */ + final ActionListener showTreeListener = new ActionListener() { + public void actionPerformed(ActionEvent e) { + if (!((JCheckBoxMenuItem)e.getSource()).isSelected()){ + if (logger.isDebugEnabled()) logger.debug("showTree was selected"); + treeCbMenuItem.setSelected(false); + if (((JRadioButtonMenuItem)viewMenu.getItem(2)).isSelected()) { + centerPanel.remove(treePanel); + centerPanel.setLeftComponent(outputPanelUp); + } + else { + centerPanel2.remove(treePanel); + centerPanel2.add(outputPanelUp, BorderLayout.CENTER); + } + } + else { + if (logger.isDebugEnabled()) logger.debug("showTree was not selected"); + treeCbMenuItem.setSelected(true); + if (((JRadioButtonMenuItem)viewMenu.getItem(2)).isSelected()) { + centerPanel.remove(outputPanelUp); + treePanel.setRightComponent(outputPanelUp); + centerPanel.setLeftComponent(treePanel); + } + else { + centerPanel2.remove(outputPanelUp); + treePanel.setRightComponent(outputPanelUp); + centerPanel2.add(treePanel, BorderLayout.CENTER); + } + } + pack(); + repaint(); + } + + }; + + treeCbMenuItem = new JCheckBoxMenuItem("Tree"); + treeCbMenuItem.setActionCommand("showTree"); + treeCbMenuItem.addActionListener(showTreeListener); + treeCbMenuItem.setSelected(true); + + viewMenu.add(treeCbMenuItem); + viewMenu.addSeparator(); + + final Action saveAction = new SaveAction(); + final Action openAction = new OpenAction(); + final Action newTopicAction = new NewTopicAction(); + final Action resetAction = new ResetAction(); + final Action quitAction = new QuitAction(); + final Action undoAction = new UndoAction(); + final Action randomAction = new RandomAction(); + final Action alphaAction = new AlphaAction(); + final Action gfCommandAction = new GfCommandAction(); + final Action readAction = new ReadAction(); + final Action splitAction = new SplitAction(); + final Action combineAction = new CombineAction(); + + JMenuItem fileMenuItem = new JMenuItem(openAction); + fileMenu.add(fileMenuItem); + fileMenuItem = new JMenuItem(newTopicAction); + fileMenu.add(fileMenuItem); + fileMenuItem = new JMenuItem(resetAction); + fileMenu.add(fileMenuItem); + fileMenuItem = new JMenuItem(saveAction); + fileMenu.add(fileMenuItem); + fileMenu.addSeparator(); + fileMenuItem = new JMenuItem(quitAction); + fileMenu.add(fileMenuItem); + + JRadioButtonMenuItem rbMenuItem = new JRadioButtonMenuItem(combineAction); + rbMenuItem.setSelected(true); + /* rbMenuItem.setMnemonic(KeyEvent.VK_R); + rbMenuItem.setAccelerator(KeyStroke.getKeyStroke( + KeyEvent.VK_1, ActionEvent.ALT_MASK)); + rbMenuItem.getAccessibleContext().setAccessibleDescription( + "This doesn't really do anything"); + */ + ButtonGroup menuGroup = new ButtonGroup(); + menuGroup.add(rbMenuItem); + viewMenu.add(rbMenuItem); + + rbMenuItem = new JRadioButtonMenuItem(splitAction); + menuGroup.add(rbMenuItem); + viewMenu.add(rbMenuItem); + + //Font stuff + final int DEFAULT_FONT_SIZE = 14; + GraphicsEnvironment gEnv = GraphicsEnvironment.getLocalGraphicsEnvironment(); + /** The list of font names our environment offers us */ + String[] envfonts = gEnv.getAvailableFontFamilyNames(); + + /** the list of fonts the environment offers us */ + Font[] fontObjs = new Font[envfonts.length]; + for (int fi = 0; fi < envfonts.length; fi++) { + fontObjs[fi] = new Font(envfonts[fi], Font.PLAIN, + DEFAULT_FONT_SIZE); + } + font = new Font(null, Font.PLAIN, DEFAULT_FONT_SIZE); + //font menus + viewMenu.addSeparator(); + fontMenu = new JMenu("Font"); + fontMenu.setToolTipText("Change font"); + sizeMenu = new JMenu("Font Size"); + sizeMenu.setToolTipText("Change font size"); + viewMenu.add(sizeMenu); + viewMenu.add(fontMenu); + + { + JMenuItem fontItem; + ActionListener fontListener = new ActionListener(){ + public void actionPerformed(ActionEvent ae) { + try { + JMenuItem source = (JMenuItem)ae.getSource(); + font = new Font(source.getText(), Font.PLAIN, font.getSize()); + fontEveryWhere(font); + } catch (ClassCastException e) { + logger.warn("Font change started on strange object\n" + e.getLocalizedMessage()); + } + } + }; + for (int i = 0; i < envfonts.length; i++) { + fontItem = new JMenuItem(envfonts[i]); + fontItem.addActionListener(fontListener); + fontItem.setFont(new Font(envfonts[i], Font.PLAIN, font.getSize())); + fontMenu.add(fontItem); + } + } + { + JMenuItem sizeItem; + ActionListener sizeListener = new ActionListener(){ + public void actionPerformed(ActionEvent ae) { + try { + JMenuItem source = (JMenuItem)ae.getSource(); + font = new Font(font.getFontName(), Font.PLAIN, Integer.parseInt(source.getText())); + fontEveryWhere(font); + } catch (ClassCastException e) { + logger.warn("Font change started on strange object\n" + e.getLocalizedMessage()); + } catch (NumberFormatException e) { + logger.warn("strange size entry\n" + e.getLocalizedMessage()); + } + } + }; + /** The list of offered font sizes */ + int[] sizes = {14,18,22,26,30}; + for (int i = 0; i < sizes.length; i++) { + sizeItem = new JMenuItem("" + sizes[i]); + sizeItem.addActionListener(sizeListener); + sizeMenu.add(sizeItem); + } + } + //font stuff over + + //TODO filter menu + filterMenu.setToolTipText("Choosing the linearization representation format"); + { + ActionListener filterActionListener = new ActionListener() { + public void actionPerformed(ActionEvent ae) { + JMenuItem jmi = (JMenuItem)ae.getSource(); + final String sendString = "f " + jmi.getActionCommand(); + send(sendString); + } + }; + JRadioButtonMenuItem jrbmi; + for (int i = 0; i < filterMenuContents.length; i++) { + jrbmi = new JRadioButtonMenuItem(filterMenuContents[i]); + jrbmi.setActionCommand(filterMenuContents[i]); + jrbmi.addActionListener(filterActionListener); + filterButtonGroup.add(jrbmi); + filterMenu.add(jrbmi); + } + } + viewMenu.addSeparator(); + viewMenu.add(filterMenu); + + modeMenu.add(mlMenu); + /** + * switches GF to either display the refinement menu commands + * either in long or short format + */ + final ActionListener longShortListener = new ActionListener() { + public void actionPerformed(ActionEvent e) { + String action = e.getActionCommand(); + if ((action.equals("long")) || (action.equals("short"))) { + send("ms " + action); + return; + } else { + logger.error("RadioListener on wrong object: " + action + "should either be 'typed' or 'untyped'"); + } + } + }; + + modeMenu.addSeparator(); + menuGroup = new ButtonGroup(); + rbMenuItemLong = new JRadioButtonMenuItem("long"); + rbMenuItemLong.setActionCommand("long"); + rbMenuItemLong.setSelected(true); + rbMenuItemLong.addActionListener(longShortListener); + menuGroup.add(rbMenuItemLong); + modeMenu.add(rbMenuItemLong); + rbMenuItem = new JRadioButtonMenuItem("short"); + rbMenuItem.setActionCommand("short"); + rbMenuItem.addActionListener(longShortListener); + menuGroup.add(rbMenuItem); + modeMenu.add(rbMenuItem); + modeMenu.addSeparator(); + + /** + * switches GF to either display the refinement menu with or + * without type annotation ala " : Type" + */ + final ActionListener unTypedListener = new ActionListener() { + public void actionPerformed(ActionEvent e) { + String action = e.getActionCommand(); + if ((action.equals("typed")) || (action.equals("untyped"))) { + send("mt " + action); + return; + } else { + logger.error("RadioListener on wrong object: " + action + "should either be 'typed' or 'untyped'"); + } + } + }; + menuGroup = new ButtonGroup(); + rbMenuItem = new JRadioButtonMenuItem("typed"); + rbMenuItem.setActionCommand("typed"); + rbMenuItem.addActionListener(unTypedListener); + rbMenuItem.setSelected(false); + menuGroup.add(rbMenuItem); + modeMenu.add(rbMenuItem); + rbMenuItemUnTyped = new JRadioButtonMenuItem("untyped"); + rbMenuItemUnTyped.setSelected(true); + rbMenuItemUnTyped.setActionCommand("untyped"); + rbMenuItemUnTyped.addActionListener(unTypedListener); + menuGroup.add(rbMenuItemUnTyped); + modeMenu.add(rbMenuItemUnTyped); + + //OCL specific stuff + selfresultCbMenuItem = new JCheckBoxMenuItem("skip self&result if possible"); + selfresultCbMenuItem.setActionCommand("selfresult"); + selfresultCbMenuItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent e) { + showSelfResult = selfresultCbMenuItem.isSelected(); + send("gf"); + } + }); + selfresultCbMenuItem.setSelected(showSelfResult); + if (this.callback != null || this.linearizations.containsKey("FromUMLTypesOCL")) { + // only visible, if we really do OCL constraints + usabilityMenu.add(selfresultCbMenuItem); + } + + subcatCbMenuItem = new JCheckBoxMenuItem("group possible refinements"); + subcatCbMenuItem.setActionCommand("subcat"); + subcatCbMenuItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent e) { + groupSubcat = subcatCbMenuItem.isSelected(); + send("gf"); + } + }); + subcatCbMenuItem.setSelected(groupSubcat); + usabilityMenu.add(subcatCbMenuItem); + + sortCbMenuItem = new JCheckBoxMenuItem("sort refinements"); + sortCbMenuItem.setActionCommand("sortRefinements"); + sortCbMenuItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent e) { + sortRefinements = sortCbMenuItem.isSelected(); + send("gf"); + } + }); + sortCbMenuItem.setSelected(sortRefinements); + usabilityMenu.add(sortCbMenuItem); + + + //now for the other elements + + //HTML components + + + this.htmlLinPane.setContentType("text/html"); + this.htmlLinPane.setEditable(false); + if (this.htmlLinPane.getStyledDocument() instanceof HTMLDocument) { + try { + URL base; + if (baseURL == null) { + base = (new File("./")).toURL(); + } else { + base = baseURL; + } + if (logger.isDebugEnabled()) { + logger.debug("base for HTML: " + base); + } + ((HTMLDocument)this.htmlLinPane.getDocument()).setBase(base); + } catch (MalformedURLException me) { + logger.error(me.getLocalizedMessage()); + } + } else { + logger.error("No HTMLDocument: " + this.htmlLinPane.getDocument().getClass().getName()); + } + this.htmlLinPane.addCaretListener(new CaretListener() { + /** + * One can either click on a leaf in the lin area, or select a larger subtree. + * The corresponding tree node is selected. + */ + public void caretUpdate(CaretEvent e) { + String jPosition ="", iPosition="", position=""; + HtmlMarkedArea jElement = null; + HtmlMarkedArea iElement = null; + int j = 0; + int i = htmlOutputVector.size()-1; + int start = htmlLinPane.getSelectionStart(); + int end = htmlLinPane.getSelectionEnd(); + if (popUpLogger.isDebugEnabled()) { + popUpLogger.debug("CARET POSITION: " + htmlLinPane.getCaretPosition() + + "\n-> SELECTION START POSITION: "+start + + "\n-> SELECTION END POSITION: "+end); + } + if (linMarkingLogger.isDebugEnabled()) { + if (end > 0 && (end < htmlLinPane.getDocument().getLength())) { + try { + linMarkingLogger.debug("CHAR: " + htmlLinPane.getDocument().getText(end, 1)); + } catch (BadLocationException ble) { + linMarkingLogger.warn(ble.getLocalizedMessage()); + } + } + } + // not null selection: + if ((i > -1) && (start < htmlLinPane.getDocument().getLength())) { + if (linMarkingLogger.isDebugEnabled()) + for (int k=0; k < htmlOutputVector.size(); k++) { + linMarkingLogger.debug("element: "+k+" begin "+((HtmlMarkedArea)htmlOutputVector.elementAt(k)).htmlBegin+" " + + "\n-> end: "+((HtmlMarkedArea)htmlOutputVector.elementAt(k)).htmlEnd+" " + + "\n-> position: "+(((HtmlMarkedArea)htmlOutputVector.elementAt(k)).position).position+" " + + "\n-> words: "+((HtmlMarkedArea)htmlOutputVector.elementAt(k)).words); + } + // localizing end: + while ((j < htmlOutputVector.size()) && (((HtmlMarkedArea)htmlOutputVector.elementAt(j)).htmlEnd < end)) { + j++; + } + // localising start: + while ((i >= 0) && (((HtmlMarkedArea)htmlOutputVector.elementAt(i)).htmlBegin > start)) { + i--; + } + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("i: "+i+" j: "+j); + } + if ((j < htmlOutputVector.size())) { + jElement = (HtmlMarkedArea)htmlOutputVector.elementAt(j); + jPosition = jElement.position.position; + // less & before: + if (i == -1) { // less: + if (end>=jElement.htmlBegin) { + iElement = (HtmlMarkedArea)htmlOutputVector.elementAt(0); + iPosition = iElement.position.position; + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("Less: "+jPosition+" and "+iPosition); + } + position = findMaxHtml(0,j); + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("SELECTEDTEXT: "+position+"\n"); + } + treeChanged = true; + send("mp "+position); + } else { // before: + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("BEFORE vector of size: "+htmlOutputVector.size()); + } + } + } else { // just: + iElement = (HtmlMarkedArea)htmlOutputVector.elementAt(i); + iPosition = iElement.position.position; + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("SELECTED TEXT Just: "+iPosition +" and "+jPosition+"\n"); + } + position = findMax(i,j); + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("SELECTEDTEXT: "+position+"\n"); + } + treeChanged = true; + send("mp "+position); + } + } else if (i>=0) { // more && after: + iElement = (HtmlMarkedArea)htmlOutputVector.elementAt(i); + iPosition = iElement.position.position; + // more + if (start<=iElement.htmlEnd) { + jElement = (HtmlMarkedArea)htmlOutputVector.elementAt(htmlOutputVector.size()-1); + jPosition = jElement.position.position; + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("MORE: "+iPosition+ " and "+jPosition); + } + position = findMax(i,htmlOutputVector.size()-1); + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("SELECTEDTEXT: "+position+"\n"); + } + treeChanged = true; + send("mp "+position); + // after: + } else if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("AFTER vector of size: "+htmlOutputVector.size()); + } + } else { // bigger: + iElement = (HtmlMarkedArea)htmlOutputVector.elementAt(0); + iPosition = iElement.position.position; + jElement = (HtmlMarkedArea)htmlOutputVector.elementAt(htmlOutputVector.size()-1); + jPosition = jElement.position.position; + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("BIGGER: "+iPosition +" and "+jPosition+"\n" + + "\n-> SELECTEDTEXT: []\n"); + } + treeChanged = true; + send("mp []"); + } + }//not null selection + } + }); + this.linSplitPane = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, + this.outputPanelText, outputPanelHtml); + + //cp = getContentPane(); + JScrollPane cpPanelScroll = new JScrollPane(coverPanel); + this.getContentPane().add(cpPanelScroll); + coverPanel.setLayout(new BorderLayout()); + linearizationArea.setToolTipText("Linearizations' display area"); + linearizationArea.addCaretListener(this); + linearizationArea.setEditable(false); + linearizationArea.setLineWrap(true); + linearizationArea.setWrapStyleWord(true); + //linearizationArea.setSelectionColor(Color.green); + + parseField.setFocusable(true); + parseField.addKeyListener(this); + parseField.addFocusListener(this); + // System.out.println(output.getFont().getFontName()); + + //Now for the command buttons in the lower part + gfCommand = new JButton(gfCommandAction); + read = new JButton(readAction); + modify.setToolTipText("Choosing a linearization method"); + alpha = new JButton(alphaAction); + random = new JButton(randomAction); + undo = new JButton(undoAction); + downPanel.add(gfCommand); + downPanel.add(read); + downPanel.add(modify); + downPanel.add(alpha); + downPanel.add(random); + downPanel.add(undo); + //downPanel.add(parse); + //downPanel.add(term); + + //now for the navigation buttons + leftMeta.setToolTipText("Moving the focus to the previous metavariable"); + rightMeta.setToolTipText("Moving the focus to the next metavariable"); + left.setToolTipText("Moving the focus to the previous term"); + right.setToolTipText("Moving the focus to the next term"); + top.setToolTipText("Moving the focus to the top term"); + middlePanelUp.add(leftMeta); + middlePanelUp.add(left); + middlePanelUp.add(top); + middlePanelUp.add(right); + middlePanelUp.add(rightMeta); + middlePanelDown.add(actionOnSubterm); + middlePanel.setLayout(new BorderLayout()); + middlePanel.add(middlePanelUp, BorderLayout.NORTH); + middlePanel.add(middlePanelDown, BorderLayout.CENTER); + + //now for the upper button bar + newTopic = new JButton(newTopicAction); + newCategoryMenu.setToolTipText("The list of available categories to start editing"); + open.setToolTipText("Reading both a new environment and an editing object from file. Current editing will be discarded"); + save.setToolTipText("Writing the current editing object to file in the term or text format"); + grammar.setToolTipText("Current Topic"); + newTopic.setToolTipText("Reading a new environment from file. Current editing will be discarded."); + upPanel.add(grammar); + upPanel.add(newCategoryMenu); + upPanel.add(open); + upPanel.add(save); + upPanel.add(newTopic); + + statusLabel.setToolTipText("The current focus type"); + refinementList.setToolTipText("The list of current refinement options"); + refinementList.setCellRenderer(new ToolTipCellRenderer()); + refinementSubcatList.setToolTipText("The list of current refinement options"); + refinementSubcatList.setCellRenderer(new ToolTipCellRenderer()); + + tree.setToolTipText("The abstract syntax tree representation of the current editing object"); + resetTree(tree); + + bgDisplayType.add(rbText); + bgDisplayType.add(rbHtml); + bgDisplayType.add(rbTextHtml); + if (showHtml) { + rbHtml.setSelected(true); + rbHtml.getAction().actionPerformed(null); + } else { + rbText.setSelected(true); + rbText.getAction().actionPerformed(null); + } + + viewMenu.addSeparator(); + viewMenu.add(rbText); + viewMenu.add(rbHtml); + viewMenu.add(rbTextHtml); + display = new Display(displayType); + + statusPanel.setLayout(new GridLayout(1,1)); + statusPanel.add(statusLabel); + treePanel = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, + tree, outputPanelUp); + treePanel.setDividerSize(5); + treePanel.setDividerLocation(100); + centerPanel2.setLayout(new BorderLayout()); + gui2.setSize(350,100); + gui2.setTitle("Select Action on Subterm"); + gui2.setLocationRelativeTo(treePanel); + centerPanelDown.setLayout(new BorderLayout()); + centerPanel = new JSplitPane(JSplitPane.VERTICAL_SPLIT, + treePanel, centerPanelDown); + centerPanel.setDividerSize(5); + centerPanel.setDividerLocation(250); + centerPanel.addKeyListener(tree); + centerPanel.setOneTouchExpandable(true); + + refinementListsContainer = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT,refinementPanel, refinementSubcatPanel); + + centerPanelDown.add(middlePanel, BorderLayout.NORTH); + centerPanelDown.add(refinementListsContainer, BorderLayout.CENTER); + //centerPanelDown.add(refinementSubcatPanel, BorderLayout.EAST); + coverPanel.add(centerPanel, BorderLayout.CENTER); + coverPanel.add(upPanel, BorderLayout.NORTH); + coverPanel.add(downPanel, BorderLayout.SOUTH); + + 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(this); + + 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(this); + + + newCategoryMenu.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent ae) { + if (!newCategoryMenu.getSelectedItem().equals("New")) { + treeChanged = true; + newObject = true; + send("n " + newCategoryMenu.getSelectedItem()); + newCategoryMenu.setSelectedIndex(0); + } + } + + }); + save.setAction(saveAction); + open.setAction(openAction); + gfCommand.addActionListener(this); + + newCategoryMenu.setFocusable(false); + save.setFocusable(false); + open.setFocusable(false); + newTopic.setFocusable(false); + gfCommand.setFocusable(false); + + leftMeta.setFocusable(false); + left.setFocusable(false); + + /** handles the clicking of the navigation buttons */ + ActionListener naviActionListener = new ActionListener() { + /** + * convenience method instead of 5 single ones + */ + public void actionPerformed(ActionEvent ae) { + Object obj = ae.getSource(); + if ( obj == leftMeta ) { + treeChanged = true; + send("<<"); + } + if ( obj == left ) { + treeChanged = true; + send("<"); + } + if ( obj == top ) { + treeChanged = true; + send("'"); + } + if ( obj == right ) { + treeChanged = true; + send(">"); + } + if ( obj == rightMeta ) { + treeChanged = true; + send(">>"); + } + } + }; + + top.addActionListener(naviActionListener); + right.addActionListener(naviActionListener); + rightMeta.addActionListener(naviActionListener); + leftMeta.addActionListener(naviActionListener); + left.addActionListener(naviActionListener); + read.addActionListener(this); + modify.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent ae) { + if (!modify.getSelectedItem().equals("Modify")) { + treeChanged = true; + send("c " + modify.getSelectedItem()); + modify.setSelectedIndex(0); + } + } + + }); + //mode.addActionListener(this); + alpha.addActionListener(this); + random.addActionListener(this); + + top.setFocusable(false); + right.setFocusable(false); + rightMeta.setFocusable(false); + //parse.setFocusable(false); + //term.setFocusable(false); + read.setFocusable(false); + modify.setFocusable(false); + //mode.setFocusable(false); + alpha.setFocusable(false); + random.setFocusable(false); + undo.setFocusable(false); + + linearizationArea.addKeyListener(tree); + this.setSize(800,600); + outputPanelUp.setPreferredSize(new Dimension(400,230)); + treePanel.setDividerLocation(0.3); + nodeTable.put(new TreePath(tree.rootNode.getPath()), new Integer(0)); + + JRadioButton termButton = new JRadioButton("Term"); + termButton.setActionCommand("term"); + termButton.setSelected(true); + JRadioButton linButton = new JRadioButton("Text"); + linButton.setActionCommand("lin"); + // Group the radio buttons. + saveTypeGroup.add(linButton); + saveTypeGroup.add(termButton); + JPanel buttonPanel = new JPanel(); + buttonPanel.setPreferredSize(new Dimension(70, 70)); + buttonPanel.add(new JLabel("Format:")); + buttonPanel.add(linButton); + buttonPanel.add(termButton); + saveFc.setAccessory(buttonPanel); + + fontEveryWhere(font); + this.setVisible(true); + + } + + /** + * send a command to GF and reads the returned XML + * @param text the command, exacltly the string that is going to be sent + */ + protected void send(String text){ + send(text, true); + } + + /** + * send a command to GF. + * @param text the command, exacltly the string that is going to be sent + * @param andRead if true, the returned XML will be read an displayed accordingly + */ + protected void send(String text, boolean andRead) { + if (sendLogger.isDebugEnabled()) { + sendLogger.debug("## send: '" + text + "'"); + } + try { + this.display = new Display(displayType); + display(true, false); + if (xmlLogger.isDebugEnabled()) { + xmlLogger.debug("output cleared\n\n\n"); + } + this.htmlOutputVector = new Vector(); + this.textOutputVector = new Vector(); + toProc.write(text, 0, text.length()); + toProc.newLine(); + toProc.flush(); + //run(); + if (andRead) { + readAndDisplay(); + } + } catch (IOException e) { + System.err.println("Could not write to external process " + e); + } + } + + /** + * a simple wrapper around readGfedit that also probes + * for unneccessary commands + */ + protected void readAndDisplay() { + readGfedit(); + probeCompletability(); + refinementList.requestFocusInWindow(); + } + + /** + * reads the front matter that GF returns when freshly started and loading a grammar. + * When <gfinit> is read, the function returns. + * @param pm to monitor the loading progress. May be null + * @param greetingsToo if the greeting text from GF is expected + */ + protected void readInit(ProgressMonitor pm, boolean greetingsToo) { + String next = ""; + if (greetingsToo) { + next = readGfGreetings(); + } else { + try { + next = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("1 " + next); + } catch (IOException e) { + System.err.println("Could not read from external process:\n" + e); + } + } + Utils.tickProgress(pm, 5300, null); + next = readGfLoading(next, pm); + if (next.equals("")) { + readGfinit(); + } + } + + + /** + * reads the greeting text from GF + * @return the last read GF line, which should be the first loading line + */ + protected String readGfGreetings() { + try { + String readresult = ""; + StringBuffer outputStringBuffer = new StringBuffer(); + readresult = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("1 "+readresult); + while ((readresult.indexOf("gf")==-1) && (readresult.trim().indexOf("<") < 0)){ + outputStringBuffer.append(readresult).append("\n"); + readresult = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("1 "+readresult); + } + this.display.addToStages(outputStringBuffer.toString(), outputStringBuffer.toString().replaceAll("\\n", "
")); + display(true, false); + return readresult; + } catch (IOException e) { + System.err.println("Could not read from external process:\n" + e); + return ""; + } + + } + + /** + * 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 the first line from >gfinit< or >gfedit< + */ + protected String readGfLoading(String readresult, ProgressMonitor pm) { + try { + StringBuffer textPure = new StringBuffer(); + StringBuffer textHtml = new StringBuffer(); + int progress = 5300; + while (!(readresult.indexOf("") > -1 || (readresult.indexOf("") > -1))){ + readresult = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("1 "+readresult); + textPure.append(readresult).append("\n"); + textHtml.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" + //without newlines + final int beginInit = readresult.indexOf(""); + if (beginInit > 0) { + textPure.append(readresult.substring(0, beginInit)).append("\n"); + textPure.append(readresult.substring(0, beginInit)).append("
\n"); + //that is the expected result + readresult = ""; + } + this.display.addToStages(textPure.toString(), textHtml.toString()); + display(true, false); + return readresult; + } catch (IOException e) { + System.err.println("Could not read from external process:\n" + e); + return ""; + } + + } + + /** + * reads the part between >gfinit< and >/gfinit< + * and feeds the editor with what was read + */ + protected void readGfinit() { + try { + //read or or (in case of no grammar loaded) + String readresult = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("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" + if (readresult.indexOf("") > -1) { + readresult = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("12 "+readresult); + } + String next = readHmsg(readresult); + + if ((next!=null) && ((next.indexOf("newcat") > -1) || (next.indexOf("topic") > -1))) { + formNewMenu(); + } + + } catch (IOException e) { + System.err.println("Could not read from external process:\n" + e); + } + + } + + /** + * reads the output from GF starting with >gfedit< and last reads >/gfedit<. + * Feeds the editor with what was read. + * @return the last read line, should be "" + */ + protected String readGfedit() { + try { + String next = ""; + //read + String readresult = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("11 "+readresult); + //read either or + readresult = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("11 "+readresult); + + //hmsg stuff + next = readHmsg(readresult); + + //reading + //seems to be the only line read here + while ((next!=null)&&((next.length()==0)||(next.indexOf(" -1)) { + if (checkTypeSelfResult(i, varself) ){ + i -=1; + } + } + if ((cmd.indexOf("r core.result") > -1)) { + if (checkTypeSelfResult(i, varresult)) { + i -= 1; + } + } + } + + //(cmd.indexOf("r core.result") > -1) + } + + } + + /** + * Compares the type of the currently offered self or result and + * removes this command from the list, if it doesn't match + * the type of the on the top level introduced bound variable + * for self resp. result + * @param i The number of the current cmd in this.listModel + * @param boundVar indicates whether self or result is to be + * checked. + * if boundVar is "VarResult", result is checked, if boundVar is + * "VarSelf", self. + * Use nothing else! + * @return true iff a command was removed from listModel + */ + private boolean checkTypeSelfResult(int i, String boundVar) { + //assert "VarSelf".equals(boundVar) || "VarResult".equals(boundVar); + final String instance = "Instance"; + + String selfType = null; + //find the bound VarSelf variable + for (int j = 0; j < this.constraintNode.boundNames.length; j++) { + if (this.constraintNode.boundTypes[j].startsWith(boundVar)) { + selfType = this.constraintNode.boundTypes[j].substring(boundVar.length()).trim(); + } + } + // check if the current node can be refined with sth + // of type Instance WhatEverClassSelfHas + if ((selfType == null) || (!(instance + " " + selfType).equals(this.currentNode.getType()))) { + //remove it from the list of offered commands + listModel.remove(i); + return true; + } else { + return false; + } + } + + /** + * prints the available command line options + */ + private static void printUsage() { + System.err.println("Usage: java -jar [-h/--html] [-b/--base baseURL] [grammarfile(s)]"); + System.err.println("where -h activates the HTML mode"); + System.err.println("and -b sets the base location to which links in HTML are relative to. " + + "Default is the current directory."); + } + + /** + * starts the editor + * @param args only the first parameter is used, it has to be a complete GF command, + * which is executed and thus should load the needed grammars + */ + public static void main(String args[]) { + Utils.configureLogger(); + //command line parsing + CmdLineParser parser = new CmdLineParser(); + CmdLineParser.Option optHtml = parser.addBooleanOption('h', "html"); + CmdLineParser.Option optBase = parser.addStringOption('b', "base"); + CmdLineParser.Option gfBin = parser.addStringOption('g', "gfbin"); + // Parse the command line options. + + try { + parser.parse(args); + } + catch (CmdLineParser.OptionException e) { + System.err.println(e.getMessage()); + printUsage(); + System.exit(2); + } + Boolean isHtml = (Boolean)parser.getOptionValue(optHtml, Boolean.FALSE); + String baseString = (String)parser.getOptionValue(optBase, null); + String gfBinString = (String)parser.getOptionValue(gfBin, null); + String[] otherArgs = parser.getRemainingArgs(); + + URL myBaseURL; + if (baseString != null) { + try { + myBaseURL = new URL(baseString); + } catch (MalformedURLException me) { + logger.error(me.getLocalizedMessage()); + me.printStackTrace(); + myBaseURL = null; + } + } else { + myBaseURL = null; + } + +// if (logger.isDebugEnabled()) { +// logger.debug(isHtml + " : " + baseString + " : " + otherArgs); +// } + //construct the call to GF + String gfCall = ((gfBinString != null && !gfBinString.equals(""))? gfBinString : "gf"); + gfCall += " -java"; + for (int i = 0; i < otherArgs.length; i++) { + gfCall = gfCall + " " + otherArgs[i]; + } + Locale.setDefault(Locale.US); + logger.info("call to GF: " + gfCall); + GFEditor2 gui = new GFEditor2(gfCall, isHtml.booleanValue(), myBaseURL); + if (logger.isDebugEnabled()) { + logger.debug("main finished"); + } + } + + /** + * Calls the Java GF GUI to edit an OCL constraint. To be called by GFinterface + * @param gfCmd the command to start the GF, must include the -java and all modules + * @param callback the callback class that knows how to store the constraints + * @param initAbs the initial abstract syntax tree (not OCL) + * @param initDefault if initAbs is empty, then initDefault is used + * @param pm to monitor the loading progress. May be null + */ + static void mainConstraint(String gfCmd, ConstraintCallback callback, String initAbs, String initDefault, ProgressMonitor pm) { + Locale.setDefault(Locale.US); + GFEditor2 gui; + if (initAbs.equals("")) { + gui = new GFEditor2(gfCmd, callback, "[ctn] g " + initDefault, pm); + } else { + gui = new GFEditor2(gfCmd, callback, "[ctn] g " + initAbs, pm); + } + + } + + + /** + * we should not end the program, just close the GF editor + * possibly sending something back to KeY + */ + protected void endProgram(){ + int returnStatus = JOptionPane.showConfirmDialog(this, "Save constraint?", "Save before quitting?", JOptionPane.YES_NO_CANCEL_OPTION, JOptionPane.QUESTION_MESSAGE ); + if (returnStatus == JOptionPane.CANCEL_OPTION) { + return; + } else if (returnStatus == JOptionPane.NO_OPTION) { + shutDown(); + return; + } + if (this.callback != null) { + try { + // quit should always work even if we cannot send something proper + // back to Together/KeY. + // Hence this try-catch + if (returnStatus == JOptionPane.YES_OPTION) { + String ocl = (String)linearizations.get(modelModulName + "OCL"); + if (ocl == null) { + //OCL not present, so switch it on + langMenuModel.setActive(modelModulName + "OCL", true); + send("on " + modelModulName + "OCL"); + ocl = (String)linearizations.get(modelModulName + "OCL"); + } + ocl = compactSpaces(ocl.trim()).trim(); + + this.callback.sendConstraint(ocl); + + } + } catch (Exception e) { // just print information about the exception + System.err.println("GFEditor2.endProgram() Caught an Exception."); + System.err.println("e.getLocalizedMessage(): " + e.getLocalizedMessage()); + System.err.println("e.toString(): " + e); + System.err.println("e.printStackTrace():"); + e.printStackTrace(System.err); + } finally { + if (this.callback != null) { // send linearization as a class invariant + Utils.cleanupFromUMLTypes(callback.getGrammarsDir()); + } + shutDown(); + } + } else if (returnStatus == JOptionPane.YES_OPTION) { + final Action saveAction = new SaveAction(); + saveAction.actionPerformed(null); + shutDown(); + } + } + + + /** + * Shuts down GF and terminates the edior + */ + private void shutDown() { + try { + send("q", false); // tell external GF process to quit + } finally { + removeAll(); + dispose(); + } + } + + /** + * 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; + } + + /** + * fills the menu with the possible actions like refinements + * with the available ones. + * Parses the GF-output between and tags + * and fills the corrsponding GUI list -"Select Action". + * seems to expect the starting menu tag to be already read + */ + protected void readRefinementMenu (){ + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("list model changing! "); + String s =""; + Vector printnameVector = new Vector(); + Vector commandVector = new Vector(); + Vector gfCommandVector = new Vector(); + HashSet processedSubcats = new HashSet(); + try { + //read item + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("8 "+result); + while (result.indexOf("/menu")==-1){ + //read show + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("8 "+result); + while (result.indexOf("/show")==-1){ + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("9 "+result); + if (result.indexOf("/show")==-1) + { + if (result.length()>8) + s+=result.trim(); + else + s+=result; + } + } + // if (s.charAt(0)!='d') + // listModel.addElement("Refine " + s); + // else + String showText = s; + printnameVector.addElement(s); + s=""; + //read /show + //read send + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("8 "+result); + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("8 "+result); + String myCommand = result; + commandVector.add(this.result); + //read /send (discarded) + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("8 "+result); + + // read /item + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("8 "+result); + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("8 "+result); + + final boolean isAbstract = "Abstract".equals(this.selectedMenuLanguage); + RealCommand gfc = new RealCommand(myCommand, processedSubcats, this.printnameManager, showText, isAbstract); + gfCommandVector.addElement(gfc); + } + } catch(IOException e){ + System.err.println(e.getMessage()); + e.printStackTrace(); + } + formRefinementMenu(gfCommandVector); + } + + /** + * Goes through the list of possible refinements and groups them + * 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. + * @param gfCommandVector contains all RealCommands, that are available + * at the moment + */ + protected void formRefinementMenu(Vector gfCommandVector) { + this.listModel.clear(); + this.refinementSubcatListModel.clear(); + this.gfcommands.clear(); + this.subcatListModelHashtable.clear(); + this.whichSubcat = null; + this.popup2.removeAll(); + Vector prelListModel = new Vector(); + + //at the moment, we don't know yet, which subcats are + //nearly empty + for (Iterator it = gfCommandVector.iterator(); it.hasNext();) { + GFCommand gfcommand = (GFCommand)it.next(); + if ((!this.groupSubcat) || (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(), this.printnameManager); + 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 (this.currentNode.isMeta()) { + if (this.currentNode.getType().equals("Int")) { + prelListModel.addElement(InputCommand.intInputCommand); + } if (this.currentNode.getType().equals("String")) { + prelListModel.addElement(InputCommand.stringInputCommand); + } + } + + //now sort the preliminary listmodel + if (sortRefinements) { + Collections.sort(prelListModel); + } + //now fill this.listModel + for (Iterator it = prelListModel.iterator(); it.hasNext();) { + Object next = it.next(); + this.listModel.addElement(next); + } + } + + /** + * 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. + * @param prevreadresult The last line read from GF + * @return the last line this method has read + */ + protected String readHmsg(String prevreadresult){ + if ((prevreadresult!=null)&&(prevreadresult.indexOf("") > -1)) { + StringBuffer s =new StringBuffer(""); + try { + String readresult = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("7 "+readresult); + while (readresult.indexOf("/hmsg")==-1){ + s.append(readresult).append('\n'); + readresult = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("7 "+readresult); + } + if (s.indexOf("c") > -1) { + //clear output before linearization + this.display = new Display(displayType); + display(false, false); + this.htmlOutputVector = new Vector(); + this.textOutputVector = new Vector(); + } + if (s.indexOf("t") > -1) { + //tree has changed + this.treeChanged = true; + } + if (s.indexOf("n") > -1) { + //a new object has been created + this.newObject = true; + } + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("7 "+result); + return result; + } catch(IOException e){ + System.err.println(e.getMessage()); + e.printStackTrace(); + return ""; + } + } else { + return prevreadresult; + } + } + + + /** + * 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 tags + */ + protected void readLin(){ + try { + linearization=""; + linearization += result+"\n"; + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("6 "+result); + while ((result!=null)&&(result.indexOf("/linearization")==-1)){ + linearization += result+"\n"; + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("6 "+result); + } + if (newObject) formLin(); + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("6 "+result); + } catch(IOException e){ + System.err.println(e.getMessage()); + e.printStackTrace(); + } + } + + /** + * 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 + */ + protected void readTree(){ + String treeString = ""; + try { + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("6 "+result); + while (result.indexOf("/tree")==-1){ + treeString += result+"\n"; + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("6 "+result); + } + if (treeChanged && (newObject)) { + formTree(tree, treeString); + treeChanged = false; + } + treeString=""; + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("6 "+result); + } catch(IOException e){ + System.err.println(e.getMessage()); + e.printStackTrace(); + } + } + + /** + * Parses the GF-output between tags + * and puts it in the linearization area. + * seems to expect the opening message tag to be already read + */ + protected void readMessage(){ + String s =""; + try { + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("7 "+result); + while (result.indexOf("/message")==-1){ + s += result+"\n"; + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("7 "+result); + } + if (s.length()>1) { + this.display.addToStages("-------------\n" + s, "
" + s); + //in case no language is displayed + display(false, false); + } + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("7 "+result); + } catch(IOException e){ + System.err.println(e.getMessage()); + e.printStackTrace(); + } + } + + /** + * reads the cat entries and puts them into menu, and after that reads + * the names of the languages and puts them into the language menu + * Parses the GF-output between tags + * and fill the New combobox in the GUI. + */ + protected void formNewMenu () { + boolean more = true; + try { + //read first cat + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) { + xmlLogger.debug("2 "+result); + } + if (result.indexOf("(none)") > -1) { + //no topics present + more = false; + } + + while (more){ + //adds new cat s to the menu + if (result.indexOf("topic")==-1) { + newCategoryMenu.addItem(result.substring(6)); + } + else + more = false; + //read + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("2 "+result); + //read + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("3 "+result); + //read actual language + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("4 "+result); + + //read the languages and select the last non-abstract + more = true; + while (more){ + if ((result.indexOf("/gfinit")==-1)&&(result.indexOf("lin")==-1)) { + //form lang and Menu menu: + final String langName = result.substring(4); + final boolean active; + if (langName.equals("Abstract")) { + active = false; + } else { + active = true; + } + this.langMenuModel.add(langName, active); + + //select FromUMLTypesOCL by default + if (langName.equals(modelModulName + "OCL")) { + this.selectedMenuLanguage = modelModulName + "OCL"; + } + //'register' the presence of this language. + this.linearizations.put(langName, null); + } else { + more = false; + } + // read + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("2 "+result); + // read or + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("3 "+result); + if ((result.indexOf("/gfinit")!=-1)||(result.indexOf("lin")!=-1)) + more = false; + if (result.indexOf("/gfinit")!=-1) + finished = true; + // registering the file name: + if (result.indexOf("language")!=-1) { + String path = result.substring(result.indexOf('=')+1, + result.indexOf('>')); + path =path.substring(path.lastIndexOf('/')+1); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("name: "+path); + fileString +="--" + path +"\n"; + if (path.lastIndexOf('.')!=path.indexOf('.')) + grammar.setText(path.substring(0, + path.indexOf('.')).toUpperCase()+" "); + } + //TODO in case of finished, read "", otherwise ... + result = fromProc.readLine(); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("4 "+result); + } + } catch(IOException e){ + logger.warn(e.getMessage()); + } + } + + /** + * Parses the GF-output between <lin> </lin> tags. + * Sets the current focusPosition, then changes all <focus> tags + * into regular <subtree> tags. + * + * Expects its argument in this.result + * + * Then control is given to appendMarked, which does the display + * @param clickable true iff the correspondent display area should be clickable + * @param doDisplay true iff the linearization should be displayed. + */ + protected StringBuffer outputAppend(boolean clickable, boolean doDisplay){ + final StringBuffer linCollector = new StringBuffer(); + //result=result.replace('\n',' '); + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("INPUT:"+result); + } + int focusTagBegin = this.result.indexOf("',typeBegin); + // status incorrect ?: + final int typeEnd; + if ((typeBegin > -1) && (this.result.substring(typeBegin,focusTagEnd).indexOf("incorrect")!=-1)) { + typeEnd = result.indexOf("status"); + } else { + typeEnd = focusTagEnd; + } + int focusTextBegin = this.result.indexOf("focus"); + if (focusTagBegin!=-1){ + // in case focus tag is cut into two lines: + if (focusTagBegin==-1){ + focusTagBegin = focusTextBegin - 7; + } + final int positionBegin=this.result.indexOf("position",focusTagBegin); + final int positionEnd=this.result.indexOf("]",positionBegin); + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("POSITION START: "+positionBegin + + "\n-> POSITION END: "+positionEnd); + } + if (xmlLogger.isDebugEnabled()) { + xmlLogger.debug("form Lin1: "+this.result); + } + this.focusPosition = new LinPosition(result.substring(positionBegin+9,positionEnd+1), + this.result.substring(positionBegin,focusTagEnd).indexOf("incorrect")==-1); + statusLabel.setText(" "+result.substring(typeBegin+5,typeEnd)); + //changing to + this.result = replaceNotEscaped(this.result, " -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(); + } + + + /** + * Parses the GF-output between tags + * + * pseudo-parses the XML lins and fills the output text area + * with the lin in all enabled languages + */ + protected void formLin(){ + //reset previous output + this.display = new Display(displayType); + this.linearizations.clear(); + + boolean firstLin=true; + //read first line like ' ' + result = linearization.substring(0,linearization.indexOf('\n')); + //the rest of the linearizations + String lin = linearization.substring(linearization.indexOf('\n')+1); + //extract the language from result + int ind = Utils.indexOfNotEscaped(result, "="); + int ind2 = Utils.indexOfNotEscaped(result, ">"); + /** The language of the linearization */ + String language = result.substring(ind+1,ind2); + //the first direct linearization + result = lin.substring(0,lin.indexOf("")); + //the rest + lin = lin.substring(lin.indexOf("")); + while (result.length()>1) { + this.langMenuModel.add(language,true); + // selected? + boolean visible = this.langMenuModel.isLangActive(language); + if (visible && !firstLin) { + // appending sth. linearizationArea + this.display.addToStages("\n************\n", "

"); + } + if (xmlLogger.isDebugEnabled()) { + xmlLogger.debug("linearization for the language: "+result); + } + // we want the side-effects of outputAppend + final boolean isAbstract = "Abstract".equals(language); + String linResult = outputAppend(!isAbstract, visible).toString(); + if (visible) { + firstLin = false; + } + linearizations.put(language, linResult); + // read + lin = lin.substring(lin.indexOf('\n')+1); + // read lin or 'end' + if (lin.length()<1) { + break; + } + + result = lin.substring(0,lin.indexOf('\n')); + lin = lin.substring(lin.indexOf('\n')+1); + if (result.indexOf("'); + language = result.substring(ind+1,ind2); + result = lin.substring(0,lin.indexOf("")); + lin = lin.substring(lin.indexOf("")); + } + } + display(true, true); + + //do highlighting + this.linearizationArea.getHighlighter().removeAllHighlights(); + this.htmlLinPane.getHighlighter().removeAllHighlights(); + final HashSet incorrectMA = new HashSet(); + for (int i = 0; i this.htmlLinPane.getDocument().getLength()) { + end = this.htmlLinPane.getDocument().getLength(); + } + this.htmlLinPane.getHighlighter().addHighlight(begin, end, new DefaultHighlighter.DefaultHighlightPainter(color)); + if (redLogger.isDebugEnabled()) { + redLogger.debug("HTML HIGHLIGHT: " + this.htmlLinPane.getDocument().getText(begin, end - begin) + "; Color:" + color); + } + } catch (BadLocationException e) { + redLogger.warn("HTML highlighting problem!\n" + e.getLocalizedMessage() + " : " + e.offsetRequested() + "\nHtmlMarkedArea: " + ma + "\nhtmlLinPane length: " + this.htmlLinPane.getDocument().getLength()); + } + } + + /** + * Highlights the given MarkedArea in linearizationArea + * @param ma the MarkedArea + * @param color the color the highlight should get + */ + private void highlight(final MarkedArea ma, Color color) { + try { + int begin = ma.begin; + int end = ma.end ; + //When creating the HtmlMarkedArea, we don't know, if + //it is going to be the last or not. + if (end > this.linearizationArea.getText().length()) { + end = this.linearizationArea.getText().length() + 1; + } + this.linearizationArea.getHighlighter().addHighlight(begin, end, new DefaultHighlighter.DefaultHighlightPainter(color)); + if (redLogger.isDebugEnabled()) { + redLogger.debug("HIGHLIGHT: " + this.linearizationArea.getText(begin, end - begin) + "; Color:" + color); + } + } catch (BadLocationException e) { + redLogger.warn("highlighting problem!\n" + e.getLocalizedMessage() + " : " + e.offsetRequested() + "\nMarkedArea: " + ma + "\nlinearizationArea length: " + this.linearizationArea.getText().length()); + } + } + + + /** + * compares two position strings and returns true, if superPosition is + * a prefix of subPosition, that is, if subPosition is in a subtree of + * superPosition + * @param superPosition the position String in Haskell notation + * ([0,1,0,4]) of the to-be super-branch of subPosition + * @param subPosition the position String in Haskell notation + * ([0,1,0,4]) of the to-be (grand-)child-branch of superPosition + * @return true iff superPosition denotes an ancestor of subPosition + */ + private static boolean isSubtreePosition(final LinPosition superPosition, final LinPosition subPosition) { + if (superPosition == null || subPosition == null) { + return false; + } + String superPos = superPosition.position; + String subPos = subPosition.position; + if (superPos.length() < 2 || subPos.length() < 2 ) { + return false; + } + superPos = superPos.substring(1, superPos.length() - 1); + subPos = subPos.substring(1, subPos.length() - 1); + boolean result = subPos.startsWith(superPos); + return result; + } + + /** + * Sets the font on all the GUI-elements to font. + * @param newFont the font everything should have afterwards + */ + protected void fontEveryWhere(Font newFont) { + linearizationArea.setFont(newFont); + htmlLinPane.setFont(newFont); + parseField.setFont(newFont); + tree.tree.setFont(newFont); + refinementList.setFont(newFont); + refinementSubcatList.setFont(newFont); + popup2.setFont(newFont); + save.setFont(newFont); + grammar.setFont(newFont); + open.setFont(newFont); + newTopic.setFont(newFont); + gfCommand.setFont(newFont); + leftMeta.setFont(newFont); + left.setFont(newFont); + top.setFont(newFont); + right.setFont(newFont); + rightMeta.setFont(newFont); + actionOnSubterm.setFont(newFont); + read.setFont(newFont); + alpha.setFont(newFont); + random.setFont(newFont); + undo.setFont(newFont); + filterMenu.setFont(newFont); + setFontRecursive(filterMenu, newFont, false); + modify.setFont(newFont); + statusLabel.setFont(newFont); + menuBar.setFont(newFont); + newCategoryMenu.setFont(newFont); + readDialog.setFont(newFont); + mlMenu.setFont(newFont); + setFontRecursive(mlMenu, newFont, false); + modeMenu.setFont(newFont); + setFontRecursive(modeMenu, newFont, false); + langMenu.setFont(newFont); + setFontRecursive(langMenu, newFont, false); + fileMenu.setFont(newFont); + setFontRecursive(fileMenu, newFont, false); + usabilityMenu.setFont(newFont); + setFontRecursive(usabilityMenu, newFont, false); + viewMenu.setFont(newFont); + setFontRecursive(viewMenu, newFont, false); + setFontRecursive(sizeMenu, newFont, false); + setFontRecursive(fontMenu, newFont, true); + //update also the HTML with the new size + display(false, true); + } + + /** + * Set the font in the submenus of menu. + * Recursion depth is 1, so subsubmenus don't get fontified. + * @param subMenu The menu whose submenus should get fontified + * @param font the chosen font + * @param onlySize If only the font size or the whole font should + * be changed + */ + private void setFontRecursive(JMenu subMenu, Font font, boolean onlySize) + { + for (int i = 0; i tags + * and build the corresponding tree. + * + * parses the already read XML for the tree and stores the tree nodes + * in nodeTable with their numbers as keys + * @param myTreePanel the panel of GFEditor2 + * @param treeString the string representation for the XML tree + */ + protected void formTree(DynamicTree2 myTreePanel, String treeString) { + if (treeLogger.isDebugEnabled()) { + treeLogger.debug("treeString: "+ treeString); + } + + /** + * stores the nodes and the indention of their children. + * Works stack like, so when all children of a node are read, + * the next brethren / uncle node 'registers' with the same + * indention depth to show that the next children are his. + */ + Hashtable parentNodes = new Hashtable(); + /** + * the path in the JTree (not in GF repesentation!) to the + * current new node. + */ + TreePath path=null; + String s = treeString; + myTreePanel.clear(); + /** consecutive node numbering */ + int index = 0; + /** the node that gets created from the current line */ + DefaultMutableTreeNode newChildNode=null; + /** is a star somewhere in treestring? 1 if so, 0 otherwise */ + int star = 0; + if (s.indexOf('*')!=-1) { + star = 1; + } + /** + * only the first node in the AST that introduces an oper + * constraint brings with it the bound variables for self + * and result. + * At least for single context constraints, but that is exactly + * that what the editor is for. + */ + boolean boundVarsEncountered = false; + while (s.length()>0) { + /** + * every two ' ' indicate one tree depth level + * shift first gets assigned the indention depth in + * characters, later the tree depth + */ + int shift = 0; + boolean selected = false; + while ((s.length()>0) && ((s.charAt(0)=='*')||(s.charAt(0)==' '))){ + if (s.charAt(0) == '*') { + selected = true; + } + s = s.substring(1); + shift++; + } + if (s.length()>0) { + + int j = s.indexOf("\n"); + //is sth like "andS : Sent ", i.e. "fun : type " before trimming + String gfline = s.substring(0, j).trim(); + GfAstNode node = new GfAstNode(gfline); + if (selected) { + this.currentNode = node; + } + //get the node that introduces self and result + if ((!boundVarsEncountered) && ("OperConstraintBody".equals(node.getType()) || "ClassConstraintBody".equals(node.getType()))) { + this.constraintNode = node; + boundVarsEncountered = true; + } + + index++; + s = s.substring(j+1); + shift = (shift - star)/2; + + /* + * we know the parent, so we can ask it for the param information + * for the next child (the parent knows how many it has already) + * and save it in an AstNodeData + */ + + DefaultMutableTreeNode parent = (DefaultMutableTreeNode)parentNodes.get(new Integer(shift)); + //default case, if we can get more information, this is overwritten + AstNodeData and; + Printname childPrintname = null; + if (!node.isMeta()) { + childPrintname = this.printnameManager.getPrintname(node.getFun()); + } + if (childPrintname != null) { + //we know this one + and = new RefinedAstNodeData(childPrintname, node); + } else if (parent != null && node.isMeta()) { + //new child without refinement + AstNodeData parentAnd = (AstNodeData)parent.getUserObject(); + Printname parentPrintname = null; + if (parentAnd != null) { + parentPrintname = parentAnd.getPrintname(); + } + if (parentPrintname != null) { + int paramPosition = parent.getChildCount(); + String paramName = parentPrintname.getParamName(paramPosition); + if (paramName == null) { + paramName = node.getFun(); + } + //if tooltip turns out to be null that's OK + String paramTooltip = parentPrintname.htmlifySingleParam(paramPosition); +// if (logger.isDebugEnabled()) { +// logger.debug("new node-parsing: '" + name + "', fun: '" + fun + "', type: '" + paramType + "'"); +// } + and = new UnrefinedAstNodeData(paramTooltip, node); + + } else { + and = new RefinedAstNodeData(null, node); + } + } else { + //something unparsable, bad luck + //or refined and not described + and = new RefinedAstNodeData(null, node); + } + + + + + newChildNode = myTreePanel.addObject(parent, and); + parentNodes.put(new Integer(shift+1), newChildNode); + path = new TreePath(newChildNode.getPath()); + nodeTable.put(path, new Integer(index)); + + if (selected) { + //show the selected as the 'selected' one in the JTree + myTreePanel.tree.setSelectionPath(path); + myTreePanel.oldSelection = index; + if (treeLogger.isDebugEnabled()) { + treeLogger.debug("new selected index "+ index); + } + } + } + } + if ((newChildNode!=null)) { + myTreePanel.tree.makeVisible(path); + gui2.toFront(); + index = 0; + } + } + + + /** Handle the key pressed event. */ + public void keyPressed(KeyEvent e) { + int keyCode = e.getKeyCode(); + Object obj = e.getSource(); + if (keyLogger.isDebugEnabled()) { + keyLogger.debug("Key pressed: " + e.toString()); + } + + if (obj==refinementSubcatList) { + if (keyCode == KeyEvent.VK_ENTER) { + listAction(refinementSubcatList, refinementSubcatList.getSelectedIndex(), true); + } else if (keyCode == KeyEvent.VK_LEFT) { + refinementList.requestFocusInWindow(); + refinementSubcatList.clearSelection(); + refinementList.setSelectionBackground(refinementSubcatList.getSelectionBackground()); + } + } else if (obj == refinementList) { + 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); + } + } + } else if (obj==parseField) { + if (keyCode == KeyEvent.VK_ENTER) { + getLayeredPane().remove(parseField); + treeChanged = true; + send("p "+parseField.getText()); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("sending parse string: "+parseField.getText()); + repaint(); + } else if (keyCode == KeyEvent.VK_ESCAPE) { + getLayeredPane().remove(parseField); + repaint(); + } + } + } + + /** + * 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 + } + + /** + * Returns the biggest position of first and second. + * Each word in the linearization area has the corresponding + * position in the tree. The position-notion is taken from + * GF-Haskell, where empty position ("[]") + * represents tree-root, "[0]" represents first child of the root, + * "[0,0]" represents the first grandchild of the root etc. + * So comparePositions("[0]","[0,0]")="[0]" + */ + private String comparePositions(String first, String second) { + String common ="[]"; + int i = 1; + while ((i SELECTION START POSITION: "+start + + "\n-> SELECTION END POSITION: "+end); + } + if (linMarkingLogger.isDebugEnabled()) { + if (end>0&&(end-1)&&(start end: "+((MarkedArea)this.htmlOutputVector.elementAt(k)).end+" " + + "\n-> position: "+(((MarkedArea)this.htmlOutputVector.elementAt(k)).position).position+" " + + "\n-> words: "+((MarkedArea)this.htmlOutputVector.elementAt(k)).words); + } + // localizing end: + while ((j< this.htmlOutputVector.size())&&(((MarkedArea)this.htmlOutputVector.elementAt(j)).end < end)) + j++; + // localising start: + while ((i>=0)&&(((MarkedArea)this.htmlOutputVector.elementAt(i)).begin > start)) + i--; + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("i: "+i+" j: "+j); + } + if ((j=jElement.begin) + { + iElement = (MarkedArea)this.htmlOutputVector.elementAt(0); + iPosition = iElement.position.position; + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("Less: "+jPosition+" and "+iPosition); + } + position = findMax(0,j); + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("SELECTEDTEXT: "+position+"\n"); + } + treeChanged = true; + send("mp "+position); + } + // before: + else + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("BEFORE vector of size: "+this.htmlOutputVector.size()); + } + } + // just: + else + { + iElement = (MarkedArea)this.htmlOutputVector.elementAt(i); + iPosition = iElement.position.position; + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("SELECTED TEXT Just: "+iPosition +" and "+jPosition+"\n"); + } + position = findMax(i,j); + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("SELECTEDTEXT: "+position+"\n"); + } + treeChanged = true; + send("mp "+position); + } + } + else + // more && after: + if (i>=0) + { + iElement = (MarkedArea)this.htmlOutputVector.elementAt(i); + iPosition = iElement.position.position; + // more + if (start<=iElement.end) + { + jElement = (MarkedArea)this.htmlOutputVector.elementAt(this.htmlOutputVector.size()-1); + jPosition = jElement.position.position; + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("MORE: "+iPosition+ " and "+jPosition); + } + position = findMax(i,this.htmlOutputVector.size()-1); + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("SELECTEDTEXT: "+position+"\n"); + } + treeChanged = true; + send("mp "+position); + } + else + // after: + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("AFTER vector of size: "+this.htmlOutputVector.size()); + } + } + else + // bigger: + { + iElement = (MarkedArea)this.htmlOutputVector.elementAt(0); + iPosition = iElement.position.position; + jElement = (MarkedArea)this.htmlOutputVector.elementAt(this.htmlOutputVector.size()-1); + jPosition = jElement.position.position; + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("BIGGER: "+iPosition +" and "+jPosition+"\n" + + "\n-> SELECTEDTEXT: []\n"); + } + treeChanged = true; + send("mp []"); + } + }//not null selection + } + + /** + * Appends the string s to the text in the linearization area + * on the screen. 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. + */ + protected String appendMarked(String restString, final boolean clickable, boolean doDisplay) { + 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 <subtree */ + int subtreeBegin; + /** position of </subtree */ + int subtreeEnd; + + if (clickable && doDisplay) { + subtreeBegin = Utils.indexOfNotEscaped(restString, "-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-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 (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("SOMETHING BEFORE THE TAG"); + } + if (this.currentPosition.size()>0) + newLength = register(currentLength, subtreeBegin, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString); + else + newLength = register(currentLength, subtreeBegin, new LinPosition("[]", + restString.substring(subtreeBegin,subtreeTagEnd).indexOf("incorrect")==-1), restString); + } else { // nothing before the tag: + //the case in the beginning + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("NOTHING BEFORE THE TAG"); + } + if (nextOpeningTagBegin>0) { + newLength = register(subtreeTagEnd+2, nextOpeningTagBegin, position, restString); + } else { + newLength = register(subtreeTagEnd+2, restString.length(), position, restString); + } + restString = removeSubTreeTag(restString,subtreeBegin, subtreeTagEnd+1); + } + currentLength += newLength ; + } else {// l tag: + if (subtreeEnd-currentLength>1) { + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("SOMETHING BEFORE THE TAG"); + } + if (this.currentPosition.size()>0) + newLength = register(currentLength, subtreeEnd, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString); + else + newLength = register(currentLength, subtreeEnd, new LinPosition("[]", + restString.substring(subtreeBegin,subtreeEnd).indexOf("incorrect")==-1), restString); + currentLength += newLength ; + } + // nothing before the tag: + else + // punctuation after the tag: + if (restString.substring(subtreeEnd+10,subtreeEnd+11).trim().length()>0) + { + if (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("PUNCTUATION AFTER THE 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 (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("STRING after cutting the 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 (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("currentLength: " + currentLength); + } + // register the punctuation: + if (this.currentPosition.size()>0) { + newLength = register(currentLength, currentLength+2, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString); + } else { + newLength = register(currentLength, currentLength+2, new LinPosition("[]", + true), restString); + } + currentLength += newLength ; + } else { + // just cutting the tag: + restString = removeSubTreeTag(restString,subtreeEnd, subtreeEnd+10); + } + } + subtreeEnd = Utils.indexOfNotEscaped(restString, ""); + 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, ""); + } + r = Utils.indexOfNotEscaped(restString, "-1) { + int t = Utils.indexOfNotEscaped(restString, ">", r); + if (t"; + 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; + } + + + + /** + * Finding position of the searchString not starting with escape symbol (\\) + * in the string s from position. + * @param s the String that is to be checked. + * @param searchString + * @param position + * @return the position of the first such a char after position + */ + private int getCharacter(String s, String searchString, int position) { + int t = s.indexOf(searchString, position); + int i = t-1; + int k = 0; + while ((i>-1)&&(s.charAt(i)=='\\')) { + k++; + i--; + } + if (k % 2 == 0) { + return t; + } else { + return getCharacter(s, searchString, t+1); + } + } + + /** + * The substring from start to end in workingString, together with + * position is saved as a MarkedArea in this.htmlOutputVector. + * 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 + * @return newLength, the difference between end and start + */ + private int register(int start, int end, LinPosition position, String workingString) { + /** + * 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 HtmlMarkedArea hma = this.display.addAsMarked(toAdd, position); + this.htmlOutputVector.add(hma); + if (htmlLogger.isDebugEnabled()) { + htmlLogger.debug("HTML added : " + hma); + } //} else if (linMarkingLogger.isDebugEnabled()) { + // linMarkingLogger.debug("whiteSpaces: " + newLength); + //} + } //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 (linMarkingLogger.isDebugEnabled()) { + linMarkingLogger.debug("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; + } + + /** + * 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. + */ + protected void listAction(JList list, int index, boolean doubleClick) { + if (index == -1) { + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("no selection"); + } else { + GFCommand command; + if (list == refinementList) { + command = (GFCommand)listModel.elementAt(index); + } else { + Vector cmdvector = (Vector)this.subcatListModelHashtable.get(this.whichSubcat); + command = (GFCommand)(cmdvector.get(index)); + } + if (command instanceof LinkCommand) { + 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; + executeInputCommand(ic); + + } else if (doubleClick){ + refinementSubcatListModel.clear(); + treeChanged = true; + send(command.getCommand()); + } else if (list == refinementList){ + refinementSubcatListModel.clear(); + } + } + } + + /** + * Pops up a window for input of the wanted data and asks ic + * afterwards, if the data has the right format. + * Then gives that to GF + * @param ic the InputCommand that specifies the wanted format/type + */ + private void executeInputCommand(InputCommand ic) { + String s = (String)JOptionPane.showInputDialog( + this, + ic.getTitleText(), + ic.getTitleText(), + JOptionPane.QUESTION_MESSAGE, + null, + null, + ""); + StringBuffer reason = new StringBuffer(); + Object value = ic.validate(s, reason); + if (value != null) { + treeChanged = true; + send("g "+value); + if (logger.isDebugEnabled()) { + logger.debug("sending string " + value); + } + } else { + this.display.addToStages("\n" + reason.toString(), "

" + reason.toString() + "

"); + display(false, false); + } + } + + + /** + * Produces the popup menu that represents the current refinements. + * An alternative to the refinement list. + * @return s.a. + */ + 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(font); + 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(font); + tempMenu.setActionCommand(gfcmd.getCommand()); + tempMenu.setToolTipText(gfcmd.getTooltipText()); + tempMenu.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent ae) { + JMenuItem mi = (JMenuItem)ae.getSource(); + refinementSubcatListModel.clear(); + treeChanged = true; + String command = mi.getActionCommand(); + send(command); + } + }); + } else if (gfcmd instanceof InputCommand) { + tempMenu = new JMenuItem(gfcmd.getDisplayText()); + tempMenu.setFont(font); + 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) { + executeInputCommand(ic); + } + } + }); + + } + return tempMenu; + } + + public void focusGained(FocusEvent e) { + //do nothing + } + public void focusLost(FocusEvent e) { + getLayeredPane().remove(parseField); + repaint(); + } + + /** + * + */ + private void resetNewCategoryMenu() { + //remove everything except "New" + while (1< newCategoryMenu.getItemCount()) + newCategoryMenu.removeItemAt(1); + } + + /** + * pop-up menu (adapted from DynamicTree2): + * @author janna + * + */ + class PopupListener extends MouseAdapter { + public void mousePressed(MouseEvent e) { + // int selStart = tree.getRowForLocation(e.getX(), e.getY()); + // output.setSelectionRow(selStart); + if (popUpLogger.isDebugEnabled()) { + popUpLogger.debug("mouse pressed2: "+linearizationArea.getSelectionStart()+" "+linearizationArea.getSelectionEnd()); + } + maybeShowPopup(e); + } + + public void mouseReleased(MouseEvent e) { + //nothing to be done here + } + protected void maybeShowPopup(MouseEvent e) { + //int i=outputVector.size()-1; + // right click: + if (e.isPopupTrigger()) { + if (popUpLogger.isDebugEnabled()) { + popUpLogger.debug("changing pop-up menu2!"); + } + popup2 = producePopup(); + popup2.show(e.getComponent(), e.getX(), e.getY()); + } + // middle click + //TODO strange code here, that doesn't work + if (e.getButton() == MouseEvent.BUTTON2) + { + // selection Exists: + if (!selectedText.equals("")) + { + if (popUpLogger.isDebugEnabled()) { + popUpLogger.debug(e.getX() + " " + e.getY()); + } + if (selectedText.length()<5) + if (treeCbMenuItem.isSelected()) + parseField.setBounds(e.getX()+(int)Math.round(tree.getBounds().getWidth()), e.getY()+80, 400, 40); + else + parseField.setBounds(e.getX(), e.getY()+80, 400, 40); + else + if (treeCbMenuItem.isSelected()) + parseField.setBounds(e.getX()+(int)Math.round(tree.getBounds().getWidth()), e.getY()+80, selectedText.length()*20, 40); + else + parseField.setBounds(e.getX(), e.getY()+80, selectedText.length()*20, 40); + getLayeredPane().add(parseField, new Integer(1), 0); + parseField.setText(selectedText); + parseField.requestFocusInWindow(); + } + } + } + + } + + /** + * Encapsulates the opening of terms or linearizations to a file. + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class OpenAction extends AbstractAction { + public OpenAction() { + super("Open", null); + putValue(SHORT_DESCRIPTION, "Opens abstract syntax trees or linearizations"); + putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_O)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_O, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + if (saveFc.getChoosableFileFilters().length<2) + saveFc.addChoosableFileFilter(new GrammarFilter()); + int returnVal = saveFc.showOpenDialog(GFEditor2.this); + if (returnVal == JFileChooser.APPROVE_OPTION) { + + /* "sending" should be fixed on the GF side: + rbMenuItemLong.setSelected(true); + send("ms long"); + rbMenuItemUnTyped.setSelected(true); + send("mt untyped"); + selectedMenuLanguage = "Abstract"; + rbMenuItemAbs.setSelected(true); + send("ml Abs"); + */ + + treeChanged = true; + newObject = true; + + resetNewCategoryMenu(); + langMenuModel.resetLanguages(); + + File file = saveFc.getSelectedFile(); + // opening the file for editing : + if (logger.isDebugEnabled()) logger.debug("opening: "+ file.getPath().replace('\\', File.separatorChar)); + if (saveTypeGroup.getSelection().getActionCommand().equals("term")) { + if (logger.isDebugEnabled()) logger.debug(" opening as a term "); + send("open "+ file.getPath().replace('\\', File.separatorChar)); + } + else { + if (logger.isDebugEnabled()) logger.debug(" opening as a linearization "); + send("openstring "+ file.getPath().replace('\\', File.separatorChar)); + } + + fileString =""; + grammar.setText("No Topic "); + } + } + } + + /** + * Encapsulates the saving of terms or linearizations to a file. + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class SaveAction extends AbstractAction { + public SaveAction() { + super("Save As", null); + putValue(SHORT_DESCRIPTION, "Saves either the current linearizations or the AST"); + putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_S)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_S, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + if (saveFc.getChoosableFileFilters().length<2) + saveFc.addChoosableFileFilter(new GrammarFilter()); + int returnVal = saveFc.showSaveDialog(GFEditor2.this); + if (returnVal == JFileChooser.APPROVE_OPTION) { + File file = saveFc.getSelectedFile(); + if (logger.isDebugEnabled()) logger.debug("saving as " + file); + final String abstractLin = linearizations.get("Abstract").toString(); + + if (saveTypeGroup.getSelection().getActionCommand().equals("term")) { + // saving as a term + writeOutput(abstractLin, file.getPath()); + } else { + // saving as a linearization: + /** collects the show linearizations */ + StringBuffer text = new StringBuffer(); + /** if sth. at all is shown already*/ + boolean sthAtAll = false; + for (Iterator it = linearizations.keySet().iterator(); it.hasNext();) { + Object key = it.next(); + if (!key.equals("Abstract")) { + if (sthAtAll) { + text.append("\n\n"); + } + text.append(linearizations.get(key)); + sthAtAll = true; + } + } + if (sthAtAll) { + writeOutput(text.toString(), file.getPath()); + if (logger.isDebugEnabled()) logger.debug(file + " saved."); + } else { + if (logger.isDebugEnabled()) logger.warn("no concrete language shown, saving abstract"); + writeOutput(abstractLin, file.getPath()); + if (logger.isDebugEnabled()) logger.debug(file + " saved."); + } + } + } + + } + } + + /** + * Encapsulates adding new languages for the current abstract grammar. + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class ImportAction extends AbstractAction { + public ImportAction() { + super("Add", null); + putValue(SHORT_DESCRIPTION, "add another concrete language for the current abstract grammar"); + putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_A)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_A, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + //add another language (Add...) + if (fc.getChoosableFileFilters().length<2) + fc.addChoosableFileFilter(new GrammarFilter()); + int returnVal = fc.showOpenDialog(GFEditor2.this); + if (returnVal == JFileChooser.APPROVE_OPTION) { + File file = fc.getSelectedFile(); + + resetNewCategoryMenu(); + langMenuModel.resetLanguages(); + // importing a new language : + if (logger.isDebugEnabled()) logger.debug("importing: "+ file.getPath().replace('\\','/')); + fileString =""; + send("i "+ file.getPath().replace('\\',File.separatorChar), false); + readGfinit(); + readAndDisplay(); + } + } + + } + + /** + * Encapsulates starting over with a new grammar. + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class NewTopicAction extends AbstractAction { + public NewTopicAction() { + super("New Topic", null); + putValue(SHORT_DESCRIPTION, "dismiss current editing and load a new grammar"); + putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_T)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_T, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + if (fc.getChoosableFileFilters().length<2) + fc.addChoosableFileFilter(new GrammarFilter()); + int returnVal = fc.showOpenDialog(GFEditor2.this); + if (returnVal == JFileChooser.APPROVE_OPTION) { + int n = JOptionPane.showConfirmDialog(GFEditor2.this, + "This will dismiss the previous editing. Would you like to continue?", + "Starting a new topic", JOptionPane.YES_NO_OPTION); + if (n == JOptionPane.YES_OPTION){ + File file = fc.getSelectedFile(); + // importing a new grammar : + newObject = false; + statusLabel.setText(status); + listModel.clear(); + resetTree(tree); + resetNewCategoryMenu(); + langMenuModel.resetLanguages(); + selectedMenuLanguage = "Abstract"; + rbMenuItemLong.setSelected(true); + rbMenuItemUnTyped.setSelected(true); + + fileString=""; + grammar.setText("No Topic "); + display = new Display(displayType); + display(true, false); + send(" e "+ file.getPath().replace('\\',File.separatorChar), false); + readInit(null, false); + readAndDisplay(); + resetPrintnames(true); + } + } + } + + } + + /** + * Encapsulates starting over without loading new grammars + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class ResetAction extends AbstractAction { + public ResetAction() { + super("Reset", null); + putValue(SHORT_DESCRIPTION, "discard everything including the loaded grammars"); + putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_R)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_R, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + newObject = false; + statusLabel.setText(status); + listModel.clear(); + resetTree(tree); + langMenuModel.resetLanguages(); + resetNewCategoryMenu(); + selectedMenuLanguage = "Abstract"; + + rbMenuItemLong.setSelected(true); + rbMenuItemUnTyped.setSelected(true); + + fileString=""; + grammar.setText("No Topic "); + send("e", false); + readGfinit(); + } + + } + + /** + * Encapsulates exiting the program + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class QuitAction extends AbstractAction { + public QuitAction() { + super("Quit", null); + putValue(SHORT_DESCRIPTION, "exit the editor"); + putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_Q)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_Q, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + endProgram(); + } + + } + + /** + * Encapsulates the random command for GF + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class RandomAction extends AbstractAction { + public RandomAction() { + super("Random", null); + putValue(SHORT_DESCRIPTION, "build a random AST from the current cursor position"); + //putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_M)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_M, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + treeChanged = true; + send("a"); + } + + } + + /** + * Encapsulates the undo command for GF + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class UndoAction extends AbstractAction { + public UndoAction() { + super("Undo", null); + putValue(SHORT_DESCRIPTION, "undo the last command"); + //putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_U)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_U, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + treeChanged = true; + send("u"); + } + } + + /** + * Encapsulates alpha command for GF + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class AlphaAction extends AbstractAction { + public AlphaAction() { + super("Alpha", null); + putValue(SHORT_DESCRIPTION, "Performing alpha-conversion, rename bound variables"); + //putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_P)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_P, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + String s = JOptionPane.showInputDialog("Type string:", alphaInput); + if (s!=null) { + alphaInput = s; + treeChanged = true; + send("x "+s); + } + } + + } + + /** + * Encapsulates the input dialog and sending of arbitrary commands to GF + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class GfCommandAction extends AbstractAction { + public GfCommandAction() { + super("GF command", null); + putValue(SHORT_DESCRIPTION, "send a command to GF"); + //putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_G)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_G, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + String s = JOptionPane.showInputDialog("Command:", commandInput); + if (s!=null) { + commandInput = s; + //s = "gf "+s; This is for debugging, otherwise shift the comment to the next line. + treeChanged = true; + if (logger.isDebugEnabled()) logger.debug("sending: "+ s); + send(s); + } } + + } + + /** + * Encapsulates the showing of the read dialog + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class ReadAction extends AbstractAction { + public ReadAction() { + super("Read", null); + putValue(SHORT_DESCRIPTION, "Refining with term or linearization from typed string or file"); + //putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_E)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_E, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + readDialog.show(); + } + + } + + /** + * Encapsulates the splitting of the main window + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class SplitAction extends AbstractAction { + public SplitAction() { + super("Split Windows", null); + putValue(SHORT_DESCRIPTION, "Splits the refinement menu into its own window"); + putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_L)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_L, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + coverPanel.remove(centerPanel); + centerPanel2.add(middlePanelUp, BorderLayout.SOUTH); + if (((JCheckBoxMenuItem)viewMenu.getItem(0)).isSelected()) { + centerPanel2.add(treePanel, BorderLayout.CENTER); + } + else { + centerPanel2.add(outputPanelUp, BorderLayout.CENTER); + } + coverPanel.add(centerPanel2, BorderLayout.CENTER); + gui2.getContentPane().add(refinementListsContainer); + gui2.setVisible(true); + pack(); + repaint(); + } + + } + + /** + * Encapsulates the combining of the main window + * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever. + * @author daniels + */ + class CombineAction extends AbstractAction { + public CombineAction() { + super("One Window", null); + putValue(SHORT_DESCRIPTION, "Refinement menu and linearization areas in one window"); + putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_W)); + putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_W, ActionEvent.CTRL_MASK)); + } + + public void actionPerformed(ActionEvent e) { + coverPanel.remove(centerPanel2); + middlePanel.add(middlePanelUp, BorderLayout.NORTH); + if (((JCheckBoxMenuItem)viewMenu.getItem(0)).isSelected()) { gui2.setVisible(false); + centerPanel.setLeftComponent(treePanel); + } + else { + centerPanel.setLeftComponent(outputPanelUp); + gui2.setVisible(false); + } + coverPanel.add(centerPanel, BorderLayout.CENTER); + centerPanelDown.add(refinementListsContainer, BorderLayout.CENTER); + centerPanelDown.add(refinementSubcatPanel, BorderLayout.EAST); + pack(); + repaint(); + } + + } + + + /** + * Takes care, which classes are present and which states they have. + * @author daniels + */ + class LangMenuModel { + Logger menuLogger = Logger.getLogger("de.uka.ilkd.key.ocl.gf.GFEditor2.MenuModel"); + /** + * Just a mutable tuple of language name and whether this language + * is displayed or not. + */ + class LangActiveTuple { + String lang; + boolean active; + public LangActiveTuple(String lang, boolean active) { + this.lang = lang; + this.active = active; + } + public String toString() { + return lang + " : " + active; + } + } + + private Vector languages = new Vector(); + /** the group containing RadioButtons for the language the menus + * should have + */ + private ButtonGroup languageGroup = new ButtonGroup(); + + void updateMenus() { + for (Iterator it = this.languages.iterator(); it.hasNext(); ) { + LangActiveTuple lat = (LangActiveTuple)it.next(); + boolean alreadyPresent = false; + // language already in the list of available languages? + for (int i=0; i "); + String boundPart = myFun.substring(2, end); + String[] bounds = boundPart.split("\\)\\s*\\,\\s*\\("); + this.boundNames = new String[bounds.length]; + this.boundTypes = new String[bounds.length]; + for (int i = 0; i < bounds.length;i++) { + //System.out.print("+" + bounds[i] + "-"); + int colon = bounds[i].indexOf(" : "); + this.boundNames[i] = bounds[i].substring(0, colon); + this.boundTypes[i] = bounds[i].substring(colon + 3); + //System.out.println(boundNames[i] + " ;; " + boundTypes[i]); + } + myFun = myFun.substring(end + 5); + } else { + this.boundNames = new String[0]; + this.boundTypes = new String[0]; + } + this.fun = myFun; + } + + 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() + "'"); + } + + } + } +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GrammarFilter.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GrammarFilter.java new file mode 100644 index 000000000..b40bc8d9c --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GrammarFilter.java @@ -0,0 +1,40 @@ +// 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 java.io.File; +import javax.swing.filechooser.*; + +public class GrammarFilter extends FileFilter { + + // Accept all directories and all gf, gfm files. + public boolean accept(File f) { + if (f.isDirectory()) { + return true; + } + + String extension = Utils.getExtension(f); + if (extension != null) { + if (extension.equals(Utils.gf) || + extension.equals(Utils.gfm)) { + return true; + } else { + return false; + } + } + + return false; + } + + // The description of this filter + public String getDescription() { + return "Just Grammars (*.gf, *.gfm)"; + } +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/HtmlMarkedArea.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/HtmlMarkedArea.java new file mode 100644 index 000000000..9d6454906 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/HtmlMarkedArea.java @@ -0,0 +1,47 @@ +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 + */ + public HtmlMarkedArea(int b, int e, LinPosition p, String w, int hb, int he) { + super(b, e, p, w); + 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); + this.htmlBegin = hb; + this.htmlEnd = he; + } + + public String toString() { + return begin + " - " + end + " : " + position + " = '" + words + "' ; HTML: " + htmlBegin + " - " + htmlEnd; + } +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/InputCommand.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/InputCommand.java new file mode 100644 index 000000000..93a965b2d --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/InputCommand.java @@ -0,0 +1,104 @@ +package de.uka.ilkd.key.ocl.gf; + +import org.apache.log4j.Logger; + +/** + * @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. + * Reason: No GUI stuff in the command. + */ +class InputCommand extends GFCommand { + protected final static Logger logger = Logger.getLogger(Printname.class.getName()); + public static InputCommand intInputCommand = new InputCommand("read in Integer", + "opens a dialog window in which an Integer can be entered", + int.class, + "Please enter an Integer"); + public static InputCommand stringInputCommand = new InputCommand("read in String", + "opens a dialog window in which a String can be entered", + String.class, + "Please enter a String"); + + protected InputCommand(final String description, final String ttt, Class type, final String title) { + this.type = type; + this.tooltipText = ttt; + this.displayText = description; + this.titleText = title; + this.command = type.getName(); + } + + protected Class type; + + /**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 */ + public String getTitleText() { + return titleText; + } + + + /**the text that is to be displayed as the tooltip */ + protected final String tooltipText; + /**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 */ + protected final String displayText; + /** the text that is to be displayed in the refinement lists */ + public String getDisplayText() { + return displayText; + } + /** 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) + * @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 + * give an empty one. + * @return an Object whose toString() should send the right + * thing to GF. + * Maybe null, if this "conversion" failed. + */ + protected Object validate(String o, StringBuffer reason) { + Object result = null; + if (type == int.class) { + int i; + try { + i = Integer.parseInt(o); + result = new Integer(i); + } catch (NumberFormatException e) { + reason.append("Input format error: '" + o + "' is no Integer"); + } + } else if (type == String.class) { + if (o != null) { + result = "\"" + o.toString() + "\""; + } + } + return result; + } + + /** + * selects the suiting InputCommand for the given full name of a type + * @param typeName at the moment, either int.class.getName() or String.class.getName() + * @return intInputCommand for int, stringInputCommand for String or null otherwise + */ + protected static InputCommand forTypeName(String typeName) { + InputCommand ic = null; + if (typeName.equals(int.class.getName())) { + ic = InputCommand.intInputCommand; + } else if (typeName.equals(String.class.getName())) { + ic = InputCommand.stringInputCommand; + } + return ic; + } + +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinPosition.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinPosition.java new file mode 100644 index 000000000..eff344e75 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinPosition.java @@ -0,0 +1,34 @@ +package de.uka.ilkd.key.ocl.gf; + +/** + * represents a position in the AST in Haskell notation together + * with a flag that indicates whether at least one constraint does not hold or + * if all hold (correct/incorrect). + * Class is immutable. + */ +public class LinPosition { + /** + * a position in the AST in Haskell notation + */ + final public String position; + + /** + * true means green, false means red (janna guesses) + */ + final public boolean correctPosition; + + /** + * creates a LinPosition + * @param p the position in the AST in Haskell notation like [0,1,2] + * @param cor false iff there are violated constraints + */ + LinPosition(String p, boolean cor) { + position = p; + correctPosition = cor; + } + + public String toString() { + return position + (correctPosition ? " correct" : " incorrect"); + } +} + diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinkCommand.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinkCommand.java new file mode 100644 index 000000000..5575defa7 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinkCommand.java @@ -0,0 +1,55 @@ +/* + * Created on 21.04.2005 + */ +package de.uka.ilkd.key.ocl.gf; + +/** + * @author daniels + * This class represents a link to a subcategory submenu. + * When it is encountered as the executed command, the corresponding + * menu gets opened. + */ +public class LinkCommand extends GFCommand { + + public LinkCommand(final String subcat, final PrintnameManager manager) { + this.command = subcat; + this.newSubcat = false; + this.commandType = Printname.SUBCAT; + this.argument = -1; + this.funName = null; + this.printname = null; + + String dtext; + String ttext; + String fullname = manager.getFullname(subcat); + if (fullname == null) { + dtext = getSubcat(); + ttext = "open submenu " + getSubcat(); + } else { + ttext = Printname.htmlPrepend(Printname.extractTooltipText(fullname), "open submenu
"); + dtext = Printname.extractDisplayText(fullname); + } + this.tooltipText = ttext; + this.displayText = dtext; + + } + + /**the text that is to be displayed as the tooltip */ + protected final String tooltipText; + /**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 */ + protected final String displayText; + /** the text that is to be displayed in the refinement lists */ + public String getDisplayText() { + return displayText; + } + /** the subcategory of this command */ + public String getSubcat() { + return this.command; + } + +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/MarkedArea.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/MarkedArea.java new file mode 100644 index 000000000..1a4dfc687 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/MarkedArea.java @@ -0,0 +1,40 @@ +package de.uka.ilkd.key.ocl.gf; + +/** + * Stores quasi a piece of the linearization area, that has a word, a beginning + * and an end in the linearization area and a position in the AST. It is used + * for clicking in the text + * + * @author janna + */ +class MarkedArea { + /** The starting position of the stored words */ + final public int begin; + /** The ending position of the stored words. + * Not final because of some punctuation issue daniels + * does not understand + */ + public int end; + /** The position in the AST */ + final public LinPosition position; + /** The actual text of this area */ + final public String words; + /** + * 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 + */ + MarkedArea(int b, int e, LinPosition p, String w) { + begin = b; + end = e; + position = p; + words = w; + } + + public String toString() { + return begin + " - " + end + " : " + position + " = '" + words + "'"; + } +} + diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java new file mode 100644 index 000000000..fbaadb435 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java @@ -0,0 +1,458 @@ +package de.uka.ilkd.key.ocl.gf; + +import java.util.Hashtable; +import java.util.Vector; + +import org.apache.log4j.Logger; + +/** + * @author daniels + * + * A Printname allows easy access for all the information that is crammed + * into a printname in the GF grammars. + * This information consists of (in this order!) + * The tooltip text which is started with $ + * The subcategory which is started with % + * The longer explanation for the subcategory which directly follows the + * subcategory and is put into parantheses + * The parameter descriptions, which start with #name and is followed + * by their actual description. + * HTML can be used inside the descriptions and the tooltip text + */ +class Printname { + protected 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\\$adds the current subtree to the clipboard.
It is offered in the refinement menu if the expected type fits to the one of the current sub-tree."); + public static final Printname printhistory = new Printname("ph", "print history\\$prints all previous command in the linearization area"); + + /** + * The character that is the borderline between the text that + * is to be displayed in the JList and the ToolTip text + */ + public final static String TT_START = "\\$"; + /** + * the string that is followed by the sub-category shorthand + * in the refinement menu + */ + public final static String SUBCAT = "\\%"; + /** + * The string that is followed by a new parameter to the GF function + */ + public final static String PARAM = "\\#"; + + + /** the name of the fun that is used in this command */ + protected final String fun; + + /** the printname of this function */ + protected final String printname; + + /** 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, + * "" means that a GF command is represented + */ + protected final String module; + /** + * the name of the module the fun belongs to + * null means that the function is saved without module information, + * "" means that a GF command is represented + */ + public String getModule() { + return module; + } + + + /** the qualified function name, not needed yet */ + /* + public String getFunQualified() { + if (module != null && !module.equals("")) { + return module + "." + fun; + } else { + return fun; + } + } + */ + + /** the subcategory of this command */ + protected final String subcat; + /** the subcategory of this command */ + public String getSubcat() { + return subcat; + } + + /** + * The hashmap for the names of the sub categories, + * with the shortname starting with '%' as the key. + * It is important that all Printnames of one session share the same + * instance of Hashtable here. + * This field is not static because there can be several instances of + * the editor that shouldn't interfere. + */ + protected final Hashtable subcatNameHashtable; + + /** + * contains the names of the paramters of this function (String). + * Parallel with paramTexts + */ + protected final Vector paramNames = new Vector(); + + /** + * fetches the name of the nth parameter + * @param n the number of the wanted paramter + * @return the corresponding name, null if not found + */ + public String getParamName(int n) { + String name = null; + try { + name = (String)this.paramNames.get(n); + } catch (ArrayIndexOutOfBoundsException e) { + subcatLogger.warn(e.getLocalizedMessage()); + } + return name; + } + /** + * contains the descriptions of the paramters of this function (String). + * Parallel with paramNames + */ + protected final Vector paramTexts = new Vector(); + + + /** + * Creates a Printname for a normal GF function + * @param myFun the function name + * @param myPrintname the printname given for this function + * @param myFullnames the Hashtable for the full names for the category + * names for the shortnames like %PREDEF + */ + public Printname(String myFun, String myPrintname, Hashtable myFullnames) { + myFun = myFun.trim(); + myPrintname = myPrintname.trim(); + this.printname = myPrintname; + this.subcatNameHashtable = myFullnames; + + //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; + } + } + + //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(); + } else { + description = ""; + } + this.paramNames.addElement(name); + this.paramTexts.addElement(description); + } + 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.isDebugEnabled()) { + subcatLogger.debug("new fullname '" + fullName + "' for category (shortname) '" + this.subcat + "'"); + } + } else { + subcat = subcatPart.trim(); + } + + } else { + this.subcat = null; + } + } + } + + /** + * a constructor for GF command that don't represent functions, + * like d, ph, ac + * @param command the GF command + * @param explanation an explanatory text what this command does + */ + protected Printname(String command, String explanation) { + this.fun = command; + this.subcatNameHashtable = null; + this.subcat = null; + this.module = ""; + this.printname = explanation; + } + + /** + * Special constructor for bound variables. + * These printnames don't get saved since they don't always exist and + * also consist of quite few information. + * @param bound The name of the bound variable + */ + public Printname(String bound) { + this.fun = bound; + this.subcatNameHashtable = null; + this.subcat = null; + this.module = null; + this.printname = bound + "$insert the bound variable" + bound; + } + + /** the text that is to be displayed in the refinement lists */ + public String getDisplayText() { + String result; + result = extractDisplayText(this.printname); + return result; + } + + /** + * the text that is to be displayed as the tooltip. + * Will always be enclosed in <html> </html> tags. + */ + public String getTooltipText() { + if (this.displayedPrintname != null) { + return this.displayedPrintname; + } else { + String result; + result = extractTooltipText(this.printname); + if (this.paramNames.size() > 0) { + String params = htmlifyParams(); + //will result in wrapping + result = htmlAppend(result, params); + } else { + //wrap in by force + result = htmlAppend(result, ""); + } + this.displayedPrintname = result; + return result; + } + } + + /** + * extracts the part of the body of the printname that is the tooltip + * @param myPrintname the body of the printname + * @return the tooltip + */ + public static String extractTooltipText(String myPrintname) { + //if the description part of the fun has no \$ to denote a tooltip, + //but the subcat description has one, than we must take extra + //caution + final int indTT = Utils.indexOfNotEscaped(myPrintname, TT_START); + final int indSC = Utils.indexOfNotEscaped(myPrintname, SUBCAT); + int ind; + if ((indSC > -1) && (indSC < indTT)) { + ind = -1; + } else { + ind = indTT; + } + String result; + if (ind > -1) { + result = myPrintname.substring(ind + TT_START.length()); + } else { + result = myPrintname; + } + ind = Utils.indexOfNotEscaped(result, SUBCAT); + if (ind > -1) { + result = result.substring(0, ind); + } + ind = Utils.indexOfNotEscaped(result, PARAM); + if (ind > -1) { + result = result.substring(0, ind); + } + return result; + } + + /** + * extracts the part of the body of the printname that is the + * text entry for the JList + * @param myPrintname the body of the printname + * @return the one-line description of this Printname's fun + */ + public static String extractDisplayText(String myPrintname) { + String result; + int ind = Utils.indexOfNotEscaped(myPrintname, TT_START); + if (ind > -1) { + result = myPrintname.substring(0, ind); + } else { + result = myPrintname; + } + ind = Utils.indexOfNotEscaped(result, SUBCAT); + if (ind > -1) { + result = result.substring(0, ind); + } + ind = Utils.indexOfNotEscaped(result, PARAM); + if (ind > -1) { + result = result.substring(0, ind); + } + + return result; + } + + /** + * Appends the given string insertion to original and + * returns the result. If original is already HTML, the appended + * text will get right before the </html> tag. + * If original is no HTML, it will be enclosed in <html> + * @param original The String that is to come before insertion + * @param insertion the String to be appended + * @return the aforementioned result. + */ + public static String htmlAppend(String original, String insertion) { + StringBuffer result = new StringBuffer(original); + int htmlindex = result.indexOf(""); + + if (htmlindex > -1) { + result.insert(htmlindex, insertion); + } else { + result.insert(0,"").append(insertion).append(""); + } + return result.toString(); + + } + + /** + * Prepends the given string insertion to original and + * returns the result. If original is already HTML, the appended + * text will get right after the <html> tag. + * If original is no HTML, it will be enclosed in <html> + * @param original The String that is to come after insertion + * @param insertion the String to be appended + * @return the aforementioned result. + */ + public static String htmlPrepend(String original, String insertion) { + StringBuffer result = new StringBuffer(original); + int htmlindex = result.indexOf(""); + + if (htmlindex > -1) { + result.insert(htmlindex, insertion); + } else { + result.insert(0,insertion).insert(0,"").append(""); + } + return result.toString(); + + } + + /** + * wraps a single parameter with explanatory text + * into <dt> and <dd> tags + * @param which the number of the parameter + * @return the resulting String, "" if the wanted parameter + * is not stored (illegal index) + */ + protected String htmlifyParam(int which) { + try { + String result = "
" + this.paramNames.get(which) + "
" + + "
" + this.paramTexts.get(which) + "
"; + return result; + } catch (ArrayIndexOutOfBoundsException e) { + subcatLogger.warn(e.getLocalizedMessage()); + return ""; + } + + } + + /** + * wraps a single parameter together with its explanatory text into + * a HTML definition list (<dl> tags). + * Also the result is wrapped in <html> tags. + * @param which the number of the parameter + * @return the resulting definition list, null if the param is not found. + */ + public String htmlifySingleParam(int which) { + String text = htmlifyParam(which); + if (text.equals("")) { + return null; + } + String result = "
" + text + "
"; + return result; + } + + /** + * wraps all parameters together with their explanatory text into + * a HTML definition list (<dl> tags). + * No <html> tags are wrapped around here, that is sth. the caller + * has to do! + * @return the resulting definition list, "" if which is larger than + * the amount of stored params + */ + public String htmlifyParams() { + if (this.paramNames.size() == 0) { + return ""; + } + StringBuffer result = new StringBuffer("

Parameters:

"); + for (int i = 0; i < this.paramNames.size(); i++) { + result.append(htmlifyParam(i)); + } + result.append("
"); + return result.toString(); + } + + /** + * a testing method that is not called from KeY. + * Probably things like this should be automated via JUnit ... + * @param args not used + */ + public static void main(String[] args) { + String SandS = "boolean 'and' for sentences$true iff both of the two given sentences is equivalent to true%BOOL#alpha the first of the two and-conjoined sentences#beta the second of the and-conjoined sentences"; + String FandS = "andS"; + Hashtable ht = new Hashtable(); + Printname pn = new Printname(FandS, SandS, ht); + System.out.println(pn); + for (int i = 0; i < pn.paramNames.size(); i++) { + System.out.println(pn.htmlifySingleParam(i)); + } + System.out.println(pn.getTooltipText()); + SandS = "boolean 'and' for sentences$true iff both of the two given sentences is equivalent to true%BOOL"; + FandS = "andS"; + pn = new Printname(FandS, SandS, ht); + System.out.println("*" + pn.getTooltipText()); + } + + public String toString() { + return getDisplayText() + " \n " + getTooltipText() + " (" + this.paramNames.size() + ")"; + } + +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameLoader.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameLoader.java new file mode 100644 index 000000000..ea12b185f --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameLoader.java @@ -0,0 +1,83 @@ +package de.uka.ilkd.key.ocl.gf; + +import java.io.BufferedReader; +import java.io.BufferedWriter; +import java.io.IOException; + +import org.apache.log4j.Logger; + +/** + * @author daniels + * + * TODO To change the template for this generated type comment go to + * Window - Preferences - Java - Code Style - Code Templates + */ +public class PrintnameLoader extends AbstractProber { + protected final PrintnameManager printnameManager; + protected static Logger nogger = Logger.getLogger(Printname.class.getName()); + /** + * @param fromGf The GF process + * @param toGf The GF process + * @param pm The PrintnameManager on which the read Printnames + * will be registered with their fun name. + */ + public PrintnameLoader(BufferedReader fromGf, BufferedWriter toGf, PrintnameManager pm) { + super(fromGf, toGf); + this.printnameManager = pm; + } + + /** + * Reads the tree child of the XML from beginning to end. + * Sets autocompleted to false, if the focus position is open. + */ + protected void readMessage() { + try { + String result = this.fromProc.readLine(); + if (nogger.isDebugEnabled()) { + nogger.debug("1 " + result); + } + //first read line is , but this one gets filtered out in the next line + while (result.indexOf("/message")==-1){ + result = result.trim(); + if (result.startsWith("printname fun ")) { + //unescape backslashes. Probably there are more + result = GFEditor2.unescapeTextFromGF(result); + this.printnameManager.addNewPrintnameLine(result); + } + + result = this.fromProc.readLine(); + if (nogger.isDebugEnabled()) { + nogger.debug("1 " + result); + } + } + if (nogger.isDebugEnabled()) { + nogger.debug("finished loading printnames"); + } + } catch(IOException e){ + System.err.println(e.getMessage()); + e.printStackTrace(); + } + + } + + /** + * asks GF to print a list of all available printnames and + * calls the registered PrintnameManager to register those. + * @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) { + //send("gf pg -lang=FromUMLTypesOCL -printer=printnames"); + //prints the printnames of the last loaded grammar, + //which can be another one than FromUMLTypesOCL + String sendString = "gf pg -printer=printnames"; + if (lang != null && !("".equals(lang))) { + sendString = sendString + " -lang=" + lang; + } + nogger.info("collecting printnames :" + sendString); + send(sendString); + readGfedit(); + } + + +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameManager.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameManager.java new file mode 100644 index 000000000..c231ce214 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameManager.java @@ -0,0 +1,139 @@ +package de.uka.ilkd.key.ocl.gf; +import java.util.Hashtable; + +import org.apache.log4j.Logger; + +/** + * @author daniels + * + * An object of this class manages a bunch of printlines which is comprised of + * storage and retrieval. Also giving the subcategory shortnames their long + * counterpart is done here. + */ +class PrintnameManager { + protected static Logger logger = Logger.getLogger(Printname.class.getName()); + + protected final static String frontMatter = "printname fun "; + + /** + * The hashmap for the names of the sub categories, + * with the shortname starting with '%' as the key. + * It is important that all Printnames of one session share the same + * instance of Hashtable here. + * This field is not static because there can be several instances of + * the editor that shouldn't interfere. + */ + protected final Hashtable subcatNames = new Hashtable(); + + /** contains all the Printnames with the fun names as keys */ + protected final Hashtable printnames = new Hashtable(); + + /** + * processes a line from the "gf pg -printer=printnames" command + * @param line the read line from GF + * Should look like + * printname fun neq = "<>," ++ ("parametrized" ++ ("disequality$to" ++ ("compare" ++ ("two" ++ ("instances" ++ ("on" ++ ("a" ++ ("specific" ++ "type%COMP")))))))) + * and needs to get like + * printname fun neq = "<>, parametrized disequality$to compare two instances on a specific type%COMP" + */ + public void addNewPrintnameLine(String line) { + line = removePluses(line); + + //remove "printname fun " (the frontMatter) + int index = line.indexOf(frontMatter); + line = line.substring(index + frontMatter.length()).trim(); + + //extract fun name + int endFun = line.indexOf(' '); + String fun = line.substring(0, endFun); + //extract printname + String printname = line.substring(line.indexOf('"') + 1, line.lastIndexOf('"')); + + addNewPrintname(fun, printname); + } + + /** + * The printname printer of pg spits out no String, but a wrapping of + * small Strings conjoined with ++ which includes lots of parantheses. + * @param line The GF line from pg -printer=printnames + * @return a String representing the actual printname without the clutter + */ + protected static String removePluses(String line) { + line = line.replaceAll("\"\\)*\\s*\\+\\+\\s*\\(*\""," "); + int index = line.lastIndexOf('"'); + line = line.substring(0, index + 1); + return line; + } + + + /** + * Constructs the actual printname and puts it into printnames + * @param myFun the GF abstract fun name + * @param myPrintname the printname given by GF + */ + protected void addNewPrintname(String myFun, String myPrintname) { + if (logger.isDebugEnabled()) { + logger.debug("addNewPrintname, myFun = '" + myFun + "' , myPrintname = '" + myPrintname + "'"); + } + Printname printname = new Printname(myFun, myPrintname, this.subcatNames); + if (logger.isDebugEnabled()) { + logger.debug("printname = '" + printname + "'"); + } + this.printnames.put(myFun, printname); + } + + /** + * looks for the Printname corresponding to the given fun. + * If the fun is qualified with a module and no Printname + * is found with module, another lookup without the module part + * is made. + * @param myFun the GF abstract fun name (with or without qualification) + * @return the corresponding Printname iff that one exists, null otherwise + */ + public Printname getPrintname(String myFun) { + Printname result = null; + if (this.printnames.containsKey(myFun)) { + result = (Printname)this.printnames.get(myFun); + } else { + int index = myFun.indexOf('.'); + if (index > -1) { + //a valid fun name must not be empty + String fun = myFun.substring(index + 1); + if (printnames.containsKey(fun)) { + result = (Printname)this.printnames.get(fun); + } + } + } + if (result == null) { + //?n indicates that myFun is a metavariable of GF, + // which does not occur in the refinement menu. + // if that is not wanted, don't call this method! + if (!myFun.startsWith("?")) { + logger.warn("no printname for '" + myFun + "', pretend that it is a bound variable"); + return new Printname(myFun); + } + } + return result; + } + + /** + * looks up the full name for the subcategory name shortname. + * This is the %SOMETHING from the printname. + * @param shortname The subcat name which should get expanded + * @return the corresponding full name, maybe null! + */ + public String getFullname(String shortname) { + String result = (String)this.subcatNames.get(shortname); + return result; + } + + public static void main(String[] args) { + String a = "printname fun stringLiteral = \"arbitrary\" ++ (\"String$click\" ++ (\"read\" ++ (\"and\" ++ (\"enter\" ++ (\"the\" ++ (\"String\" ++ (\"in\" ++ (\"the\" ++ (\"dialog\" ++ (\"TODO%STRING(String\" ++ \"operations)\"))))))))))"; + System.out.println(a); + System.out.println(removePluses(a)); + a = "printname fun count = \"count\" ++ (\"the\" ++ (\"occurances\" ++ (\"of\" ++ (\"an\" ++ (\"object\" ++ (\"in\" ++ (\"the\" ++ \"collection.\")))))))++ (\"%COLL\" ++ (\"#collElemType\" ++ (\"The\" ++ (\"official\" ++ (\"element\" ++ (\"type\" ++ (\"of\" ++ (\"coll.
That\" ++ (\"is,\" ++ (\"the\" ++ (\"parameter\" ++ (\"type\" ++ (\"of\" ++ \"coll\")))))))))))++ (\"#set\" ++ (\"The\" ++ (\"Set\" ++ (\"in\" ++ (\"which\" ++ (\"occurances\" ++ (\"of\" ++ (\"elem\" ++ (\"are\" ++ (\"to\" ++ (\"be\" ++ \"counted.\")))))))))) ++ (\"#elem\" ++ (\"The\" ++ (\"instance\" ++ (\"of\" ++ (\"which\" ++ (\"the\" ++ (\"occurances\" ++ (\"in\" ++ (\"coll\" ++ (\"are\" ++ \"counted.\")))))))))))))"; + System.out.println(a); + System.out.println(removePluses(a)); + } + +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ReadDialog.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ReadDialog.java new file mode 100644 index 000000000..0a76d8df9 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ReadDialog.java @@ -0,0 +1,193 @@ +/* + * Created on 13.05.2005 + * + * TODO To change the template for this generated file go to + * Window - Preferences - Java - Code Style - Code Templates + */ +package de.uka.ilkd.key.ocl.gf; + +import java.awt.BorderLayout; +import java.awt.Dimension; +import java.awt.Font; +import java.awt.GridLayout; +import java.awt.event.ActionEvent; +import java.awt.event.ActionListener; +import java.io.File; + +import javax.swing.ButtonGroup; +import javax.swing.JButton; +import javax.swing.JDialog; +import javax.swing.JFileChooser; +import javax.swing.JLabel; +import javax.swing.JPanel; +import javax.swing.JRadioButton; +import javax.swing.JTextField; + +import org.apache.log4j.Logger; + +/** + * Takes care of reading in Strings that are to be parsed and terms. + * @author daniels + * + */ +class ReadDialog implements ActionListener{ + /** XML parsing debug messages */ + protected static Logger xmlLogger = Logger.getLogger(GFEditor2.class.getName() + "_XML"); + /** The window to which this class belongs */ + protected final GFEditor2 owner; + /** is the main thing of this class */ + protected final JDialog readDialog; + /** main area of the Read dialog (content pane)*/ + private final JPanel inputPanel = new JPanel(); + /** OK, Cancel, Browse in the Read dialog */ + private final JPanel inputPanel2 = new JPanel(); + /** in the Read dialog the OK button */ + private final JButton ok = new JButton("OK"); + /** in the Read dialog the Cancel button */ + private final JButton cancel = new JButton("Cancel"); + /** in the Read dialog the Browse button */ + private final JButton browse = new JButton("Browse..."); + /** groups inputField and inputLabel */ + private final JPanel inputPanel3 = new JPanel(); + /** for 'Read' to get the input */ + private final JTextField inputField = new JTextField(); + /** "Read: " */ + private final JLabel inputLabel = new JLabel("Read: "); + /** the radio group in the Read dialog to select Term or String */ + private final ButtonGroup readGroup = new ButtonGroup(); + /** to select to input a Term in the Read dialog */ + private final JRadioButton termReadButton = new JRadioButton("Term"); + /** 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("./"); + /** + * if a user sends a custom command to GF, he might want to do this + * again with the same command. + * Therefore it is saved. + */ + private String parseInput = ""; + /** + * if the user enters a term, he perhaps wants to input the same text again. + * Therefore it is saved. + */ + private String termInput = ""; + + /** + * creates a modal dialog + * @param owner The parent for which this dialog shall be modal. + */ + protected ReadDialog(GFEditor2 owner) { + this.owner = owner; + readDialog= new JDialog(owner, "Input", true); + readDialog.setLocationRelativeTo(owner); + readDialog.getContentPane().add(inputPanel); + readDialog.setSize(480,135); + + termReadButton.setActionCommand("term"); + stringReadButton.setSelected(true); + stringReadButton.setActionCommand("lin"); + // Group the radio buttons. + readGroup.add(stringReadButton); + readGroup.add(termReadButton); + JPanel readButtonPanel = new JPanel(); + readButtonPanel.setLayout(new GridLayout(3,1)); + readButtonPanel.setPreferredSize(new Dimension(70, 70)); + readButtonPanel.add(new JLabel("Format:")); + readButtonPanel.add(stringReadButton); + readButtonPanel.add(termReadButton); + inputPanel.setLayout(new BorderLayout(10,10)); + inputPanel3.setLayout(new GridLayout(2,1,5,5)); + inputPanel3.add(inputLabel); + inputPanel3.add(inputField); + ok.addActionListener(this); + browse.addActionListener(this); + cancel.addActionListener(this); + inputField.setPreferredSize(new Dimension(300,23)); + inputPanel.add(inputPanel3, BorderLayout.CENTER); + inputPanel.add(new JLabel(" "), BorderLayout.WEST); + inputPanel.add(readButtonPanel, BorderLayout.EAST); + inputPanel.add(inputPanel2, BorderLayout.SOUTH); + inputPanel2.add(ok); + inputPanel2.add(cancel); + inputPanel2.add(browse); + } + + /** + * Shows this modal dialog. + * The previous input text will be there again. + * + */ + protected void show() { + if (stringReadButton.isSelected()) { + inputField.setText(this.parseInput); + } else { + inputField.setText(this.termInput); + } + this.readDialog.setVisible(true); + } + + /** + * Sets the font of all GUI elements to font + * @param font + */ + protected void setFont(Font font) { + ok.setFont(font); + cancel.setFont(font); + inputLabel.setFont(font); + browse.setFont(font); + termReadButton.setFont(font); + stringReadButton.setFont(font); + } + + /** + * the ActionListener method that does the user interaction + */ + public void actionPerformed(ActionEvent ae) { + Object obj = ae.getSource(); + + if ( obj == cancel ) { + readDialog.setVisible(false); + } + + if ( obj == browse ) { + if (fc.getChoosableFileFilters().length<2) + fc.addChoosableFileFilter(new GrammarFilter()); + int returnVal = fc.showOpenDialog(owner); + if (returnVal == JFileChooser.APPROVE_OPTION) { + File file = fc.getSelectedFile(); + inputField.setText(file.getPath().replace('\\','/')); + } + } + + if ( obj == ok ) { + owner.treeChanged = true; + if (termReadButton.isSelected()) { + termInput = inputField.getText(); + if (termInput.indexOf(File.separatorChar)==-1){ + owner.send("g "+termInput); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("sending term string"); + } + else { + owner.send("tfile "+termInput); + if (xmlLogger.isDebugEnabled()) { + xmlLogger.debug("sending file term: "+termInput); + } + } + } else { //String selected + parseInput = inputField.getText(); + if (parseInput.indexOf(File.separatorChar)==-1){ + owner.send("p "+parseInput); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("sending parse string: "+parseInput); + } + else { + owner.send("pfile "+parseInput); + if (xmlLogger.isDebugEnabled()) xmlLogger.debug("sending file parse string: "+parseInput); + } + } + readDialog.setVisible(false); + } + + } + +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RealCommand.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RealCommand.java new file mode 100644 index 000000000..cfe1a0cfe --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RealCommand.java @@ -0,0 +1,146 @@ +/* + * Created on 21.04.2005 + * + */ +package de.uka.ilkd.key.ocl.gf; + +import java.util.HashSet; +import java.util.HashMap; +import org.apache.log4j.Logger; + +/** + * @author daniels + * This class represents a command, that is sent to GF + */ +class RealCommand extends GFCommand { + + private final static HashMap fullnames = new HashMap(); + + protected final static Logger logger = Logger.getLogger(Printname.class.getName()); + + /** + * 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. + */ + public RealCommand(final String myCommand, HashSet processedSubcats, final PrintnameManager manager, final String myShowText, boolean mlAbstract) { + if (fullnames.isEmpty()) { + fullnames.put("w", "wrap"); + fullnames.put("ch", "change head"); + fullnames.put("rc", "refine from history:"); + } + if (logger.isDebugEnabled()) { + logger.debug("new RealCommand: " + myCommand); + } + 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); + } else { + this.commandType = this.command; + } + + //extract the argument position for wrapping commands and cut that part + if (this.commandType.equals("w")) { + int beforeNumber = this.command.lastIndexOf(' '); + int protoarg; + try { + String argumentAsString = this.command.substring(beforeNumber + 1); + protoarg = Integer.parseInt(argumentAsString); + } catch (Exception e) { + protoarg = -1; + } + this.argument = protoarg; + } else { + this.argument = -1; + } + + //extract the fun of the GF command + if (this.commandType.equals("w")) { + int beforePos = this.command.indexOf(' '); + int afterPos = this.command.lastIndexOf(' '); + if (beforePos > -1 && afterPos > beforePos) { + this.funName = this.command.substring(beforePos + 1, afterPos); + } else { + this.funName = null; + } + } else { + int beforePos = this.command.indexOf(' '); + if (beforePos > -1) { + this.funName = this.command.substring(beforePos + 1); + } else { + this.funName = null; + } + } + + //get corresponding Printname + if (this.commandType.equals("d")) { + 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
" + subtree); + } else if (mlAbstract) { + //create a new Printname + this.printname = new Printname(funName, myShowText, null); + } else { + this.printname = manager.getPrintname(funName); + } + if (this.getSubcat() != null) { + if (processedSubcats.contains(this.getSubcat())) { + newSubcat = false; + } else { + newSubcat = true; + processedSubcats.add(this.getSubcat()); + } + } else { + newSubcat = false; + } + } + + /** the text that is to be displayed in the refinement lists */ + public String getDisplayText() { + String result = ""; + if (fullnames.containsKey(this.commandType)) { + result = fullnames.get(this.commandType) + " '"; + } + result = result + this.printname.getDisplayText(); + if (fullnames.containsKey(this.commandType)) { + result = result + "'"; + } + if (this.commandType.equals("w")) { + String insertion = " as argument " + (this.argument + 1); + result = result + insertion; + } + return result; + } + + /**the text that is to be displayed as the tooltip */ + public String getTooltipText() { + String result; + result = this.printname.getTooltipText(); + if (this.commandType.equals("w")) { + String insertion = "
The selected sub-tree will be the " + (this.argument + 1) + ". argument of this refinement."; + result = Printname.htmlAppend(result, insertion); + } + return result; + } + + public String getSubcat() { + return this.printname.getSubcat(); + } + + protected final String showText; +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinedAstNodeData.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinedAstNodeData.java new file mode 100644 index 000000000..616ad87ec --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinedAstNodeData.java @@ -0,0 +1,58 @@ +/* + * Created on 27.04.2005 + */ +package de.uka.ilkd.key.ocl.gf; + +/** + * @author daniels + * An object of this class represents a line in the GF abstract syntax tree + * in the graphical form. Well, not really, but how this line appears there + * and what its tooltip is is stored here. + * RefinedAstNodeData has its tooltip from the function it represents, not + * from its parent node. + */ +class RefinedAstNodeData implements AstNodeData { + + protected final Printname printname; + protected final GfAstNode node; + + /** + * all we have to know about an already refined node is its Printname + * and the GF line representing it + * @param pname the suiting Printname, may be null if the line could + * not be parsed + * @param node the GfAstNode for the current line + */ + public RefinedAstNodeData(Printname pname, GfAstNode node) { + this.printname = pname; + this.node = node; + } + + /** + * @return the printname associated with this object + */ + public Printname getPrintname() { + return this.printname; + } + + /** + * @return displays the tooltip of the registered Printname, + * which may be null + */ + public String getParamTooltip() { + if (getPrintname() != null) { + return getPrintname().getTooltipText(); + } else { + return null; + } + } + + public boolean isMeta() { + return this.node.isMeta(); + } + + public String toString() { + return this.node.getLine(); + } + +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ToolTipCellRenderer.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ToolTipCellRenderer.java new file mode 100644 index 000000000..a25aa1bc2 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ToolTipCellRenderer.java @@ -0,0 +1,66 @@ +/* + * Created on 13.04.2005 + * + * TODO To change the template for this generated file go to + * Window - Preferences - Java - Code Style - Code Templates + */ +package de.uka.ilkd.key.ocl.gf; + +import java.awt.Component; +import org.apache.log4j.Logger; +import javax.swing.JLabel; +import javax.swing.JList; +import javax.swing.ListCellRenderer; + +/** + * A cell renderer, that returns JLables, that put everything after the first + * '$' character into their tooltip + * @author daniels + */ +public class ToolTipCellRenderer extends JLabel implements ListCellRenderer { + + protected static Logger logger = Logger.getLogger(ToolTipCellRenderer.class.getName()); + + /** + * Returns a JLabel with a tooltip in which everything after the + * first '$' character is. + * @param list Well, the list this cell belongs to + * @param value value to display + * @param index cell index + * @param isSelected is the cell selected + * @param cellHasFocus the list and the cell have the focus + * @return a suiting JLabel + */ + public Component getListCellRendererComponent(JList list, Object value, int index, boolean isSelected, boolean cellHasFocus) { + if (isSelected) { + setBackground(list.getSelectionBackground()); + setForeground(list.getSelectionForeground()); + } + else { + setBackground(list.getBackground()); + setForeground(list.getForeground()); + } + setEnabled(list.isEnabled()); + setFont(list.getFont()); + setOpaque(true); + + + if (value == null) { + setText("Null-Value!!! Something went terribly wrong here!"); + } else if (value instanceof GFCommand){ + GFCommand gfc = (GFCommand)value; + String disText = gfc.getDisplayText(); + if (gfc instanceof LinkCommand) { + //italic font could be an alternative + disText = "-> " + disText; + } + setText(disText); + setToolTipText(gfc.getTooltipText()); + } else { + setText(value.toString()); + setToolTipText("Strange thing of class '" + value.getClass() + "'"); + } + return this; + } + +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/UnrefinedAstNodeData.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/UnrefinedAstNodeData.java new file mode 100644 index 000000000..79ef4a9df --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/UnrefinedAstNodeData.java @@ -0,0 +1,50 @@ +/* + * Created on 27.04.2005 + * + */ +package de.uka.ilkd.key.ocl.gf; + +/** + * @author daniels + * + * represents an open, unrefined node in the AST. + * It knows, how it is called and described (tooltip). + */ +public class UnrefinedAstNodeData implements AstNodeData { + protected final GfAstNode node; + protected final String paramTooltip; + + /** + * For a child we have to know its name, its type and the tooltip + * @param pTooltip + * @param node The GfAstNode for the current AST node, for which + * this AstNodeData is the data for. + */ + public UnrefinedAstNodeData(String pTooltip, GfAstNode node) { + this.node = node; + this.paramTooltip = pTooltip; + } + /** + * @return no refinement, no printname, thus null + */ + public Printname getPrintname() { + return null; + } + + /** + * @return the parameter tooltip that this node has as a child + * of its parent (who gave it to it depending on its position) + */ + public String getParamTooltip() { + return this.paramTooltip; + } + + public boolean isMeta() { + return this.node.isMeta(); + } + + public String toString() { + return this.node.toString(); + } + +} diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java new file mode 100644 index 000000000..0ecd5eb43 --- /dev/null +++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java @@ -0,0 +1,156 @@ +// 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 java.io.File; + +import javax.swing.ProgressMonitor; + +import org.apache.log4j.Logger; + +public class Utils { + protected static Logger timeLogger = Logger.getLogger("de.uka.ilkd.key.ocl.gf.utils.timer"); + protected static Logger deleteLogger = Logger.getLogger("de.uka.ilkd.key.ocl.gf.utils.delete"); + + private Utils() { + //non-instantiability enforced + } + + public static final String gf = "gf"; + public static final String gfm = "gfm"; + + /* + * Get the extension of a file. + */ + public static String getExtension(File f) { + String ext = null; + String s = f.getName(); + int i = s.lastIndexOf('.'); + + if (i > 0 && i < s.length() - 1) { + ext = s.substring(i+1).toLowerCase(); + } + return ext; + } + /** + * Sets the progress on the given ProgressMonitor and logs the current time. + * @param pm the monitor which is to be updated. If null, only logging is done + * @param progress The progress in absolute ticks + * @param note The note that is to be displayed above the progress monitor + */ + public static void tickProgress(ProgressMonitor pm, int progress, String note) { + if (note != null) { + if (timeLogger.isDebugEnabled()) { + timeLogger.debug(System.currentTimeMillis() + " : " + note); + } + } + if (pm == null) { + return; + } + pm.setProgress(progress); + if (note != null) { + pm.setNote(note); + } + } + + /** + * schedules all Eng, OCL and Ger grammar files for deletion. + * @param grammarsDir The directory where those files are + */ + public static void cleanupFromUMLTypes(String grammarsDir) { + String[] endings = {"Eng.gf", "Eng.gfc", "Ger.gf", "Ger.gfc", "OCL.gf", "OCL.gfc", ".gf", ".gfc"}; + for (int i = 0; i < endings.length; i++) { + String filename = grammarsDir + File.separator + GFEditor2.modelModulName + endings[i]; + File file = new File(filename); + file.deleteOnExit(); + if (deleteLogger.isDebugEnabled()) { + deleteLogger.debug("scheduled for deletion: " + filename); + } + } + File file = new File(grammarsDir); + file.deleteOnExit(); + file = file.getParentFile(); + file.deleteOnExit(); + } + + /** + * shamelessly copied from de.uka.ilkd.key.gui.Main + * With that, the editor is compilable without changes. + */ + private static final String LOGGER_CONFIGURATION = + System.getProperty("user.home")+ + File.separator+".key"+File.separator+"logger.props"; + + /** + * shamelessly copied from de.uka.ilkd.key.gui.Main + * With that, the editor is compilable without changes. + * Only gets called in stand-alone mode, not when run with KeY. + */ + public static void configureLogger() { + if ((new File(LOGGER_CONFIGURATION)).exists()) + org.apache.log4j.PropertyConfigurator.configureAndWatch( + LOGGER_CONFIGURATION, 1500); + else { + org.apache.log4j.BasicConfigurator.configure(); + Logger.getRootLogger().setLevel(org.apache.log4j.Level.ERROR); + } + } + + /** + * Searches for the first occurace not escaped with '\' of toBeFound in s. + * Works like String::indexOf otherwise + * @param s the String to search in + * @param toBeFound the String to search for + * @return the index of toBeFound, -1 if not found (or only escaped) + */ + public static int indexOfNotEscaped(String s, String toBeFound) { + return indexOfNotEscaped(s, toBeFound, 0); + } + + /** + * Searches for the first occurace not escaped with '\' of toBeFound in s. + * Works like String::indexOf otherwise + * @param s the String to search in + * @param toBeFound the String to search for + * @param startIndex the index in s, from which the search starts + * @return the index of toBeFound, -1 if not found (or only escaped) + */ + public static int indexOfNotEscaped(String s, String toBeFound, int startIndex) { + for (int from = startIndex; from < s.length();) { + int i = s.indexOf(toBeFound, from); + if (i <= 0) { + //-1 is not found at all, 0 can't have a '\' before + return i; + } else if (s.charAt(i-1) != '\\') { + return i; + } else { + from = i + 1; + } + } + return -1; + } + + /** + * a simple replaceAll replacement, that uses NO regexps + * and thus needs no freaking amount of backslashes + * @param original The String in which the replacements should take place + * @param toReplace the String literal that is to be replaced + * @param replacement the replacement string + * @return original, but with replacements + */ + 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)) { + sb.replace(i, i + toReplace.length(), replacement); + } + return sb.toString(); + } +} diff --git a/src/JavaGUI2/jargs-1.0.jar b/src/JavaGUI2/jargs-1.0.jar new file mode 100644 index 000000000..cdbc80bb3 Binary files /dev/null and b/src/JavaGUI2/jargs-1.0.jar differ diff --git a/src/JavaGUI2/log4j-1.2.8.jar b/src/JavaGUI2/log4j-1.2.8.jar new file mode 100644 index 000000000..493a3ccc1 Binary files /dev/null and b/src/JavaGUI2/log4j-1.2.8.jar differ diff --git a/src/Makefile b/src/Makefile index c167f2fd4..878733668 100644 --- a/src/Makefile +++ b/src/Makefile @@ -7,6 +7,7 @@ GHCFLAGS+= -fglasgow-exts -package util GHCOPTFLAGS=-O2 GHCFUDFLAG= JAVAFLAGS=-target 1.4 -source 1.4 +GFEDITOR=JavaGUI2 DIST_DIR=GF-$(PACKAGE_VERSION) NOT_IN_DIST= \ @@ -93,10 +94,12 @@ shell: clean: find . '(' -name '*~' -o -name '*.hi' -o -name '*.ghi' -o -name '*.o' ')' -exec rm -f '{}' ';' -rm -f JavaGUI/*.class + -rm -f $(GFEDITOR)/de/uka/ilkd/key/ocl/gf/*.class -rm -f gf.wixobj distclean: clean -rm -f JavaGUI/gf-java.jar jgf + -rm -f $(GFEDITOR)/gfeditor.jar jgf -rm -f tools/$(GF_DOC_EXE) -rm -f config.status config.mk config.log -rm -f *.tgz *.zip @@ -111,9 +114,12 @@ today: javac: $(JAVAC) $(JAVAFLAGS) JavaGUI/*.java + $(JAVAC) $(JAVAFLAGS) -classpath $(GFEDITOR):$(GFEDITOR)/log4j-1.2.8.jar:$(GFEDITOR)/jargs-1.0.jar $(GFEDITOR)/de/uka/ilkd/key/ocl/gf/*.java + jar: javac - cd JavaGUI; $(JAR) -cmf manifest.txt gf-java.jar *.class + cd JavaGUI; $(JAR) -cmf manifest.txt gf-java.jar *.class ; cd .. + cd $(GFEDITOR) ; rm -rf jarcontents ; mkdir jarcontents ; cp -r de/ ManifestMain.txt jarcontents ; cat jargs-1.0.jar | (cd jarcontents; jar -x jargs) ; cat log4j-1.2.8.jar | (cd jarcontents; jar -x org) ; cd jarcontents ; $(JAR) -cmf ManifestMain.txt ../gfeditor.jar de/uka/ilkd/key/ocl/gf/*.class org jargs ; cd .. ; rm -rf jarcontents ; cd .. showflags: @echo $(GHCFLAGS) @@ -187,6 +193,7 @@ binary-dist: $(MAKE) all $(INSTALL) ../bin/$(GF_EXE) tools/$(GF_DOC_EXE) $(BIN_DIST_DIR) $(INSTALL) -m 0644 JavaGUI/gf-java.jar $(BIN_DIST_DIR) + $(INSTALL) -m 0644 $(GFEDITOR)/gfeditor.jar $(BIN_DIST_DIR) $(INSTALL) configure config.guess config.sub install-sh $(BIN_DIST_DIR) $(INSTALL) -m 0644 config.mk.in jgf.in $(BIN_DIST_DIR) $(INSTALL) -m 0644 ../README ../LICENSE $(BIN_DIST_DIR) @@ -229,8 +236,13 @@ install-editor: $(INSTALL) -d $(datadir)/GF-$(PACKAGE_VERSION) $(INSTALL) jgf $(bindir) $(INSTALL) -m 0644 JavaGUI/gf-java.jar $(datadir)/GF-$(PACKAGE_VERSION) + $(INSTALL) gfeditor $(bindir) + $(INSTALL) -m 0644 $(GFEDITOR)/gfeditor.jar $(datadir)/GF-$(PACKAGE_VERSION) install-java: javac -rm -f ../bin/JavaGUI ln -s ../src/JavaGUI ../bin @echo "PLEASE edit GFHOME in bin/jgf" + -rm -f ../bin/$(GFEDITOR) + ln -s ../src/$(GFEDITOR) ../bin + diff --git a/src/Makefile.binary b/src/Makefile.binary index 669af92cc..c60fd81c7 100644 --- a/src/Makefile.binary +++ b/src/Makefile.binary @@ -8,7 +8,9 @@ install: $(INSTALL) gf$(EXEEXT) gfdoc$(EXEEXT) jgf $(bindir) $(INSTALL) -d $(GF_DATA_DIR) $(INSTALL) -m 0644 gf-java.jar $(GF_DATA_DIR) + $(INSTALL) -m 0644 gfeditor.jar $(GF_DATA_DIR) uninstall: -rm -f $(bindir)/gf$(EXEEXT) $(bindir)/gfdoc$(EXEEXT) $(bindir)/jgf -rm -f $(GF_DATA_DIR)/gf-java.jar + -rm -f $(GF_DATA_DIR)/gfeditor.jar diff --git a/src/configure.ac b/src/configure.ac index 90a5d7e01..229d6254d 100644 --- a/src/configure.ac +++ b/src/configure.ac @@ -4,9 +4,9 @@ AC_INIT([GF],[2.2],[aarne@cs.chalmers.se],[GF]) AC_PREREQ(2.53) -AC_REVISION($Revision: 1.23 $) +AC_REVISION($Revision: 1.24 $) -AC_CONFIG_FILES([config.mk jgf]) +AC_CONFIG_FILES([config.mk jgf gfeditor]) AC_CANONICAL_HOST diff --git a/src/gfeditor.in b/src/gfeditor.in new file mode 100644 index 000000000..9a390195b --- /dev/null +++ b/src/gfeditor.in @@ -0,0 +1,39 @@ +#!/bin/sh + +prefix=@prefix@ +exec_prefix=@exec_prefix@ +GF_BIN_DIR=@bindir@ +GF_DATA_DIR=@datadir@/GF-@PACKAGE_VERSION@ + +JAVA="@JAVA@" + +GF=$GF_BIN_DIR/gf +JARFILE=$GF_DATA_DIR/gfeditor.jar + +if [ ! -x "${JAVA}" ]; then + JAVA=`which java` +fi + +if [ ! -x "${JAVA}" ]; then + echo "No Java VM found" + exit 1 +fi + +if [ ! -f "${JARFILE}" ]; then + echo "JAR file ${JARFILE} not found" + exit 1 +fi + +if [ ! -x "${GF}" ]; then + GF=`which gf` +fi + +if [ ! -x "${GF}" ]; then + echo "gf not found" + exit 1 +fi + +COMMAND= ${JAVA} -jar ${JARFILE} -g $GF $* + +echo ${COMMAND} +exec ${COMMAND}