--- a/src/Tools/jEdit/src/proofdocument/command.scala Sun Jan 10 17:10:32 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/command.scala Sun Jan 10 20:14:21 2010 +0100
@@ -51,8 +51,10 @@
def content(i: Int, j: Int): String = content.substring(i, j)
lazy val symbol_index = new Symbol.Index(content)
+ def length: Int = content.length
+
def start(doc: Document) = doc.token_start(tokens.first)
- def stop(doc: Document) = doc.token_start(tokens.last) + tokens.last.length
+ def stop(doc: Document) = start(doc) + length
def contains(p: Token) = tokens.contains(p)