msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

removed JavaGUIs from src

Browse Source
This commit is contained in:
aarne
2008-06-25 17:05:19 +00:00
parent 4e5c83fa74
commit 15d44712f6
57 changed files with 0 additions and 16085 deletions
Download Patch File Download Diff File Expand all files Collapse all files

272
src/JavaGUI/DynamicTree.java
View File

@@ -1,272 +0,0 @@
/*
* 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 java.util.Vector;
import java.awt.event.*;
public class DynamicTree extends JPanel implements KeyListener,
ActionListener{
public static DefaultMutableTreeNode rootNode;
protected DefaultTreeModel treeModel;
public JTree tree;
public int oldSelection = 0;
private Toolkit toolkit = Toolkit.getDefaultToolkit();
JPopupMenu popup = new JPopupMenu();
JMenuItem menuItem;
Timer timer = new Timer(500, this);
MouseEvent m;
public DynamicTree() {
timer.setRepeats(false);
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() {
public void valueChanged(TreeSelectionEvent e) {
if (tree.getSelectionRows()!=null) {
if (GFEditor.nodeTable == null)
{if (GFEditor.debug) System.out.println("null node table");}
else
{if (GFEditor.debug) System.out.println("node table: "+
GFEditor.nodeTable.contains(new Integer(0)) +" "+
GFEditor.nodeTable.keys().nextElement()); }
if (tree.getSelectionPath() == null)
{if (GFEditor.debug) System.out.println("null root path"); }
else
{if (GFEditor.debug) System.out.println("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);
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 currently selected node. */
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);
}
public DefaultMutableTreeNode addObject(DefaultMutableTreeNode parent,
Object child) {
return addObject(parent, child, false);
}
public DefaultMutableTreeNode addObject(DefaultMutableTreeNode parent,
Object child,
boolean shouldBeVisible) {
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) {}
if (GFEditor.debug) System.out.println
("The user has finished editing the node.");
if (GFEditor.debug) System.out.println(
"New value: " + node.getUserObject());
}
public void treeNodesInserted(TreeModelEvent e) {
}
public void treeNodesRemoved(TreeModelEvent e) {
}
public void treeStructureChanged(TreeModelEvent e) {
}
}
private class MyRenderer extends DefaultTreeCellRenderer {
ImageIcon tutorialIcon;
public MyRenderer() {
tutorialIcon = new ImageIcon("images/middle.gif");
}
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 (leaf && isTutorialBook(value))
setIcon(tutorialIcon);
return this;
}
protected boolean isTutorialBook(Object value) {
DefaultMutableTreeNode node =
(DefaultMutableTreeNode)value;
String nodeInfo =
(String)(node.getUserObject());
if (nodeInfo.indexOf("?") >= 0) {
return true;
}
return false;
}
}//class
class PopupListener extends MouseAdapter {
public void mousePressed(MouseEvent e) {
int selRow = tree.getRowForLocation(e.getX(), e.getY());
tree.setSelectionRow(selRow);
if (GFEditor.debug) System.out.println("selection changed!");
maybeShowPopup(e);
}
public void mouseReleased(MouseEvent e) {
if (GFEditor.debug) System.out.println("mouse released!");
maybeShowPopup(e);
}
}
void maybeShowPopup(MouseEvent e) {
if (GFEditor.debug) System.out.println("may be!");
if (e.isPopupTrigger()) {
m=e;
timer.start();
}
}
void addMenuItem(String name){
menuItem = new JMenuItem(name);
menuItem.addActionListener(this);
popup.add(menuItem);
}
public void actionPerformed(ActionEvent ae)
{
if (ae.getSource()==timer){
if (GFEditor.debug) System.out.println("changing menu!");
popup.removeAll();
for (int i = 0; i<GFEditor.listModel.size() ; i++)
addMenuItem(GFEditor.listModel.elementAt(i).toString());
popup.show(m.getComponent(), m.getX(), m.getY());
}
else{
GFEditor.treeChanged = true;
GFEditor.send((String)GFEditor.commands.elementAt
(popup.getComponentIndex((JMenuItem)(ae.getSource()))));
}
}
/** Handle the key pressed event. */
public void keyPressed(KeyEvent e) {
int keyCode = e.getKeyCode();
switch (keyCode){
case 32: GFEditor.send("'"); break;
case 127: GFEditor.send("d"); break;
}
}
/** Handle the key typed event. */
public void keyTyped(KeyEvent e) {
}
/** Handle the key released event. */
public void keyReleased(KeyEvent e) {
}
}

272
src/JavaGUI/DynamicTree2.java
View File

@@ -1,272 +0,0 @@
/*
* 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 java.util.Vector;
import java.awt.event.*;
public class DynamicTree2 extends JPanel implements KeyListener,
ActionListener{
public static DefaultMutableTreeNode rootNode;
protected DefaultTreeModel treeModel;
public JTree tree;
public int oldSelection = 0;
private Toolkit toolkit = Toolkit.getDefaultToolkit();
public JPopupMenu popup = new JPopupMenu();
JMenuItem menuItem;
Timer timer = new Timer(500, this);
MouseEvent m;
public DynamicTree2() {
timer.setRepeats(false);
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() {
public void valueChanged(TreeSelectionEvent e) {
if (tree.getSelectionRows()!=null) {
if (GFEditor2.nodeTable == null)
{if (GFEditor2.debug) System.out.println("null node table");}
else
{if (GFEditor2.debug) System.out.println("node table: "+
GFEditor2.nodeTable.contains(new Integer(0)) +" "+
GFEditor2.nodeTable.keys().nextElement()); }
if (tree.getSelectionPath() == null)
{if (GFEditor2.debug) System.out.println("null root path"); }
else
{if (GFEditor2.debug) System.out.println("selected path"+
tree.getSelectionPath());}
int i = ((Integer)GFEditor2.nodeTable.get(
tree.getSelectionPath())).intValue();
int j = oldSelection;
GFEditor2.treeChanged = true;
if (i>j) GFEditor2.send("> "+String.valueOf(i-j));
else GFEditor2.send("< "+String.valueOf(j-i));
}
}
});
tree.setCellRenderer(new MyRenderer());
tree.setShowsRootHandles(true);
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 currently selected node. */
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);
}
public DefaultMutableTreeNode addObject(DefaultMutableTreeNode parent,
Object child) {
return addObject(parent, child, false);
}
public DefaultMutableTreeNode addObject(DefaultMutableTreeNode parent,
Object child,
boolean shouldBeVisible) {
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) {}
if (GFEditor2.debug) System.out.println
("The user has finished editing the node.");
if (GFEditor2.debug) System.out.println(
"New value: " + node.getUserObject());
}
public void treeNodesInserted(TreeModelEvent e) {
}
public void treeNodesRemoved(TreeModelEvent e) {
}
public void treeStructureChanged(TreeModelEvent e) {
}
}
private class MyRenderer extends DefaultTreeCellRenderer {
ImageIcon tutorialIcon;
public MyRenderer() {
tutorialIcon = new ImageIcon("images/middle.gif");
}
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 (leaf && isTutorialBook(value))
setIcon(tutorialIcon);
return this;
}
protected boolean isTutorialBook(Object value) {
DefaultMutableTreeNode node =
(DefaultMutableTreeNode)value;
String nodeInfo =
(String)(node.getUserObject());
if (nodeInfo.indexOf("?") >= 0) {
return true;
}
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.debug) System.out.println("selection changed!");
maybeShowPopup(e);
}
public void mouseReleased(MouseEvent e) {
if (GFEditor2.debug) System.out.println("mouse released!");
maybeShowPopup(e);
}
}
void maybeShowPopup(MouseEvent e) {
if (GFEditor2.debug) System.out.println("may be!");
if (e.isPopupTrigger()) {
m = e;
timer.start();
}
}
void addMenuItem(String name){
menuItem = new JMenuItem(name);
menuItem.addActionListener(this);
popup.add(menuItem);
}
public void actionPerformed(ActionEvent ae)
{
if (ae.getSource()==timer){
if (GFEditor2.debug) System.out.println("changing menu!");
popup.removeAll();
for (int i = 0; i<GFEditor2.listModel.size() ; i++)
addMenuItem(GFEditor2.listModel.elementAt(i).toString());
popup.show(m.getComponent(), m.getX(), m.getY());
}
else{
GFEditor2.treeChanged = true;
GFEditor2.send((String)GFEditor2.commands.elementAt
(popup.getComponentIndex((JMenuItem)(ae.getSource()))));
}
}
/** Handle the key pressed event. */
public void keyPressed(KeyEvent e) {
int keyCode = e.getKeyCode();
switch (keyCode){
case 32: GFEditor2.send("'"); break;
case 127: GFEditor2.send("d"); break;
}
}
/** Handle the key typed event. */
public void keyTyped(KeyEvent e) {
}
/** Handle the key released event. */
public void keyReleased(KeyEvent e) {
}
}

