diff options
| -rw-r--r-- | CHANGES | 7 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 8 | ||||
| -rw-r--r-- | printing/printer.ml | 41 |
3 files changed, 41 insertions, 15 deletions
@@ -65,6 +65,9 @@ Tools - coqc accepts a -o option to specify the output file name - coqtop accepts --print-version to print Coq and OCaml versions in easy to parse format +- Setting [Printing Dependent Evars Line] can be unset to disable the + computation associated with printing the "dependent evars: " line in + -emacs mode Changes from V8.5pl1 to V8.5pl2 =============================== @@ -507,8 +510,8 @@ Tactics - When given a reference as argument, simpl, vm_compute and native_compute now strictly interpret it as the head of a pattern starting with this reference. -- The "change p with c" tactic semantics changed, now type-checking - "c" at each matching occurrence "t" of the pattern "p", and +- The "change p with c" tactic semantics changed, now type-checking + "c" at each matching occurrence "t" of the pattern "p", and converting "t" with "c". - Now "appcontext" and "context" behave the same. The old buggy behavior of "context" can be retrieved at parse time by setting the diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index aea2bae38..6a8bda35d 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -947,6 +947,14 @@ 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 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. + +\subsection[\tt Unset Printing Dependent Evars Line.]{\tt Unset Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}} +This command disables the printing of the ``{\tt (dependent evars: \ldots)}'' +line when {\tt -emacs} is passed. + %\subsection{\tt Abstraction ...} %Not yet documented. diff --git a/printing/printer.ml b/printing/printer.ml index 8af2af98a..0bac2755b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -496,6 +496,18 @@ let print_evar_constraints gl sigma cstrs = in prlist_with_sep fnl pr_evconstr cstrs +let should_print_dependent_evars = ref true + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "Printing Dependent Evars Line"; + optkey = ["Printing";"Dependent";"Evars";"Line"]; + optread = (fun () -> !should_print_dependent_evars); + optwrite = (fun v -> should_print_dependent_evars := v) } + let print_dependent_evars gl sigma seeds = let constraints = let _, cstrs = Evd.extract_all_conv_pbs sigma in @@ -504,21 +516,25 @@ let print_dependent_evars gl sigma seeds = ++ str":" ++ fnl () ++ hov 0 (print_evar_constraints gl sigma cstrs) in let evars () = - let evars = Evarutil.gather_dependent_evars sigma seeds in - let evars = - Evar.Map.fold begin fun e i s -> - let e' = pr_internal_existential_key e in - match i with - | None -> s ++ str" " ++ e' ++ str " open," - | Some i -> - s ++ str " " ++ e' ++ str " using " ++ - Evar.Set.fold begin fun d s -> - pr_internal_existential_key d ++ str " " ++ s - end i (str ",") - end evars (str "") + if !should_print_dependent_evars then + let evars = Evarutil.gather_dependent_evars sigma seeds in + let evars = + Evar.Map.fold begin fun e i s -> + let e' = pr_internal_existential_key e in + match i with + | None -> s ++ str" " ++ e' ++ str " open," + | Some i -> + s ++ str " " ++ e' ++ str " using " ++ + Evar.Set.fold begin fun d s -> + pr_internal_existential_key d ++ str " " ++ s + end i (str ",") + end evars (str "") in fnl () ++ str "(dependent evars:" ++ evars ++ str ")" ++ fnl () + else + fnl () ++ + str "(dependent evars: (printing disabled) )" ++ fnl () in constraints ++ delayed_emacs_cmd evars @@ -869,4 +885,3 @@ let pr_polymorphic b = let pr_universe_instance evd ctx = let inst = Univ.UContext.instance ctx in str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}" - |