GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-05-20 08:32:50 -06:00
Code Issues Packages Projects Releases Wiki Activity

parsing via middle-click works now

Browse Source
This commit is contained in:
hdaniels
2005-06-29 17:53:04 +00:00
parent ffe5c1b999
commit 6b83de3263
5 changed files with 521 additions and 319 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -153,10 +153,11 @@ class Display {
* create an HtmlMarkedArea object, which is ready to be used in GFEditor2. * 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 toAdd The String that the to-be-produced MarkedArea should represent
* @param position The position String in Haskell notation * @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 * @return the HtmlMarkedArea object that represents the given information
* and knows about its beginning and end in the display areas. * and knows about its beginning and end in the display areas.
*/ */
protected HtmlMarkedArea addAsMarked(String toAdd, LinPosition position) { protected HtmlMarkedArea addAsMarked(String toAdd, LinPosition position, String language) {
/** the length of the displayed HTML before the current append */ /** the length of the displayed HTML before the current append */
int oldLengthHtml = 0; int oldLengthHtml = 0;
if (doHtml) { if (doHtml) {
@@ -198,7 +199,7 @@ class Display {
if (doText) { if (doText) {
newLengthText = this.linStagesText.lastElement().toString().length(); newLengthText = this.linStagesText.lastElement().toString().length();
} }
final HtmlMarkedArea hma = new HtmlMarkedArea(oldLengthText, newLengthText, position, toAdd, oldLengthHtml, newLengthHtml); final HtmlMarkedArea hma = new HtmlMarkedArea(oldLengthText, newLengthText, position, toAdd, oldLengthHtml, newLengthHtml, language);
return hma; return hma;
} }
/** /**

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

@@ -316,24 +316,13 @@ ActionListener{
if (GFEditor2.treeLogger.isLoggable(Level.FINER)) { if (GFEditor2.treeLogger.isLoggable(Level.FINER)) {
GFEditor2.treeLogger.finer("selection changed!"); GFEditor2.treeLogger.finer("selection changed!");
} }
maybeShowPopup(e); //for the popup or parse field, do the same as for the linearization areas
gfeditor.maybeShowPopup(e);
} }
public void mouseReleased(MouseEvent e) { public void mouseReleased(MouseEvent e) {
//nothing to be done here //nothing to be done here
} }
void maybeShowPopup(MouseEvent e) {
if (GFEditor2.treeLogger.isLoggable(Level.FINER)) {
GFEditor2.treeLogger.finer("may be show Popup!");
}
if (e.isPopupTrigger()) {
if (GFEditor2.treeLogger.isLoggable(Level.FINER)) {
GFEditor2.treeLogger.finer("changing menu!");
}
popup = gfeditor.producePopup();
popup.show(e.getComponent(), e.getX(), e.getY());
}
}
} }
public void actionPerformed(ActionEvent ae) { public void actionPerformed(ActionEvent ae) {

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

@@ -30,8 +30,7 @@ import java.net.MalformedURLException;
import java.util.logging.*; import java.util.logging.*;
import jargs.gnu.CmdLineParser; import jargs.gnu.CmdLineParser;
public class GFEditor2 extends JFrame implements ActionListener, CaretListener, public class GFEditor2 extends JFrame {
KeyListener, FocusListener {
/** the main logger for this class */ /** the main logger for this class */
protected static Logger logger = Logger.getLogger(GFEditor2.class.getName()); protected static Logger logger = Logger.getLogger(GFEditor2.class.getName());
@@ -83,12 +82,6 @@ KeyListener, FocusListener {
*/ */
public JTextField parseField = new JTextField("textField!"); public JTextField parseField = new JTextField("textField!");
/**
* to save the old selection before editing i field
* or the new selection?
*/
public String selectedText="";
/** /**
* The position of the focus, that is, the currently selected node in the AST * The position of the focus, that is, the currently selected node in the AST
*/ */
@@ -969,7 +962,7 @@ KeyListener, FocusListener {
if (linMarkingLogger.isLoggable(Level.FINER)) { if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("Less: "+jPosition+" and "+iPosition); linMarkingLogger.finer("Less: "+jPosition+" and "+iPosition);
} }
position = findMaxHtml(0,j); position = findMax(0,j);
if (linMarkingLogger.isLoggable(Level.FINER)) { if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTEDTEXT: "+position+"\n"); linMarkingLogger.finer("SELECTEDTEXT: "+position+"\n");
} }
@@ -1036,15 +1029,164 @@ KeyListener, FocusListener {
this.getContentPane().add(cpPanelScroll); this.getContentPane().add(cpPanelScroll);
coverPanel.setLayout(new BorderLayout()); coverPanel.setLayout(new BorderLayout());
linearizationArea.setToolTipText("Linearizations' display area"); linearizationArea.setToolTipText("Linearizations' display area");
linearizationArea.addCaretListener(this); linearizationArea.addCaretListener(new CaretListener() {
/**
* One can either click on a leaf in the lin area, or select a larger subtree.
* The corresponding tree node is selected.
*/
public void caretUpdate(CaretEvent e) {
String jPosition ="", iPosition="", position="";
MarkedArea jElement = null;
MarkedArea iElement = null;
int j = 0;
int i = htmlOutputVector.size() - 1;
int start = linearizationArea.getSelectionStart();
int end = linearizationArea.getSelectionEnd();
if (popUpLogger.isLoggable(Level.FINER)) {
popUpLogger.finer("CARET POSITION: "+linearizationArea.getCaretPosition()
+ "\n-> SELECTION START POSITION: "+start
+ "\n-> SELECTION END POSITION: "+end);
}
if (linMarkingLogger.isLoggable(Level.FINER)) {
if (end>0&&(end<linearizationArea.getText().length())) {
linMarkingLogger.finer("CHAR: "+linearizationArea.getText().charAt(end));
}
}
// not null selection:
if ((i>-1)&&(start<linearizationArea.getText().length()-1)) {
if (linMarkingLogger.isLoggable(Level.FINER))
for (int k = 0; k < htmlOutputVector.size(); k++) {
linMarkingLogger.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 (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.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 (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("Less: "+jPosition+" and "+iPosition);
}
position = findMax(0,j);
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTEDTEXT: "+position+"\n");
}
treeChanged = true;
send("mp "+position);
} else if (linMarkingLogger.isLoggable(Level.FINER)) { // before:
linMarkingLogger.finer("BEFORE vector of size: " + htmlOutputVector.size());
}
} else { // just:
iElement = (MarkedArea)htmlOutputVector.elementAt(i);
iPosition = iElement.position.position;
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTED TEXT Just: "+iPosition +" and "+jPosition+"\n");
}
position = findMax(i,j);
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTEDTEXT: "+position+"\n");
}
treeChanged = true;
send("mp "+position);
}
} 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 (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("MORE: "+iPosition+ " and "+jPosition);
}
position = findMax(i, htmlOutputVector.size()-1);
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTEDTEXT: "+position+"\n");
}
treeChanged = true;
send("mp "+position);
} else if (linMarkingLogger.isLoggable(Level.FINER)) { // after:
linMarkingLogger.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 (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("BIGGER: "+iPosition +" and "+jPosition+"\n"
+ "\n-> SELECTEDTEXT: []\n");
}
treeChanged = true;
send("mp []");
}
}//not null selection
}
});
linearizationArea.setEditable(false); linearizationArea.setEditable(false);
linearizationArea.setLineWrap(true); linearizationArea.setLineWrap(true);
linearizationArea.setWrapStyleWord(true); linearizationArea.setWrapStyleWord(true);
//linearizationArea.setSelectionColor(Color.green);
parseField.setFocusable(true); parseField.setFocusable(true);
parseField.addKeyListener(this); parseField.addKeyListener(new KeyListener() {
parseField.addFocusListener(this); /** Handle the key pressed event. */
public void keyPressed(KeyEvent e) {
int keyCode = e.getKeyCode();
if (keyLogger.isLoggable(Level.FINER)) {
keyLogger.finer("Key pressed: " + e.toString());
}
if (keyCode == KeyEvent.VK_ENTER) {
getLayeredPane().remove(parseField);
treeChanged = true;
send("p "+parseField.getText());
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("sending parse string: "+parseField.getText());
repaint();
} else if (keyCode == KeyEvent.VK_ESCAPE) {
getLayeredPane().remove(parseField);
repaint();
}
}
/**
* Handle the key typed event.
* We are not really interested in typed characters, thus empty
*/
public void keyTyped(KeyEvent e) {
//needed for KeyListener, but not used
}
/** Handle the key released event. */
public void keyReleased(KeyEvent e) {
//needed for KeyListener, but not used
}
});
parseField.addFocusListener(new FocusListener() {
public void focusGained(FocusEvent e) {
//do nothing
}
public void focusLost(FocusEvent e) {
getLayeredPane().remove(parseField);
repaint();
}
});
// System.out.println(output.getFont().getFontName()); // System.out.println(output.getFont().getFontName());
//Now for the command buttons in the lower part //Now for the command buttons in the lower part
@@ -1156,7 +1298,45 @@ KeyListener, FocusListener {
} }
}; };
refinementList.addMouseListener(mlRefinementList); refinementList.addMouseListener(mlRefinementList);
refinementList.addKeyListener(this); refinementList.addKeyListener(new KeyListener() {
/** Handle the key pressed event for the refinement list. */
public void keyPressed(KeyEvent e) {
int keyCode = e.getKeyCode();
if (keyLogger.isLoggable(Level.FINER)) {
keyLogger.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); refinementSubcatList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
@@ -1168,7 +1348,35 @@ KeyListener, FocusListener {
} }
}; };
refinementSubcatList.addMouseListener(mlRefinementSubcatList); refinementSubcatList.addMouseListener(mlRefinementSubcatList);
refinementSubcatList.addKeyListener(this); refinementSubcatList.addKeyListener(new KeyListener() {
/** Handle the key pressed event. */
public void keyPressed(KeyEvent e) {
int keyCode = e.getKeyCode();
if (keyLogger.isLoggable(Level.FINER)) {
keyLogger.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
}
});
newCategoryMenu.addActionListener(new ActionListener() { newCategoryMenu.addActionListener(new ActionListener() {
@@ -1184,7 +1392,6 @@ KeyListener, FocusListener {
}); });
save.setAction(saveAction); save.setAction(saveAction);
open.setAction(openAction); open.setAction(openAction);
gfCommand.addActionListener(this);
newCategoryMenu.setFocusable(false); newCategoryMenu.setFocusable(false);
save.setFocusable(false); save.setFocusable(false);
@@ -1230,20 +1437,15 @@ KeyListener, FocusListener {
rightMeta.addActionListener(naviActionListener); rightMeta.addActionListener(naviActionListener);
leftMeta.addActionListener(naviActionListener); leftMeta.addActionListener(naviActionListener);
left.addActionListener(naviActionListener); left.addActionListener(naviActionListener);
read.addActionListener(this);
modify.addActionListener(new ActionListener() { modify.addActionListener(new ActionListener() {
public void actionPerformed(ActionEvent ae) { public void actionPerformed(ActionEvent ae) {
if (!modify.getSelectedItem().equals("Modify")) { if (!modify.getSelectedItem().equals("Modify")) {
treeChanged = true; treeChanged = true;
send("c " + modify.getSelectedItem()); send("c " + modify.getSelectedItem());
modify.setSelectedIndex(0); modify.setSelectedIndex(0);
}
} }
}
}); });
//mode.addActionListener(this);
alpha.addActionListener(this);
random.addActionListener(this);
top.setFocusable(false); top.setFocusable(false);
right.setFocusable(false); right.setFocusable(false);
@@ -1893,6 +2095,13 @@ KeyListener, FocusListener {
Object next = it.next(); Object next = it.next();
this.listModel.addElement(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());
} }
/** /**
@@ -2138,8 +2347,9 @@ KeyListener, FocusListener {
* Then control is given to appendMarked, which does the display * Then control is given to appendMarked, which does the display
* @param clickable true iff the correspondent display area should be clickable * @param clickable true iff the correspondent display area should be clickable
* @param doDisplay true iff the linearization should be displayed. * @param doDisplay true iff the linearization should be displayed.
* @param language the current linearization language
*/ */
protected StringBuffer outputAppend(boolean clickable, boolean doDisplay){ protected StringBuffer outputAppend(boolean clickable, boolean doDisplay, String language){
final StringBuffer linCollector = new StringBuffer(); final StringBuffer linCollector = new StringBuffer();
//result=result.replace('\n',' '); //result=result.replace('\n',' ');
if (linMarkingLogger.isLoggable(Level.FINER)) { if (linMarkingLogger.isLoggable(Level.FINER)) {
@@ -2177,12 +2387,12 @@ KeyListener, FocusListener {
this.result = replaceNotEscaped(this.result, "<focus", "<subtree"); this.result = replaceNotEscaped(this.result, "<focus", "<subtree");
this.result = replaceNotEscaped(this.result, "</focus", "</subtree"); this.result = replaceNotEscaped(this.result, "</focus", "</subtree");
String appended = appendMarked(this.result + '\n', clickable, doDisplay); String appended = appendMarked(this.result + '\n', clickable, doDisplay, language);
linCollector.append(appended); linCollector.append(appended);
} else {//no focus at all (message?): } else {//no focus at all (message?):
this.focusPosition = null; this.focusPosition = null;
// beware the side-effects! They are, what counts // beware the side-effects! They are, what counts
linCollector.append(appendMarked(this.result + '\n', clickable, doDisplay)); linCollector.append(appendMarked(this.result + '\n', clickable, doDisplay, language));
} }
// if (logger.isLoggable(Level.FINER)) { // if (logger.isLoggable(Level.FINER)) {
// logger.finer("collected appended linearizations:\n" + linCollector.toString()); // logger.finer("collected appended linearizations:\n" + linCollector.toString());
@@ -2250,7 +2460,7 @@ KeyListener, FocusListener {
} }
// we want the side-effects of outputAppend // we want the side-effects of outputAppend
final boolean isAbstract = "Abstract".equals(language); final boolean isAbstract = "Abstract".equals(language);
String linResult = outputAppend(!isAbstract, visible).toString(); String linResult = outputAppend(!isAbstract, visible, language).toString();
if (visible) { if (visible) {
firstLin = false; firstLin = false;
} }
@@ -2506,14 +2716,6 @@ KeyListener, FocusListener {
} }
} }
/**
* the big ActionListener method that does nearly all user interaction
*/
public void actionPerformed(ActionEvent ae) {
//all gone into smaller inner classes
}
/** /**
* Writes the given String to the given Filename * Writes the given String to the given Filename
* @param str the text to be written * @param str the text to be written
@@ -2714,66 +2916,6 @@ KeyListener, FocusListener {
} }
/** Handle the key pressed event. */
public void keyPressed(KeyEvent e) {
int keyCode = e.getKeyCode();
Object obj = e.getSource();
if (keyLogger.isLoggable(Level.FINER)) {
keyLogger.finer("Key pressed: " + e.toString());
}
if (obj==refinementSubcatList) {
if (keyCode == KeyEvent.VK_ENTER) {
listAction(refinementSubcatList, refinementSubcatList.getSelectedIndex(), true);
} else if (keyCode == KeyEvent.VK_LEFT) {
refinementList.requestFocusInWindow();
refinementSubcatList.clearSelection();
refinementList.setSelectionBackground(refinementSubcatList.getSelectionBackground());
}
} else if (obj == refinementList) {
int index = refinementList.getSelectedIndex();
if (index == -1) {
//nothing selected, so nothing to be seen here, please move along
} else if (keyCode == KeyEvent.VK_ENTER) {
listAction(refinementList, refinementList.getSelectedIndex(), true);
} else if (keyCode == KeyEvent.VK_DOWN && index < listModel.getSize() - 1) {
listAction(refinementList, index + 1, false);
} else if (keyCode == KeyEvent.VK_UP && index > 0) {
listAction(refinementList, index - 1, false);
} else if (keyCode == KeyEvent.VK_RIGHT) {
if (refinementSubcatList.getModel().getSize() > 0) {
refinementSubcatList.requestFocusInWindow();
refinementSubcatList.setSelectedIndex(0);
refinementList.setSelectionBackground(Color.GRAY);
}
}
} else if (obj==parseField) {
if (keyCode == KeyEvent.VK_ENTER) {
getLayeredPane().remove(parseField);
treeChanged = true;
send("p "+parseField.getText());
if (xmlLogger.isLoggable(Level.FINER)) xmlLogger.finer("sending parse string: "+parseField.getText());
repaint();
} else if (keyCode == KeyEvent.VK_ESCAPE) {
getLayeredPane().remove(parseField);
repaint();
}
}
}
/**
* Handle the key typed event.
* We are not really interested in typed characters, thus empty
*/
public void keyTyped(KeyEvent e) {
//needed for KeyListener, but not used
}
/** Handle the key released event. */
public void keyReleased(KeyEvent e) {
//needed for KeyListener, but not used
}
/** /**
* Returns the biggest position of first and second. * Returns the biggest position of first and second.
* Each word in the linearization area has the corresponding * Each word in the linearization area has the corresponding
@@ -2813,148 +2955,7 @@ KeyListener, FocusListener {
return max; return max;
} }
/**
* Returns the widest position (see comments to comparePositions)
* covered in the string from begin to end in htmlLinPane
* @param begin
* @param end
* @return the position in GF Haskell notation (hdaniels guesses)
*/
private String findMaxHtml(int begin, int end) {
String max = (((HtmlMarkedArea)this.htmlOutputVector.elementAt(begin)).position).position;
for (int i = begin+1; i <= end; i++)
max = comparePositions(max,(((MarkedArea)htmlOutputVector.elementAt(i)).position).position);
return max;
}
/**
* One can either click on a leaf in the lin area, or select a larger subtree.
* The corresponding tree node is selected.
*/
public void caretUpdate(CaretEvent e)
{
String jPosition ="", iPosition="", position="";
MarkedArea jElement = null;
MarkedArea iElement = null;
int j = 0;
int i = this.htmlOutputVector.size()-1;
int start = linearizationArea.getSelectionStart();
int end = linearizationArea.getSelectionEnd();
if (popUpLogger.isLoggable(Level.FINER)) {
popUpLogger.finer("CARET POSITION: "+linearizationArea.getCaretPosition()
+ "\n-> SELECTION START POSITION: "+start
+ "\n-> SELECTION END POSITION: "+end);
}
if (linMarkingLogger.isLoggable(Level.FINER)) {
if (end>0&&(end<linearizationArea.getText().length())) {
linMarkingLogger.finer("CHAR: "+linearizationArea.getText().charAt(end));
}
}
// not null selection:
if ((i>-1)&&(start<linearizationArea.getText().length()-1))
{
if (linMarkingLogger.isLoggable(Level.FINER))
for (int k=0; k<this.htmlOutputVector.size(); k++) {
linMarkingLogger.finer("element: "+k+" begin "+((MarkedArea)this.htmlOutputVector.elementAt(k)).begin+" "
+ "\n-> end: "+((MarkedArea)this.htmlOutputVector.elementAt(k)).end+" "
+ "\n-> position: "+(((MarkedArea)this.htmlOutputVector.elementAt(k)).position).position+" "
+ "\n-> words: "+((MarkedArea)this.htmlOutputVector.elementAt(k)).words);
}
// localizing end:
while ((j< this.htmlOutputVector.size())&&(((MarkedArea)this.htmlOutputVector.elementAt(j)).end < end))
j++;
// localising start:
while ((i>=0)&&(((MarkedArea)this.htmlOutputVector.elementAt(i)).begin > start))
i--;
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("i: "+i+" j: "+j);
}
if ((j<this.htmlOutputVector.size()))
{
jElement = (MarkedArea)this.htmlOutputVector.elementAt(j);
jPosition = jElement.position.position;
// less & before:
if (i==-1)
{ // less:
if (end>=jElement.begin)
{
iElement = (MarkedArea)this.htmlOutputVector.elementAt(0);
iPosition = iElement.position.position;
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("Less: "+jPosition+" and "+iPosition);
}
position = findMax(0,j);
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTEDTEXT: "+position+"\n");
}
treeChanged = true;
send("mp "+position);
}
// before:
else
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("BEFORE vector of size: "+this.htmlOutputVector.size());
}
}
// just:
else
{
iElement = (MarkedArea)this.htmlOutputVector.elementAt(i);
iPosition = iElement.position.position;
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTED TEXT Just: "+iPosition +" and "+jPosition+"\n");
}
position = findMax(i,j);
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTEDTEXT: "+position+"\n");
}
treeChanged = true;
send("mp "+position);
}
}
else
// more && after:
if (i>=0)
{
iElement = (MarkedArea)this.htmlOutputVector.elementAt(i);
iPosition = iElement.position.position;
// more
if (start<=iElement.end)
{
jElement = (MarkedArea)this.htmlOutputVector.elementAt(this.htmlOutputVector.size()-1);
jPosition = jElement.position.position;
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("MORE: "+iPosition+ " and "+jPosition);
}
position = findMax(i,this.htmlOutputVector.size()-1);
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTEDTEXT: "+position+"\n");
}
treeChanged = true;
send("mp "+position);
}
else
// after:
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("AFTER vector of size: "+this.htmlOutputVector.size());
}
}
else
// bigger:
{
iElement = (MarkedArea)this.htmlOutputVector.elementAt(0);
iPosition = iElement.position.position;
jElement = (MarkedArea)this.htmlOutputVector.elementAt(this.htmlOutputVector.size()-1);
jPosition = jElement.position.position;
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("BIGGER: "+iPosition +" and "+jPosition+"\n"
+ "\n-> SELECTEDTEXT: []\n");
}
treeChanged = true;
send("mp []");
}
}//not null selection
}
/** /**
* Appends the string s to the text in the linearization area * Appends the string s to the text in the linearization area
@@ -2965,8 +2966,9 @@ KeyListener, FocusListener {
* parsed. If false, the text is appended, but the subtree tags are ignored. * parsed. If false, the text is appended, but the subtree tags are ignored.
* @param doDisplay true iff the output is to be displayed. * @param doDisplay true iff the output is to be displayed.
* Implies, if false, that clickable is treated as false. * Implies, if false, that clickable is treated as false.
* @param language the current linearization language
*/ */
protected String appendMarked(String restString, final boolean clickable, boolean doDisplay) { protected String appendMarked(String restString, final boolean clickable, boolean doDisplay, String language) {
String appendedPureText = ""; String appendedPureText = "";
if (restString.length()>0) { if (restString.length()>0) {
/** /**
@@ -3010,19 +3012,19 @@ KeyListener, FocusListener {
linMarkingLogger.finer("SOMETHING BEFORE THE TAG"); linMarkingLogger.finer("SOMETHING BEFORE THE TAG");
} }
if (this.currentPosition.size()>0) if (this.currentPosition.size()>0)
newLength = register(currentLength, subtreeBegin, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString); newLength = register(currentLength, subtreeBegin, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString, language);
else else
newLength = register(currentLength, subtreeBegin, new LinPosition("[]", newLength = register(currentLength, subtreeBegin, new LinPosition("[]",
restString.substring(subtreeBegin,subtreeTagEnd).indexOf("incorrect")==-1), restString); restString.substring(subtreeBegin,subtreeTagEnd).indexOf("incorrect")==-1), restString, language);
} else { // nothing before the tag: } else { // nothing before the tag:
//the case in the beginning //the case in the beginning
if (linMarkingLogger.isLoggable(Level.FINER)) { if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("NOTHING BEFORE THE TAG"); linMarkingLogger.finer("NOTHING BEFORE THE TAG");
} }
if (nextOpeningTagBegin>0) { if (nextOpeningTagBegin>0) {
newLength = register(subtreeTagEnd+2, nextOpeningTagBegin, position, restString); newLength = register(subtreeTagEnd+2, nextOpeningTagBegin, position, restString, language);
} else { } else {
newLength = register(subtreeTagEnd+2, restString.length(), position, restString); newLength = register(subtreeTagEnd+2, restString.length(), position, restString, language);
} }
restString = removeSubTreeTag(restString,subtreeBegin, subtreeTagEnd+1); restString = removeSubTreeTag(restString,subtreeBegin, subtreeTagEnd+1);
} }
@@ -3034,10 +3036,10 @@ KeyListener, FocusListener {
linMarkingLogger.finer("SOMETHING BEFORE THE </subtree> TAG"); linMarkingLogger.finer("SOMETHING BEFORE THE </subtree> TAG");
} }
if (this.currentPosition.size()>0) if (this.currentPosition.size()>0)
newLength = register(currentLength, subtreeEnd, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString); newLength = register(currentLength, subtreeEnd, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString, language);
else else
newLength = register(currentLength, subtreeEnd, new LinPosition("[]", newLength = register(currentLength, subtreeEnd, new LinPosition("[]",
restString.substring(subtreeBegin,subtreeEnd).indexOf("incorrect")==-1), restString); restString.substring(subtreeBegin,subtreeEnd).indexOf("incorrect")==-1), restString, language);
currentLength += newLength ; currentLength += newLength ;
} }
// nothing before the tag: // nothing before the tag:
@@ -3070,10 +3072,10 @@ KeyListener, FocusListener {
} }
// register the punctuation: // register the punctuation:
if (this.currentPosition.size()>0) { if (this.currentPosition.size()>0) {
newLength = register(currentLength, currentLength+2, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString); newLength = register(currentLength, currentLength+2, (LinPosition)this.currentPosition.elementAt(this.currentPosition.size()-1), restString, language);
} else { } else {
newLength = register(currentLength, currentLength+2, new LinPosition("[]", newLength = register(currentLength, currentLength+2, new LinPosition("[]",
true), restString); true), restString, language);
} }
currentLength += newLength ; currentLength += newLength ;
} else { } else {
@@ -3190,9 +3192,10 @@ KeyListener, FocusListener {
* the to be registered text * the to be registered text
* @param workingString the String from which the displayed * @param workingString the String from which the displayed
* characters are taken from * characters are taken from
* @param language the current linearization language
* @return newLength, the difference between end and start * @return newLength, the difference between end and start
*/ */
private int register(int start, int end, LinPosition position, String workingString) { 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 * the length of the piece of text that is to be appended now
*/ */
@@ -3204,7 +3207,7 @@ KeyListener, FocusListener {
//get oldLength and add the new text //get oldLength and add the new text
String toAdd = unescapeTextFromGF(stringToAppend); String toAdd = unescapeTextFromGF(stringToAppend);
final HtmlMarkedArea hma = this.display.addAsMarked(toAdd, position); final HtmlMarkedArea hma = this.display.addAsMarked(toAdd, position, language);
this.htmlOutputVector.add(hma); this.htmlOutputVector.add(hma);
if (htmlLogger.isLoggable(Level.FINER)) { if (htmlLogger.isLoggable(Level.FINER)) {
htmlLogger.finer("HTML added : " + hma); htmlLogger.finer("HTML added : " + hma);
@@ -3400,13 +3403,6 @@ KeyListener, FocusListener {
return tempMenu; return tempMenu;
} }
public void focusGained(FocusEvent e) {
//do nothing
}
public void focusLost(FocusEvent e) {
getLayeredPane().remove(parseField);
repaint();
}
/** /**
* *
@@ -3417,10 +3413,248 @@ KeyListener, FocusListener {
newCategoryMenu.removeItemAt(1); newCategoryMenu.removeItemAt(1);
} }
/**
* Handles the showing of the popup menu and the parse field
* @param e the MouseEvent, that caused the call of this function
*/
protected void maybeShowPopup(MouseEvent e) {
//int i=outputVector.size()-1;
// right click:
if (e.isPopupTrigger()) {
if (popUpLogger.isLoggable(Level.FINER)) {
popUpLogger.finer("changing pop-up menu2!");
}
popup2 = producePopup();
popup2.show(e.getComponent(), e.getX(), e.getY());
}
// middle click
//TODO parsing via middle click
if (e.getButton() == MouseEvent.BUTTON2) {
// selection Exists:
if (popUpLogger.isLoggable(Level.FINER)) {
popUpLogger.finer(e.getX() + " " + e.getY());
}
String selectedText;
if (currentNode.isMeta()) {
// we do not want the ?3 to be in parseField, that disturbs
selectedText = "";
} else {
final String language;
//put together the currently focused text
if (e.getComponent() instanceof JTextComponent) {
JTextComponent jtc = (JTextComponent)e.getComponent();
int pos = jtc.viewToModel(e.getPoint());
MarkedArea ma = null;
if (jtc instanceof JTextPane) {
//HTML
for (int i = 0; i < htmlOutputVector.size(); i++) {
if ((pos >= ((HtmlMarkedArea)htmlOutputVector.get(i)).htmlBegin) && (pos <= ((HtmlMarkedArea)htmlOutputVector.get(i)).htmlEnd)) {
ma = (HtmlMarkedArea)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";
}
} else {
language = "Abstract";
}
StringBuffer sel = new StringBuffer();
for (int i = 0; i<htmlOutputVector.size(); i++) {
final HtmlMarkedArea ma = (HtmlMarkedArea)htmlOutputVector.elementAt(i);
if (language.equals(ma.language) && isSubtreePosition(focusPosition, ma.position)) {
sel.append(ma.words);
}
}
selectedText = sel.toString();
}
//compute the size of parseField
if (selectedText.length()<5)
// if (treeCbMenuItem.isSelected())
// parseField.setBounds(e.getX()+(int)Math.round(tree.getBounds().getWidth()), e.getY()+80, 400, 40);
// else
parseField.setBounds(e.getX(), e.getY()+80, 400, 40);
else
// if (treeCbMenuItem.isSelected())
// parseField.setBounds(e.getX()+(int)Math.round(tree.getBounds().getWidth()), e.getY()+80, selectedText.length()*20, 40);
// else
parseField.setBounds(e.getX(), e.getY()+80, selectedText.length()*20, 40);
getLayeredPane().add(parseField, new Integer(1), 0);
parseField.setText(selectedText);
parseField.requestFocusInWindow();
}
}
/**
* gets the LinPosition according to the given start and end of
* the selection in comp.
* Is meant as a unified replacement of large parts of caretUpdate
* @param start start of the selection in comp
* @param end end of the selection in comp
* @param comp either a JTextArea or a JTextPane
* @return s.a.
*/
String getLinPosition(int start, int end, JTextComponent comp) {
final int maType;
if (comp instanceof JTextPane) {
//if a JTextPane is given, calculate for HTML
maType = 1;
} else {
maType = 0;
}
String jPosition ="", iPosition="", position="", resultPosition = null;
MarkedArea jElement = null;
MarkedArea iElement = null;
int j = 0;
int i = htmlOutputVector.size() - 1;
if (popUpLogger.isLoggable(Level.FINER)) {
popUpLogger.finer("CARET POSITION: "+comp.getCaretPosition()
+ "\n-> SELECTION START POSITION: "+start
+ "\n-> SELECTION END POSITION: "+end);
}
if (linMarkingLogger.isLoggable(Level.FINER)) {
if (end > 0 && (end < comp.getDocument().getLength())) {
try {
linMarkingLogger.finer("CHAR: "+comp.getDocument().getText(end, 1));
} catch (BadLocationException ble) {
linMarkingLogger.fine(ble.getLocalizedMessage());
ble.printStackTrace();
}
}
}
// not null selection:
if ((i>-1)&&(start<comp.getDocument().getLength()-1)) {
if (linMarkingLogger.isLoggable(Level.FINER))
for (int k = 0; k < htmlOutputVector.size(); k++) {
MarkedArea kma = normalizeMarkedArea((MarkedArea)htmlOutputVector.elementAt(k), maType);
linMarkingLogger.finer("element: " + k + " begin " + kma.begin + " "
+ "\n-> end: " + kma.end+" "
+ "\n-> position: " + (kma.position).position+" "
+ "\n-> words: " + kma.words);
}
// localizing end:
while ((j < htmlOutputVector.size()) && (normalizeMarkedArea((MarkedArea)htmlOutputVector.elementAt(j), maType).end < end)) {
j++;
}
// localising start:
while ((i >= 0) && (normalizeMarkedArea((MarkedArea)htmlOutputVector.elementAt(i), maType).begin > start))
i--;
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("i: " + i + " j: " + j);
}
if ((j < htmlOutputVector.size())) {
jElement = normalizeMarkedArea((MarkedArea)htmlOutputVector.elementAt(j), maType);
jPosition = jElement.position.position;
// less & before:
if (i == -1) { // less:
if (end >= jElement.begin) {
iElement = normalizeMarkedArea((MarkedArea)htmlOutputVector.elementAt(0), maType);
iPosition = iElement.position.position;
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("Less: "+jPosition+" and "+iPosition);
}
position = findMax(0,j);
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTEDTEXT: "+position+"\n");
}
treeChanged = true;
resultPosition = position;
} else if (linMarkingLogger.isLoggable(Level.FINER)) { // before:
linMarkingLogger.finer("BEFORE vector of size: " + htmlOutputVector.size());
}
} else { // just:
iElement = normalizeMarkedArea((MarkedArea)htmlOutputVector.elementAt(i), maType);
iPosition = iElement.position.position;
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTED TEXT Just: "+iPosition +" and "+jPosition+"\n");
}
position = findMax(i,j);
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTEDTEXT: "+position+"\n");
}
treeChanged = true;
resultPosition = position;
}
} else if (i>=0) { // more && after:
iElement = normalizeMarkedArea((MarkedArea)htmlOutputVector.elementAt(i), maType);
iPosition = iElement.position.position;
// more
if (start<=iElement.end) {
jElement = normalizeMarkedArea((MarkedArea)htmlOutputVector.elementAt(htmlOutputVector.size() - 1), maType);
jPosition = jElement.position.position;
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("MORE: "+iPosition+ " and "+jPosition);
}
position = findMax(i, htmlOutputVector.size()-1);
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("SELECTEDTEXT: "+position+"\n");
}
treeChanged = true;
resultPosition = position;
} else if (linMarkingLogger.isLoggable(Level.FINER)) { // after:
linMarkingLogger.finer("AFTER vector of size: " + htmlOutputVector.size());
}
} else {
// bigger:
iElement = normalizeMarkedArea((MarkedArea)htmlOutputVector.elementAt(0), maType);
iPosition = iElement.position.position;
jElement = normalizeMarkedArea((MarkedArea)htmlOutputVector.elementAt(htmlOutputVector.size() - 1), maType);
jPosition = jElement.position.position;
if (linMarkingLogger.isLoggable(Level.FINER)) {
linMarkingLogger.finer("BIGGER: "+iPosition +" and "+jPosition+"\n"
+ "\n-> SELECTEDTEXT: []\n");
}
treeChanged = true;
resultPosition = "[]";
}
}//not null selection
return resultPosition;
}
/**
* Takes a MarkedArea and transforms it into a MarkedArea,
* that has begin and and set as the valid fields.
* If a HtmlMarkedArea is given and type == 1, then the htmlBegin
* and htmlEnd fields are used as begin and end.
* For type == 0, the normal begin and end fields are used.
* @param ma The MarkedArea to 'normalize'
* @param type 0 for pure text, 1 for HTML. begin and end will be -1 for other values.
* @return a MarkedArea as described above
*/
private MarkedArea normalizeMarkedArea(MarkedArea ma, int type) {
int begin, end;
if (type == 0) {
begin = ma.begin;
end = ma.end;
} else if (type == 1 && (ma instanceof HtmlMarkedArea)) {
HtmlMarkedArea hma = (HtmlMarkedArea)ma;
begin = hma.htmlBegin;
end = hma.htmlEnd;
} else {
begin = -1;
end = -1;
linMarkingLogger.info("Illegal number-code of MarkedArea encountered: " + type + "\nor alternatively, HTML is expected, but a " + ma.getClass().getName() + " was given");
}
return new MarkedArea(begin, end, ma.position, ma.words, ma.language);
}
/** /**
* pop-up menu (adapted from DynamicTree2): * pop-up menu (adapted from DynamicTree2):
* @author janna * @author janna
*
*/ */
class PopupListener extends MouseAdapter { class PopupListener extends MouseAdapter {
public void mousePressed(MouseEvent e) { public void mousePressed(MouseEvent e) {
@@ -3435,43 +3669,6 @@ KeyListener, FocusListener {
public void mouseReleased(MouseEvent e) { public void mouseReleased(MouseEvent e) {
//nothing to be done here //nothing to be done here
} }
protected void maybeShowPopup(MouseEvent e) {
//int i=outputVector.size()-1;
// right click:
if (e.isPopupTrigger()) {
if (popUpLogger.isLoggable(Level.FINER)) {
popUpLogger.finer("changing pop-up menu2!");
}
popup2 = producePopup();
popup2.show(e.getComponent(), e.getX(), e.getY());
}
// middle click
//TODO strange code here, that doesn't work
if (e.getButton() == MouseEvent.BUTTON2)
{
// selection Exists:
if (!selectedText.equals(""))
{
if (popUpLogger.isLoggable(Level.FINER)) {
popUpLogger.finer(e.getX() + " " + e.getY());
}
if (selectedText.length()<5)
if (treeCbMenuItem.isSelected())
parseField.setBounds(e.getX()+(int)Math.round(tree.getBounds().getWidth()), e.getY()+80, 400, 40);
else
parseField.setBounds(e.getX(), e.getY()+80, 400, 40);
else
if (treeCbMenuItem.isSelected())
parseField.setBounds(e.getX()+(int)Math.round(tree.getBounds().getWidth()), e.getY()+80, selectedText.length()*20, 40);
else
parseField.setBounds(e.getX(), e.getY()+80, selectedText.length()*20, 40);
getLayeredPane().add(parseField, new Integer(1), 0);
parseField.setText(selectedText);
parseField.requestFocusInWindow();
}
}
}
} }
/** /**

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

@@ -36,9 +36,10 @@ class HtmlMarkedArea extends MarkedArea {
* @param w The actual text of this area * @param w The actual text of this area
* @param hb the start index in the HTML area * @param hb the start index in the HTML area
* @param he the end index in the HTML area * @param he the end index in the HTML area
* @param lang the language of the current linearization
*/ */
public HtmlMarkedArea(int b, int e, LinPosition p, String w, int hb, int he) { public HtmlMarkedArea(int b, int e, LinPosition p, String w, int hb, int he, String lang) {
super(b, e, p, w); super(b, e, p, w, lang);
this.htmlBegin = hb; this.htmlBegin = hb;
this.htmlEnd = he; this.htmlEnd = he;
} }
@@ -51,7 +52,7 @@ class HtmlMarkedArea extends MarkedArea {
* @param he the end index in the HTML area * @param he the end index in the HTML area
*/ */
HtmlMarkedArea(final MarkedArea orig, final int hb, final int he) { HtmlMarkedArea(final MarkedArea orig, final int hb, final int he) {
super(orig.begin, orig.end, orig.position, orig.words); super(orig.begin, orig.end, orig.position, orig.words, orig.language);
this.htmlBegin = hb; this.htmlBegin = hb;
this.htmlEnd = he; this.htmlEnd = he;
} }

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

@@ -23,29 +23,43 @@ package de.uka.ilkd.key.ocl.gf;
* @author janna * @author janna
*/ */
class MarkedArea { class MarkedArea {
/** The starting position of the stored words */ /**
* The starting position of the stored words
*/
final public int begin; final public int begin;
/** The ending position of the stored words. /**
* The ending position of the stored words.
* Not final because of some punctuation issue daniels * Not final because of some punctuation issue daniels
* does not understand * does not understand
*/ */
public int end; public int end;
/** The position in the AST */ /**
* The position in the AST
*/
final public LinPosition position; final public LinPosition position;
/** The actual text of this area */ /**
* The actual text of this area
*/
final public String words; final public String words;
/**
* the concrete grammar (or better, its linearization)
* this MarkedArea belongs to
*/
final public String language;
/** /**
* Creates a new MarkedArea and initializes the fields with the parameters * Creates a new MarkedArea and initializes the fields with the parameters
* @param b The starting position of the stored words * @param b The starting position of the stored words
* @param e The ending position of the stored words * @param e The ending position of the stored words
* @param p The position in the AST * @param p The position in the AST
* @param w The actual text of this area * @param w The actual text of this area
* @param lang the language of the current linearization
*/ */
MarkedArea(int b, int e, LinPosition p, String w) { MarkedArea(int b, int e, LinPosition p, String w, String lang) {
begin = b; begin = b;
end = e; end = e;
position = p; position = p;
words = w; words = w;
language = lang;
} }
public String toString() { public String toString() {