1420
src/JavaGUI/GFEditor.java
View File

File diff suppressed because it is too large Load Diff

2357
src/JavaGUI/GFEditor2.java
View File

File diff suppressed because it is too large Load Diff

30
src/JavaGUI/GrammarFilter.java
View File

@@ -1,30 +0,0 @@
import java.io.File;
import javax.swing.*;
import javax.swing.filechooser.*;
public class GrammarFilter extends FileFilter {
// Accept all directories and all gf, gfcm 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.gfcm)) {
return true;
} else {
return false;
}
}
return false;
}
// The description of this filter
public String getDescription() {
return "Just Grammars";
}
}

13
src/JavaGUI/LinPosition.java
View File

@@ -1,13 +0,0 @@
//package javaGUI;
public class LinPosition
{
public String position;
public boolean correctPosition = true;
LinPosition(String p, boolean cor)
{
position = p;
correctPosition = cor ;
}
}

18
src/JavaGUI/MarkedArea.java
View File

@@ -1,18 +0,0 @@
//package javaGUI;
public class MarkedArea
{
public int begin;
public int end;
public LinPosition position;
public String words;
MarkedArea(int b, int e, LinPosition p, String w)
{
begin = b;
end = e;
position = p;
words = w;
}
}

1552
src/JavaGUI/Numerals.java
View File

File diff suppressed because it is too large Load Diff

22
src/JavaGUI/Utils.java
View File

@@ -1,22 +0,0 @@
import java.io.File;
public class Utils {
public final static String gf = "gf";
public final static String gfcm = "gfcm";
/*
* 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;
}
}

1
src/JavaGUI/manifest.txt
View File

@@ -1 +0,0 @@
Main-Class: GFEditor2

1
src/JavaGUI/runNumerals
View File

@@ -1 +0,0 @@
java -cp ./ Numerals "GF +java ../../grammars/numerals/old/numerals.Ita.gf ../../grammars/numerals/old/numerals.Mag.gf ../../grammars/numerals/old/numerals.Tam.gf ../../grammars/numerals/old/numerals.Suo.gf ../../grammars/numerals/old/numerals.NorB.gf ../../grammars/numerals/old/numerals.Slo.gf ../../grammars/numerals/old/numerals.Spa.gf ../../grammars/numerals/old/numerals.Swe.gf ../../grammars/numerals/old/numerals.Deu.gf ../../grammars/numerals/old/numerals.Fra.gf ../../grammars/numerals/old/numerals.Malay.gf ../../grammars/numerals/old/numerals.Ned.gf ../../grammars/numerals/old/numerals.Pol.gf ../../grammars/numerals/old/numerals.ChiU.gf ../../grammars/numerals/old/numerals.Dec.gf "

29
src/JavaGUI2/LICENCE_jargs
View File

@@ -1,29 +0,0 @@
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
View File

@@ -1,3 +0,0 @@
Manifest-Version: 1.0
Main-Class: de.uka.ilkd.key.ocl.gf.GFEditor2
Class-Path: log4j-1.2.8.jar jargs-1.0.jar

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

@@ -1,182 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.io.IOException;
import java.util.logging.*;
/**
* A class that offers a basic readGfEdit method with a lot of
* hot spots where subclasses can plug in
* @author daniels
*
*/
abstract class AbstractProber {
/**
* reference to the editor whose readRefinementMenu method is used
*/
protected final GfCapsule gfCapsule;
protected static Logger logger = Logger.getLogger(AbstractProber.class.getName());
/**
* A constructor which sets some fields
* @param gfCapsule The encapsulation of GF
*/
public AbstractProber(GfCapsule gfCapsule) {
this.gfCapsule = gfCapsule;
}
/**
* 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>")) {
gfCapsule.skipChild("<hmsg>");
try {
String next = gfCapsule.fromProc.readLine();
if (logger.isLoggable(Level.FINER)) {
logger.finer("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) {
gfCapsule.skipChild("<linearizations>");
}
/**
* Reads the tree child of the XML from beginning to end
*/
protected void readTree() {
gfCapsule.skipChild("<tree>");
}
/**
* Reads the message child of the XML from beginning to end
*/
protected void readMessage() {
gfCapsule.skipChild("<message>");
}
/**
* Reads the menu child of the XML from beginning to end
*/
protected void readMenu() {
gfCapsule.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 = gfCapsule.fromProc.readLine();
if (logger.isLoggable(Level.FINER)) {
logger.finer("1 " + next);
}
//read either <hsmg> or <lineatization>
readresult = gfCapsule.fromProc.readLine();
if (logger.isLoggable(Level.FINER)) {
logger.finer("1 " + next);
}
Hmsg hmsg = gfCapsule.readHmsg(readresult);
next = hmsg.lastline;
//in case there comes sth. unexpected before <linearizations>
//usually the while body is never entered
// %%%
while ((next!=null)&&((next.length()==0)||(!next.trim().equals("<linearizations>")))) {
next = gfCapsule.fromProc.readLine();
if (next!=null){
if (logger.isLoggable(Level.FINER)) {
logger.finer("1 " + next);
}
} else {
System.exit(0);
}
}
readLinearizations(next);
readTree();
readMessage();
readMenu();
for (int i=0; i<3 && !next.equals(""); i++){
next = gfCapsule.fromProc.readLine();
if (logger.isLoggable(Level.FINER)) {
logger.finer("1 " + next);
}
}
} 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.isLoggable(Level.FINE)) {
logger.fine("## send: '" + text + "'");
}
gfCapsule.realSend(text);
}
/**
* Just reads the complete output of a GF run and ignores it.
*/
protected void readAndIgnore() {
try {
StringBuffer debugCollector = new StringBuffer();
String readresult = gfCapsule.fromProc.readLine();
debugCollector.append(readresult).append('\n');
if (logger.isLoggable(Level.FINER)) logger.finer("14 "+readresult);
while (readresult.indexOf("</gfedit>") == -1) {
readresult = gfCapsule.fromProc.readLine();
debugCollector.append(readresult).append('\n');
if (logger.isLoggable(Level.FINER)) logger.finer("14 "+readresult);
}
//read trailing newline:
readresult = gfCapsule.fromProc.readLine();
debugCollector.append(readresult).append('\n');
if (logger.isLoggable(Level.FINER)) logger.finer("14 "+readresult);
} catch (IOException e) {
System.err.println("Could not read from external process:\n" + e);
}
}
}

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

