option editor_output_state;
authorwenzelm
Mon Sep 21 16:41:20 2015 +0200 (2015-09-21)
changeset 612130b1a092385c7
parent 61212 cb9d0c99bd36
child 61214 a00bee2dfbd1
option editor_output_state;
etc/options
src/Pure/PIDE/command.ML
     1.1 --- a/etc/options	Mon Sep 21 16:23:48 2015 +0200
     1.2 +++ b/etc/options	Mon Sep 21 16:41:20 2015 +0200
     1.3 @@ -140,6 +140,9 @@
     1.4  public option editor_continuous_checking : bool = true
     1.5    -- "continuous checking of proof document (visible and required parts)"
     1.6  
     1.7 +public option editor_output_state : bool = true
     1.8 +  -- "implicit output of proof state"
     1.9 +
    1.10  option editor_execution_delay : real = 0.02
    1.11    -- "delay for start of execution process after document update (seconds)"
    1.12  
     2.1 --- a/src/Pure/PIDE/command.ML	Mon Sep 21 16:23:48 2015 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Mon Sep 21 16:41:20 2015 +0200
     2.3 @@ -357,7 +357,8 @@
     2.4  val _ =
     2.5    print_function "print_state"
     2.6      (fn {keywords, command_name, ...} =>
     2.7 -      if Keyword.is_printed keywords command_name then
     2.8 +      if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name
     2.9 +      then
    2.10          SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
    2.11            print_fn = fn _ => fn st =>
    2.12              if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st)