# HG changeset patch
# User wenzelm
# Date 1372857576 -7200
# Node ID 98475be0b1a211e2b7e4e2c069345f75aaa99824
# Parent  27925b58d6bdf67b95d462b92b932c03deb963f9
tuned;

diff -r 27925b58d6bd -r 98475be0b1a2 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Jul 03 15:11:15 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Jul 03 15:19:36 2013 +0200
@@ -68,7 +68,7 @@
 
 abstype node = Node of
  {header: node_header,  (*master directory, theory header, errors*)
-  perspective: perspective,  (*visible commands, last*)
+  perspective: perspective,  (*visible commands, last visible command*)
   entries: (exec_id * exec) option Entries.T * bool,  (*command entries with excecutions, stable*)
   result: exec option}  (*result of last execution*)
 and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
@@ -336,7 +336,7 @@
 
     val _ =
       (singleton o Future.forks)
-        {name = "execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
+        {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
         (fn () =>
          (OS.Process.sleep (seconds 0.02);
           nodes_of (the_version state version_id) |> String_Graph.schedule
@@ -551,7 +551,7 @@
 
 (** global state **)
 
-val global_state = Synchronized.var "Document" init_state;
+val global_state = Synchronized.var "Document.global_state" init_state;
 
 fun state () = Synchronized.value global_state;
 val change_state = Synchronized.change global_state;
diff -r 27925b58d6bd -r 98475be0b1a2 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Jul 03 15:11:15 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Jul 03 15:19:36 2013 +0200
@@ -278,9 +278,14 @@
     def revert(i: Text.Offset): Text.Offset
     def revert(range: Text.Range): Text.Range
     def eq_content(other: Snapshot): Boolean
-    def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
+    def cumulate_markup[A](
+      range: Text.Range,
+      info: A,
+      elements: Option[Set[String]],
       result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
-    def select_markup[A](range: Text.Range, elements: Option[Set[String]],
+    def select_markup[A](
+      range: Text.Range,
+      elements: Option[Set[String]],
       result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
   }