separate exec_id assignment for Command.print states, without affecting result of eval;
tuned signature;
tuned;

--- a/src/Pure/Isar/toplevel.ML	Thu Jul 04 16:04:53 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Jul 04 23:51:47 2013 +0200
@@ -81,8 +81,7 @@
   val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
   val skip_proof: (int -> int) -> transition -> transition
   val skip_proof_to_theory: (int -> bool) -> transition -> transition
-  val get_id: transition -> string option
-  val put_id: string -> transition -> transition
+  val put_id: int -> transition -> transition
   val unknown_theory: transition -> transition
   val unknown_proof: transition -> transition
   val unknown_context: transition -> transition
@@ -584,13 +583,10 @@
 
 (** toplevel transactions **)
 
-(* identification *)
+(* runtime position *)
 
-fun get_id (Transition {pos, ...}) = Position.get_id pos;
-fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr;
-
-
-(* thread position *)
+fun put_id id (tr as Transition {pos, ...}) =
+  position (Position.put_id (Markup.print_int id) pos) tr;
 
 fun setmp_thread_position (Transition {pos, ...}) f x =
   Position.setmp_thread_data pos f x;

--- a/src/Pure/PIDE/command.ML	Thu Jul 04 16:04:53 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Thu Jul 04 23:51:47 2013 +0200
@@ -23,8 +23,8 @@
   val no_eval: eval
   val eval: span -> Toplevel.transition -> eval_state -> eval_state
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
-  type print = {name: string, pri: int, print: unit memo}
-  val print: string -> eval -> print list
+  type print = {name: string, pri: int, exec_id: int, print: unit memo}
+  val print: (unit -> int) -> string -> eval -> print list
   val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
 end;
 
@@ -175,7 +175,7 @@
 
 (* print *)
 
-type print = {name: string, pri: int, print: unit memo};
+type print = {name: string, pri: int, exec_id: int, print: unit memo};
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
 local
@@ -192,18 +192,28 @@
 
 in
 
