--- a/src/Tools/jEdit/src/jedit/document_model.scala Sun Jan 10 20:14:21 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Sun Jan 10 20:38:23 2010 +0100
@@ -84,8 +84,10 @@
def lines_of_command(doc: Document, cmd: Command): (Int, Int) =
{
- (buffer.getLineOfOffset(to_current(doc, cmd.start(doc))),
- buffer.getLineOfOffset(to_current(doc, cmd.stop(doc))))
+ val start = cmd.start(doc)
+ val stop = start + cmd.length
+ (buffer.getLineOfOffset(to_current(doc, start)),
+ buffer.getLineOfOffset(to_current(doc, stop)))
}