diff options
-rw-r--r-- | CHANGES | 6 | ||||
-rw-r--r-- | doc/refman/RefMan-oth.tex | 16 | ||||
-rw-r--r-- | printing/printer.ml | 45 | ||||
-rw-r--r-- | printing/printer.mli | 5 | ||||
-rw-r--r-- | test-suite/output/CompactContexts.out | 7 | ||||
-rw-r--r-- | test-suite/output/CompactContexts.v | 5 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 9 |
7 files changed, 85 insertions, 8 deletions
@@ -23,6 +23,12 @@ Tactics type of the variables that the tactic "refine" introduces in the context, producing types a priori closer to the expectations. +Vernacular Commands + +- Goals context can be printed in a more compact way when "Set + Printing Compact Contexts" is activated. + + Standard Library - New file PropExtensionality.v to explicitly work in the axiomatic diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index a25da7d92..3daaac88b 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -960,6 +960,22 @@ time of writing this documentation, the default value is 50). \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}} This command displays the current nesting depth used for display. +\subsection[\tt Unset Printing Compact Contexts.]{\tt Unset Printing Compact Contexts.\optindex{Printing Compact Contexts}} +This command resets the displaying of goals contexts to non compact +mode (default at the time of writing this documentation). Non compact +means that consecutive variables of different types are printed on +different lines. + +\subsection[\tt Set Printing Compact Contexts.]{\tt Set Printing Compact Contexts.\optindex{Printing Compact Contexts}} +This command sets the displaying of goals contexts to compact mode. +The printer tries to reduce the vertical size of goals contexts by +putting several variables (even if of different types) on the same +line provided it does not exceed the printing width (See {\tt Set + Printing Width} above). + +\subsection[\tt Test Printing Compact Contexts.]{\tt Test Printing Compact Contexts.\optindex{Printing Compact Contexts}} +This command displays the current state of compaction of goal d'isolat. + \subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}} This command enables the printing of the ``{\tt (dependent evars: \ldots)}'' line when {\tt -emacs} is passed. diff --git a/printing/printer.ml b/printing/printer.ml index 91a7d2289..e0ca51f0c 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -303,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) -> @@ -383,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 @@ -401,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 *) diff --git a/printing/printer.mli b/printing/printer.mli index c28295054..24107394e 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -116,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 @@ -137,7 +140,7 @@ 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 diff --git a/test-suite/output/CompactContexts.out b/test-suite/output/CompactContexts.out new file mode 100644 index 000000000..9d1d19877 --- /dev/null +++ b/test-suite/output/CompactContexts.out @@ -0,0 +1,7 @@ +1 subgoal + + hP1 : True + a : nat b : list nat h : forall x : nat, {y : nat | y > x} + h2 : True + ============================ + False diff --git a/test-suite/output/CompactContexts.v b/test-suite/output/CompactContexts.v new file mode 100644 index 000000000..07588d34f --- /dev/null +++ b/test-suite/output/CompactContexts.v @@ -0,0 +1,5 @@ +Set Printing Compact Contexts. + +Lemma f (hP1:True) (a:nat) (b:list nat) (h:forall (x:nat) , { y:nat | y > x}) (h2:True): False. +Show. +Abort.
\ No newline at end of file diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 2cb6f3918..d4e6af995 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1412,6 +1412,15 @@ let _ = optwrite = (fun _ -> ()) } let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "display compact goal contexts"; + optkey = ["Printing";"Compact";"Contexts"]; + optread = (fun () -> Printer.get_compact_context()); + optwrite = (fun b -> Printer.set_compact_context b) } + +let _ = declare_int_option { optsync = true; optdepr = false; |