@@ -1,105 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.logging.*;
/**
* @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.
* Knows nothing directly of the type of the node, which an object of this class
* represents. That's whats GfAstNode is for.
*/
abstract class AstNodeData {
protected static Logger logger = Logger.getLogger(DynamicTree2.class.getName());
/**
* @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();
/**
* keeps track of the number of children of this node.
* It has to be increased whenever a new child of this node is
* added.
*/
public int childNum = 0;
/**
* The position String in the GF AST for this node
* in Haskell notation.
*/
public final String position;
/**
* the GF node connected to this NodeData, not the JTree node
*/
public final GfAstNode node;
/**
* If a subtyping witness is missing, then this flag is false
*/
public boolean subtypingStatus = true;
/**
* if this is the active, selected, focused node
*/
public final boolean selected;
/**
* The constraint, that is valid on this node.
* If this node introduced a node itself and did not just inherit
* one, they are just concatenated.
* Until now, only the presence of a non-empty string here is used,
* so that is not important yet.
*/
public final String constraint;
/**
* some nodes like coerce should, if possible, be covered from the
* users eyes. If this variable is greater than -1, the child
* with that number is shown instead of this node.
* This node will not appear in the tree.
*/
public int showInstead = -1;
/**
* A simple setter constructor, that sets the fields of this class (except showInstead)
* @param node the GF node connected to this NodeData, not the JTree node
* @param pos The position String in the GF AST for this node
* in Haskell notation.
* @param selected if this is the active, selected, focused node
* @param constraint The GF constraint introduced in this node
*/
protected AstNodeData(GfAstNode node, String pos, boolean selected, String constraint) {
this.node = node;
this.position = pos;
this.selected = selected;
// I have no better idea, how to clutch them together, since
// I don't need the content of this field right now.
this.constraint = node.constraint + constraint;
}
public String toString() {
return this.node.getLine();
}
}

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

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

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

@@ -1,64 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.logging.*;
/**
* @author daniels
* Offers the interface that GFEditor2 uses to send back the constraint after editing.
* Has no dependancies on KeY or TogetherCC.
*/
abstract class ConstraintCallback {
/**
* Does the logging. What else should it do?
*/
protected static Logger logger = Logger.getLogger(ConstraintCallback.class.getName());
/**
* The path name of the directory where the grammars reside
*/
String grammarsDir;
/**
* sets the directory where the grammars reside
* @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);
/**
* Sends the unfinished OCL constraint back to Together to save it
* as a GF tree as a JavaDoc comment.
* @param abs The GF tree in question
*/
abstract void sendAbstract(String abs);
}

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

@@ -1,249 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
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 {
/**
* If the linearization should be displayed as pure text
*/
private boolean doText;
/**
* If the linearization should be displayed as HTML
*/
private boolean doHtml;
/**
* collects the linearization after each append.
* what's in here are Strings
*/
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) {
setDisplayType(dt);
this.htmlLengthPane.setContentType("text/html");
this.htmlLengthPane.setEditable(false);
}
/**
* (de-)activates display of text and HTML according to dt
* @param dt 1 if only text is to be shown, 2 for only HTML, 3 for both.
*/
protected void setDisplayType(int dt) {
switch (dt) {
case 1:
doText = true;
doHtml = false;
break;
case 2:
doText = false;
doHtml = true;
break;
case 3:
doText = true;
doHtml = true;
break;
default:
doText = true;
doHtml = true;
break;
}
}
/**
* Resets the stored text, but leaves the scroll markers untouched.
*/
public void resetLin() {
linStagesHtml.clear();
linStagesText.clear();
htmlLengthPane.setText("");
}
/**
* @param font The Font, that is to be used. If null, the default of JTextPane is taken.
* @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
* @param language the language of the current linearization
* @return the HtmlMarkedArea object that represents the given information
* and knows about its beginning and end in the display areas.
*/
protected MarkedArea addAsMarked(String toAdd, LinPosition position, String language) {
/** 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 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 MarkedArea hma = new MarkedArea(oldLengthText, newLengthText, position, toAdd, oldLengthHtml, newLengthHtml, language);
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();
/**
* To store the scroll state of the pure text linearization area
*/
int scrollText = 0;
/**
* To store the scroll state of the HTML linearization area
*/
int scrollHtml = 0;
public String toString() {
return getText();
}
}

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

@@ -1,366 +0,0 @@
//Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/*
* 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 java.util.logging.*;
//import de.uka.ilkd.key.util.KeYResourceManager;
import java.awt.event.*;
/**
* A GUI class, does store the tree, but does not create it.
* The tree is created in GFEditor2.
* This class displays the tree and let the user interact with it via mouse clicks.
*/
public class DynamicTree2 extends JPanel implements KeyListener {
protected static Logger logger = Logger.getLogger(DynamicTree2.class.getName());
public DefaultMutableTreeNode rootNode;
private DefaultTreeModel treeModel;
public JTree tree;
private Toolkit toolkit = Toolkit.getDefaultToolkit();
private GFEditor2 gfeditor;
protected TreePath oldSelection = null;
/**
* Initializes the display state of the tree panel, sets up the
* event handlers.
* Does not initialize the tree.
* @param gfe The editor object this object belongs to.
*/
public DynamicTree2(GFEditor2 gfe) {
this.gfeditor = gfe;
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);
//Add listener to components that can bring up popup menus.
MouseListener popupListener = new PopupListener();
tree.addMouseListener(popupListener);
tree.addTreeSelectionListener(new TreeSelectionListener() {
/**
* Moves to the position of the selected node in GF.
* the following is assumed:
* gfeditor.nodeTable contains the positions for all selectionPathes.
*/
public void valueChanged(TreeSelectionEvent e) {
if ((tree.getSelectionPath() != null) && tree.getSelectionPath().equals(oldSelection)) {
//nothing to be done here, probably
//triggered by showTree
return;
}
if (tree.getSelectionRows() != null) {
if (tree.getSelectionPath() == null) {
if (logger.isLoggable(Level.FINER)) {
logger.finer("null root path");
}
} else {
if (logger.isLoggable(Level.FINER)) {
logger.finer("selected path" + tree.getSelectionPath());
}
}
String pos = gfeditor.getNodePosition(tree.getSelectionPath());
if (pos == null || "".equals(pos)) {
//default to sth. sensible
pos = "[]";
}
gfeditor.send("[t] mp " + pos);
}
oldSelection = tree.getSelectionPath();
}
});
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 in the tree and
* form a dummy tree in treePanel
*/
protected void resetTree() {
((DefaultTreeModel)(tree.getModel())).setRoot(new DefaultMutableTreeNode("Root"));
((DefaultTreeModel)(tree.getModel())).reload();
}
/** Remove all nodes except the root node. */
public void clear() {
((DefaultTreeModel)(tree.getModel())).setRoot(null);
oldSelection = null;
//((DefaultTreeModel)(tree.getModel())).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.isLoggable(Level.FINER)) {
logger.finer("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 (logger.isLoggable(Level.FINER)) {
logger.finer("The user has finished editing the node.");
logger.finer("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
}
}
/**
* This tree cell renderer got overwritten to make it possible to show
* tooltips according to the user object
*/
private class MyRenderer extends DefaultTreeCellRenderer {
//int counter = 0;
//final ImageIcon iconFilled;
//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);
// }
/**
* The heart of this class, sets display and tooltip text
* depending on the user data
*/
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();
if (!and.subtypingStatus ) {
this.setForeground(Color.RED);
ptt = Printname.htmlAppend(ptt, "<p>Subtyping proof is missing. <br>If no refinements are offered here, then there is a subtyping error.");
}
this.setToolTipText(ptt);
this.setText(and.toString());
// if (and.isMeta()) {
// 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) {
gfeditor.maybeShowPopup(e);
}
public void mouseReleased(MouseEvent e) {
//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
}
}

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

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

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

@@ -1,137 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/**
* @author daniels
* 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{
/**
* 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. Then the InputCommand (more than one
* does not happen). If that does not decide, the display name as a String does.
* @param o the other command.
* @return see above.
*/
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;
}
//LinkCommands are dealt with, so from now on, they don't occur
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();
}
}

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

