A friendlier printing of remaining goals when no goal is focused.

Only their conclusion is printed (with a "subgoal n" header) like every goal
but the first in the usual case.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15591 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 19 insertions, 12 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index d95ccef89..bae75011b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -354,7 +354,9 @@ let emacs_print_dependent_evars sigma seeds =
 
 (* Print open subgoals. Checks for uninstantiated existential variables *)
 (* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
-let default_pr_subgoals close_cmd sigma seeds stack goals =
+(* spiwack: [pr_first] is true when the first goal must be singled out
+   and printed in its entirety. *)
+let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
   let rec print_stack a = function
     | [] -> Pp.int a
     | b::l -> Pp.int a ++ str"-" ++ print_stack b l
@@ -369,6 +371,13 @@ let default_pr_subgoals close_cmd sigma seeds stack goals =
         let prest = pr_rec (n+1) rest in
         (cut () ++ pc ++ prest)
   in
+  let print_multiple_goals g l =
+    if pr_first then
+      default_pr_goal { it = g ; sigma = sigma } ++
+      pr_rec 2 l
+    else 
+      pr_rec 1 (g::l)
+  in
   match goals,stack with
   | [],_ ->
       begin
@@ -401,22 +410,20 @@ let default_pr_subgoals close_cmd sigma seeds stack goals =
 	++ emacs_print_dependent_evars sigma seeds
       )
   | g1::rest,[] ->
-      let pg1 = default_pr_goal { it = g1 ; sigma = sigma } in
-      let prest = pr_rec 2 rest in
+      let goals = print_multiple_goals g1 rest in
       v 0 (
 	int(List.length rest+1) ++ str" subgoals" ++
           str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
-	++ pg1 ++ prest
+	++ goals
 	++ emacs_print_dependent_evars sigma seeds
       )
   | g1::rest,a::l ->
-      let pg1 = default_pr_goal { it = g1 ; sigma = sigma } in
-      let prest = pr_rec 2 rest in
+      let goals = print_multiple_goals g1 rest in
       v 0 (
 	int(List.length rest+1) ++ str" focused subgoals (" ++
           print_unfocused a l ++ str")" ++ cut () ++
           str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
-	++ pg1 ++ prest
+	++ goals
 	++ emacs_print_dependent_evars sigma seeds
       )
 
@@ -425,7 +432,7 @@ let default_pr_subgoals close_cmd sigma seeds stack goals =
 
 
 type printer_pr = {
- pr_subgoals            : string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 }
@@ -440,7 +447,7 @@ let printer_pr = ref default_printer_pr
 
 let set_printer_pr = (:=) printer_pr
 
-let pr_subgoals x = !printer_pr.pr_subgoals x
+let pr_subgoals ?pr_first x = !printer_pr.pr_subgoals ?pr_first x
 let pr_subgoal  x = !printer_pr.pr_subgoal  x
 let pr_goal     x = !printer_pr.pr_goal     x
 
@@ -460,7 +467,7 @@ let pr_open_subgoals () =
   | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
           begin match bgoals with
 	  | [] -> pr_subgoals None sigma seeds stack goals
-	  | _ -> str"This subproof is complete, but there are still unfocused goals." ++ fnl () ++ fnl () ++ pr_subgoals None bsigma seeds [] bgoals
+	  | _ -> str"This subproof is complete, but there are still unfocused goals." ++ fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] bgoals
 	  end
   | _ -> pr_subgoals None sigma seeds stack goals
   end
diff --git a/printing/printer.mli b/printing/printer.mli
index 83155fbc3..b8bf17576 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -104,7 +104,7 @@ val pr_transparent_state   : transparent_state -> std_ppcmds
 (** Proofs *)
 
 val pr_goal                : goal sigma -> std_ppcmds
-val pr_subgoals            : string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds
+val pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds
 val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
 val pr_concl               : int -> evar_map -> goal -> std_ppcmds
 
@@ -141,7 +141,7 @@ val pr_assumptionset :
 val pr_goal_by_id : string -> std_ppcmds
 
 type printer_pr = {
- pr_subgoals            : string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 };;