GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-09 04:59:31 -06:00
Code Issues Packages Projects Releases Wiki Activity

added daniels' version of the Java editor

Browse Source
This commit is contained in:
hdaniels
2005-06-21 18:40:22 +00:00
parent 0c71d62d4c
commit 6693b50c9d
31 changed files with 6808 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

29
src/JavaGUI2/LICENCE_jargs Normal file
View File

@@ -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.

3
src/JavaGUI2/ManifestMain.txt Normal file
View File

@@ -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

172
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AbstractProber.java Normal file
View File

@@ -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("<hmsg>")) {
skipChild("<hmsg>");
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("<linearizations>");
}
/** Reads the tree child of the XML from beginning to end */
protected void readTree() {
skipChild("<tree>");
}
/** Reads the message child of the XML from beginning to end */
protected void readMessage() {
skipChild("<message>");
}
/** Reads the menu child of the XML from beginning to end */
protected void readMenu() {
skipChild("<menu>");
}
/**
* reads the output from GF starting with &gt;gfedit&lt;
* and last reads &gt;/gfedit&lt;.
*/
protected void readGfedit() {
try {
String next = "";
//read <gfedit>
String readresult = fromProc.readLine();
if (logger.isDebugEnabled()) {
logger.debug("1 " + next);
}
//read either <hsmg> or <lineatization>
readresult = fromProc.readLine();
if (logger.isDebugEnabled()) {
logger.debug("1 " + next);
}
next = readHmsg(readresult);
//in case there comes sth. unexpected before <linearizations>
//usually the while body is never entered
// %%%
while ((next!=null)&&((next.length()==0)||(!next.trim().equals("<linearizations>")))) {
next = fromProc.readLine();
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 &gt;gfinit&lt;
*/
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);
}
}
}

30
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/AstNodeData.java Normal file
View File

@@ -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();
}

40
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ConstraintCallback.java Normal file
View File

@@ -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);
}

202
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Display.java Normal file
View File

@@ -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.
* &lt;html&gt; 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 ="<html><body" + fontface + ">" + this.linStagesHtml.get(this.linStagesHtml.size() - 1).toString() + "</body></html>";
} 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();
}
}

347
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/DynamicTree2.java Normal file
View File

@@ -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
}
}

104
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFCommand.java Normal file
View File

@@ -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();
}
}

4033
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java Normal file
View File

File diff suppressed because it is too large Load Diff

123
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GfAstNode.java Normal file
View File

@@ -0,0 +1,123 @@
/*
* Created on 06.05.2005
*
*/
package de.uka.ilkd.key.ocl.gf;
/**
* @author daniels
* This Class represents a parsed node in the GF AST.
*/
class GfAstNode {
protected final String[] boundTypes;
protected final String[] boundNames;
/** The type of this AST node */
private final String type;
/**
* @return The type of this AST node
*/
protected String getType() {
return type;
}
/** the fun represented in this AST node */
private final String fun;
/**
* @return the fun represented in this AST node.
* Can be a metavariable like "?1"
*/
protected String getFun() {
return fun;
}
/**
* @return true iff the node is a metavariable, i.e. open and not
* yet refined.
*/
protected boolean isMeta() {
return fun.startsWith("?");
}
/** the line that was used to build this node */
private final String line;
/**
* @return the line that was used to build this node
*/
protected String getLine() {
return line;
}
/**
* feed this constructor the line that appears in the GF AST and
* it will get chopped at the right points.
* @param line The line from GF without the * in the beginning.
*/
protected GfAstNode(final String line) {
this.line = line.trim();
final int index = this.line.lastIndexOf(" : ");
this.type = this.line.substring(index + 3);
String myFun = this.line.substring(0, index);
if (myFun.startsWith("\\(")) {
final int end = myFun.lastIndexOf(") -> ");
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() + "'");
}
}
}
}

40
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GrammarFilter.java Normal file
View File

@@ -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)";
}
}

47
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/HtmlMarkedArea.java Normal file
View File

@@ -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;
}
}

104
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/InputCommand.java Normal file
View File

@@ -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;
}
}

34
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinPosition.java Normal file
View File

@@ -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");
}
}

55
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/LinkCommand.java Normal file
View File

