# HG changeset patch
# User wenzelm
# Date 1738756804 -3600
# Node ID c0f4968fa96ef5dfd63c28db88a462bdad1b3f32
# Parent  2b4892e30a42ec4f3c7f5518ed025c89450e24fc
tuned output;

diff -r 2b4892e30a42 -r c0f4968fa96e src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Wed Feb 05 12:11:13 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Feb 05 13:00:04 2025 +0100
@@ -253,22 +253,20 @@
     val n = the_default "(none)" (get_solver ctxt);
     val opts = solver_options_of ctxt;
 
-    val t = string_of_real (Config.get ctxt timeout);
-
     val certs_filename =
       (case get_certificates_path ctxt of
         SOME path => Path.print path
       | NONE => "(disabled)");
-  in
-    Pretty.writeln (Pretty.big_list "SMT setup:" [
-      Pretty.str ("Current SMT solver: " ^ n),
+
+    val items =
+     [Pretty.str ("Current SMT solver: " ^ n),
       Pretty.str ("Current SMT solver options: " ^ implode_space opts),
       Pretty.str_list "Available SMT solvers: "  "" ns,
-      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
+      Pretty.str ("Current timeout: " ^ Value.print_real (Config.get ctxt timeout) ^ " seconds"),
       Pretty.str ("With proofs: " ^ Value.print_bool (not (Config.get ctxt oracle))),
       Pretty.str ("Certificates cache: " ^ certs_filename),
-      Pretty.str ("Fixed certificates: " ^ Value.print_bool (Config.get ctxt read_only_certificates))])
-  end;
+      Pretty.str ("Fixed certificates: " ^ Value.print_bool (Config.get ctxt read_only_certificates))];
+  in Pretty.writeln (Pretty.big_list "SMT setup:" (map (Pretty.item o single) items)) end;
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>smt_status\<close>