Ticket #259: parser.patch

src/ed/inf/proofgeneral/editor/lazyparser/Parser.java

@@ -130 +130 @@
                 String parseText = "";
                 int results = 0;
                 int linestoAdd = 0;
-                int endOffset;
+                int nextOffset;
                 try {
                         int endLine = doc.getLineOfOffset(startOffset+length-1);
                         do {
-                                endOffset = doc.getLineLength(endLine) + doc.getLineOffset(endLine) - 1;
-                                parseText = doc.getDesymbolised(startOffset, endOffset-startOffset);
+                                nextOffset = doc.getLineLength(endLine) + doc.getLineOffset(endLine);
+                                parseText = doc.getDesymbolised(startOffset, nextOffset-startOffset);
                                 parseResult = parseText(parseText, doc, startOffset,monitor);
                                 results = parseResultContentSize(parseResult);
 
@@ -150 +150 @@
                                                 endLine = doc.getNumberOfLines() - 1;
                                         }
                                 }
-                        } while (results <= 1 && endOffset + 1 < doc.getLength());
+                        } while (results <= 1 && nextOffset < doc.getLength());
                 } catch (BadLocationException badloc) {
                         // Shouldn't happen unless client called us incorrectly
                         throw new ParsingException("Bad location during parsing"); 
@@ -161 +161 @@
                 try {
                         // TODO: perhaps this should be in a workspace runnable, to ensure
                         // thread safe access to document 
-                        ProofScriptMarkers.cleanMarkers(doc,startOffset,endOffset-startOffset); // NB: removes all types of marker
+                        ProofScriptMarkers.cleanMarkers(doc,startOffset,nextOffset-startOffset); // NB: removes all types of marker
                         linkParseresult(parseResult,doc,startOffset); 
                         doc.recalculateFoldingStructure();
                 } catch (UnparseableException x) {