# 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>\smt_status\