# HG changeset patch
# User wenzelm
# Date 1288727712 -3600
# Node ID bf39a257b3d38d1b3ff15622a525efaa8d807fb4
# Parent  d4487353b3a0b9879090d876115a5ea497dc3f67
simplified some time constants;

diff -r d4487353b3a0 -r bf39a257b3d3 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Nov 02 20:31:46 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Nov 02 20:55:12 2010 +0100
@@ -497,8 +497,8 @@
     |> snd
   end
 
-val try_inner_timeout = Time.fromSeconds 5
-val try_outer_timeout = Time.fromSeconds 30
+val try_inner_timeout = seconds 5.0
+val try_outer_timeout = seconds 30.0
 
 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
   let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
diff -r d4487353b3a0 -r bf39a257b3d3 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Nov 02 20:31:46 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Nov 02 20:55:12 2010 +0100
@@ -248,7 +248,7 @@
   end
 
 fun is_executable_term thy t =
-  can (TimeLimit.timeLimit (Time.fromMilliseconds 2000)
+  can (TimeLimit.timeLimit (seconds 2.0)
     (Quickcheck.test_term
       (Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 0)))) (ProofContext.init_global thy))
       (SOME "SML"))) (preprocess thy [] t)
diff -r d4487353b3a0 -r bf39a257b3d3 src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Nov 02 20:31:46 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Nov 02 20:55:12 2010 +0100
@@ -125,7 +125,7 @@
   limited_predicates = [],
   replacing = [],
   manual_reorder = [],
-  timeout = Time.fromSeconds 10,
+  timeout = seconds 10.0,
   prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 
diff -r d4487353b3a0 -r bf39a257b3d3 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Nov 02 20:31:46 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Nov 02 20:55:12 2010 +0100
@@ -120,7 +120,7 @@
 structure System_Config = Generic_Data
 (
   type T = system_configuration
-  val empty = {timeout = Time.fromSeconds 10, prolog_system = SWI_PROLOG}
+  val empty = {timeout = seconds 10.0, prolog_system = SWI_PROLOG}
   val extend = I;
   fun merge ({timeout = timeout1, prolog_system = prolog_system1},
         {timeout = timeout2, prolog_system = prolog_system2}) =
diff -r d4487353b3a0 -r bf39a257b3d3 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Nov 02 20:31:46 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Nov 02 20:55:12 2010 +0100
@@ -1809,7 +1809,7 @@
           let
             val [nrandom, size, depth] = arguments
           in
-            rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
+            rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (DSequence.yieldn k
               (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
                 thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
                   t' [] nrandom size
@@ -1817,14 +1817,14 @@
               depth true)) ())
           end
       | DSeq =>
