# HG changeset patch
# User wenzelm
# Date 1326550829 -3600
# Node ID 4cab63a6dc160f2d7e8e3a0b49eb8c5f046a987a
# Parent  e76b77356ed6aff2359b6f29d0aa8ccd49b58840
tuned signature;

diff -r e76b77356ed6 -r 4cab63a6dc16 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Jan 14 14:34:42 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Jan 14 15:20:29 2012 +0100
@@ -234,7 +234,6 @@
     val version: Version
     val node: Node
     val is_outdated: Boolean
-    def command_state(command: Command): Command.State
     def convert(i: Text.Offset): Text.Offset
     def convert(range: Text.Range): Text.Range
     def revert(i: Text.Offset): Text.Offset
@@ -465,7 +464,6 @@
         val version = stable.version.get_finished
         val node = version.nodes(name)
         val is_outdated = !(pending_edits.isEmpty && latest == stable)
-        def command_state(command: Command): Command.State = state.command_state(version, command)
 
         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
         def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
@@ -478,7 +476,7 @@
           val former_range = revert(range)
           for {
             (command, command_start) <- node.command_range(former_range).toStream
-            Text.Info(r0, a) <- command_state(command).markup.
+            Text.Info(r0, a) <- state.command_state(version, command).markup.
               cumulate[A]((former_range - command_start).restrict(command.range), info, elements,
                 {
                   case (a, Text.Info(r0, b))
diff -r e76b77356ed6 -r 4cab63a6dc16 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Sat Jan 14 14:34:42 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Sat Jan 14 15:20:29 2012 +0100
@@ -58,9 +58,9 @@
 
   def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
   {
-    val state = snapshot.command_state(command)
     if (snapshot.is_outdated) None
     else {
+      val state = snapshot.state.command_state(snapshot.version, command)
       val status = Protocol.command_status(state.status)
 
       if (status.is_unprocessed) Some(unprocessed_color)
diff -r e76b77356ed6 -r 4cab63a6dc16 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Jan 14 14:34:42 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Jan 14 15:20:29 2012 +0100
@@ -152,7 +152,8 @@
     val root = data.root
     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
-      snapshot.command_state(command).markup.swing_tree(root)((info: Text.Markup) =>
+      snapshot.state.command_state(snapshot.version, command).markup
+        .swing_tree(root)((info: Text.Markup) =>
           {
             val range = info.range + command_start
             val content = command.source(info.range).replace('\n', ' ')
diff -r e76b77356ed6 -r 4cab63a6dc16 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sat Jan 14 14:34:42 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Jan 14 15:20:29 2012 +0100
@@ -86,11 +86,13 @@
             case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
               val snapshot = doc_view.update_snapshot()
               val filtered_results =
-                snapshot.command_state(cmd).results.iterator.map(_._2) filter {
-                  case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing  // FIXME not scalable
-                  case _ => true
-                }
-              html_panel.render(filtered_results.toList)
+                snapshot.state.command_state(snapshot.version, cmd).results.iterator
+                  .map(_._2).filter(
+                  { // FIXME not scalable
+                    case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
+                    case _ => true
+                  }).toList
+              html_panel.render(filtered_results)
             case _ =>
           }
         case None =>