diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 1 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 4 | ||||
| -rw-r--r-- | vernac/search.ml | 2 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 51 | ||||
| -rw-r--r-- | vernac/topfmt.mli | 4 |
6 files changed, 49 insertions, 15 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ca3fb392fe..86dcb6d4dc 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -909,6 +909,7 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env Evd.empty t2) | IncompatibleConstraints cst -> str " the expected (polymorphic) constraints do not imply " ++ + let cst = Univ.UContext.constraints (Univ.instantiate_univ_context cst) in quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c0acdaf57d..5a1c260b1f 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -362,7 +362,7 @@ let get_body obl = match obl.obl_body with | None -> None | Some (DefinedObl c) -> - let u = Environ.constant_instance (Global.env ()) c in + let u = Univ.AUContext.instance (Environ.constant_context (Global.env ()) c) in let pc = (c, u) in Some (DefinedObl pc) | Some (TermObl c) -> diff --git a/vernac/record.ml b/vernac/record.ml index d61f44cac8..366f504545 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -265,7 +265,7 @@ let warn_non_primitive_record = let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in - let u = Declareops.inductive_polymorphic_instance mib in + let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let poly = Declareops.inductive_is_polymorphic mib in let ctx = @@ -547,7 +547,7 @@ let add_inductive_class ind = let mind, oneind = Global.lookup_inductive ind in let k = let ctx = oneind.mind_arity_ctxt in - let inst = Declareops.inductive_polymorphic_instance mind in + let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mind) in let ty = Inductive.type_of_inductive (push_rel_context ctx (Global.env ())) ((mind,oneind),inst) diff --git a/vernac/search.ml b/vernac/search.ml index 00536e52ec..788a2aa4a9 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -85,7 +85,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) = let mib = Global.lookup_mind mind in let iter_packet i mip = let ind = (mind, i) in - let u = Declareops.inductive_polymorphic_instance mib in + let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in let i = (ind, u) in let typ = Inductiveops.type_of_inductive env i in let () = fn (IndRef ind) env typ in diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index b3810f7d53..e7b14309d1 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -149,7 +149,7 @@ let gen_logger dbg warn ?pre_hdr level msg = match level with (** Standard loggers *) (* We provide a generic clear_log_backend callback for backends - wanting to do clenaup after the print. + wanting to do cleanup after the print. *) let std_logger_cleanup = ref (fun () -> ()) @@ -207,6 +207,8 @@ let make_style_stack () = italic = Some false; underline = Some false; negative = Some false; + prefix = None; + suffix = None; }) in let style_stack = ref [] in @@ -235,20 +237,49 @@ let make_style_stack () = let clear () = style_stack := [] in push, pop, clear -let init_color_output () = +let make_printing_functions () = + let empty = Terminal.make () in + let print_prefix ft tag = + let style = + try CString.Map.find tag !tag_map + with | Not_found -> empty + in + match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> () + in + let print_suffix ft tag = + let style = + try CString.Map.find tag !tag_map + with | Not_found -> empty + in + match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> () + in + print_prefix, print_suffix + +let init_terminal_output ~color = init_tag_map (default_tag_map ()); let push_tag, pop_tag, clear_tag = make_style_stack () in - std_logger_cleanup := clear_tag; - let tag_handler = { + let print_prefix, print_suffix = make_printing_functions () in + let tag_handler ft = { Format.mark_open_tag = push_tag; Format.mark_close_tag = pop_tag; - Format.print_open_tag = ignore; - Format.print_close_tag = ignore; + Format.print_open_tag = print_prefix ft; + Format.print_close_tag = print_suffix ft; } in - Format.pp_set_mark_tags !std_ft true; - Format.pp_set_mark_tags !err_ft true; - Format.pp_set_formatter_tag_functions !std_ft tag_handler; - Format.pp_set_formatter_tag_functions !err_ft tag_handler + if color then + (* Use 0-length markers *) + begin + std_logger_cleanup := clear_tag; + Format.pp_set_mark_tags !std_ft true; + Format.pp_set_mark_tags !err_ft true + end + else + (* Use textual markers *) + begin + Format.pp_set_print_tags !std_ft true; + Format.pp_set_print_tags !err_ft true + end; + Format.pp_set_formatter_tag_functions !std_ft (tag_handler !std_ft); + Format.pp_set_formatter_tag_functions !err_ft (tag_handler !err_ft) (* Rules for emacs: - Debug/info: emacs_quote_info diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 0e781bcc1b..6e006fc6c9 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -41,11 +41,13 @@ val std_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit (** Color output *) -val init_color_output : unit -> unit val clear_styles : unit -> unit val parse_color_config : string -> unit val dump_tags : unit -> (string * Terminal.style) list +(** Initialization of interpretation of tags *) +val init_terminal_output : color:bool -> unit + (** Error printing *) (* To be deprecated when we can fully move to feedback-based error printing. *) |