--- a/NEWS Wed Aug 18 16:13:40 2021 +0200
+++ b/NEWS Wed Aug 18 23:04:58 2021 +0200
@@ -9,6 +9,17 @@
*** General ***
+* Configuration option "show_results" controls output of final results
+in commands like 'definition' or 'theorem'. Output is normally enabled
+in interactive mode, but it could occasionally cause unnecessary
+slowdown. It can be disabled like this:
+
+ context notes [[show_results = true]]
+ begin
+ definition "test = True"
+ theorem test by (simp add: test_def)
+ end
+
* Timeouts for Isabelle/ML tools are subject to system option
"timeout_scale" --- this already used for the overall session build
process before, and allows to adapt to slow machines. The underlying
--- a/src/Pure/Isar/attrib.ML Wed Aug 18 16:13:40 2021 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Aug 18 23:04:58 2021 +0200
@@ -602,6 +602,7 @@
register_config_bool Thm.show_consts #>
register_config_bool Thm.show_hyps #>
register_config_bool Thm.show_tags #>
+ register_config_bool Proof_Display.show_results #>
register_config_bool Pattern.unify_trace_failure #>
register_config_int Unify.trace_bound #>
register_config_int Unify.search_bound #>
--- a/src/Pure/Isar/proof_display.ML Wed Aug 18 16:13:40 2021 +0200
+++ b/src/Pure/Isar/proof_display.ML Wed Aug 18 23:04:58 2021 +0200
@@ -22,6 +22,7 @@
val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
val method_error: string -> Position.T ->
{context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
+ val show_results: bool Config.T
val print_results: bool -> Position.T -> Proof.context ->
((string * string) * (string * thm list) list) -> unit
val print_consts: bool -> Position.T -> Proof.context ->
@@ -263,6 +264,14 @@
fun position_markup pos = Pretty.mark (Position.markup pos Markup.position);
+val interactive =
+ Config.declare_bool ("interactive", \<^here>) (K false);
+
+val show_results =
+ Config.declare_bool ("show_results", \<^here>) (fn context => Config.get_generic context interactive);
+
+fun no_print int ctxt = not (Config.get (Config.put interactive int ctxt) show_results);
+
local
fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind)
@@ -276,8 +285,8 @@
in
-fun print_results do_print pos ctxt ((kind, name), facts) =
- if not do_print orelse kind = "" then ()
+fun print_results int pos ctxt ((kind, name), facts) =
+ if kind = "" orelse no_print int ctxt then ()
else if name = "" then
(Output.state o Pretty.string_of)
(Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
@@ -315,8 +324,8 @@
in
-fun print_consts do_print pos ctxt pred cs =
- if not do_print orelse null cs then ()
+fun print_consts int pos ctxt pred cs =
+ if null cs orelse no_print int ctxt then ()
else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs));
end;