1.1 --- a/src/Pure/PIDE/command.ML	Mon Jul 29 13:24:15 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Jul 29 13:28:27 2013 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    type print_fn = Toplevel.transition -> Toplevel.state -> unit
     1.5    val print_function: string ->
     1.6      ({command_name: string} ->
     1.7 -      {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
     1.8 +      {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
     1.9    val no_print_function: string -> unit
    1.10    type exec = eval * print list
    1.11    val no_exec: exec
    1.12 @@ -189,14 +189,14 @@
    1.13  (* print *)
    1.14  
    1.15  datatype print = Print of
    1.16 - {name: string, delay: Time.time, pri: int, persistent: bool,
    1.17 + {name: string, delay: Time.time option, pri: int, persistent: bool,
    1.18    exec_id: Document_ID.exec, print_process: unit memo};
    1.19  
    1.20  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
    1.21  
    1.22  type print_function =
    1.23    {command_name: string} ->
    1.24 -    {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option;
    1.25 +    {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
    1.26  
    1.27  local
    1.28  
    1.29 @@ -243,8 +243,7 @@
    1.30          | Exn.Res (SOME pr) => SOME (make_print false pr)
    1.31          | Exn.Exn exn =>
    1.32              SOME (make_print true
    1.33 -              {delay = Time.zeroTime, pri = 0, persistent = false,
    1.34 -                print_fn = fn _ => fn _ => reraise exn}))
    1.35 +              {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
    1.36        end;
    1.37  
    1.38      val new_prints =
    1.39 @@ -272,7 +271,7 @@
    1.40  val _ =
    1.41    print_function "print_state"
    1.42      (fn {command_name} =>
    1.43 -      SOME {delay = Time.zeroTime, pri = 1, persistent = true,
    1.44 +      SOME {delay = NONE, pri = 1, persistent = true,
    1.45          print_fn = fn tr => fn st' =>
    1.46            let
    1.47              val is_init = Keyword.is_theory_begin command_name;
    1.48 @@ -303,8 +302,9 @@
    1.49          memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
    1.50            execution_id print_process;
    1.51      in
    1.52 -      if delay = Time.zeroTime then fork ()
    1.53 -      else ignore (Event_Timer.request (Time.+ (Time.now (), delay)) fork)
    1.54 +      (case delay of
    1.55 +        NONE => fork ()
    1.56 +      | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork))
    1.57      end
    1.58    else memo_exec execution_id print_process;
    1.59