Merge branch 'master' into ltac2-hooks

3 files changed, 157 insertions, 63 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 3041ac259e..b546c39aec 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -151,8 +151,8 @@ let tag_var = tag Tag.variable
 
   let pr_univ l =
     match l with
-      | [_,x] -> str x
-      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")"
+      | [_,x] -> pr_name x
+      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> pr_name (snd x)) l ++ str")"
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
@@ -166,7 +166,7 @@ let tag_var = tag Tag.variable
     | GProp -> tag_type (str "Prop")
     | GSet -> tag_type (str "Set")
     | GType None -> tag_type (str "Type")
-    | GType (Some (_, u)) -> tag_type (str u)
+    | GType (Some (_, u)) -> tag_type (pr_name u)
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
@@ -191,7 +191,7 @@ let tag_var = tag Tag.variable
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | Some (_,u) -> str u
+        | Some (_,u) -> pr_name u
         | None -> tag_type (str "Type"))
 
   let pr_universe_instance l =
diff --git a/printing/printer.ml b/printing/printer.ml
index 93d221f03f..e0ca51f0c9 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -28,12 +28,53 @@ module CompactedDecl = Context.Compacted.Declaration
 
 let emacs_str s =
   if !Flags.print_emacs then s else ""
-let delayed_emacs_cmd s =
-  if !Flags.print_emacs then s () else str ""
 
 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                                                             *)
 
@@ -262,6 +303,13 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*)
 (**********************************************************************)
 (* Contexts and declarations                                          *)
 
+
+(* Flag for compact display of goals *)
+
+let get_compact_context,set_compact_context =
+  let compact_context = ref false in
+  (fun () -> !compact_context),(fun b  -> compact_context := b)
+
 let pr_compacted_decl env sigma decl =
   let ids, pbody, typ = match decl with
     | CompactedDecl.LocalAssum (ids, typ) ->
@@ -342,15 +390,40 @@ let pr_ne_context_of header env sigma =
     List.is_empty (Environ.named_context env)  then (mt ())
   else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ())
 
+(* Heuristic for horizontalizing hypothesis that the user probably
+   considers as "variables": An hypothesis H:T where T:S and S<>Prop. *)
+let should_compact env sigma typ =
+  get_compact_context() &&
+    let type_of_typ = Retyping.get_type_of env sigma (EConstr.of_constr typ) in
+    not (is_Prop (EConstr.to_constr sigma type_of_typ))
+
+
+(* If option Compact Contexts is set, we pack "simple" hypothesis in a
+   hov box (with three sapaces as a separator), the global box being a
+   v box *)
 let rec bld_sign_env env sigma ctxt pps =
   match ctxt with
   | [] -> pps
+  | CompactedDecl.LocalAssum (ids,typ)::ctxt' when should_compact env sigma typ ->
+    let pps',ctxt' = bld_sign_env_id env sigma ctxt (mt ()) true in
+    (* putting simple hyps in a more horizontal flavor *)
+    bld_sign_env env sigma ctxt' (pps ++ brk (0,0) ++ hov 0 pps')
   | d:: ctxt' ->
-     let pidt = pr_var_list_decl env sigma d in
-     let pps' = pps ++ brk (0,0) ++ pidt in
-     bld_sign_env env sigma ctxt' pps'
+    let pidt = pr_var_list_decl env sigma d in
+    let pps' = pps ++ brk (0,0) ++ pidt in
+    bld_sign_env env sigma ctxt' pps'
+and bld_sign_env_id env sigma ctxt pps is_start =
+  match ctxt with
+  | [] -> pps,ctxt
+ | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ ->
+    let pidt = pr_var_list_decl env sigma d in
+    let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in
+    bld_sign_env_id env sigma ctxt' pps' false
+  | _ -> pps,ctxt
 
 
+(* compact printing an env (variables and de Bruijn). Separator: three
+   spaces between simple hyps, and newline otherwise *)
 let pr_context_limit_compact ?n env sigma =
   let ctxt = Termops.compact_named_context (named_context env) in
   let lgth = List.length ctxt in
@@ -360,15 +433,14 @@ let pr_context_limit_compact ?n env sigma =
     | Some n when n > lgth -> lgth
     | Some n -> n in
   let ctxt_chopped,ctxt_hidden = Util.List.chop n_capped ctxt in
-  (* a dot line hinting the number of hiden hyps. *)
+  (* a dot line hinting the number of hidden hyps. *)
   let hidden_dots = String.make (List.length ctxt_hidden) '.' in
   let sign_env = v 0 (str hidden_dots ++ (mt ())
                  ++ bld_sign_env env sigma (List.rev ctxt_chopped) (mt ())) in
   let db_env =
-    fold_rel_context
-      (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d)
+    fold_rel_context (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d)
       env ~init:(mt ()) in
-  (sign_env ++ db_env)
+  sign_env ++ db_env
 
 (* The number of printed hypothesis in a goal *)
 (* If [None], no limit *)
@@ -419,23 +491,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 +565,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 +659,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 +699,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 +716,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 mt () else cut ())
+      ++ pr_rec 2 l
     else 
       pr_rec 1 (g::l)
   in
@@ -658,32 +733,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 +762,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 +796,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 +813,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 =
diff --git a/printing/printer.mli b/printing/printer.mli
index 504392e35f..24107394e6 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -18,6 +18,11 @@ open Glob_term
 
 (** These are the entry points for printing terms, context, tac, ... *)
 
+
+val enable_unfocused_goal_printing: bool ref
+val enable_goal_tags_printing      : bool ref
+val enable_goal_names_printing     : bool ref
+
 (** Terms *)
 
 val pr_lconstr_env         : env -> evar_map -> constr -> std_ppcmds
@@ -111,6 +116,9 @@ val pr_pconstructor        : env -> pconstructor -> std_ppcmds
 
 
 (** Contexts *)
+(** Display compact contexts of goals (simple hyps on the same line) *)
+val set_compact_context : bool -> unit
+val get_compact_context : unit -> bool
 
 val pr_context_unlimited   : env -> evar_map -> std_ppcmds
 val pr_ne_context_of       : std_ppcmds -> env -> evar_map -> std_ppcmds
@@ -132,10 +140,22 @@ val pr_cpred               : Cpred.t -> std_ppcmds
 val pr_idpred              : Id.Pred.t -> std_ppcmds
 val pr_transparent_state   : transparent_state -> std_ppcmds
 
-(** Proofs *)
+(** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
 
 val pr_goal                : goal sigma -> std_ppcmds
-val 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 pp sigma seeds shelf focus_stack unfocused goals]
+   prints the goals of the list [goals] followed by the goals in
+   [unfocused], in a short way (typically only the conclusion) except
+   for the first goal if [pr_first] is true. This function can be
+   replaced by another one by calling [set_printer_pr] (see below),
+   typically by plugin writers. The default printer prints only the
+   focused goals unless the conrresponding option
+   [enable_unfocused_goal_printing] is set. [seeds] is for printing
+   dependent evars (mainly for emacs proof tree mode). *)
+val pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list
+                             -> goal list -> goal list -> std_ppcmds
+
 val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
 val pr_concl               : int -> evar_map -> goal -> std_ppcmds
 
@@ -190,7 +210,7 @@ val pr_goal_by_id : Id.t -> std_ppcmds
 val pr_goal_by_uid : string -> std_ppcmds
 
 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;
 };;