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

Fixed double r 'refine ...' or even refine 'refine ...'

Browse Source
This commit is contained in:
hdaniels
2005-06-23 15:23:32 +00:00
parent 29b53fc0ce
commit 1a100c47e5
3 changed files with 30 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -589,6 +589,7 @@ KeyListener, FocusListener {
//Add listener to components that can bring up popup menus.
MouseListener popupListener2 = new PopupListener();
linearizationArea.addMouseListener(popupListener2);
htmlLinPane.addMouseListener(popupListener2);
//now for the menus

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

@@ -38,10 +38,15 @@ class Printname {
public static final Printname delete = new Printname("d", "delete current sub-tree");
public static final Printname addclip = new Printname("ac", "add to clipboard\\$<html>adds the current subtree to the clipboard.<br>It is offered in the refinement menu if the expected type fits to the one of the current sub-tree.</html>");
public static final Printname printhistory = new Printname("ph", "print history\\$prints all previous command in the linearization area");
public static final Printname printhistory = new Printname("ph", "peel head\\$removes this fun and moves its first argument at its place instead");
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
@@ -145,7 +150,8 @@ class Printname {
* @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 TODO
* @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();
@@ -153,7 +159,14 @@ class Printname {
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('.');
@@ -244,6 +257,7 @@ class Printname {
this.module = "";
this.printname = explanation;
this.type = null;
this.funPresent = false;
}
/**
@@ -259,6 +273,7 @@ class Printname {
this.module = null;
this.printname = bound;
this.type = null;
this.funPresent = false;
}
/** the text that is to be displayed in the refinement lists */

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

@@ -44,6 +44,7 @@ class RealCommand extends GFCommand {
public RealCommand(final String myCommand, final HashSet processedSubcats, final PrintnameManager manager, final String myShowText, final boolean mlAbstract) {
if (fullnames.isEmpty()) {
fullnames.put("w", "wrap");
fullnames.put("r", "refine");
fullnames.put("ch", "change head");
fullnames.put("rc", "refine from history:");
}
@@ -124,12 +125,16 @@ class RealCommand extends GFCommand {
/** the text that is to be displayed in the refinement lists */
public String getDisplayText() {
String result = "";
if (fullnames.containsKey(this.commandType)) {
result = fullnames.get(this.commandType) + " '";
}
result = result + this.printname.getDisplayText();
if (fullnames.containsKey(this.commandType)) {
result = result + "'";
if (this.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);