1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jul 04 16:04:53 2013 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jul 04 23:51:47 2013 +0200
     1.3 @@ -81,8 +81,7 @@
     1.4    val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
     1.5    val skip_proof: (int -> int) -> transition -> transition
     1.6    val skip_proof_to_theory: (int -> bool) -> transition -> transition
     1.7 -  val get_id: transition -> string option
     1.8 -  val put_id: string -> transition -> transition
     1.9 +  val put_id: int -> transition -> transition
    1.10    val unknown_theory: transition -> transition
    1.11    val unknown_proof: transition -> transition
    1.12    val unknown_context: transition -> transition
    1.13 @@ -584,13 +583,10 @@
    1.14  
    1.15  (** toplevel transactions **)
    1.16  
    1.17 -(* identification *)
    1.18 +(* runtime position *)
    1.19  
    1.20 -fun get_id (Transition {pos, ...}) = Position.get_id pos;
    1.21 -fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr;
    1.22 -
    1.23 -
    1.24 -(* thread position *)
    1.25 +fun put_id id (tr as Transition {pos, ...}) =
    1.26 +  position (Position.put_id (Markup.print_int id) pos) tr;
    1.27  
    1.28  fun setmp_thread_position (Transition {pos, ...}) f x =
    1.29    Position.setmp_thread_data pos f x;

     2.1 --- a/src/Pure/PIDE/command.ML	Thu Jul 04 16:04:53 2013 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Thu Jul 04 23:51:47 2013 +0200
     2.3 @@ -23,8 +23,8 @@
     2.4    val no_eval: eval
     2.5    val eval: span -> Toplevel.transition -> eval_state -> eval_state
     2.6    type print_fn = Toplevel.transition -> Toplevel.state -> unit
     2.7 -  type print = {name: string, pri: int, print: unit memo}
     2.8 -  val print: string -> eval -> print list
     2.9 +  type print = {name: string, pri: int, exec_id: int, print: unit memo}
    2.10 +  val print: (unit -> int) -> string -> eval -> print list
    2.11    val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
    2.12  end;
    2.13  
    2.14 @@ -175,7 +175,7 @@
    2.15  
    2.16  (* print *)
    2.17  
    2.18 -type print = {name: string, pri: int, print: unit memo};
    2.19 +type print = {name: string, pri: int, exec_id: int, print: unit memo};
    2.20  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
    2.21  
    2.22  local
    2.23 @@ -192,18 +192,28 @@
    2.24  
    2.25  in
    2.26  
    2.27 -fun print command_name eval =
    2.28 +fun print new_id command_name eval =
    2.29    rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
    2.30      (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
    2.31        Exn.Res NONE => NONE
    2.32      | Exn.Res (SOME print_fn) =>
    2.33 -        SOME {name = name, pri = pri,
    2.34 -          print = memo (fn () =>
    2.35 -            let val {failed, command = tr, state = st', ...} = memo_result eval
    2.36 -            in if failed then () else print_error tr (fn () => print_fn tr st') () end)}
    2.37 +        let
    2.38 +          val exec_id = new_id ();
    2.39 +          fun body () =
    2.40 +            let
    2.41 +              val {failed, command, state = st', ...} = memo_result eval;
    2.42 +              val tr = Toplevel.put_id exec_id command;
    2.43 +            in if failed then () else print_error tr (fn () => print_fn tr st') () end;
    2.44 +        in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
    2.45      | Exn.Exn exn =>
    2.46 -        SOME {name = name, pri = pri,
    2.47 -          print = memo (fn () => output_error (#command (memo_result eval)) exn)}));
    2.48 +        let
    2.49 +          val exec_id = new_id ();
    2.50 +          fun body () =
    2.51 +            let
    2.52 +              val {command, ...} = memo_result eval;
    2.53 +              val tr = Toplevel.put_id exec_id command;
    2.54 +            in output_error tr exn end;
    2.55 +        in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end));
    2.56  
    2.57  fun print_function {name, pri} f =
    2.58    Synchronized.change print_functions (fn funs =>

     3.1 --- a/src/Pure/PIDE/command.scala	Thu Jul 04 16:04:53 2013 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Thu Jul 04 23:51:47 2013 +0200
     3.3 @@ -75,7 +75,7 @@
     3.4      private def add_status(st: Markup): State = copy(status = st :: status)
     3.5      private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
     3.6  
     3.7 -    def + (alt_id: Document.ID, message: XML.Elem): Command.State =
     3.8 +    def + (alt_id: Document.ID, message: XML.Elem): State =
     3.9        message match {
    3.10          case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    3.11            (this /: msgs)((state, msg) =>
    3.12 @@ -125,6 +125,9 @@
    3.13              case _ => System.err.println("Ignored message without serial number: " + message); this
    3.14            }
    3.15        }
    3.16 +
    3.17 +    def ++ (other: State): State =
    3.18 +      copy(results = results ++ other.results)  // FIXME merge more content!?
    3.19    }
    3.20  
    3.21  
    3.22 @@ -240,4 +243,6 @@
    3.23  
    3.24    val init_state: Command.State =
    3.25      Command.State(this, results = init_results, markup = init_markup)
    3.26 +
    3.27 +  val empty_state: Command.State = Command.State(this)
    3.28  }

     4.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 04 16:04:53 2013 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 04 23:51:47 2013 +0200
     4.3 @@ -31,7 +31,7 @@
     4.4    val start_execution: state -> unit
     4.5    val timing: bool Unsynchronized.ref
     4.6    val update: version_id -> version_id -> edit list -> state ->
     4.7 -    (command_id * exec_id option) list * state
     4.8 +    (command_id * exec_id list) list * state
     4.9    val state: unit -> state
    4.10    val change_state: (state -> state) -> unit
    4.11  end;
    4.12 @@ -61,11 +61,13 @@
    4.13  type exec = exec_id * (Command.eval * Command.print list);  (*eval/print process*)
    4.14  val no_exec: exec = (no_id, (Command.no_eval, []));
    4.15  
    4.16 +fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
    4.17 +
    4.18  fun exec_result ((_, (eval, _)): exec) = Command.memo_result eval;
    4.19  
    4.20  fun exec_run ((_, (eval, prints)): exec) =
    4.21   (Command.memo_eval eval;
    4.22 -  prints |> List.app (fn {name, pri, print} =>
    4.23 +  prints |> List.app (fn {name, pri, print, ...} =>
    4.24      Command.memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
    4.25  
    4.26  
    4.27 @@ -121,7 +123,6 @@
    4.28    map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
    4.29  
    4.30  val visible_commands = #1 o get_perspective;
    4.31 -val visible_command = Inttab.defined o visible_commands;
    4.32  val visible_last = #2 o get_perspective;
    4.33  val visible_node = is_some o visible_last
    4.34  
    4.35 @@ -313,10 +314,14 @@
    4.36  
    4.37  (* consolidated states *)
    4.38  
    4.39 -fun stable_command ((exec_id, (eval, prints)): exec) =
    4.40 -  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
    4.41 -  Command.memo_stable eval andalso
    4.42 -  forall (Command.memo_stable o #print) prints;
    4.43 +fun stable_goals exec_id =
    4.44 +  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
    4.45 +
    4.46 +fun stable_eval ((exec_id, (eval, _)): exec) =
    4.47 +  stable_goals exec_id andalso Command.memo_stable eval;
    4.48 +
    4.49 +fun stable_print ({exec_id, print, ...}: Command.print) =
    4.50 +  stable_goals exec_id andalso Command.memo_stable print;
    4.51  
    4.52  fun finished_theory node =
    4.53    (case Exn.capture (Command.memo_result o the) (get_result node) of
    4.54 @@ -422,7 +427,7 @@
    4.55              | SOME (exec_id, exec) =>
    4.56                  (case lookup_entry node0 id of
    4.57                    NONE => false
    4.58 -                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command (exec_id, exec)));
    4.59 +                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_eval (exec_id, exec)));
    4.60          in SOME (same', (prev, flags')) end
    4.61        else NONE;
    4.62      val (same, (common, flags)) =
    4.63 @@ -438,11 +443,11 @@
    4.64    if not proper_init andalso is_none init then NONE
    4.65    else
    4.66      let
    4.67 -      val (name, span) = the_command state command_id' ||> Lazy.force;
    4.68 +      val (command_name, span) = the_command state command_id' ||> Lazy.force;
    4.69  
    4.70        fun illegal_init _ = error "Illegal theory header after end of theory";
    4.71        val (modify_init, init') =
    4.72 -        if Keyword.is_theory_begin name then
    4.73 +        if Keyword.is_theory_begin command_name then
    4.74            (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
    4.75          else (I, init);
    4.76  
    4.77 @@ -456,13 +461,29 @@
    4.78                  (fn () =>
    4.79                    Command.read span
    4.80                    |> modify_init
    4.81 -                  |> Toplevel.put_id (print_id exec_id')) ();
    4.82 +                  |> Toplevel.put_id exec_id') ();
    4.83            in Command.eval span tr eval_state end);
    4.84 -      val prints' = if command_visible then Command.print name eval' else [];
    4.85 -
    4.86 +      val prints' = if command_visible then Command.print new_id command_name eval' else [];
    4.87        val command_exec' = (command_id', (exec_id', (eval', prints')));
    4.88      in SOME (command_exec' :: execs, command_exec', init') end;
    4.89  
    4.90 +fun update_prints state node command_id =
    4.91 +  (case the_entry node command_id of
    4.92 +    SOME (exec_id, (eval, prints)) =>
    4.93 +      let
    4.94 +        val (command_name, _) = the_command state command_id;
    4.95 +        val new_prints = Command.print new_id command_name eval;
    4.96 +        val prints' =
    4.97 +          new_prints |> map (fn new_print =>
    4.98 +            (case find_first (fn {name, ...} => name = #name new_print) prints of
    4.99 +              SOME print => if stable_print print then print else new_print
   4.100 +            | NONE => new_print));
   4.101 +      in
   4.102 +        if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
   4.103 +        else SOME (command_id, (exec_id, (eval, prints')))
   4.104 +      end
   4.105 +  | NONE => NONE);
   4.106 +
   4.107  in
   4.108  
   4.109  fun update (old_id: version_id) (new_id: version_id) edits state =
   4.110 @@ -483,10 +504,10 @@
   4.111              (fn () =>
   4.112                let
   4.113                  val imports = map (apsnd Future.join) deps;
   4.114 -                val updated_imports = exists (is_some o #3 o #1 o #2) imports;
   4.115 +                val changed_imports = exists (#4 o #1 o #2) imports;
   4.116                  val node_required = is_required name;
   4.117                in
   4.118 -                if updated_imports orelse AList.defined (op =) edits name orelse
   4.119 +                if changed_imports orelse AList.defined (op =) edits name orelse
   4.120                    not (stable_entries node) orelse not (finished_theory node)
   4.121                  then
   4.122                    let
   4.123 @@ -496,9 +517,12 @@
   4.124                        check_theory false name node andalso
   4.125                        forall (fn (name, (_, node)) => check_theory true name node) imports;
   4.126  
   4.127 +                    val visible_commands = visible_commands node;
   4.128 +                    val visible_command = Inttab.defined visible_commands;
   4.129                      val last_visible = visible_last node;
   4.130 +
   4.131                      val (common, (still_visible, initial)) =
   4.132 -                      if updated_imports then (NONE, (true, true))
   4.133 +                      if changed_imports then (NONE, (true, true))
   4.134                        else last_common state last_visible node0 node;
   4.135                      val common_command_exec = the_default_entry node common;
   4.136  
   4.137 @@ -508,13 +532,18 @@
   4.138                          iterate_entries_after common
   4.139                            (fn ((prev, id), _) => fn res =>
   4.140                              if not node_required andalso prev = last_visible then NONE
   4.141 -                            else new_exec state proper_init (visible_command node id) id res) node;
   4.142 +                            else new_exec state proper_init (visible_command id) id res) node;
   4.143 +
   4.144 +                    val updated_execs =
   4.145 +                      (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
   4.146 +                        if exists (fn (_, (id', _)) => id = id') new_execs then I
   4.147 +                        else append (the_list (update_prints state node id)));
   4.148  
   4.149                      val no_execs =
   4.150                        iterate_entries_after common
   4.151                          (fn ((_, id0), exec0) => fn res =>
   4.152                            if is_none exec0 then NONE
   4.153 -                          else if exists (fn (_, (id, _)) => id0 = id) new_execs
   4.154 +                          else if exists (fn (_, (id, _)) => id0 = id) updated_execs
   4.155                            then SOME res
   4.156                            else SOME (id0 :: res)) node0 [];
   4.157  
   4.158 @@ -525,20 +554,21 @@
   4.159  
   4.160                      val node' = node
   4.161                        |> fold reset_entry no_execs
   4.162 -                      |> fold (fn (id, exec) => update_entry id (SOME exec)) new_execs
   4.163 -                      |> entries_stable (null new_execs)
   4.164 +                      |> fold (fn (id, exec) => update_entry id (SOME exec)) updated_execs
   4.165 +                      |> entries_stable (null updated_execs)
   4.166                        |> set_result result;
   4.167                      val updated_node =
   4.168 -                      if null no_execs andalso null new_execs then NONE
   4.169 +                      if null no_execs andalso null updated_execs then NONE
   4.170                        else SOME (name, node');
   4.171 -                  in ((no_execs, new_execs, updated_node), node') end
   4.172 -                else (([], [], NONE), node)
   4.173 +                    val changed_result = not (null no_execs) orelse not (null new_execs);
   4.174 +                  in ((no_execs, updated_execs, updated_node, changed_result), node') end
   4.175 +                else (([], [], NONE, false), node)
   4.176                end))
   4.177        |> Future.joins |> map #1);
   4.178  
   4.179      val command_execs =
   4.180 -      map (rpair NONE) (maps #1 updated) @
   4.181 -      map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
   4.182 +      map (rpair []) (maps #1 updated) @
   4.183 +      map (fn (command_id, exec) => (command_id, exec_ids_of exec)) (maps #2 updated);
   4.184      val updated_nodes = map_filter #3 updated;
   4.185  
   4.186      val state' = state

     5.1 --- a/src/Pure/PIDE/document.scala	Thu Jul 04 16:04:53 2013 +0200
     5.2 +++ b/src/Pure/PIDE/document.scala	Thu Jul 04 23:51:47 2013 +0200
     5.3 @@ -289,7 +289,7 @@
     5.4        result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
     5.5    }
     5.6  
     5.7 -  type Assign = List[(Document.Command_ID, Option[Document.Exec_ID])]  // exec state assignment
     5.8 +  type Assign = List[(Document.Command_ID, List[Document.Exec_ID])]  // exec state assignment
     5.9  
    5.10    object State
    5.11    {
    5.12 @@ -301,19 +301,19 @@
    5.13      }
    5.14  
    5.15      final class Assignment private(
    5.16 -      val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
    5.17 +      val command_execs: Map[Command_ID, List[Exec_ID]] = Map.empty,
    5.18        val is_finished: Boolean = false)
    5.19      {
    5.20        def check_finished: Assignment = { require(is_finished); this }
    5.21        def unfinished: Assignment = new Assignment(command_execs, false)
    5.22  
    5.23 -      def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])]): Assignment =
    5.24 +      def assign(add_command_execs: List[(Command_ID, List[Exec_ID])]): Assignment =
    5.25        {
    5.26          require(!is_finished)
    5.27          val command_execs1 =
    5.28            (command_execs /: add_command_execs) {
    5.29 -            case (res, (command_id, None)) => res - command_id
    5.30 -            case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
    5.31 +            case (res, (command_id, Nil)) => res - command_id
    5.32 +            case (res, assign) => res + assign
    5.33            }
    5.34          new Assignment(command_execs1, true)
    5.35        }
    5.36 @@ -357,8 +357,8 @@
    5.37        }
    5.38  
    5.39      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
    5.40 -    def the_command_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
    5.41 -    def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
    5.42 +    def the_read_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
    5.43 +    def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
    5.44      def the_assignment(version: Version): State.Assignment =
    5.45        assignments.getOrElse(version.id, fail)
    5.46  
    5.47 @@ -383,12 +383,17 @@
    5.48        val (changed_commands, new_execs) =
    5.49          ((Nil: List[Command], execs) /: command_execs) {
    5.50            case ((commands1, execs1), (cmd_id, exec)) =>
    5.51 -            val st = the_command_state(cmd_id)
    5.52 -            val commands2 = st.command :: commands1
    5.53 +            val st1 = the_read_state(cmd_id)
    5.54 +            val command = st1.command
    5.55 +            val st0 = command.empty_state
    5.56 +
    5.57 +            val commands2 = command :: commands1
    5.58              val execs2 =
    5.59                exec match {
    5.60 -                case None => execs1
    5.61 -                case Some(exec_id) => execs1 + (exec_id -> st)
    5.62 +                case Nil => execs1
    5.63 +                case eval_id :: print_ids =>
    5.64 +                  execs1 + (eval_id -> execs.getOrElse(eval_id, st1)) ++
    5.65 +                    print_ids.iterator.map(id => id -> execs.getOrElse(id, st0))
    5.66                }
    5.67              (commands2, execs2)
    5.68          }
    5.69 @@ -445,12 +450,11 @@
    5.70          command <- node.commands.iterator
    5.71        } {
    5.72          val id = command.id
    5.73 -        if (!commands1.isDefinedAt(id) && commands.isDefinedAt(id))
    5.74 -          commands1 += (id -> commands(id))
    5.75 -        if (command_execs.isDefinedAt(id)) {
    5.76 -          val exec_id = command_execs(id)
    5.77 -          if (!execs1.isDefinedAt(exec_id) && execs.isDefinedAt(exec_id))
    5.78 -            execs1 += (exec_id -> execs(exec_id))
    5.79 +        if (!commands1.isDefinedAt(id))
    5.80 +          commands.get(id).foreach(st => commands1 += (id -> st))
    5.81 +        for (exec_id <- command_execs.getOrElse(id, Nil)) {
    5.82 +          if (!execs1.isDefinedAt(exec_id))
    5.83 +            execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
    5.84          }
    5.85        }
    5.86        copy(versions = versions1, commands = commands1, execs = execs1, assignments = assignments1)
    5.87 @@ -460,12 +464,15 @@
    5.88      {
    5.89        require(is_assigned(version))
    5.90        try {
    5.91 -        the_exec(the_assignment(version).check_finished.command_execs
    5.92 -          .getOrElse(command.id, fail))
    5.93 +        the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
    5.94 +          .map(the_exec_state(_)) match {
    5.95 +            case eval_state :: print_states => (eval_state /: print_states)(_ ++ _)
    5.96 +            case Nil => fail
    5.97 +          }
    5.98        }
    5.99        catch {
   5.100          case _: State.Fail =>
   5.101 -          try { the_command_state(command.id) }
   5.102 +          try { the_read_state(command.id) }
   5.103            catch { case _: State.Fail => command.init_state }
   5.104        }
   5.105      }

     6.1 --- a/src/Pure/PIDE/protocol.ML	Thu Jul 04 16:04:53 2013 +0200
     6.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Jul 04 23:51:47 2013 +0200
     6.3 @@ -53,7 +53,7 @@
     6.4            Output.protocol_message Markup.assign_execs
     6.5              ((new_id, assignment) |>
     6.6                let open XML.Encode
     6.7 -              in pair int (list (pair int (option int))) end
     6.8 +              in pair int (list (pair int (list int))) end
     6.9                |> YXML.string_of_body);
    6.10  
    6.11          val _ = List.app Future.cancel_group (Goal.reset_futures ());

     7.1 --- a/src/Pure/PIDE/protocol.scala	Thu Jul 04 16:04:53 2013 +0200
     7.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Jul 04 23:51:47 2013 +0200
     7.3 @@ -17,7 +17,7 @@
     7.4        try {
     7.5          import XML.Decode._
     7.6          val body = YXML.parse_body(text)
     7.7 -        Some(pair(long, list(pair(long, option(long))))(body))
     7.8 +        Some(pair(long, list(pair(long, list(long))))(body))
     7.9        }
    7.10        catch {
    7.11          case ERROR(_) => None

     8.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Jul 04 16:04:53 2013 +0200
     8.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Jul 04 23:51:47 2013 +0200
     8.3 @@ -38,7 +38,7 @@
     8.4      val state1 =
     8.5        state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
     8.6          .define_version(version1, state0.the_assignment(version0))
     8.7 -        .assign(version1.id, List(command.id -> Some(Document.new_id())))._2
     8.8 +        .assign(version1.id, List(command.id -> List(Document.new_id())))._2
     8.9  
    8.10      (command.source, state1)
    8.11    }