--- 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)"
--- 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)