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
2.1 --- a/src/Tools/try.ML Mon Jul 29 13:24:15 2013 +0200
2.2 +++ b/src/Tools/try.ML Mon Jul 29 13:28:27 2013 +0200
2.3 @@ -120,7 +120,7 @@
2.4 (fn {command_name} =>
2.5 if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
2.6 SOME
2.7 - {delay = seconds (Options.default_real @{option auto_time_start}),
2.8 + {delay = SOME (seconds (Options.default_real @{option auto_time_start})),
2.9 pri = ~ weight,
2.10 persistent = true,
2.11 print_fn = fn _ => fn st =>