# HG changeset patch
# User wenzelm
# Date 1263239518 -3600
# Node ID d0057d9777ce5c9caedea8352aa8acdcb0917e15
# Parent  a4fe43df58b3187c78fb6da3a4cccfe3b74061d2
more tobust treatment of Document.current_state;
some timing;

diff -r a4fe43df58b3 -r d0057d9777ce src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Mon Jan 11 18:28:31 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Mon Jan 11 20:51:58 2010 +0100
@@ -25,10 +25,10 @@
 {
   def choose_color(command: Command, doc: Document): Color =
   {
-    doc.current_state(command).status match {
-      case Command.Status.UNPROCESSED => new Color(255, 228, 225)
-      case Command.Status.FINISHED => new Color(234, 248, 255)
-      case Command.Status.FAILED => new Color(255, 193, 193)
+    doc.current_state(command).map(_.status) match {
+      case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225)
+      case Some(Command.Status.FINISHED) => new Color(234, 248, 255)
+      case Some(Command.Status.FAILED) => new Color(255, 193, 193)
       case _ => Color.red
     }
   }
@@ -146,7 +146,7 @@
       val offset = model.from_current(document, text_area.xyToOffset(x, y))
       document.command_at(offset) match {
         case Some((command, command_start)) =>
-          document.current_state(command).type_at(offset - command_start).getOrElse(null)
+          document.current_state(command).get.type_at(offset - command_start).getOrElse(null)
         case None => null
       }
     }
diff -r a4fe43df58b3 -r d0057d9777ce src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Mon Jan 11 18:28:31 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Mon Jan 11 20:51:58 2010 +0100
@@ -45,7 +45,7 @@
         val offset = model.from_current(document, original_offset)
         document.command_at(offset) match {
           case Some((command, command_start)) =>
-            document.current_state(command).ref_at(offset - command_start) match {
+            document.current_state(command).get.ref_at(offset - command_start) match {
               case Some(ref) =>
                 val begin = model.to_current(document, command_start + ref.start)
                 val line = buffer.getLineOfOffset(begin)
diff -r a4fe43df58b3 -r d0057d9777ce src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Mon Jan 11 18:28:31 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Mon Jan 11 20:51:58 2010 +0100
@@ -45,7 +45,7 @@
       case Some(model) =>
         val document = model.recent_document()
         for ((command, command_start) <- document.command_range(0) if !stopped) {
-          root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
+          root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
               {
                 val content = command.source(node.start, node.stop)
                 val id = command.id
diff -r a4fe43df58b3 -r d0057d9777ce src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Mon Jan 11 18:28:31 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Mon Jan 11 20:51:58 2010 +0100
@@ -116,7 +116,7 @@
     var next_x = start
     for {
       (command, command_start) <- document.command_range(from(start), from(stop))
-      markup <- document.current_state(command).highlight.flatten
+      markup <- document.current_state(command).get.highlight.flatten
       val abs_start = to(command_start + markup.start)
       val abs_stop = to(command_start + markup.stop)
       if (abs_stop > start)
diff -r a4fe43df58b3 -r d0057d9777ce src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Jan 11 18:28:31 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Jan 11 20:51:58 2010 +0100
@@ -38,9 +38,7 @@
           Swing_Thread.now { Document_Model(view.getBuffer) } match {
             case None =>
             case Some(model) =>
-              val body =
-                if (cmd == null) Nil  // FIXME ??
-                else model.recent_document.current_state(cmd).results
+              val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
               html_panel.render(body)
           }
 
diff -r a4fe43df58b3 -r d0057d9777ce src/Tools/jEdit/src/proofdocument/document.scala
--- a/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 18:28:31 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 20:51:58 2010 +0100
@@ -123,25 +123,28 @@
 
     /* phase 3: resulting document edits */
 
-    val commands0 = old_doc.commands
-    val commands1 = edit_text(edits, commands0)
-    val commands2 = parse_spans(commands1)
+    val result = Library.timeit("text_edits") {
+      val commands0 = old_doc.commands
+      val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
+      val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
 
-    val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
-    val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
+      val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
+      val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
 
-    val doc_edits =
-      removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
-      inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
+      val doc_edits =
+        removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
+        inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
-    val former_states = old_doc.assignment.join -- removed_commands
+      val former_states = old_doc.assignment.join -- removed_commands
 
-    phase0 = edits
-    phase1 = commands1
-    phase2 = commands2
-    phase3 = doc_edits
+      phase0 = edits
+      phase1 = commands1
+      phase2 = commands2
+      phase3 = doc_edits
 
-    (doc_edits, new Document(new_id, commands2, former_states))
+      (doc_edits, new Document(new_id, commands2, former_states))
+    }
+    result
   }
 }
 
@@ -184,9 +187,9 @@
     tmp_states = Map()
   }
 
-  def current_state(cmd: Command): State =
+  def current_state(cmd: Command): Option[State] =
   {
     require(assignment.is_finished)
-    (assignment.join)(cmd).current_state
+    (assignment.join).get(cmd).map(_.current_state)
   }
 }