@@ -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), "<i>open submenu</i> <br> ");
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;
}
}

40
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/MarkedArea.java Normal file
View File

@@ -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 + "'";
}
}

458
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Printname.java Normal file
View File

@@ -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\\$<html>adds the current subtree to the clipboard.<br>It is offered in the refinement menu if the expected type fits to the one of the current sub-tree.</html>");
public static final Printname printhistory = new Printname("ph", "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 &lt;html&gt; &lt;/html&gt; 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 <html> wrapping
result = htmlAppend(result, params);
} else {
//wrap in <html> 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 &lt;/html&gt; tag.
* If original is no HTML, it will be enclosed in &lt;html&gt;
* @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("</html>");
if (htmlindex > -1) {
result.insert(htmlindex, insertion);
} else {
result.insert(0,"<html>").append(insertion).append("</html>");
}
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 &lt;html&gt; tag.
* If original is no HTML, it will be enclosed in &lt;html&gt;
* @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("<html>");
if (htmlindex > -1) {
result.insert(htmlindex, insertion);
} else {
result.insert(0,insertion).insert(0,"<html>").append("</html>");
}
return result.toString();
}
/**
* wraps a single parameter with explanatory text
* into &lt;dt&gt; and &lt;dd&gt; 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 = "<dt>" + this.paramNames.get(which) + "</dt>"
+ "<dd>" + this.paramTexts.get(which) + "</dd>";
return result;
} catch (ArrayIndexOutOfBoundsException e) {
subcatLogger.warn(e.getLocalizedMessage());
return "";
}
}
/**
* wraps a single parameter together with its explanatory text into
* a HTML definition list (&lt;dl&gt; tags).
* Also the result is wrapped in &lt;html&gt; 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 = "<html><dl>" + text + "</dl></html>";
return result;
}
/**
* wraps all parameters together with their explanatory text into
* a HTML definition list (&lt;dl&gt; tags).
* No &lt;html&gt; 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("<h4>Parameters:</h4><dl>");
for (int i = 0; i < this.paramNames.size(); i++) {
result.append(htmlifyParam(i));
}
result.append("</dl>");
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() + ")";
}
}

83
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameLoader.java Normal file
View File

@@ -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 <message>, 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();
}
}

139
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/PrintnameManager.java Normal file
View File

@@ -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\" ++ (\"<i>coll</i>.<br>That\" ++ (\"is,\" ++ (\"the\" ++ (\"parameter\" ++ (\"type\" ++ (\"of\" ++ \"<i>coll</i>\")))))))))))++ (\"#set\" ++ (\"The\" ++ (\"Set\" ++ (\"in\" ++ (\"which\" ++ (\"occurances\" ++ (\"of\" ++ (\"<i>elem</i>\" ++ (\"are\" ++ (\"to\" ++ (\"be\" ++ \"counted.\")))))))))) ++ (\"#elem\" ++ (\"The\" ++ (\"instance\" ++ (\"of\" ++ (\"which\" ++ (\"the\" ++ (\"occurances\" ++ (\"in\" ++ (\"<i>coll</i>\" ++ (\"are\" ++ \"counted.\")))))))))))))";
System.out.println(a);
System.out.println(removePluses(a));
}
}

193
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ReadDialog.java Normal file
View File

@@ -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);
}
}
}

146
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RealCommand.java Normal file
View File

@@ -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<br>" + 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 = "<br>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;
}

58
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/RefinedAstNodeData.java Normal file
View File

@@ -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();
}
}

66
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ToolTipCellRenderer.java Normal file
View File

@@ -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;
}
}

50
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/UnrefinedAstNodeData.java Normal file
View File

@@ -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();
}
}

156
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/Utils.java Normal file
View File

@@ -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();
}
}

BIN
src/JavaGUI2/jargs-1.0.jar Normal file
View File

Binary file not shown.

BIN
src/JavaGUI2/log4j-1.2.8.jar Normal file
View File

Binary file not shown.

14
src/Makefile
View File

@@ -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

2
src/Makefile.binary
View File

@@ -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

4
src/configure.ac
View File

@@ -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

39
src/gfeditor.in Normal file
View File

@@ -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}