allow multiple print functions;

--- a/src/Pure/PIDE/command.ML	Wed Jul 03 16:58:35 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Jul 03 17:50:47 2013 +0200
@@ -17,8 +17,9 @@
   val read: span -> Toplevel.transition
   val eval: span -> Toplevel.transition ->
     Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
-  val no_print: unit lazy
-  val print: Toplevel.transition -> Toplevel.state -> unit lazy
+  val print: Toplevel.transition -> Toplevel.state -> (string * unit lazy) list
+  val print_function: string ->
+    ({tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option) -> unit
 end;
 
 structure Command: COMMAND =
@@ -150,21 +151,38 @@
 
 (* print *)
 
-val no_print = Lazy.value ();
+local
+
+type print_function =
+  {tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option;
+
+val print_functions =
+  Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
+
+in
 
 fun print tr st' =
+  rev (Synchronized.value print_functions) |> map_filter (fn (name, f) =>
+    (case f {tr = tr, state = st'} of
+      SOME pr => SOME (name, (Lazy.lazy o Toplevel.setmp_thread_position tr) pr)
+    | NONE => NONE));
+
+fun print_function name f =
+  Synchronized.change print_functions (fn funs =>
+   (if not (AList.defined (op =) funs name) then ()
+    else warning ("Redefining command print function: " ^ quote name);
+    AList.update (op =) (name, f) funs));
+
+end;
+
+val _ = print_function "print_state" (fn {tr, state} =>
   let
     val is_init = Toplevel.is_init tr;
     val is_proof = Keyword.is_proof (Toplevel.name_of tr);
     val do_print =
       not is_init andalso
-        (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
-  in
-    if do_print then
-      (Lazy.lazy o Toplevel.setmp_thread_position tr)
-        (fn () => Toplevel.print_state false st')
-    else no_print
-  end;
+        (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof state));
+  in if do_print then SOME (fn () => Toplevel.print_state false state) else NONE end);
 
 end;
 

--- a/src/Pure/PIDE/document.ML	Wed Jul 03 16:58:35 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Jul 03 17:50:47 2013 +0200
@@ -63,8 +63,9 @@
 type perspective = (command_id -> bool) * command_id option;
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
-type exec = ((Toplevel.state * {malformed: bool}) * unit lazy) Command.memo;  (*eval/print process*)
-val no_exec = Command.memo_value ((Toplevel.toplevel, {malformed = false}), Lazy.value ());
+type print = string * unit lazy;
+type exec = ((Toplevel.state * {malformed: bool}) * print list) Command.memo; (*eval/print process*)
+val no_exec = Command.memo_value ((Toplevel.toplevel, {malformed = false}), []);
 
 abstype node = Node of
  {header: node_header,  (*master directory, theory header, errors*)
@@ -327,8 +328,10 @@
       let
         val (_, print) = Command.memo_eval exec;
         val _ =
-          if visible_command node command_id
-          then ignore (Lazy.future Future.default_params print)
+          if visible_command node command_id then
+            print |> List.app (fn (a, pr) =>
+              ignore
+                (Lazy.future {name = a, group = NONE, deps = [], pri = 0, interrupts = true} pr))
           else ();
       in () end;
 
@@ -459,7 +462,7 @@
             val (st, _) = Command.memo_result (snd (snd command_exec));
             val tr = read ();
             val ({failed}, (st', malformed')) = Command.eval span tr st;
-            val print = if failed then Command.no_print else Command.print tr st';
+            val print = if failed then [] else Command.print tr st';
           in ((st', malformed'), print) end);
       val command_exec' = (command_id', (exec_id', exec'));
     in SOME (command_exec' :: execs, command_exec', init') end;