# HG changeset patch
# User wenzelm
# Date 1263152303 -3600
# Node ID aa9e22d9f9a73610817680c00730e8d8f4c34629
# Parent  81d0410dc3acb9bd7b9ba5db8f24cc3288b62e8b
eliminated Command.stop, which tends to case duplicate traversal of commands;

diff -r 81d0410dc3ac -r aa9e22d9f9a7 src/Tools/jEdit/src/jedit/document_model.scala
--- 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)))
   }
 
 
diff -r 81d0410dc3ac -r aa9e22d9f9a7 src/Tools/jEdit/src/jedit/document_view.scala
--- 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))
diff -r 81d0410dc3ac -r aa9e22d9f9a7 src/Tools/jEdit/src/proofdocument/command.scala
--- 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)