GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-05-28 12:18:54 -06:00
Code Issues Packages Projects Releases Wiki Activity

*** empty log message ***

Browse Source
This commit is contained in:
janna
2003-12-02 22:36:34 +00:00
parent e3dd913ce3
commit 57d4300f86
1 changed files with 4 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
src/JavaGUI/GFEditor2.java
View File

@@ -1641,11 +1641,11 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
restString = s; restString = s;
int m2, m1; int m2, m1;
String position = ""; String position = "";
if (selectionStart>-1) if ((selectionStart>-1)&&(selectionEnd>selectionStart))
{ {
selStart = selectionStart; selStart = selectionStart;
selEnd = selectionEnd; selEnd = selectionEnd;
if (debug2) //if (debug2)
System.out.println("SELECTION: " + selStart + " "+selEnd+ "TOTAL: "+s.length()); System.out.println("SELECTION: " + selStart + " "+selEnd+ "TOTAL: "+s.length());
if (selEnd>-1) if (selEnd>-1)
selectionCheck = (s.substring(selStart, selEnd).indexOf("<")==-1); selectionCheck = (s.substring(selStart, selEnd).indexOf("<")==-1);
@@ -1880,6 +1880,7 @@ public class GFEditor2 extends JFrame implements ActionListener, CaretListener,
currentPosition.addElement(restString.substring(positionStart, positionEnd+1)); currentPosition.addElement(restString.substring(positionStart, positionEnd+1));
} }
else else
if (currentPosition.size()>0)
currentPosition.removeElementAt(currentPosition.size()-1); currentPosition.removeElementAt(currentPosition.size()-1);
if (start>0) if (start>0)
restString = restString.substring(0,start)+restString.substring(end+1); restString = restString.substring(0,start)+restString.substring(end+1);