Adding an option "Printing Unfocused".

Off by default.

+ small refactoring of emacs hacks in printer.ml.

1 files changed, 92 insertions, 47 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 93d221f03..3d67e89f5 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -34,6 +34,49 @@ let delayed_emacs_cmd s =
 let get_current_context () =
   Pfedit.get_current_context ()
 
+let enable_unfocused_goal_printing = ref false
+let enable_goal_tags_printing = ref false
+let enable_goal_names_printing = ref false
+
+let should_tag() = !enable_goal_tags_printing
+let should_unfoc() = !enable_unfocused_goal_printing
+let should_gname() = !enable_goal_names_printing
+
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "printing of unfocused goal";
+      optkey   = ["Printing";"Unfocused"];
+      optread  = (fun () -> !enable_unfocused_goal_printing);
+      optwrite = (fun b -> enable_unfocused_goal_printing:=b) }
+
+(* This is set on by proofgeneral proof-tree mode. But may be used for
+   other purposes *)
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "printing of goal tags";
+      optkey   = ["Printing";"Goal";"Tags"];
+      optread  = (fun () -> !enable_goal_tags_printing);
+      optwrite = (fun b -> enable_goal_tags_printing:=b) }
+
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "printing of goal names";
+      optkey   = ["Printing";"Goal";"Names"];
+      optread  = (fun () -> !enable_goal_names_printing);
+      optwrite = (fun b -> enable_goal_names_printing:=b) }
+
+
 (**********************************************************************)
 (** Terms                                                             *)
 
@@ -419,23 +462,25 @@ let default_pr_goal gs =
 (* display a goal tag *)
 let pr_goal_tag g =
   let s = " (ID " ^ Goal.uid g ^ ")" in
-  str (emacs_str s)
-
-let display_name = false
+  str s
 
 (* display a goal name *)
 let pr_goal_name sigma g =
-  if display_name then str " " ++ Pp.surround (pr_existential_key sigma g)
+  if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g)
   else mt ()
 
+let pr_goal_header nme sigma g =
+  let (g,sigma) = Goal.V82.nf_evar sigma g in
+  str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"")
+  ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())  
+
 (* display the conclusion of a goal *)
 let pr_concl n sigma g =
   let (g,sigma) = Goal.V82.nf_evar sigma g in
   let env = Goal.V82.env sigma g in
   let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in
-    str (emacs_str "")  ++
-      str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++
-      str " is:" ++ cut () ++ str" "  ++ pc
+  let header = pr_goal_header (int n) sigma g in
+  header ++ str " is:" ++ cut () ++ str" "  ++ pc
 
 (* display evar type: a context and a type *)
 let pr_evgl_sign sigma evi =
@@ -491,8 +536,8 @@ let pr_ne_evar_set hd tl sigma l =
 
 let pr_selected_subgoal name sigma g =
   let pg = default_pr_goal { sigma=sigma ; it=g; } in
-  v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g
-       ++ str " is:" ++ cut () ++ pg)
+  let header = pr_goal_header name sigma g in
+  v 0 (header ++ str " is:" ++ cut () ++ pg)
 
 let default_pr_subgoal n sigma =
   let rec prrec p = function
@@ -585,27 +630,27 @@ let print_dependent_evars gl sigma seeds =
 	      end i (str ",")
 	end evars (str "")
     in
-    fnl () ++
-    str "(dependent evars:" ++ evars ++ str ")" ++ fnl ()
-    else
-      fnl () ++
-	str "(dependent evars: (printing disabled) )" ++ fnl ()
+    cut () ++ cut () ++
+    str "(dependent evars:" ++ evars ++ str ")"
+    else if !Flags.print_emacs then
+      (* IDEs prefer something dummy instead of nothing *)
+      cut () ++ cut () ++ str "(dependent evars: (printing disabled) )"
+    else mt ()
   in
