iterators for ranges of commands/starts -- avoid extra array per document;
try/finally for saved_color;
misc tuning;

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Sun Jan 10 17:10:32 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sun Jan 10 20:14:21 2010 +0100
@@ -126,31 +126,27 @@
     {
       def from_current(pos: Int) = model.from_current(document, pos)
       def to_current(pos: Int) = model.to_current(document, pos)
+      val metrics = text_area.getPainter.getFontMetrics
       val saved_color = gfx.getColor
-
-      val metrics = text_area.getPainter.getFontMetrics
-
-      // encolor phase
-      var cmd = document.command_at(from_current(start))
-      while (cmd.isDefined && cmd.get.start(document) < end) {
-        val e = cmd.get
-        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,
-          Document_View.choose_color(e, document), true)
-        cmd = document.commands.next(e)
+      try {
+        for ((command, command_start) <-
+          document.command_range(from_current(start), from_current(end)))
+        {
+          val begin = start max to_current(command_start)
+          val finish = (end - 1) min to_current(command_start + command.length)
+          encolor(gfx, y, metrics.getHeight, begin, finish,
+            Document_View.choose_color(command, document), true)
+        }
       }
-
-      gfx.setColor(saved_color)
+      finally { gfx.setColor(saved_color) }
     }
 
     override def getToolTipText(x: Int, y: Int): String =
     {
       val offset = model.from_current(document, text_area.xyToOffset(x, y))
       document.command_at(offset) match {
-        case Some(cmd) =>
-          document.token_start(cmd.tokens.first)
-          document.current_state(cmd).type_at(offset - cmd.start(document)).getOrElse(null)
+        case Some((command, command_start)) =>
+          document.current_state(command).type_at(offset - command_start).getOrElse(null)
         case None => null
       }
     }
@@ -169,12 +165,11 @@
 
   private val caret_listener = new CaretListener
   {
-    override def caretUpdate(e: CaretEvent) {
+    override def caretUpdate(e: CaretEvent)
+    {
       document.command_at(e.getDot) match {
-        case Some(cmd)
-          if (document.token_start(cmd.tokens.first) <= e.getDot &&
-            selected_command != cmd) =>
-          selected_command = cmd  // FIXME !?
+        case Some((command, command_start)) if (selected_command != command) =>
+          selected_command = command
         case _ =>
       }
     }

--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Jan 10 17:10:32 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Jan 10 20:14:21 2010 +0100
@@ -44,10 +44,9 @@
         val document = model.recent_document()
         val offset = model.from_current(document, original_offset)
         document.command_at(offset) match {
-          case Some(command) =>
-            document.current_state(command).ref_at(offset - command.start(document)) match {
+          case Some((command, command_start)) =>
+            document.current_state(command).ref_at(offset - command_start) match {
               case Some(ref) =>
-                val command_start = command.start(document)
                 val begin = model.to_current(document, command_start + ref.start)
                 val line = buffer.getLineOfOffset(begin)
                 val end = model.to_current(document, command_start + ref.stop)

--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun Jan 10 17:10:32 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun Jan 10 20:14:21 2010 +0100
@@ -115,37 +115,32 @@
     def from: Int => Int = model.from_current(document, _)
 
     var next_x = start
-    var cmd = document.command_at(from(start))
-    while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
-      val command = cmd.get
-      for {
-        markup <- document.current_state(command).highlight.flatten
-        command_start = command.start(document)
-        abs_start = to(command_start + markup.start)
-        abs_stop = to(command_start + markup.stop)
-        if (abs_stop > start)
-        if (abs_start < stop)
-        byte = Isabelle_Token_Marker.choose_byte(markup.info.toString)
-        token_start = (abs_start - start) max 0
-        token_length =
-          (abs_stop - abs_start) -
-          ((start - abs_start) max 0) -
-          ((abs_stop - stop) max 0)
-      } {
+    for {
+      (command, command_start) <- document.command_range(from(start), from(stop))
+      markup <- document.current_state(command).highlight.flatten
+      val abs_start = to(command_start + markup.start)
+      val abs_stop = to(command_start + markup.stop)
+      if (abs_stop > start)
+      if (abs_start < stop)
+      val byte = Isabelle_Token_Marker.choose_byte(markup.info.toString)
+      val token_start = (abs_start - start) max 0
+      val token_length =
+        (abs_stop - abs_start) -
+        ((start - abs_start) max 0) -
+        ((abs_stop - 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)
+        handler.handleToken(line_segment, byte, token_start, token_length, context)
         next_x = start + token_start + token_length
       }
-      cmd = document.commands.next(command)
-    }
     if (next_x < stop)
       handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
 
     handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
     handler.setLineContext(context)
-    return context
+    context
   }
 }

--- 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)
 

--- a/src/Tools/jEdit/src/proofdocument/document.scala	Sun Jan 10 17:10:32 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/document.scala	Sun Jan 10 20:14:21 2010 +0100
@@ -245,6 +245,7 @@
   }
 }
 
+
 class Document(
     val id: Isar_Document.Document_ID,
     val tokens: Linear_Set[Token],   // FIXME plain List, inside Command
@@ -252,10 +253,41 @@
     val commands: Linear_Set[Command],
     old_states: Map[Command, Command])
 {
+  // FIXME eliminate
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)
 
 
-  /* command/state assignment */
+  /* command source positions */
+
+  def command_starts: Iterator[(Command, Int)] =
+  {
+    var offset = 0
+    for (cmd <- commands.elements) yield {
+      // val start = offset  FIXME new
+      val start = token_start(cmd.tokens.first)   // FIXME old
+      offset += cmd.length
+      (cmd, start)
+    }
+  }
+
+  def command_start(cmd: Command): Option[Int] =
+    command_starts.find(_._1 == cmd).map(_._2)
+
+  def command_range(i: Int): Iterator[(Command, Int)] =
+    command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
+
+  def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
+    command_range(i) takeWhile { case (_, start) => start < j }
+
+  def command_at(i: Int): Option[(Command, Int)] =
+  {
+    val range = command_range(i)
+    if (range.hasNext) Some(range.next) else None
+  }
+
+
+
+  /* command state assignment */
 
   val assignment = Future.promise[Map[Command, Command]]
   def await_assignment { assignment.join }
@@ -273,33 +305,4 @@
     require(assignment.is_finished)
     (assignment.join)(cmd).current_state
   }
-
-
-  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
-  }
-
-  def command_at(pos: Int): Option[Command] =
-    find_command(pos, 0, commands_offsets.length)
-
-  // use a binary search to find commands for a given offset
-  private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] =
-  {
-    val middle_index = (array_start + array_stop) / 2
-    if (middle_index >= commands_offsets.length) return None
-    val (middle, (start, stop)) = commands_offsets(middle_index)
-    // does middle contain pos?
-    if (start <= pos && pos < stop)
-      Some(middle)
-    else if (start > pos)
-      find_command(pos, array_start, middle_index)
-    else if (stop <= pos)
-      find_command(pos, middle_index + 1, array_stop)
-    else error("impossible")
-  }
 }