src/Pure/PIDE/document.ML
changeset 52508 98475be0b1a2
parent 51294 0850d43cb355
child 52509 2193d2c7f586
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 03 15:11:15 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 03 15:19:36 2013 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  
     1.5  abstype node = Node of
     1.6   {header: node_header,  (*master directory, theory header, errors*)
     1.7 -  perspective: perspective,  (*visible commands, last*)
     1.8 +  perspective: perspective,  (*visible commands, last visible command*)
     1.9    entries: (exec_id * exec) option Entries.T * bool,  (*command entries with excecutions, stable*)
    1.10    result: exec option}  (*result of last execution*)
    1.11  and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
    1.12 @@ -336,7 +336,7 @@
    1.13  
    1.14      val _ =
    1.15        (singleton o Future.forks)
    1.16 -        {name = "execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
    1.17 +        {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
    1.18          (fn () =>
    1.19           (OS.Process.sleep (seconds 0.02);
    1.20            nodes_of (the_version state version_id) |> String_Graph.schedule
    1.21 @@ -551,7 +551,7 @@
    1.22  
    1.23  (** global state **)
    1.24  
    1.25 -val global_state = Synchronized.var "Document" init_state;
    1.26 +val global_state = Synchronized.var "Document.global_state" init_state;
    1.27  
    1.28  fun state () = Synchronized.value global_state;
    1.29  val change_state = Synchronized.change global_state;