-fun print command_name eval =
+fun print new_id command_name eval =
   rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
     (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
       Exn.Res NONE => NONE
     | Exn.Res (SOME print_fn) =>
-        SOME {name = name, pri = pri,
-          print = memo (fn () =>
-            let val {failed, command = tr, state = st', ...} = memo_result eval
-            in if failed then () else print_error tr (fn () => print_fn tr st') () end)}
+        let
+          val exec_id = new_id ();
+          fun body () =
+            let
+              val {failed, command, state = st', ...} = memo_result eval;
+              val tr = Toplevel.put_id exec_id command;
+            in if failed then () else print_error tr (fn () => print_fn tr st') () end;
+        in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
     | Exn.Exn exn =>
-        SOME {name = name, pri = pri,
-          print = memo (fn () => output_error (#command (memo_result eval)) exn)}));
+        let
+          val exec_id = new_id ();
+          fun body () =
+            let
+              val {command, ...} = memo_result eval;
+              val tr = Toplevel.put_id exec_id command;
+            in output_error tr exn end;
+        in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end));
 
 fun print_function {name, pri} f =
   Synchronized.change print_functions (fn funs =>

--- a/src/Pure/PIDE/command.scala	Thu Jul 04 16:04:53 2013 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Jul 04 23:51:47 2013 +0200
@@ -75,7 +75,7 @@
     private def add_status(st: Markup): State = copy(status = st :: status)
     private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
 
-    def + (alt_id: Document.ID, message: XML.Elem): Command.State =
+    def + (alt_id: Document.ID, message: XML.Elem): State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>
@@ -125,6 +125,9 @@
             case _ => System.err.println("Ignored message without serial number: " + message); this
           }
       }
+
+    def ++ (other: State): State =
+      copy(results = results ++ other.results)  // FIXME merge more content!?
   }
 
 
@@ -240,4 +243,6 @@
 
   val init_state: Command.State =
     Command.State(this, results = init_results, markup = init_markup)
+
+  val empty_state: Command.State = Command.State(this)
 }

--- a/src/Pure/PIDE/document.ML	Thu Jul 04 16:04:53 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Jul 04 23:51:47 2013 +0200
@@ -31,7 +31,7 @@
   val start_execution: state -> unit
   val timing: bool Unsynchronized.ref
   val update: version_id -> version_id -> edit list -> state ->
-    (command_id * exec_id option) list * state
+    (command_id * exec_id list) list * state
   val state: unit -> state
   val change_state: (state -> state) -> unit
 end;
@@ -61,11 +61,13 @@
 type exec = exec_id * (Command.eval * Command.print list);  (*eval/print process*)
 val no_exec: exec = (no_id, (Command.no_eval, []));
 
+fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
+
 fun exec_result ((_, (eval, _)): exec) = Command.memo_result eval;
 
 fun exec_run ((_, (eval, prints)): exec) =
  (Command.memo_eval eval;
-  prints |> List.app (fn {name, pri, print} =>
+  prints |> List.app (fn {name, pri, print, ...} =>
     Command.memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
 
 
@@ -121,7 +123,6 @@
   map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
 
 val visible_commands = #1 o get_perspective;
-val visible_command = Inttab.defined o visible_commands;
 val visible_last = #2 o get_perspective;
 val visible_node = is_some o visible_last
 
@@ -313,10 +314,14 @@
 
 (* consolidated states *)
 
-fun stable_command ((exec_id, (eval, prints)): exec) =
-  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
-  Command.memo_stable eval andalso
-  forall (Command.memo_stable o #print) prints;
+fun stable_goals exec_id =
+  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
+
+fun stable_eval ((exec_id, (eval, _)): exec) =
+  stable_goals exec_id andalso Command.memo_stable eval;
+
+fun stable_print ({exec_id, print, ...}: Command.print) =
+  stable_goals exec_id andalso Command.memo_stable print;
 
 fun finished_theory node =
   (case Exn.capture (Command.memo_result o the) (get_result node) of
@@ -422,7 +427,7 @@
             | SOME (exec_id, exec) =>
                 (case lookup_entry node0 id of
                   NONE => false
-                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command (exec_id, exec)));
+                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_eval (exec_id, exec)));
         in SOME (same', (prev, flags')) end
       else NONE;
     val (same, (common, flags)) =
@@ -438,11 +443,11 @@
   if not proper_init andalso is_none init then NONE
   else
     let
-      val (name, span) = the_command state command_id' ||> Lazy.force;
+      val (command_name, span) = the_command state command_id' ||> Lazy.force;
 
       fun illegal_init _ = error "Illegal theory header after end of theory";
       val (modify_init, init') =
-        if Keyword.is_theory_begin name then
+        if Keyword.is_theory_begin command_name then
           (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
         else (I, init);
 
@@ -456,13 +461,29 @@
                 (fn () =>
                   Command.read span
                   |> modify_init
-                  |> Toplevel.put_id (print_id exec_id')) ();
+                  |> Toplevel.put_id exec_id') ();
           in Command.eval span tr eval_state end);
-      val prints' = if command_visible then Command.print name eval' else [];
-
+      val prints' = if command_visible then Command.print new_id command_name eval' else [];
       val command_exec' = (command_id', (exec_id', (eval', prints')));
     in SOME (command_exec' :: execs, command_exec', init') end;
 
+fun update_prints state node command_id =
+  (case the_entry node command_id of
+    SOME (exec_id, (eval, prints)) =>
+      let
+        val (command_name, _) = the_command state command_id;
+        val new_prints = Command.print new_id command_name eval;
+        val prints' =
+          new_prints |> map (fn new_print =>
+            (case find_first (fn {name, ...} => name = #name new_print) prints of
+              SOME print => if stable_print print then print else new_print
+            | NONE => new_print));
+      in
+        if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
+        else SOME (command_id, (exec_id, (eval, prints')))
+      end
+  | NONE => NONE);
+
 in
 
 fun update (old_id: version_id) (new_id: version_id) edits state =
@@ -483,10 +504,10 @@
             (fn () =>
               let
                 val imports = map (apsnd Future.join) deps;
-                val updated_imports = exists (is_some o #3 o #1 o #2) imports;
+                val changed_imports = exists (#4 o #1 o #2) imports;
                 val node_required = is_required name;
               in
-                if updated_imports orelse AList.defined (op =) edits name orelse
+                if changed_imports orelse AList.defined (op =) edits name orelse
                   not (stable_entries node) orelse not (finished_theory node)
                 then
                   let
@@ -496,9 +517,12 @@
                       check_theory false name node andalso
                       forall (fn (name, (_, node)) => check_theory true name node) imports;
 
+                    val visible_commands = visible_commands node;
+                    val visible_command = Inttab.defined visible_commands;
                     val last_visible = visible_last node;
+
                     val (common, (still_visible, initial)) =
-                      if updated_imports then (NONE, (true, true))
+                      if changed_imports then (NONE, (true, true))
                       else last_common state last_visible node0 node;
                     val common_command_exec = the_default_entry node common;
 
@@ -508,13 +532,18 @@
                         iterate_entries_after common
                           (fn ((prev, id), _) => fn res =>
                             if not node_required andalso prev = last_visible then NONE
-                            else new_exec state proper_init (visible_command node id) id res) node;
+                            else new_exec state proper_init (visible_command id) id res) node;
+
+                    val updated_execs =
+                      (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
+                        if exists (fn (_, (id', _)) => id = id') new_execs then I
+                        else append (the_list (update_prints state node id)));
 
                     val no_execs =
                       iterate_entries_after common
                         (fn ((_, id0), exec0) => fn res =>
                           if is_none exec0 then NONE
-                          else if exists (fn (_, (id, _)) => id0 = id) new_execs
+                          else if exists (fn (_, (id, _)) => id0 = id) updated_execs
                           then SOME res
                           else SOME (id0 :: res)) node0 [];
 
@@ -525,20 +554,21 @@
 
                     val node' = node
                       |> fold reset_entry no_execs
-                      |> fold (fn (id, exec) => update_entry id (SOME exec)) new_execs
-                      |> entries_stable (null new_execs)
+                      |> fold (fn (id, exec) => update_entry id (SOME exec)) updated_execs
+                      |> entries_stable (null updated_execs)
                       |> set_result result;
                     val updated_node =
-                      if null no_execs andalso null new_execs then NONE
+                      if null no_execs andalso null updated_execs then NONE
                       else SOME (name, node');
-                  in ((no_execs, new_execs, updated_node), node') end
-                else (([], [], NONE), node)
+                    val changed_result = not (null no_execs) orelse not (null new_execs);
+                  in ((no_execs, updated_execs, updated_node, changed_result), node') end
+                else (([], [], NONE, false), node)
               end))
       |> Future.joins |> map #1);
 
     val command_execs =
-      map (rpair NONE) (maps #1 updated) @
-      map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
+      map (rpair []) (maps #1 updated) @
+      map (fn (command_id, exec) => (command_id, exec_ids_of exec)) (maps #2 updated);
     val updated_nodes = map_filter #3 updated;
 
     val state' = state

--- a/src/Pure/PIDE/document.scala	Thu Jul 04 16:04:53 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Jul 04 23:51:47 2013 +0200
@@ -289,7 +289,7 @@
       result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
   }
 
-  type Assign = List[(Document.Command_ID, Option[Document.Exec_ID])]  // exec state assignment
+  type Assign = List[(Document.Command_ID, List[Document.Exec_ID])]  // exec state assignment
 
   object State
   {
@@ -301,19 +301,19 @@
     }
 
     final class Assignment private(
-      val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
+      val command_execs: Map[Command_ID, List[Exec_ID]] = Map.empty,
       val is_finished: Boolean = false)
     {
       def check_finished: Assignment = { require(is_finished); this }
       def unfinished: Assignment = new Assignment(command_execs, false)
 
-      def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])]): Assignment =
+      def assign(add_command_execs: List[(Command_ID, List[Exec_ID])]): Assignment =
       {
         require(!is_finished)
         val command_execs1 =
           (command_execs /: add_command_execs) {
-            case (res, (command_id, None)) => res - command_id
-            case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
+            case (res, (command_id, Nil)) => res - command_id
+            case (res, assign) => res + assign
           }
         new Assignment(command_execs1, true)
       }
@@ -357,8 +357,8 @@
       }
 
     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
-    def the_command_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
-    def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
+    def the_read_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
+    def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
     def the_assignment(version: Version): State.Assignment =
       assignments.getOrElse(version.id, fail)
 
@@ -383,12 +383,17 @@
       val (changed_commands, new_execs) =
         ((Nil: List[Command], execs) /: command_execs) {
           case ((commands1, execs1), (cmd_id, exec)) =>
-            val st = the_command_state(cmd_id)
-            val commands2 = st.command :: commands1
+            val st1 = the_read_state(cmd_id)
+            val command = st1.command
+            val st0 = command.empty_state
+
+            val commands2 = command :: commands1
             val execs2 =
               exec match {
-                case None => execs1
-                case Some(exec_id) => execs1 + (exec_id -> st)
+                case Nil => execs1
+                case eval_id :: print_ids =>
+                  execs1 + (eval_id -> execs.getOrElse(eval_id, st1)) ++
+                    print_ids.iterator.map(id => id -> execs.getOrElse(id, st0))
               }
             (commands2, execs2)
         }
@@ -445,12 +450,11 @@
         command <- node.commands.iterator
       } {
         val id = command.id
-        if (!commands1.isDefinedAt(id) && commands.isDefinedAt(id))
-          commands1 += (id -> commands(id))
-        if (command_execs.isDefinedAt(id)) {
-          val exec_id = command_execs(id)
-          if (!execs1.isDefinedAt(exec_id) && execs.isDefinedAt(exec_id))
-            execs1 += (exec_id -> execs(exec_id))
+        if (!commands1.isDefinedAt(id))
+          commands.get(id).foreach(st => commands1 += (id -> st))
+        for (exec_id <- command_execs.getOrElse(id, Nil)) {
+          if (!execs1.isDefinedAt(exec_id))
+            execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
         }
       }
       copy(versions = versions1, commands = commands1, execs = execs1, assignments = assignments1)
@@ -460,12 +464,15 @@
     {
       require(is_assigned(version))
       try {
-        the_exec(the_assignment(version).check_finished.command_execs
-          .getOrElse(command.id, fail))
+        the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
+          .map(the_exec_state(_)) match {
+            case eval_state :: print_states => (eval_state /: print_states)(_ ++ _)
+            case Nil => fail
+          }
       }
       catch {
         case _: State.Fail =>
-          try { the_command_state(command.id) }
+          try { the_read_state(command.id) }
           catch { case _: State.Fail => command.init_state }
       }
     }

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

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

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