src/Pure/PIDE/command.ML

--- 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 =>