--- 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)))
}
--- a/src/Tools/jEdit/src/jedit/document_view.scala Sun Jan 10 20:14:21 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Sun Jan 10 20:38:23 2010 +0100
@@ -263,9 +263,9 @@
super.paintComponent(gfx)
val buffer = model.buffer
- for (command <- document.commands) {
- val line1 = buffer.getLineOfOffset(model.to_current(document, command.start(document)))
- val line2 = buffer.getLineOfOffset(model.to_current(document, command.stop(document))) + 1
+ for ((command, start) <- document.command_range(0)) {
+ val line1 = buffer.getLineOfOffset(model.to_current(document, start))
+ val line2 = buffer.getLineOfOffset(model.to_current(document, start + command.length)) + 1
val y = line_to_y(line1)
val height = HEIGHT * (line2 - line1)
gfx.setColor(Document_View.choose_color(command, document))
--- a/src/Tools/jEdit/src/proofdocument/command.scala Sun Jan 10 20:14:21 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/command.scala Sun Jan 10 20:38:23 2010 +0100
@@ -54,8 +54,8 @@
def length: Int = content.length
def start(doc: Document) = doc.token_start(tokens.first)
- def stop(doc: Document) = start(doc) + length
+ // FIXME eliminate
def contains(p: Token) = tokens.contains(p)