# HG changeset patch
# User wenzelm
# Date 1442846480 -7200
# Node ID 0b1a092385c7f29506a397edaf9b2062572bb274
# Parent  cb9d0c99bd36ec508d7678ff547cdd1b7c1b0b2f
option editor_output_state;

diff -r cb9d0c99bd36 -r 0b1a092385c7 etc/options
--- a/etc/options	Mon Sep 21 16:23:48 2015 +0200
+++ b/etc/options	Mon Sep 21 16:41:20 2015 +0200
@@ -140,6 +140,9 @@
 public option editor_continuous_checking : bool = true
   -- "continuous checking of proof document (visible and required parts)"
 
+public option editor_output_state : bool = true
+  -- "implicit output of proof state"
+
 option editor_execution_delay : real = 0.02
   -- "delay for start of execution process after document update (seconds)"
 
diff -r cb9d0c99bd36 -r 0b1a092385c7 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Sep 21 16:23:48 2015 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Sep 21 16:41:20 2015 +0200
@@ -357,7 +357,8 @@
 val _ =
   print_function "print_state"
     (fn {keywords, command_name, ...} =>
-      if Keyword.is_printed keywords command_name then
+      if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name
+      then
         SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
           print_fn = fn _ => fn st =>
             if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st)