# HG changeset patch
# User wenzelm
# Date 1375097307 -7200
# Node ID c2a6e220f157800d81b2387590cad2fe3956bd6d
# Parent  909167fdd367c76702aea09799c5a932fc6f0267
tuned signature;

diff -r 909167fdd367 -r c2a6e220f157 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Jul 29 13:24:15 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Jul 29 13:28:27 2013 +0200
@@ -16,7 +16,7 @@
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
   val print_function: string ->
     ({command_name: string} ->
-      {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
+      {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
   val no_print_function: string -> unit
   type exec = eval * print list
   val no_exec: exec
@@ -189,14 +189,14 @@
 (* print *)
 
 datatype print = Print of
- {name: string, delay: Time.time, pri: int, persistent: bool,
+ {name: string, delay: Time.time option, pri: int, persistent: bool,
   exec_id: Document_ID.exec, print_process: unit memo};
 
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
 type print_function =
   {command_name: string} ->
-    {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option;
+    {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
 
 local
 
@@ -243,8 +243,7 @@
         | Exn.Res (SOME pr) => SOME (make_print false pr)
         | Exn.Exn exn =>
             SOME (make_print true
-              {delay = Time.zeroTime, pri = 0, persistent = false,
-                print_fn = fn _ => fn _ => reraise exn}))
+              {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
       end;
 
     val new_prints =
@@ -272,7 +271,7 @@
 val _ =
   print_function "print_state"
     (fn {command_name} =>
-      SOME {delay = Time.zeroTime, pri = 1, persistent = true,
+      SOME {delay = NONE, pri = 1, persistent = true,
         print_fn = fn tr => fn st' =>
           let
             val is_init = Keyword.is_theory_begin command_name;
@@ -303,8 +302,9 @@
         memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
           execution_id print_process;
     in
-      if delay = Time.zeroTime then fork ()
-      else ignore (Event_Timer.request (Time.+ (Time.now (), delay)) fork)
+      (case delay of
+        NONE => fork ()
+      | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork))
     end
   else memo_exec execution_id print_process;
 
diff -r 909167fdd367 -r c2a6e220f157 src/Tools/try.ML
--- a/src/Tools/try.ML	Mon Jul 29 13:24:15 2013 +0200
+++ b/src/Tools/try.ML	Mon Jul 29 13:28:27 2013 +0200
@@ -120,7 +120,7 @@
     (fn {command_name} =>
       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
         SOME
-         {delay = seconds (Options.default_real @{option auto_time_start}),
+         {delay = SOME (seconds (Options.default_real @{option auto_time_start})),
           pri = ~ weight,
           persistent = true,
           print_fn = fn _ => fn st =>