Adding an option "Printing Unfocused".

Off by default.

+ small refactoring of emacs hacks in printer.ml.

1 files changed, 5 insertions, 1 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 3a1d87787..cd45e2fcd 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -519,6 +519,7 @@ struct
   let all_basic = ["Printing"; "All"]
   let existential = ["Printing"; "Existential"; "Instances"]
   let universes = ["Printing"; "Universes"]
+  let unfocused = ["Printing"; "Unfocused"]
 
   type bool_descr = { opts : t list; init : bool; label : string }
 
@@ -534,7 +535,8 @@ struct
       label = "Display _existential variable instances" };
     { opts = [universes]; init = false; label = "Display _universe levels" };
     { opts = [all_basic;existential;universes]; init = false;
-      label = "Display all _low-level contents" }
+      label = "Display all _low-level contents" };
+    { opts = [unfocused]; init = false; label = "Display _unfocused goals" }
   ]
 
   (** The current status of the boolean options *)
@@ -549,6 +551,8 @@ struct
 
   let _ = reset ()
 
+  let printing_unfocused () = Hashtbl.find current_state unfocused
+
   (** Transmitting options to coqtop *)
 
   let enforce h k =