-  constraints ++ delayed_emacs_cmd evars
+  constraints ++ evars ()
 
 (* Print open subgoals. Checks for uninstantiated existential variables *)
 (* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
 (* spiwack: [pr_first] is true when the first goal must be singled out
    and printed in its entirety. *)
-(* courtieu: in emacs mode, even less cases where the first goal is printed
-   in its entirety *)
-let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals =
+let default_pr_subgoals ?(pr_first=true)
+                        close_cmd sigma seeds shelf stack unfocused goals =
   (** Printing functions for the extra informations. *)
   let rec print_stack a = function
     | [] -> Pp.int a
     | b::l -> Pp.int a ++ str"-" ++ print_stack b l
   in
-  let print_unfocused l =
+  let print_unfocused_nums l =
     match l with
     | [] -> None
     | a::l -> Some (str"unfocused: " ++ print_stack a l)
@@ -625,7 +670,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
     | [] -> Pp.mt ()
     | a::l -> Pp.spc () ++ str"(" ++ print_comma_separated_list a l ++ str")"
   in
-  let extra = Option.List.flatten [ print_unfocused stack ; print_shelf shelf ] in
+  let extra = Option.List.flatten [ print_unfocused_nums stack ; print_shelf shelf ] in
   let print_extra = print_extra_list extra in
   let focused_if_needed =
     let needed = not (CList.is_empty extra) && pr_first in
@@ -642,8 +687,9 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
   in
   let print_multiple_goals g l =
     if pr_first then
-      default_pr_goal { it = g ; sigma = sigma; } ++ fnl () ++
-      pr_rec 2 l
+      default_pr_goal { it = g ; sigma = sigma; }
+      ++ (if l=[] then str"" else cut ())
+      ++ pr_rec 2 l
     else 
       pr_rec 1 (g::l)
   in
@@ -658,32 +704,27 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
       begin
 	let exl = Evarutil.non_instantiated sigma in
 	if Evar.Map.is_empty exl then
-	  (str"No more subgoals."
-	   ++ print_dependent_evars None sigma seeds)
+	  (str"No more subgoals." ++ print_dependent_evars None sigma seeds)
 	else
 	  let pei = pr_evars_int sigma 1 exl in
-	  (str "No more subgoals, but there are non-instantiated existential variables:"
-	   ++ fnl () ++ (hov 0 pei)
-	   ++ print_dependent_evars None sigma seeds ++ fnl () ++
-           str "You can use Grab Existential Variables.")
+	  v 0 ((str "No more subgoals,"
+                ++ str " but there are non-instantiated existential variables:"
+	        ++ cut () ++ (hov 0 pei)
+                ++ print_dependent_evars None sigma seeds
+                ++ cut () ++ str "You can use Grab Existential Variables."))
       end
-  | [g] when not !Flags.print_emacs && pr_first ->
-      let pg = default_pr_goal { it = g ; sigma = sigma; } in
-      v 0 (
-	str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra
-        ++ pr_goal_tag g ++ pr_goal_name sigma g ++ cut () ++ pg
-	++ print_dependent_evars (Some g) sigma seeds
-      )
   | g1::rest ->
       let goals = print_multiple_goals g1 rest in
       let ngoals = List.length rest+1 in
       v 0 (
-	int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++
-          print_extra ++
-          str ((if display_name then (fun x -> x) else emacs_str) ", subgoal 1")
-        ++ pr_goal_tag g1
-        ++ pr_goal_name sigma g1 ++ cut ()
-	++ goals
+	int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal")
+        ++ print_extra
+        ++ str (if (should_gname()) then ", subgoal 1" else "")
+        ++ (if should_tag() then pr_goal_tag g1 else str"")
+        ++ pr_goal_name sigma g1 ++ cut () ++ goals
+        ++ (if unfocused=[] then str ""
+           else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut()
+                 ++ pr_rec (List.length rest + 2) unfocused))
 	++ print_dependent_evars (Some g1) sigma seeds
       )
 
@@ -692,7 +733,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
 
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 }
@@ -726,16 +767,16 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
   begin match goals with
   | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
           begin match bgoals,shelf,given_up with
-	  | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
+	  | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack [] goals
           | [] , [] , _ ->
 	     Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:");
 	     fnl ()
-            ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up
+            ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] given_up
             ++ fnl () ++ str "You need to go back and solve them."
           | [] , _ , _ ->
 	    Feedback.msg_info (str "All the remaining goals are on the shelf.");
 	    fnl ()
-            ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
+            ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] shelf
 	  | _ , _, _ ->
             let end_cmd =
               str "This subproof is complete, but there are some unfocused goals." ++
@@ -743,9 +784,13 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
                if Pp.ismt s then s else fnl () ++ s) ++
               fnl ()
             in
-	    pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals
+	    pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] [] bgoals
 	  end
-  | _ -> pr_subgoals None sigma seeds shelf stack goals
+  | _ -> 
+     let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
+     let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in
+     let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in
+     pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused
   end
 
 let pr_nth_open_subgoal n =