# HG changeset patch
# User wenzelm
# Date 1738842373 -3600
# Node ID 93195437fdee6f20885d3999a3f8ea785d3a0644
# Parent  2c9c06a9f61fbd09f547b82ba706531d0748f349
clarified signature;
clarified modules;

diff -r 2c9c06a9f61f -r 93195437fdee src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Feb 06 12:18:56 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Feb 06 12:46:13 2025 +0100
@@ -112,8 +112,8 @@
 
     val output = drop_suffix (equal "") res
     val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output
-    val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
-    val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
+    val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Time.message elapsed]
+    val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Time.message elapsed]
 
     val _ = member (op =) (normal_return_codes name) return_code orelse
       raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
diff -r 2c9c06a9f61f -r 93195437fdee src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Thu Feb 06 12:18:56 2025 +0100
+++ b/src/Pure/Concurrent/timeout.ML	Thu Feb 06 12:46:13 2025 +0100
@@ -15,7 +15,7 @@
   val end_time: Time.time -> Time.time
   val apply: Time.time -> ('a -> 'b) -> 'a -> 'b
   val apply_physical: Time.time -> ('a -> 'b) -> 'a -> 'b
-  val print: Time.time -> string
+  val message: Time.time -> string
 end;
 
 structure Timeout: TIMEOUT =
@@ -59,6 +59,6 @@
 fun apply timeout f x = apply' {physical = false, timeout = timeout} f x;
 fun apply_physical timeout f x = apply' {physical = true, timeout = timeout} f x;
 
-fun print t = "Timeout after " ^ Value.print_time t ^ "s";
+fun message t = "Timeout after " ^ Time.message t;
 
 end;
diff -r 2c9c06a9f61f -r 93195437fdee src/Pure/General/time.ML
--- a/src/Pure/General/time.ML	Thu Feb 06 12:18:56 2025 +0100
+++ b/src/Pure/General/time.ML	Thu Feb 06 12:46:13 2025 +0100
@@ -10,6 +10,9 @@
   val min: time * time -> time
   val max: time * time -> time
   val scale: real -> time -> time
+  val parse: string -> time
+  val print: time -> string
+  val message: time -> string
 end;
 
 structure Time: TIME =
@@ -22,4 +25,15 @@
 
 fun scale s t = Time.fromNanoseconds (Real.ceil (s * Real.fromInt (Time.toNanoseconds t)));
 
+fun parse s =
+  (case Time.fromString s of
+    SOME t => t
+  | NONE => raise Fail ("Bad time " ^ quote s));
+
+fun print t =
+  if t < Time.zeroTime then "-" ^ Time.toString (Time.zeroTime - t)
+  else Time.toString t;
+
+fun message t = print t ^ "s";
+
 end;
diff -r 2c9c06a9f61f -r 93195437fdee src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Thu Feb 06 12:18:56 2025 +0100
+++ b/src/Pure/General/timing.ML	Thu Feb 06 12:46:13 2025 +0100
@@ -86,9 +86,9 @@
   is_relevant_time gc;
 
 fun message {elapsed, cpu, gc} =
-  Value.print_time elapsed ^ "s elapsed time, " ^
-  Value.print_time cpu ^ "s cpu time, " ^
-  Value.print_time gc ^ "s GC time" handle Time.Time => "";
+  Time.message elapsed ^ " elapsed time, " ^
+  Time.message cpu ^ " cpu time, " ^
+  Time.message gc ^ " GC time" handle Time.Time => "";
 
 fun cond_timeit enabled msg e =
   if enabled then
diff -r 2c9c06a9f61f -r 93195437fdee src/Pure/General/value.ML
--- a/src/Pure/General/value.ML	Thu Feb 06 12:18:56 2025 +0100
+++ b/src/Pure/General/value.ML	Thu Feb 06 12:46:13 2025 +0100
@@ -13,8 +13,6 @@
   val print_int: int -> string
   val parse_real: string -> real
   val print_real: real -> string
-  val parse_time: string -> Time.time
-  val print_time: Time.time -> string
 end;
 
 structure Value: VALUE =
@@ -82,16 +80,4 @@
     | _ => s)
   end;
 
-
-(* time *)
-
-fun parse_time s =
-  (case Time.fromString s of
-    SOME x => x
-  | NONE => raise Fail ("Bad time " ^ quote s));
-
-fun print_time x =
-  if x < Time.zeroTime then "-" ^ Time.toString (Time.zeroTime - x)
-  else Time.toString x;
-
 end;
diff -r 2c9c06a9f61f -r 93195437fdee src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Feb 06 12:18:56 2025 +0100
+++ b/src/Pure/Isar/runtime.ML	Thu Feb 06 12:46:13 2025 +0100
@@ -113,7 +113,7 @@
         let
           val msg =
             (case exn of
-              Timeout.TIMEOUT t => Timeout.print t
+              Timeout.TIMEOUT t => Timeout.message t
             | TOPLEVEL_ERROR => "Error"
             | ERROR "" => "Error"
             | ERROR msg => msg
diff -r 2c9c06a9f61f -r 93195437fdee src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Feb 06 12:18:56 2025 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Feb 06 12:46:13 2025 +0100
@@ -703,9 +703,9 @@
 val gcN = "gc";
 
 fun timing_properties {elapsed, cpu, gc} =
- [(elapsedN, Value.print_time elapsed),
-  (cpuN, Value.print_time cpu),
-  (gcN, Value.print_time gc)];
+ [(elapsedN, Time.print elapsed),
+  (cpuN, Time.print cpu),
+  (gcN, Time.print gc)];
 
 val timingN = "timing";
 fun timing t = (timingN, timing_properties t);
diff -r 2c9c06a9f61f -r 93195437fdee src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Feb 06 12:18:56 2025 +0100
+++ b/src/Pure/ROOT.ML	Thu Feb 06 12:46:13 2025 +0100
@@ -54,6 +54,7 @@
 ML_file "General/value.ML";
 ML_file "General/properties.ML";
 ML_file "General/output.ML";
+ML_file "General/time.ML";
 ML_file "PIDE/markup.ML";
 ML_file "General/utf8.ML";
 ML_file "General/scan.ML";
@@ -94,7 +95,6 @@
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";
 ML_file "General/seq.ML";
-ML_file "General/time.ML";
 ML_file "General/timing.ML";
 ML_file "General/sha1.ML";