1.1 --- a/src/Pure/PIDE/command.ML	Sat Jul 13 18:13:09 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Sat Jul 13 18:33:33 2013 +0200
     1.3 @@ -16,7 +16,8 @@
     1.4    val print: bool -> string -> eval -> print list -> print list option
     1.5    type print_fn = Toplevel.transition -> Toplevel.state -> unit
     1.6    val print_function: string ->
     1.7 -    ({command_name: string} -> {pri: int, persistent: bool, print_fn: print_fn} option) -> unit
     1.8 +    ({command_name: string} ->
     1.9 +      {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
    1.10    val no_print_function: string -> unit
    1.11    type exec = eval * print list
    1.12    val no_exec: exec
    1.13 @@ -192,13 +193,14 @@
    1.14  (* print *)
    1.15  
    1.16  datatype print = Print of
    1.17 - {name: string, pri: int, persistent: bool,
    1.18 + {name: string, delay: Time.time, pri: int, persistent: bool,
    1.19    exec_id: Document_ID.exec, print_process: unit memo};
    1.20  
    1.21  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
    1.22  
    1.23  type print_function =
    1.24 -  {command_name: string} -> {pri: int, persistent: bool, print_fn: print_fn} option;
    1.25 +  {command_name: string} ->
    1.26 +    {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option;
    1.27  
    1.28  local
    1.29  
    1.30 @@ -224,7 +226,7 @@
    1.31    let
    1.32      fun new_print (name, get_pr) =
    1.33        let
    1.34 -        fun make_print strict {pri, persistent, print_fn} =
    1.35 +        fun make_print strict {delay, pri, persistent, print_fn} =
    1.36            let
    1.37              val exec_id = Document_ID.make ();
    1.38              fun process () =
    1.39 @@ -237,7 +239,7 @@
    1.40                end;
    1.41            in
    1.42             Print {
    1.43 -             name = name, pri = pri, persistent = persistent,
    1.44 +             name = name, delay = delay, pri = pri, persistent = persistent,
    1.45               exec_id = exec_id, print_process = memo exec_id process}
    1.46            end;
    1.47        in
    1.48 @@ -246,7 +248,8 @@
    1.49          | Exn.Res (SOME pr) => SOME (make_print false pr)
    1.50          | Exn.Exn exn =>
    1.51              SOME (make_print true
    1.52 -              {pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
    1.53 +              {delay = Time.zeroTime, pri = 0, persistent = false,
    1.54 +                print_fn = fn _ => fn _ => reraise exn}))
    1.55        end;
    1.56  
    1.57      val new_prints =
    1.58 @@ -273,14 +276,16 @@
    1.59  
    1.60  val _ =
    1.61    print_function "print_state"
    1.62 -    (fn {command_name} => SOME {pri = 0, persistent = true, print_fn = fn tr => fn st' =>
    1.63 -      let
    1.64 -        val is_init = Keyword.is_theory_begin command_name;
    1.65 -        val is_proof = Keyword.is_proof command_name;
    1.66 -        val do_print =
    1.67 -          not is_init andalso
    1.68 -            (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
    1.69 -      in if do_print then Toplevel.print_state false st' else () end});
    1.70 +    (fn {command_name} =>
    1.71 +      SOME {delay = Time.zeroTime, pri = 0, persistent = true,
    1.72 +        print_fn = fn tr => fn st' =>
    1.73 +          let
    1.74 +            val is_init = Keyword.is_theory_begin command_name;
    1.75 +            val is_proof = Keyword.is_proof command_name;
    1.76 +            val do_print =
    1.77 +              not is_init andalso
    1.78 +                (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
    1.79 +          in if do_print then Toplevel.print_state false st' else () end});
    1.80  
    1.81  
    1.82  (* combined execution *)
    1.83 @@ -295,10 +300,18 @@
    1.84  
    1.85  local
    1.86  
    1.87 -fun run_print execution_id (Print {name, pri, print_process, ...}) =
    1.88 -  (if Multithreading.enabled () then
    1.89 -    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
    1.90 -  else memo_exec) execution_id print_process;
    1.91 +fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
    1.92 +  if Multithreading.enabled () then
    1.93 +    let
    1.94 +      val group = Future.worker_subgroup ();
    1.95 +      fun fork () =
    1.96 +        memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
    1.97 +          execution_id print_process;
    1.98 +    in
    1.99 +      if delay = Time.zeroTime then fork ()
   1.100 +      else ignore (Event_Timer.request (Time.+ (Time.now (), delay)) fork)
   1.101 +    end
   1.102 +  else memo_exec execution_id print_process;
   1.103  
   1.104  in
   1.105