# HG changeset patch
# User wenzelm
# Date 1629320698 -7200
# Node ID ecf80e37ed1ae7f38fc4ef66e450cecac87a18aa
# Parent  0faa68dedce54674db8d3ae64d6208ea5c6d6163
support configuration options "show_results";

diff -r 0faa68dedce5 -r ecf80e37ed1a NEWS
--- 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
diff -r 0faa68dedce5 -r ecf80e37ed1a src/Pure/Isar/attrib.ML
--- 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 #>
diff -r 0faa68dedce5 -r ecf80e37ed1a src/Pure/Isar/proof_display.ML
--- 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;