File diff suppressed because it is too large Load Diff

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

@@ -1,121 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/**
* @author daniels
* This Class represents a parsed node in the GF AST.
* It knows about types, bound variables, funs.
* But nothing about printnames. That's what AstNodeData is for.
*/
class GfAstNode {
/**
* contains the types of the bound variables in the order of their occurence
*/
protected final String[] boundTypes;
/**
* contains the names of the bound variables in the order of their occurence
*/
protected final String[] boundNames;
/**
* The type of this AST node
*/
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;
}
/**
* The constraint attached to this node
*/
public final String constraint;
/**
* 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(" : ");
String typeString = this.line.substring(index + 3);
final int constraintIndex = typeString.indexOf(" {");
if (constraintIndex > -1) {
this.constraint = typeString.substring(constraintIndex + 1).trim();
this.type = typeString.substring(0, constraintIndex).trim();
} else {
this.constraint = "";
this.type = typeString;
}
String myFun = this.line.substring(0, index);
if (myFun.startsWith("\\(")) {
final int end = myFun.lastIndexOf(") -> ");
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;
}
}

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

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

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

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

46
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GrammarFilter.java
View File

@@ -1,46 +0,0 @@
//Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.io.File;
import javax.swing.filechooser.*;
public class GrammarFilter extends FileFilter {
// Accept all directories and all gf, gfcm 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.gfcm)) {
return true;
} else {
return false;
}
}
return false;
}
// The description of this filter
public String getDescription() {
return "Just Grammars (*.gf, *.gfcm)";
}
}

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

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

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

@@ -1,141 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.HashSet;
/**
* @author daniels
*
* This class represents a fake command, i.e. nothing is send to GF here.
* Instead this class acts more like a placeholder for the input dialog.
* This dialog is handled in GFEditor2 when a InputCommand is executed.
* Reason: No GUI stuff in the command.
*/
class InputCommand extends GFCommand {
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;
}
/**
* stores the entered values, so they can be offered to the user
* the next time, in case, he wants them again.
*/
protected final HashSet enteredValues = new HashSet();
/**
* the text that is to be displayed as the tooltip
*/
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).
* If that is possible, the converted object is saved
* in enteredValues for later redisplay for the user.
* @param o The String the user has typed
* @param reason If the entered String is not parseable as the expected
* type, an error message is appended to this StringBuffer, so better
* 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() + "\"";
}
}
if (result != null) {
this.enteredValues.add(result);
}
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;
}
}

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

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

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

@@ -1,157 +0,0 @@
//Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/**
* 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.
*/
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;
}
/**
* Creates a position string in Haskell notation for the argument
* number nr of this node.
* @param nr The number of the wanted argument
* @return the position string for the nrth child
*/
public String childPosition(int nr) {
return calculateChildPosition(this.position, nr);
}
/**
* Creates a position string in Haskell notation for the argument
* number nr for the position pos
* @param pos The position of the to be parent
* @param nr The number of the wanted argument
* @return the position string for the nrth child of pos
*/
protected static String calculateChildPosition(String pos, int nr) {
if ("[]".equals(pos)) {
return "[" + nr + "]";
} else {
return pos.trim().substring(0, pos.length() - 1) + "," + nr + "]";
}
}
/**
* Creates a position string in Haskell notation for the argument
* number nr for the position pos' parent, i.e. brethren number nr.
* Example: calculateBrethrenPosition("[0,0,1]", 3).equals("[0,0,3]")
* @param pos The position of a brethren of the wanted
* @param nr The number of the wanted brethren
* @return the position string for the nrth brother of pos
*/
protected static String calculateBrethrenPosition(String pos, int nr) {
if ("[]".equals(pos)) {
return "[]"; //no brethren possible here
} else if (pos.lastIndexOf(',') == -1) {
return "[" + nr + "]"; //one below top
} else {
final String newPos = pos.substring(0, pos.lastIndexOf(',') + 1) + nr + "]";
return newPos;
}
}
/**
* compares two position strings and returns true, if superPosition is
* a prefix of subPosition, that is, if subPosition is in a subtree of
* superPosition
* @param superPosition the position String in Haskell notation
* ([0,1,0,4]) of the to-be super-branch of subPosition
* @param subPosition the position String in Haskell notation
* ([0,1,0,4]) of the to-be (grand-)child-branch of superPosition
* @return true iff superPosition denotes an ancestor of subPosition
*/
public static boolean isSubtreePosition(final LinPosition superPosition, final LinPosition subPosition) {
if (superPosition == null || subPosition == null) {
return false;
}
String superPos = superPosition.position;
String subPos = subPosition.position;
if (superPos.length() < 2 || subPos.length() < 2 ) {
return false;
}
superPos = superPos.substring(1, superPos.length() - 1);
subPos = subPos.substring(1, subPos.length() - 1);
boolean result = subPos.startsWith(superPos);
return result;
}
/**
* Returns the biggest position of first and second.
* Each word in the linearization area has the corresponding
* position in the tree. The position-notion is taken from
* GF-Haskell, where empty position ("[]")
* represents tree-root, "[0]" represents first child of the root,
* "[0,0]" represents the first grandchild of the root etc.
* So comparePositions("[0]","[0,0]")="[0]"
*/
public static String maxPosition(String first, String second) {
String common ="[]";
int i = 1;
while ((i<Math.min(first.length()-1,second.length()-1))&&(first.substring(0,i+1).equals(second.substring(0,i+1)))) {
common=first.substring(0,i+1);
i+=2;
}
if (common.charAt(common.length()-1)==']') {
return common;
} else {
return common+"]";
}
}
/**
* @return The Haskell position string for the parent of this position.
* If self is already the top node, [] is returned.
*/
public String parentPosition() {
if (this.position.equals("[]")) {
return this.position;
} else if (this.position.lastIndexOf(',') == -1) {
return "[]"; //one below top
} else {
final String newPos = this.position.substring(0, this.position.lastIndexOf(',')) + "]";
return newPos;
}
}
public String toString() {
return position + (correctPosition ? " correct" : " incorrect");
}
}

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

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

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

@@ -1,85 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/**
* @author daniels
* 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 {
/**
* Since LinkCommand is not a real command, that is sent to GF,
* most fields are given dummy values here.
* The subcat is assigned its full display name and tooltip
* @param subcat The subcategory of the menu behind this command
* @param manager The PrintnameManager, that can map subcat to its
* full name
*/
public LinkCommand(final String subcat, final PrintnameManager manager) {
this.command = subcat;
this.newSubcat = false;
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;
}
}

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

