# HG changeset patch
# User wenzelm
# Date 1281562157 -7200
# Node ID 443fb83a21e8d8535f0c357503924f48335b6a60
# Parent  8cb265fb12fe5328ada78e5dcc8d585665318ef3
consider command state as part of Snapshot, not Document;

diff -r 8cb265fb12fe -r 443fb83a21e8 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Aug 11 22:41:26 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Aug 11 23:29:17 2010 +0200
@@ -101,6 +101,7 @@
     val is_outdated: Boolean
     def convert(offset: Int): Int
     def revert(offset: Int): Int
+    def state(command: Command): State
   }
 
   object Change
@@ -145,6 +146,7 @@
         val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
         def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
         def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+        def state(command: Command): State = document.current_state(command)
       }
     }
   }
diff -r 8cb265fb12fe -r 443fb83a21e8 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Wed Aug 11 22:41:26 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Wed Aug 11 23:29:17 2010 +0200
@@ -278,7 +278,7 @@
       for {
         (command, command_start) <-
           snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
-        markup <- snapshot.document.current_state(command).highlight.flatten
+        markup <- snapshot.state(command).highlight.flatten
         val abs_start = snapshot.convert(command_start + markup.start)
         val abs_stop = snapshot.convert(command_start + markup.stop)
         if (abs_stop > start)
diff -r 8cb265fb12fe -r 443fb83a21e8 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Wed Aug 11 22:41:26 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Wed Aug 11 23:29:17 2010 +0200
@@ -26,7 +26,7 @@
 {
   def choose_color(snapshot: Document.Snapshot, command: Command): Color =
   {
-    val state = snapshot.document.current_state(command)
+    val state = snapshot.state(command)
     if (snapshot.is_outdated) new Color(240, 240, 240)
     else if (state.forks > 0) new Color(255, 228, 225)
     else if (state.forks < 0) Color.red
@@ -203,7 +203,7 @@
       val offset = snapshot.revert(text_area.xyToOffset(x, y))
       snapshot.node.command_at(offset) match {
         case Some((command, command_start)) =>
-          snapshot.document.current_state(command).type_at(offset - command_start) match {
+          snapshot.state(command).type_at(offset - command_start) match {
             case Some(text) => Isabelle.tooltip(text)
             case None => null
           }
diff -r 8cb265fb12fe -r 443fb83a21e8 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Aug 11 22:41:26 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Aug 11 23:29:17 2010 +0200
@@ -47,7 +47,7 @@
         val offset = snapshot.revert(original_offset)
         snapshot.node.command_at(offset) match {
           case Some((command, command_start)) =>
-            snapshot.document.current_state(command).ref_at(offset - command_start) match {
+            snapshot.state(command).ref_at(offset - command_start) match {
               case Some(ref) =>
                 val begin = snapshot.convert(command_start + ref.start)
                 val line = buffer.getLineOfOffset(begin)
diff -r 8cb265fb12fe -r 443fb83a21e8 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Aug 11 22:41:26 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Aug 11 23:29:17 2010 +0200
@@ -130,7 +130,7 @@
     val root = data.root
     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
-      root.add(snapshot.document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
+      root.add(snapshot.state(command).markup_root.swing_tree((node: Markup_Node) =>
           {
             val content = command.source(node.start, node.stop).replace('\n', ' ')
             val id = command.id
diff -r 8cb265fb12fe -r 443fb83a21e8 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed Aug 11 22:41:26 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed Aug 11 23:29:17 2010 +0200
@@ -67,7 +67,7 @@
             case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
               val snapshot = doc_view.model.snapshot()
               val filtered_results =
-                snapshot.document.current_state(cmd).results filter {
+                snapshot.state(cmd).results filter {
                   case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
                   case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
                   case _ => true