-          rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
+          rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (DSequence.yieldn k
             (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
               thy NONE DSequence.map t' []) (the_single arguments) true)) ())
       | Pos_Generator_DSeq =>
           let
             val depth = (the_single arguments)
           in
-            rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
+            rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Lazy_Sequence.yieldn k
               (Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
               thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.mapa proc)
               t' [] depth))) ())
@@ -1835,7 +1835,7 @@
             val seed = Random_Engine.next_seed ()
           in
             if stats then
-              apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (Time.fromSeconds 20)
+              apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (seconds 20.0)
               (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
@@ -1844,7 +1844,7 @@
                     |> Lazy_Sequence.mapa (apfst proc))
                     t' [] nrandom size seed depth))) ()))
             else rpair NONE
-              (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
+              (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
                   thy NONE 
@@ -1853,7 +1853,7 @@
                     t' [] nrandom size seed depth))) ())
           end
       | _ =>
-          rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Predicate.yieldn k
+          rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Predicate.yieldn k
             (Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
               thy NONE Predicate.map t' []))) ()))
      handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
diff -r d4487353b3a0 -r bf39a257b3d3 src/HOL/Tools/async_manager.ML
--- a/src/HOL/Tools/async_manager.ML	Tue Nov 02 20:31:46 2010 +0100
+++ b/src/HOL/Tools/async_manager.ML	Tue Nov 02 20:55:12 2010 +0100
@@ -80,8 +80,8 @@
 
 (* main manager thread -- only one may exist *)
 
-val min_wait_time = Time.fromMilliseconds 300;
-val max_wait_time = Time.fromSeconds 10;
+val min_wait_time = seconds 0.3;
+val max_wait_time = seconds 10.0;
 
 fun replace_all bef aft =
   let
diff -r d4487353b3a0 -r bf39a257b3d3 src/HOL/Tools/try.ML
--- a/src/HOL/Tools/try.ML	Tue Nov 02 20:31:46 2010 +0100
+++ b/src/HOL/Tools/try.ML	Tue Nov 02 20:55:12 2010 +0100
@@ -20,7 +20,7 @@
   ProofGeneralPgip.add_preference Preferences.category_tracing
       (Preferences.bool_pref auto "auto-try" "Try standard proof methods.")
 
-val default_timeout = Time.fromSeconds 5
+val default_timeout = seconds 5.0
 
 fun can_apply timeout_opt pre post tac st =
   let val {goal, ...} = Proof.goal st in
diff -r d4487353b3a0 -r bf39a257b3d3 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Nov 02 20:31:46 2010 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Nov 02 20:55:12 2010 +0100
@@ -253,7 +253,7 @@
 val status_ticks = Unsynchronized.ref 0;
 
 val last_round = Unsynchronized.ref Time.zeroTime;
-val next_round = Time.fromMilliseconds 50;
+val next_round = seconds 0.05;
 
 fun scheduler_next () = (*requires SYNCHRONIZED*)
   let
diff -r d4487353b3a0 -r bf39a257b3d3 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Nov 02 20:31:46 2010 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Nov 02 20:55:12 2010 +0100
@@ -120,10 +120,10 @@
 fun tracing_time detailed time =
   tracing
    (if not detailed then 5
-    else if Time.>= (time, Time.fromMilliseconds 1000) then 1
-    else if Time.>= (time, Time.fromMilliseconds 100) then 2
-    else if Time.>= (time, Time.fromMilliseconds 10) then 3
-    else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
+    else if Time.>= (time, seconds 1.0) then 1
+    else if Time.>= (time, seconds 0.1) then 2
+    else if Time.>= (time, seconds 0.01) then 3
+    else if Time.>= (time, seconds 0.001) then 4 else 5);
 
 fun real_time f x =
   let
@@ -202,13 +202,13 @@
               Posix.Signal.int)
       | NONE => ())
       handle OS.SysErr _ => () | IO.Io _ =>
-        (OS.Process.sleep (Time.fromMilliseconds 100); if n > 0 then kill (n - 1) else ());
+        (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
 
     val _ =
       while ! result = Wait do
         let val res =
           sync_wait (SOME orig_atts)
-            (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
+            (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
         in if Exn.is_interrupt_exn res then kill 10 else () end;
 
     (*cleanup*)
diff -r d4487353b3a0 -r bf39a257b3d3 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Nov 02 20:31:46 2010 +0100
+++ b/src/Pure/System/isabelle_process.ML	Tue Nov 02 20:55:12 2010 +0100
@@ -81,7 +81,7 @@
       (case receive mbox of
         SOME msg =>
          (List.app (fn s => TextIO.output (out_stream, s)) msg;
-          loop (Mailbox.receive_timeout (Time.fromMilliseconds 20)))
+          loop (Mailbox.receive_timeout (seconds 0.02)))
       | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
   in fn () => loop (SOME o Mailbox.receive) end;
 
@@ -165,7 +165,7 @@
 
 fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
   let
-    val _ = OS.Process.sleep (Time.fromMilliseconds 500);  (*yield to raw ML toplevel*)
+    val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
     val _ = Output.raw_stdout Symbol.STX;
 
     val _ = quick_and_dirty := true;  (* FIXME !? *)