@@ -1,84 +0,0 @@
//Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
/**
* 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, daniels
*/
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;
/**
* the concrete grammar (or better, its linearization)
* this MarkedArea belongs to
*/
final public String language;
/**
* 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 begin The starting position of the stored words
* @param end The ending position of the stored words
* @param position The position in the AST
* @param words The actual text of this area
* @param htmlBegin the start index in the HTML area
* @param htmlEnd the end index in the HTML area
* @param language the language of the current linearization
*/
public MarkedArea(int begin, int end, LinPosition position, String words, int htmlBegin, int htmlEnd, String language) {
this.begin = begin;
this.end = end;
this.position = position;
this.words = words;
this.language = language;
this.htmlBegin = htmlBegin;
this.htmlEnd = htmlEnd;
}
public String toString() {
return begin + " - " + end + " : " + position + " = '" + words + "' ; HTML: " + htmlBegin + " - " + htmlEnd;
}
}

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

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

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

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

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

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

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

@@ -1,569 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.Hashtable;
import java.util.Vector;
import java.util.logging.*;
/**
* @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 {
private static Logger subcatLogger = Logger.getLogger(Printname.class.getName());
/**
* delete is always the same and only consists of one letter, therefore static.
*/
public static final Printname delete = new Printname("d", "delete current sub-tree", false);
/**
* The ac command i always the same, therefore static
*/
public static final Printname addclip = new Printname("ac", "add to clipboard\\$<html>adds the current subtree to the clipboard.<br>It is offered in the refinement menu if the expected type fits to the one of the current sub-tree.</html>", false);
/**
* @param arg The number of the argument,
* that will take the place of the selected fun
* @return a Printname for the 'ph arg' command
*/
public static Printname peelHead(int arg) {
final String cmd = "ph " + arg;
final String show = "peel head " + arg + "\\$removes this fun and moves its " + (arg + 1) + ". argument at its place instead";
return new Printname(cmd, show, true);
}
/**
* the type of the fun behind that printname (if applicable)
*/
protected final String type;
/**
* If the command type will already
* be present in the display name and does not need to be added.
*/
protected final boolean funPresent;
/**
* 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 = "\\#";
/**
* If that follows "\#" in the parameter descriptions, then do an
* auto-coerce when this param is meta and selected
*/
public final static String AUTO_COERCE = "!";
/**
* the name of the fun that is used in this command
*/
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.fine(e.getLocalizedMessage());
}
return name;
}
/**
* contains the descriptions of the paramters of this function (String).
* Parallel with paramNames
*/
protected final Vector paramTexts = new Vector();
/**
* tells, whether the nth parameter should be auto-coerced
* @param n the number of the parameter in question
* @return whether the nth parameter should be auto-coerced
*/
public boolean getParamAutoCoerce(int n) {
boolean result = false;
try {
result = ((Boolean)this.paramAutoCoerce.get(n)).booleanValue();
} catch (ArrayIndexOutOfBoundsException e) {
subcatLogger.fine(e.getLocalizedMessage());
}
return result;
}
/**
* stores for the parameters whether they should be auto-coerced or not.
* parallel with paramNames
*/
protected final Vector paramAutoCoerce = new Vector();
/**
* Creates a Printname for a normal GF function
* @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
* @param type The type of this fun.
* If null, it won't be displayed in the refinement menu.
*/
public Printname(String myFun, String myPrintname, Hashtable myFullnames, String type) {
myFun = myFun.trim();
myPrintname = myPrintname.trim();
this.printname = myPrintname;
this.subcatNameHashtable = myFullnames;
this.type = type;
if (myFullnames == null) {
//if the menu language is abstract, no fullnames are loaded
//and the fun will be in the used showname
this.funPresent = true;
} else {
this.funPresent = false;
}
//parse the fun name
{
int index = myFun.indexOf('.');
if (index > -1) {
//a valid fun name must not be empty
this.fun = myFun.substring(index + 1);
this.module = myFun.substring(0, index);
} else {
this.fun = myFun;
this.module = null;
}
}
//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];
boolean autocoerce = false;
if (AUTO_COERCE.equals(current.substring(0,1))) {
autocoerce = true;
//cut the !
current = current.substring(1);
}
int nameEnd = current.indexOf(' ');
int nameEnd2 = Utils.indexOfNotEscaped(current, PARAM);
if (nameEnd == -1) {
nameEnd = current.length();
}
String name = current.substring(0, nameEnd);
String description;
if (nameEnd < current.length() - 1) {
description = current.substring(nameEnd + 1).trim();
} else {
description = "";
}
this.paramNames.addElement(name);
this.paramTexts.addElement(description);
this.paramAutoCoerce.addElement(new Boolean(autocoerce));
}
myPrintname = myPrintname.substring(0, index);
}
}
//extract the subcategory part and cut that part
{
int index = Utils.indexOfNotEscaped(myPrintname, SUBCAT);
if (index > -1) {
String subcatPart = myPrintname.substring(index);
myPrintname = myPrintname.substring(0, index);
int indFull = subcatPart.indexOf('{');
if (indFull > -1) {
int indFullEnd = subcatPart.indexOf('}', indFull + 1);
if (indFullEnd == -1) {
indFullEnd = subcatPart.length();
}
String fullName = subcatPart.substring(indFull + 1, indFullEnd);
this.subcat = subcatPart.substring(0, indFull).trim();
this.subcatNameHashtable.put(this.subcat, fullName);
if (subcatLogger.isLoggable(Level.FINER)) {
subcatLogger.finer("new fullname '" + fullName + "' for category (shortname) '" + this.subcat + "'");
}
} 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
* @param funPresent If explanation already contains the fun.
* If true, the fun won't be printed in the refinement menu.
*/
protected Printname(String command, String explanation, boolean funPresent) {
this.fun = command;
this.subcatNameHashtable = null;
this.subcat = null;
this.module = "";
this.printname = explanation;
this.type = null;
this.funPresent = funPresent;
}
/**
* 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;
this.type = null;
this.funPresent = false;
}
/**
* 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;
if (original != null) {
result = new StringBuffer(original);
} else {
result = new StringBuffer();
}
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.fine(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;
}
/**
* looks up the description for parameter number 'which' and returns it.
* Returns null, if no parameter description is present.
* @param which The number of the parameter
* @return s.a.
*/
public String getParamDescription(int which) {
return (String)paramTexts.get(which);
}
/**
* 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, null);
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, null);
System.out.println("*" + pn.getTooltipText());
}
public String toString() {
return getDisplayText() + " \n " + getTooltipText() + " (" + this.paramNames.size() + ")";
}
}

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

@@ -1,112 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.io.IOException;
import java.util.Hashtable;
import java.util.logging.*;
/**
* @author daniels
* asks GF to print all available printnames, parses that list and generates
* the suiting Printname objects.
*/
public class PrintnameLoader extends AbstractProber {
private final static Logger nogger = Logger.getLogger(Printname.class.getName());
/**
* The PrintnameManager on which the read Printnames
* will be registered with their fun name.
*/
private final PrintnameManager printnameManager;
/**
* Here, the funs with their types get stored
*/
private final Hashtable funTypes = new Hashtable();
/**
* if the Printnames should have their type appended to their display names
*/
private final boolean loadTypes;
/**
* an initializing constructor, does nothing except setting fields
* @param gfCapsule the read/write encapsulation of GF
* @param pm The PrintnameManager on which the read Printnames
* will be registered with their fun name.
* @param withTypes true iff the Printnames should have their type
* appended to their display names
*/
public PrintnameLoader(GfCapsule gfCapsule, PrintnameManager pm, boolean withTypes) {
super(gfCapsule);
this.printnameManager = pm;
this.loadTypes = withTypes;
}
/**
* 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 = gfCapsule.fromProc.readLine();
if (nogger.isLoggable(Level.FINER)) {
nogger.finer("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 = Linearization.unescapeTextFromGF(result);
this.printnameManager.addNewPrintnameLine(result, this.funTypes);
}
result = gfCapsule.fromProc.readLine();
if (nogger.isLoggable(Level.FINER)) {
nogger.finer("1 " + result);
}
}
if (nogger.isLoggable(Level.FINER)) {
nogger.finer("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.
*/
protected void readPrintnames(String lang) {
//before, we want the types to be read.
if (this.loadTypes) {
TypesLoader tl = new TypesLoader(gfCapsule, this.funTypes);
tl.readTypes();
}
//prints the printnames of the last loaded grammar,
String sendString = "gf pg -printer=printnames";
if (lang != null && !("".equals(lang))) {
sendString = sendString + " -lang=" + lang;
}
nogger.fine("collecting printnames :" + sendString);
send(sendString);
readGfedit();
}
}

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

@@ -1,174 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.Hashtable;
import java.util.logging.*;
/**
* @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 {
/**
* This constructor is a bit of a hack.
* It puts the \%SELF subcat into this.printnames.
* This subcat does not appear in the grammars and thus is
* introduced here. If it is defined there although, this
* definition is used. So it does not hurt.
*/
public PrintnameManager() {
this.subcatNames.put(SELF_SUBCAT, "properties of self\\$shortcuts to the properties of self, that have a fitting type");
}
/**
* The name of the subcat, that is used for the easy property access
* of self.
*/
static final String SELF_SUBCAT = "\\%SELF";
private static Logger logger = Logger.getLogger(Printname.class.getName());
protected final static String frontMatter = "printname fun ";
/**
* 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"
* @param funTypes contains funs, mapped to their types
*/
public void addNewPrintnameLine(String line, Hashtable funTypes) {
line = removePluses(line);
//remove "printname fun " (the frontMatter)
final int index = line.indexOf(frontMatter);
line = line.substring(index + frontMatter.length()).trim();
//extract fun name
final int endFun = line.indexOf(' ');
final String fun = line.substring(0, endFun);
final String type = (String)funTypes.get(fun);
//extract printname
String printname = line.substring(line.indexOf('"') + 1, line.lastIndexOf('"'));
addNewPrintname(fun, printname, type);
}
/**
* 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, String type) {
if (logger.isLoggable(Level.FINER)) {
logger.finer("addNewPrintname, myFun = '" + myFun + "' , myPrintname = '" + myPrintname + "'");
}
Printname printname = new Printname(myFun, myPrintname, this.subcatNames, type);
if (logger.isLoggable(Level.FINER)) {
logger.finer("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.fine("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));
}
}

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

@@ -1,200 +0,0 @@
//Copyright (c) Janna Khegai 2004, Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.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 java.util.logging.*;
/**
* Takes care of reading in Strings that are to be parsed and terms.
* @author daniels
*
*/
class ReadDialog implements ActionListener{
/** XML parsing debug messages */
private static Logger xmlLogger = Logger.getLogger(GFEditor2.class.getName() + "_XML");
/** The window to which this class belongs */
private final GFEditor2 owner;
/** is the main thing of this class */
private final JDialog readDialog;
/** main area of the Read dialog (content pane)*/
private final JPanel inputPanel = new JPanel();
/** OK, Cancel, Browse in the Read dialog */
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) */
private final JFileChooser fc = new JFileChooser("./");
/**
* if a user sends a custom command to GF, he might want to do this
* again with the same command.
* 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 ) {
if (termReadButton.isSelected()) {
termInput = inputField.getText();
if (termInput.indexOf(File.separatorChar)==-1){
owner.send("[t] g "+termInput);
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("sending term string");
} else {
owner.send("[t] tfile "+termInput);
if (xmlLogger.isLoggable(Level.FINER)) {
xmlLogger.finer("sending file term: "+termInput);
}
}
} else { //String selected
parseInput = inputField.getText();
if (parseInput.indexOf(File.separatorChar)==-1){
owner.send("[t] p "+parseInput);
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("sending parse string: "+parseInput);
}
else {
owner.send("[t] pfile "+parseInput);
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("sending file parse string: "+parseInput);
}
}
readDialog.setVisible(false);
}
}
}

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

@@ -1,255 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.HashSet;
import java.util.HashMap;
import java.util.logging.*;
/**
* @author daniels
* This class represents a command, that is sent to GF.
* TODO Refactor the chain command stuff out of this class and make it a subclass
*/
class RealCommand extends GFCommand {
/**
* maps shorthands to fullnames
*/
private final static HashMap fullnames = new HashMap();
private final static Logger logger = Logger.getLogger(Printname.class.getName());
/**
* The number of undo steps that is needed to undo this fun call
*/
public final int undoSteps;
/**
* The text that GF sent to describe the command
*/
protected final String showText;
protected final String subcat;
/**
* Creates a Command that stands for a GF command, no link command
* sets all the attributes of this semi-immutable class.
* @param myCommand the actual GF command
* @param processedSubcats
* @param manager maps funs to previously read Printnames.
* Thus needs to be the same object.
* @param myShowText The text GF prints in the show part of the XML
* which should be the command followed by the printname
* @param mlAbstract is true, iff the menu language is set to Abstract
* Then no preloaded printnames are used.
* @param toAppend will be appended to the command, that is sent to GF.
* Normally, toAppend will be the empty String "".
* But it can be a chain command's second part.
* It will not be shown to the user.
*/
public RealCommand(final String myCommand, final HashSet processedSubcats, final PrintnameManager manager, final String myShowText, final boolean mlAbstract, final String toAppend) {
this(myCommand, processedSubcats, manager, myShowText, mlAbstract, toAppend, 1, null, null);
}
/**
* Creates a Command that stands for a GF command, no link command
* sets all the attributes of this semi-immutable class.
* @param myCommand the actual GF command
* @param processedSubcats
* @param manager maps funs to previously read Printnames.
* Thus needs to be the same object.
* @param myShowText The text GF prints in the show part of the XML
* which should be the command followed by the printname
* @param mlAbstract is true, iff the menu language is set to Abstract
* Then no preloaded printnames are used.
* @param toAppend will be appended to the command, that is sent to GF.
* Normally, toAppend will be the empty String "".
* But it can be a chain command's second part.
* It will not be shown to the user.
* @param undoSteps The number of undo steps that is needed to undo this fun call
* @param printnameFun If the fun, that selects the printname, should not be read from
* myCommand. For single commands, this is the only fun. For chain command, the last is
* taken. With this parameter, this behaviour can be overwritten
* @param subcat Normally, every fun has its own Printname, which has a fixed
* category. Sometimes, for the properies of self for example,
* this should be overwritten. If null, the subcat from the printname is used.
*/
public RealCommand(final String myCommand, final HashSet processedSubcats, final PrintnameManager manager, final String myShowText, final boolean mlAbstract, String toAppend, int undoSteps, String printnameFun, String subcat) {
if (fullnames.isEmpty()) {
fullnames.put("w", "wrap");
fullnames.put("r", "refine");
fullnames.put("ch", "change head");
fullnames.put("rc", "refine from history:");
fullnames.put("ph", "peel head");
}
if (logger.isLoggable(Level.FINEST)) {
logger.finest("new RealCommand: " + myCommand);
}
//if we have a ChainCommand, but undoSteps is just 1, count the undoSteps.
if ((undoSteps == 1) && (myCommand.indexOf(";;") > -1)) {
int occ = Utils.countOccurances(Utils.removeQuotations(myCommand), ";;") + 1;
this.undoSteps = occ;
} else {
this.undoSteps = undoSteps;
}
this.command = myCommand.trim();
this.showText = myShowText;
this.subcat = subcat;
//handle chain commands.
//Only the last command counts for the printname selection
final String lastCommand;
if (this.undoSteps > 1) {
//TODO: sth. like refine " f ;;d" ;; mp [2] will break here.
final int chainIndex = this.command.lastIndexOf(";;");
lastCommand = this.command.substring(chainIndex + 2).trim();
} else {
lastCommand = this.command;
}
//extract command type
int ind = lastCommand.indexOf(' ');
if (ind > -1) {
this.commandType = lastCommand.substring(0, ind);
} else {
this.commandType = lastCommand;
}
//extract the argument position for wrapping commands and cut that part
if (this.commandType.equals("w") || this.commandType.equals("ph")) {
int beforeNumber = lastCommand.lastIndexOf(' ');
int protoarg;
try {
String argumentAsString = lastCommand.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 = lastCommand.indexOf(' ');
int afterPos = lastCommand.lastIndexOf(' ');
if (beforePos > -1 && afterPos > beforePos) {
this.funName = lastCommand.substring(beforePos + 1, afterPos);
} else {
this.funName = null;
}
} else {
int beforePos = lastCommand.indexOf(' ');
if (beforePos > -1) {
this.funName = lastCommand.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("rc")) {
String subtree = this.showText.substring(3);
this.printname = new Printname(this.getCommand(), subtree + "\\$paste the previously copied subtree here<br>" + subtree, false);
} else if (this.commandType.equals("ph")) {
this.printname = Printname.peelHead(this.argument);
} else if (mlAbstract) {
//create a new Printname
this.printname = new Printname(funName, myShowText, null, null);
} else { //standard case
if (printnameFun == null) {
this.printname = manager.getPrintname(funName);
} else {
//overwrite mode. Until now, only for properties of self.
this.printname = manager.getPrintname(printnameFun);
}
}
if (this.getSubcat() != null) {
if (processedSubcats.contains(this.getSubcat())) {
newSubcat = false;
} else {
newSubcat = true;
processedSubcats.add(this.getSubcat());
}
} else {
newSubcat = false;
}
//now append toAppend before it is too late.
//Only now, since it must not interfere with the things above.
if (toAppend != null) {
this.command += toAppend;
}
}
/**
* the text that is to be displayed in the refinement lists
*/
public String getDisplayText() {
String result = "";
if (this.printname.funPresent) {
result = this.printname.getDisplayText();
} else {
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;
}
if (this.printname.type != null) {
result = result + " : " + this.printname.type;
}
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;
}
/**
* returns the subcat of this command
*/
public String getSubcat() {
if (this.subcat == null) {
return this.printname.getSubcat();
} else {
//special case, only for properties of self so far
return this.subcat;
}
}
}

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

@@ -1,68 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.logging.*;
/**
* @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 extends AstNodeData {
protected final Printname printname;
/**
* 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
* @param pos The position in the GF AST of this node in Haskell notation
* @param selected if this is the selected node in the GF AST
* @param constraint A constraint from a parent node, that also
* applies for this node.
*/
public RefinedAstNodeData(Printname pname, GfAstNode node, String pos, boolean selected, String constraint) {
super(node, pos, selected, constraint);
this.printname = pname;
if (logger.isLoggable(Level.FINEST)) {
logger.finest(this.toString() + " - " + position);
}
}
/**
* @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;
}
}
}

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

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

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

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

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

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

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

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

84
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/SelfResultProber.java
View File

@@ -1,84 +0,0 @@
package de.uka.ilkd.key.ocl.gf;
import java.util.logging.*;
/**
* asks GF if the given commands leads to a situation, where
* something could be filled in automatically.
* This class is meant for self and result.
* @author daniels
*/
class SelfResultProber extends AbstractProber {
/**
* This field is true in the beginning of each run, and
* set to false, if the focus position when checking is found
* to be open.
*/
protected boolean autocompleted = true;
protected static Logger nogger = Logger.getLogger(SelfResultProber.class.getName());
/**
* A constructor which sets some fields
* @param gfCapsule The encapsulation of the running GF process
*/
public SelfResultProber(GfCapsule gfCapsule) {
super(gfCapsule);
}
/**
* asks GF if the given commands leads to a situation, where
* something could be filled in automatically.
* This function is meant for self and result.
* IMPORTANT: Must be called <b>after</b> &lt;/gfedit&gt;
* when no other method reads sth. from GF.
* It uses the same GF as everything else, since it tests if
* sth. is possible there.
* @param gfCommand the command to be tested.
* One has to chain a mp command to make GF go to the right place afterwards
* @param chainCount The number of chained commands in gfCommand.
* So many undos are done to clean up afterwards.
* @return true iff sth. could be filled in automatically
*/
public boolean isAutoCompletable(String gfCommand, int chainCount) {
this.autocompleted = true;
send(gfCommand);
readGfedit();
final boolean result = this.autocompleted;
this.autocompleted = true;
//clean up and undo
send("u " + chainCount);
readAndIgnore();
if (nogger.isLoggable(Level.FINE)) {
nogger.fine(result + " is the result for: '" + gfCommand +"'");
}
return result;
}
/**
* Reads the tree child of the XML from beginning to end.
* Sets autocompleted to false, if the focus position is open.
*/
protected void readTree() {
String treeString = gfCapsule.readTree();
String[] treeArray = treeString.split("\\n");
for (int i = 0; i < treeArray.length; i++) {
String result = treeArray[i].trim();
if (result.startsWith("*")) {
result = result.substring(1).trim();
if (result.startsWith("?")) {
//the normal case, focus position open
this.autocompleted = false;
} else if ((i >= 6) //that we could be at the instance argument at all
&& (treeArray[i - 6].indexOf("coerce") > -1) //we are below a coerce
&& (treeArray[i - 3].trim().startsWith("?")) //the Subtype argument is not filled in
// The super argument cannot be OclAnyC or even unrefined, because then this
// method wouldn't have been called. Thus, the Subtype argument is unique.
){
//we are below a coerce, but self would have a non-suiting subtype
this.autocompleted = false;
}
}
}
}
}

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

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

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

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

71
src/JavaGUI2/de/uka/ilkd/key/ocl/gf/ToolTipCellRenderer.java
View File

@@ -1,71 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.awt.Component;
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 {
/**
* Returns a JLabel with a tooltip, which is given by the GFCommand
* @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;
}
}

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

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

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

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

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

@@ -1,120 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.io.IOException;
import java.util.Hashtable;
import java.util.logging.*;
/**
* @author daniels
* If the entries of the refinement menu should have to appear there with
* type information appended to them, then the printnames have to get this
* knowledge at the time of their creation.
* When the entries are displayed, the display text line of GF is *not* looked
* at. And even if it would be, it would mess up the architecture, that the
* printnames, and only they, are responsible for their linearization.
* Appending their type later on would break that architecture.
* So they have to be prepared.
*/
public class TypesLoader extends AbstractProber {
/**
* The hash in which the funs as keys and
* types as values get saved. Both are Strings.
*/
protected final Hashtable hashtable;
private static Logger nogger = Logger.getLogger(TypesLoader.class.getName());
/**
* @param gfCapsule the read/write encapsulation of the running GF
* @param myHashMap The hash in which the funs as keys and
* types as values get saved. Both are Strings.
*/
public TypesLoader(GfCapsule gfCapsule, Hashtable myHashMap) {
super(gfCapsule);
this.hashtable = myHashMap;
}
/**
* 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 = gfCapsule.fromProc.readLine();
if (nogger.isLoggable(Level.FINER)) {
nogger.finer("7 " + 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("fun ")) {
//unescape backslashes. Probably there are more
readType(result);
}
result = gfCapsule.fromProc.readLine();
if (nogger.isLoggable(Level.FINER)) {
nogger.finer("7 " + result);
}
}
if (nogger.isLoggable(Level.FINER)) {
nogger.finer("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.
*/
public void readTypes() {
//prints the last loaded grammar,
String sendString = "gf pg";
if (nogger.isLoggable(Level.FINE)) {
nogger.fine("collecting types :" + sendString);
}
send(sendString);
readGfedit();
}
/**
* Reads a fun line from pg and puts it into hashMap with the fun
* as the key and the type as the value
* @param line One line which describes the signature of a fun
*/
private void readType(String line) {
final int funStartIndex = 4; //length of "fun "
final String fun = line.substring(funStartIndex, line.indexOf(" : "));
final int typeStartIndex = line.indexOf(" : ") + 3;
final int typeEndIndex = line.lastIndexOf(" = ");
try {
final String type = line.substring(typeStartIndex, typeEndIndex);
this.hashtable.put(fun, type);
} catch (StringIndexOutOfBoundsException e) {
System.err.println("line: '" + line + "'");
System.err.println("fun: '" + fun + "'");
System.err.println("typeStartIndex: " + typeStartIndex);
System.err.println("typeEndIndex: " + typeEndIndex);
System.err.println(e.getLocalizedMessage());
}
}
}

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

@@ -1,64 +0,0 @@
//Copyright (c) Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.util.logging.*;
/**
* @author daniels
*
* represents an open, unrefined node in the AST.
* It knows, how it is called and described (tooltip).
*/
public class UnrefinedAstNodeData extends AstNodeData {
/**
* The tooltip that this node as a parameter should get
*/
protected final String paramTooltip;
/**
* For a child we have to know its name, its type and the tooltip
* @param pTooltip The tooltip that this node as a parameter should get
* @param node The GfAstNode for the current AST node, for which
* this AstNodeData is the data for.
* @param pos The position in the GF AST of this node in Haskell notation
* @param selected if this is the selected node in the GF AST
* @param constraint A constraint from a parent node, that also
* applies for this node.
*/
public UnrefinedAstNodeData(String pTooltip, GfAstNode node, String pos, boolean selected, String constraint) {
super(node, pos, selected, constraint);
this.paramTooltip = pTooltip;
if (logger.isLoggable(Level.FINEST)) {
logger.finest(this.toString() + " - " + position);
}
}
/**
* @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;
}
}

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

@@ -1,243 +0,0 @@
//Copyright (c) Kristofer Johanisson 2005, Hans-Joachim Daniels 2005
//
//This program is free software; you can redistribute it and/or modify
//it under the terms of the GNU General Public License as published by
//the Free Software Foundation; either version 2 of the License, or
//(at your option) any later version.
//
//This program is distributed in the hope that it will be useful,
//but WITHOUT ANY WARRANTY; without even the implied warranty of
//MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//GNU General Public License for more details.
//
//You can either finde the file LICENSE or LICENSE.TXT in the source
//distribution or in the .jar file of this application
package de.uka.ilkd.key.ocl.gf;
import java.io.File;
import java.util.logging.*;
import javax.swing.ProgressMonitor;
import java.util.Vector;
/**
* consists of a bunch of static methods, mostly for String
* @author daniels
*
*/
public class Utils {
private static Logger timeLogger = Logger.getLogger(Utils.class.getName() + ".timer");
private static Logger deleteLogger = Logger.getLogger(Utils.class.getName() + ".delete");
private static Logger stringLogger = Logger.getLogger(Utils.class.getName() + ".string");
private Utils() {
//non-instantiability enforced
}
public static final String gf = "gf";
public static final String gfcm = "gfcm";
/**
* 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.isLoggable(Level.FINER)) {
timeLogger.finer(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.isLoggable(Level.FINER)) {
deleteLogger.fine("scheduled for deletion: " + filename);
}
}
File file = new File(grammarsDir);
file.deleteOnExit();
file = file.getParentFile();
file.deleteOnExit();
}
/**
* 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, i + replacement.length())) {
sb.replace(i, i + toReplace.length(), replacement);
}
return sb.toString();
}
/**
* Removes all parts, that are inside "quotation marks" from s.
* Assumes no nesting of those, like in Java.
* " escaped with \ like \" do not count as quotation marks
* @param s The String, that possibly contains quotations
* @return a String described above, s without quotations.
*/
public static String removeQuotations(String s) {
if (s.indexOf('"') == -1) {
return s;
}
for (int begin = indexOfNotEscaped(s, "\""); begin > -1 ; begin = indexOfNotEscaped(s, "\"", begin)) {//yes, I want an unescaped '"'!
int end = indexOfNotEscaped(s, "\"", begin + 1);
if (end > -1) {
s = s.substring(0, begin) + s.substring(end + 1);
} else {
stringLogger.info("Strange String given: '" + s + "'");
s = s.substring(0, begin);
}
}
return s;
}
/**
* counts the occurances of toSearch in s
* @param s The String in which the search shall take place
* @param toSearch The String that should be counted
* @return the number of occurances, 0 if s is null
*/
public static int countOccurances(String s, String toSearch) {
if (s == null) {
return 0;
}
int result = 0;
for (int i = s.indexOf(toSearch); i > -1; i = s.indexOf(toSearch, i)) {
result++;
i += toSearch.length();
}
return result;
}
/**
* Takes an arbitrary Vector and executes toString on each element and
* puts these into a String[] of the same size as the Vector
* @param strings A Vector of Object, preferably String
* @return The Vector as a String[]
*/
public static String[] vector2Array(Vector strings) {
String[] result = new String[strings.size()];
for (int i = 0; i < strings.size(); i++) {
result[i] = strings.get(i).toString();
}
return result;
}
/**
* just replace sequences of spaces with one space
* @param s The string to be compacted
* @return the compacted result
*/
static String compactSpaces(String s) {
String localResult = new String();
boolean spaceIncluded = false;
for (int i = 0; i < s.length(); i++) {
char c = s.charAt(i);
if (c != ' ') { // include all non-spaces
localResult += String.valueOf(c);
spaceIncluded = false;
} else {// we have a space
if (!spaceIncluded) {
localResult += " ";
spaceIncluded = true;
} // else just skip
}
}
return localResult;
}
/**
* Replaces all occurances of toBeReplaced, that are not escaped by '\'
* with replacement
* @param working the String in which substrings should be replaced
* @param toBeReplaced The substring, that should be replaced by replacement
* @param replacement well, the replacement string
* @return The String with the replaced parts
*/
public static String replaceNotEscaped(String working, String toBeReplaced, String replacement) {
StringBuffer w = new StringBuffer(working);
for (int i = w.indexOf(toBeReplaced); i > -1 && i < w.length(); i = w.indexOf(toBeReplaced, i)) {
if (i == 0 || w.charAt(i - 1) != '\\') {
w.replace(i, i + toBeReplaced.length(), replacement);
i += replacement.length();
} else {
i += 1;
}
}
return w.toString();
}
}

BIN
src/JavaGUI2/gf-icon.gif
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 798 B

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

Binary file not shown.