# HG changeset patch
# User immler@in.tum.de
# Date 1243974123 -7200
# Node ID 2b46d92e46429341b3fdfa05283a0e4b63324427
# Parent  0e0e08aaddb52279c0e2e4e604977e7cdec6d3c6
linearset works faster here

diff -r 0e0e08aaddb5 -r 2b46d92e4642 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Tue Jun 02 19:40:20 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Tue Jun 02 22:22:03 2009 +0200
@@ -84,21 +84,25 @@
     def from: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.from_current(document.id, _)
 
     var next_x = start
-    for {
-      command <- document.commands.dropWhile(_.stop(document) <= from(start)).takeWhile(_.start(document) < from(stop))
-      markup <- command.highlight_node.flatten
-      if(to(markup.abs_stop(document)) > start)
-      if(to(markup.abs_start(document)) < stop)
-      byte = DynamicTokenMarker.choose_byte(markup.info.toString)
-      token_start = to(markup.abs_start(document)) - start max 0
-      token_length = to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
-                     (start - to(markup.abs_start(document)) max 0) -
-                     (to(markup.abs_stop(document)) - stop max 0)
-    } {
-      if (start + token_start > next_x)
-        handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
-      handler.handleToken(line_segment, byte, token_start, token_length, context)
-      next_x = start + token_start + token_length
+
+    var command = document.find_command_at(from(start))
+    while (command != null && command.start(document) < from(stop)) {
+      for {
+        markup <- command.highlight_node.flatten
+        if(to(markup.abs_stop(document)) > start)
+        if(to(markup.abs_start(document)) < stop)
+        byte = DynamicTokenMarker.choose_byte(markup.info.toString)
+        token_start = to(markup.abs_start(document)) - start max 0
+        token_length = to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
+                       (start - to(markup.abs_start(document)) max 0) -
+                       (to(markup.abs_stop(document)) - stop max 0)
+      } {
+        if (start + token_start > next_x)
+          handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
+        handler.handleToken(line_segment, byte, token_start, token_length, context)
+        next_x = start + token_start + token_length
+      }
+      command = document.commands.next(command).getOrElse(null)
     }
     if (next_x < stop)
       handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
diff -r 0e0e08aaddb5 -r 2b46d92e4642 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jun 02 19:40:20 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jun 02 22:22:03 2009 +0200
@@ -193,14 +193,14 @@
     val saved_color = gfx.getColor
 
     val metrics = text_area.getPainter.getFontMetrics
+
+    // encolor phase
     var e = document.find_command_at(from_current(start))
-    val commands = document.commands.dropWhile(_.stop(document) <= from_current(start)).
-      takeWhile(c => to_current(c.start(document)) < end)
-    // encolor phase
-    for (e <- commands) {
+    while (e != null && e.start(document) < end) {
       val begin = start max to_current(e.start(document))
       val finish = end - 1 min to_current(e.stop(document))
       encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
+      e = document.commands.next(e).getOrElse(null)
     }
 
     gfx.setColor(saved_color)
diff -r 0e0e08aaddb5 -r 2b46d92e4642 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jun 02 19:40:20 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jun 02 22:22:03 2009 +0200
@@ -141,11 +141,6 @@
   
   /** command view **/
 
-  def find_command_at(pos: Int): Command = {
-    for (cmd <- commands) { if (pos < cmd.stop(this)) return cmd }
-    return null
-  }
-
   private def token_changed(new_id: String,
                             before_change: Option[Token],
                             inserted_tokens: List[Token],
@@ -223,4 +218,30 @@
       new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset, active, is_command_keyword)
     return (doc, change)
   }
+
+  val commands_offsets = {
+    var last_stop = 0
+    (for (c <- commands) yield {
+      val r = c -> (last_stop,c.stop(this))
+      last_stop = c.stop(this)
+      r
+    }).toArray
+  }
+
+  // use a binary search to find commands for a given offset
+  def find_command_at(pos: Int): Command = find_command_at(pos, 0, commands_offsets.length)
+  private def find_command_at(pos: Int, array_start: Int, array_stop: Int): Command = {
+    val middle_index = (array_start + array_stop) / 2
+    if (middle_index >= commands_offsets.length) return null
+    val (middle, (start, stop)) = commands_offsets(middle_index)
+    // does middle contain pos?
+    if (start <= pos && stop > pos)
+      middle
+    else if (start > pos)
+      find_command_at(pos, array_start, middle_index)
+    else if (stop <= pos)
+      find_command_at(pos, middle_index + 1, array_stop)
+    else error("can't be")
+  }
+
 }