# HG changeset patch
# User wenzelm
# Date 1252241725 -7200
# Node ID 4f0ee5ab03802f94e512bb225e0457f3a8c6d644
# Parent  dad4c06acd7be7c0849371aaa785d9cdfd7e3e0a
replaced find_command_at by command_at -- null-free, proper Option;
tuned;

diff -r dad4c06acd7b -r 4f0ee5ab0380 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sun Sep 06 13:43:54 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sun Sep 06 14:55:25 2009 +0200
@@ -121,9 +121,10 @@
     def to: Int => Int = theory_view.to_current(document, _)
     def from: Int => Int = theory_view.from_current(document, _)
 
-    var command = document.find_command_at(from(start))
     var next_x = start
-    while (command != null && command.start(document) < from(stop)) {
+    var cmd = document.command_at(from(start))
+    while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
+      val command = cmd.get
       for {
         markup <- command.highlight_node(document).flatten
         command_start = command.start(document)
@@ -145,7 +146,7 @@
           token_start, token_length, context)
         next_x = start + token_start + token_length
       }
-      command = document.commands.next(command).getOrElse(null)
+      cmd = document.commands.next(command)
     }
     if (next_x < stop)
       handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
diff -r dad4c06acd7b -r 4f0ee5ab0380 src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Sun Sep 06 13:43:54 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Sun Sep 06 14:55:25 2009 +0200
@@ -51,30 +51,30 @@
       val theory_view = theory_view_opt.get
       val document = theory_view.current_document()
       val offset = theory_view.from_current(document, original_offset)
-      val command = document.find_command_at(offset)
-      if (command != null) {
-        val ref_o = command.ref_at(document, offset - command.start(document))
-        if (!ref_o.isDefined) null
-        else {
-          val ref = ref_o.get
-          val command_start = command.start(document)
-          val begin = theory_view.to_current(document, command_start + ref.start)
-          val line = buffer.getLineOfOffset(begin)
-          val end = theory_view.to_current(document, command_start + ref.stop)
-          ref.info match {
-            case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
-              new ExternalHyperlink(begin, end, line, ref_file, ref_line)
-            case Command.RefInfo(_, _, Some(id), Some(offset)) =>
-              prover.get.command(id) match {
-                case Some(ref_cmd) =>
-                  new InternalHyperlink(begin, end, line,
-                    theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
+      document.command_at(offset) match {
+        case Some(command) =>
+          command.ref_at(document, offset - command.start(document)) match {
+            case Some(ref) =>
+              val command_start = command.start(document)
+              val begin = theory_view.to_current(document, command_start + ref.start)
+              val line = buffer.getLineOfOffset(begin)
+              val end = theory_view.to_current(document, command_start + ref.stop)
+              ref.info match {
+                case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
+                  new ExternalHyperlink(begin, end, line, ref_file, ref_line)
+                case Command.RefInfo(_, _, Some(id), Some(offset)) =>
+                  prover.get.command(id) match {
+                    case Some(ref_cmd) =>
+                      new InternalHyperlink(begin, end, line,
+                        theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
+                    case None => null
+                  }
                 case _ => null
               }
-            case _ => null
+            case None => null
           }
-        }
-      } else null
+        case None => null
+      }
     }
   }
 }
diff -r dad4c06acd7b -r 4f0ee5ab0380 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Sep 06 13:43:54 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Sep 06 14:55:25 2009 +0200
@@ -54,10 +54,13 @@
   private val selected_state_controller = new CaretListener {
     override def caretUpdate(e: CaretEvent) = {
       val doc = current_document()
-      val cmd = doc.find_command_at(e.getDot)
-      if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot &&
-          Isabelle.plugin.selected_state != cmd)
-        Isabelle.plugin.selected_state = cmd
+      doc.command_at(e.getDot) match {
+        case Some(cmd)
+          if (doc.token_start(cmd.tokens.first) <= e.getDot &&
+            Isabelle.plugin.selected_state != cmd) =>
+          Isabelle.plugin.selected_state = cmd
+        case _ =>
+      }
     }
   }
 
@@ -270,13 +273,14 @@
     val metrics = text_area.getPainter.getFontMetrics
 
     // encolor phase
-    var e = document.find_command_at(from_current(start))
-    while (e != null && e.start(document) < end) {
+    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,
         TheoryView.choose_color(e, document), true)
-      e = document.commands.next(e).getOrElse(null)
+      cmd = document.commands.next(e)
     }
 
     gfx.setColor(saved_color)
@@ -286,11 +290,12 @@
   {
     val document = current_document()
     val offset = from_current(document, text_area.xyToOffset(x, y))
-    val cmd = document.find_command_at(offset)
-    if (cmd != null) {
-      document.token_start(cmd.tokens.first)
-      cmd.type_at(document, offset - cmd.start(document))
-    } else null
+    document.command_at(offset) match {
+      case Some(cmd) =>
+        document.token_start(cmd.tokens.first)
+        cmd.type_at(document, offset - cmd.start(document))
+      case None => null
+    }
   }
 
 
diff -r dad4c06acd7b -r 4f0ee5ab0380 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Sun Sep 06 13:43:54 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Sun Sep 06 14:55:25 2009 +0200
@@ -260,20 +260,22 @@
     }).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
-  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 = {
+  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 null
+    if (middle_index >= commands_offsets.length) return None
     val (middle, (start, stop)) = commands_offsets(middle_index)
     // does middle contain pos?
-    if (start <= pos && stop > pos)
-      middle
+    if (start <= pos && pos < stop)
+      Some(middle)
     else if (start > pos)
-      find_command_at(pos, array_start, middle_index)
+      find_command(pos, array_start, middle_index)
     else if (stop <= pos)
-      find_command_at(pos, middle_index + 1, array_stop)
-    else error("can't be")
+      find_command(pos, middle_index + 1, array_stop)
+    else error("impossible")
   }
-
 }