1.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 03 16:58:35 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Jul 03 17:50:47 2013 +0200
     1.3 @@ -17,8 +17,9 @@
     1.4    val read: span -> Toplevel.transition
     1.5    val eval: span -> Toplevel.transition ->
     1.6      Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
     1.7 -  val no_print: unit lazy
     1.8 -  val print: Toplevel.transition -> Toplevel.state -> unit lazy
     1.9 +  val print: Toplevel.transition -> Toplevel.state -> (string * unit lazy) list
    1.10 +  val print_function: string ->
    1.11 +    ({tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option) -> unit
    1.12  end;
    1.13  
    1.14  structure Command: COMMAND =
    1.15 @@ -150,21 +151,38 @@
    1.16  
    1.17  (* print *)
    1.18  
    1.19 -val no_print = Lazy.value ();
    1.20 +local
    1.21 +
    1.22 +type print_function =
    1.23 +  {tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option;
    1.24 +
    1.25 +val print_functions =
    1.26 +  Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
    1.27 +
    1.28 +in
    1.29  
    1.30  fun print tr st' =
    1.31 +  rev (Synchronized.value print_functions) |> map_filter (fn (name, f) =>
    1.32 +    (case f {tr = tr, state = st'} of
    1.33 +      SOME pr => SOME (name, (Lazy.lazy o Toplevel.setmp_thread_position tr) pr)
    1.34 +    | NONE => NONE));
    1.35 +
    1.36 +fun print_function name f =
    1.37 +  Synchronized.change print_functions (fn funs =>
    1.38 +   (if not (AList.defined (op =) funs name) then ()
    1.39 +    else warning ("Redefining command print function: " ^ quote name);
    1.40 +    AList.update (op =) (name, f) funs));
    1.41 +
    1.42 +end;
    1.43 +
    1.44 +val _ = print_function "print_state" (fn {tr, state} =>
    1.45    let
    1.46      val is_init = Toplevel.is_init tr;
    1.47      val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    1.48      val do_print =
    1.49        not is_init andalso
    1.50 -        (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
    1.51 -  in
    1.52 -    if do_print then
    1.53 -      (Lazy.lazy o Toplevel.setmp_thread_position tr)
    1.54 -        (fn () => Toplevel.print_state false st')
    1.55 -    else no_print
    1.56 -  end;
    1.57 +        (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof state));
    1.58 +  in if do_print then SOME (fn () => Toplevel.print_state false state) else NONE end);
    1.59  
    1.60  end;
    1.61  

     2.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 03 16:58:35 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 03 17:50:47 2013 +0200
     2.3 @@ -63,8 +63,9 @@
     2.4  type perspective = (command_id -> bool) * command_id option;
     2.5  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
     2.6  
     2.7 -type exec = ((Toplevel.state * {malformed: bool}) * unit lazy) Command.memo;  (*eval/print process*)
     2.8 -val no_exec = Command.memo_value ((Toplevel.toplevel, {malformed = false}), Lazy.value ());
     2.9 +type print = string * unit lazy;
    2.10 +type exec = ((Toplevel.state * {malformed: bool}) * print list) Command.memo; (*eval/print process*)
    2.11 +val no_exec = Command.memo_value ((Toplevel.toplevel, {malformed = false}), []);
    2.12  
    2.13  abstype node = Node of
    2.14   {header: node_header,  (*master directory, theory header, errors*)
    2.15 @@ -327,8 +328,10 @@
    2.16        let
    2.17          val (_, print) = Command.memo_eval exec;
    2.18          val _ =
    2.19 -          if visible_command node command_id
    2.20 -          then ignore (Lazy.future Future.default_params print)
    2.21 +          if visible_command node command_id then
    2.22 +            print |> List.app (fn (a, pr) =>
    2.23 +              ignore
    2.24 +                (Lazy.future {name = a, group = NONE, deps = [], pri = 0, interrupts = true} pr))
    2.25            else ();
    2.26        in () end;
    2.27  
    2.28 @@ -459,7 +462,7 @@
    2.29              val (st, _) = Command.memo_result (snd (snd command_exec));
    2.30              val tr = read ();
    2.31              val ({failed}, (st', malformed')) = Command.eval span tr st;
    2.32 -            val print = if failed then Command.no_print else Command.print tr st';
    2.33 +            val print = if failed then [] else Command.print tr st';
    2.34            in ((st', malformed'), print) end);
    2.35        val command_exec' = (command_id', (exec_id', exec'));
    2.36      in SOME (command_exec' :: execs, command_exec', init') end;