tuned;
authorwenzelm
Wed Jul 03 15:19:36 2013 +0200 (2013-07-03)
changeset 5250898475be0b1a2
parent 52507 27925b58d6bd
child 52509 2193d2c7f586
tuned;
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
     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;
     2.1 --- a/src/Pure/PIDE/document.scala	Wed Jul 03 15:11:15 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Wed Jul 03 15:19:36 2013 +0200
     2.3 @@ -278,9 +278,14 @@
     2.4      def revert(i: Text.Offset): Text.Offset
     2.5      def revert(range: Text.Range): Text.Range
     2.6      def eq_content(other: Snapshot): Boolean
     2.7 -    def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
     2.8 +    def cumulate_markup[A](
     2.9 +      range: Text.Range,
    2.10 +      info: A,
    2.11 +      elements: Option[Set[String]],
    2.12        result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
    2.13 -    def select_markup[A](range: Text.Range, elements: Option[Set[String]],
    2.14 +    def select_markup[A](
    2.15 +      range: Text.Range,
    2.16 +      elements: Option[Set[String]],
    2.17        result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
    2.18    }
    2.19