diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/explainErr.ml | 42 | ||||
| -rw-r--r-- | vernac/explainErr.mli | 2 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 245 | ||||
| -rw-r--r-- | vernac/topfmt.mli | 49 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 12 |
6 files changed, 320 insertions, 31 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 5b91af03c..f1e0c48f0 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -45,15 +45,9 @@ let _ = CErrors.register_handler explain_exn_default (** Pre-explain a vernac interpretation error *) -let wrap_vernac_error with_header (exn, info) strm = - if with_header then - let header = Pp.tag Ppstyle.error_tag (str "Error:") in - let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in - (e, info) - else - (EvaluatedError (strm, None), info) +let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info) -let process_vernac_interp_error with_header exn = match fst exn with +let process_vernac_interp_error exn = match fst exn with | Univ.UniverseInconsistency i -> let msg = if !Constrextern.print_universes then @@ -61,40 +55,40 @@ let process_vernac_interp_error with_header exn = match fst exn with Univ.explain_universe_inconsistency Universes.pr_with_global_universes i else mt() in - wrap_vernac_error with_header exn (str "Universe inconsistency" ++ msg ++ str ".") + wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> - wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te) + wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te) | PretypeError(ctx,sigma,te) -> - wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te) + wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) | Typeclasses_errors.TypeClassError(env, te) -> - wrap_vernac_error with_header exn (Himsg.explain_typeclass_error env te) + wrap_vernac_error exn (Himsg.explain_typeclass_error env te) | InductiveError e -> - wrap_vernac_error with_header exn (Himsg.explain_inductive_error e) + wrap_vernac_error exn (Himsg.explain_inductive_error e) | Modops.ModuleTypingError e -> - wrap_vernac_error with_header exn (Himsg.explain_module_error e) + wrap_vernac_error exn (Himsg.explain_module_error e) | Modintern.ModuleInternalizationError e -> - wrap_vernac_error with_header exn (Himsg.explain_module_internalization_error e) + wrap_vernac_error exn (Himsg.explain_module_internalization_error e) | RecursionSchemeError e -> - wrap_vernac_error with_header exn (Himsg.explain_recursion_scheme_error e) + wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e) | Cases.PatternMatchingError (env,sigma,e) -> - wrap_vernac_error with_header exn (Himsg.explain_pattern_matching_error env sigma e) + wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) | Tacred.ReductionTacticError e -> - wrap_vernac_error with_header exn (Himsg.explain_reduction_tactic_error e) + wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) | Logic.RefinerError e -> - wrap_vernac_error with_header exn (Himsg.explain_refiner_error e) + wrap_vernac_error exn (Himsg.explain_refiner_error e) | Nametab.GlobalizationError q -> - wrap_vernac_error with_header exn + wrap_vernac_error exn (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ spc () ++ str "was not found" ++ spc () ++ str "in the current" ++ spc () ++ str "environment.") | Refiner.FailError (i,s) -> let s = Lazy.force s in - wrap_vernac_error with_header exn + wrap_vernac_error exn (str "Tactic failure" ++ (if Pp.ismt s then s else str ": " ++ s) ++ if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").") | AlreadyDeclared msg -> - wrap_vernac_error with_header exn (msg ++ str ".") + wrap_vernac_error exn (msg ++ str ".") | _ -> exn @@ -108,9 +102,9 @@ let additional_error_info = ref [] let register_additional_error_info f = additional_error_info := f :: !additional_error_info -let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) = +let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) = let exc = strip_wrapping_exceptions exc in - let e = process_vernac_interp_error with_header (exc, info) in + let e = process_vernac_interp_error (exc, info) in let () = if not allow_uncaught && not (CErrors.handled (fst e)) then let (e, info) = e in diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli index a67c887af..370ad7e3b 100644 --- a/vernac/explainErr.mli +++ b/vernac/explainErr.mli @@ -11,7 +11,7 @@ exception EvaluatedError of Pp.std_ppcmds * exn option (** Pre-explain a vernac interpretation error *) -val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn +val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn (** General explain function. Should not be used directly now, see instead function [Errors.print] and variants *) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml new file mode 100644 index 000000000..85981c386 --- /dev/null +++ b/vernac/topfmt.ml @@ -0,0 +1,245 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Feedback +open Pp + +(** Pp control also belongs here as the terminal is private to the toplevel *) + +type pp_global_params = { + margin : int; + max_indent : int; + max_depth : int; + ellipsis : string } + +(* Default parameters of pretty-printing *) + +let dflt_gp = { + margin = 78; + max_indent = 50; + max_depth = 50; + ellipsis = "..." } + +(* A deeper pretty-printer to print proof scripts *) + +let deep_gp = { + margin = 78; + max_indent = 50; + max_depth = 10000; + ellipsis = "..." } + +(* set_gp : Format.formatter -> pp_global_params -> unit + * set the parameters of a formatter *) + +let set_gp ft gp = + Format.pp_set_margin ft gp.margin ; + Format.pp_set_max_indent ft gp.max_indent ; + Format.pp_set_max_boxes ft gp.max_depth ; + Format.pp_set_ellipsis_text ft gp.ellipsis + +let set_dflt_gp ft = set_gp ft dflt_gp + +let get_gp ft = + { margin = Format.pp_get_margin ft (); + max_indent = Format.pp_get_max_indent ft (); + max_depth = Format.pp_get_max_boxes ft (); + ellipsis = Format.pp_get_ellipsis_text ft () } + +(* with_fp : 'a pp_formatter_params -> Format.formatter + * returns of formatter for given formatter functions *) + +let with_fp chan out_function flush_function = + let ft = Format.make_formatter out_function flush_function in + Format.pp_set_formatter_out_channel ft chan; + ft + +(* Output on a channel ch *) + +let with_output_to ch = + let ft = with_fp ch (output_substring ch) (fun () -> flush ch) in + set_gp ft deep_gp; + ft + +let std_ft = ref Format.std_formatter +let _ = set_dflt_gp !std_ft + +let err_ft = ref Format.err_formatter +let _ = set_gp !err_ft deep_gp + +let deep_ft = ref (with_output_to stdout) +let _ = set_gp !deep_ft deep_gp + +(* For parametrization through vernacular *) +let default = Format.pp_get_max_boxes !std_ft () +let default_margin = Format.pp_get_margin !std_ft () + +let get_depth_boxes () = Some (Format.pp_get_max_boxes !std_ft ()) +let set_depth_boxes v = + Format.pp_set_max_boxes !std_ft (match v with None -> default | Some v -> v) + +let get_margin () = Some (Format.pp_get_margin !std_ft ()) +let set_margin v = + let v = match v with None -> default_margin | Some v -> v in + Format.pp_set_margin Format.str_formatter v; + Format.pp_set_margin !std_ft v; + Format.pp_set_margin !deep_ft v; + (* Heuristic, based on usage: the column on the right of max_indent + column is 20% of width, capped to 30 characters *) + let m = max (64 * v / 100) (v-30) in + Format.pp_set_max_indent Format.str_formatter m; + Format.pp_set_max_indent !std_ft m; + Format.pp_set_max_indent !deep_ft m + +(** Console display of feedback *) + +type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit + +let msgnl_with ?pp_tag fmt strm = + pp_with ?pp_tag fmt (strm ++ fnl ()); + Format.pp_print_flush fmt () + +(* XXX: This is really painful! *) +module Emacs = struct + + (* Special chars for emacs, to detect warnings inside goal output *) + let emacs_quote_start = String.make 1 (Char.chr 254) + let emacs_quote_end = String.make 1 (Char.chr 255) + + let emacs_quote_err g = + hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end) + + let emacs_quote_info_start = "<infomsg>" + let emacs_quote_info_end = "</infomsg>" + + let emacs_quote_info g = + hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end) + +end + +open Emacs + +let dbg_str = tag Ppstyle.debug_tag (str "Debug:") ++ spc () +let info_str = mt () +let warn_str = tag Ppstyle.warning_tag (str "Warning:") ++ spc () +let err_str = tag Ppstyle.error_tag (str "Error:") ++ spc () + +let make_body quoter info ?loc s = + let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in + quoter (hov 0 (loc ++ info ++ s)) + +(* Generic logger *) +let gen_logger ?pp_tag dbg err ?loc level msg = match level with + | Debug -> msgnl_with ?pp_tag !std_ft (make_body dbg dbg_str ?loc msg) + | Info -> msgnl_with ?pp_tag !std_ft (make_body dbg info_str ?loc msg) + (* XXX: What to do with loc here? *) + | Notice -> msgnl_with ?pp_tag !std_ft msg + | Warning -> Flags.if_warn (fun () -> + msgnl_with ?pp_tag !err_ft (make_body err warn_str ?loc msg)) () + | Error -> msgnl_with ?pp_tag !err_ft (make_body err err_str ?loc msg) + +(** Standard loggers *) + +(* We provide a generic clear_log_backend callback for backends + wanting to do clenaup after the print. +*) +let std_logger_tag = ref None +let std_logger_cleanup = ref (fun () -> ()) + +let std_logger ?loc level msg = + gen_logger (fun x -> x) (fun x -> x) ?pp_tag:!std_logger_tag ?loc level msg; + !std_logger_cleanup () + +(** Color logging. Moved from pp_style, it may need some more refactoring *) + +(** Not thread-safe. We should put a lock somewhere if we print from + different threads. Do we? *) +let make_style_stack () = + (** Default tag is to reset everything *) + let empty = Terminal.make () in + let default_tag = Terminal.({ + fg_color = Some `DEFAULT; + bg_color = Some `DEFAULT; + bold = Some false; + italic = Some false; + underline = Some false; + negative = Some false; + }) + in + let style_stack = ref [] in + let peek () = match !style_stack with + | [] -> default_tag (** Anomalous case, but for robustness *) + | st :: _ -> st + in + let push tag = + let style = match Ppstyle.get_style_format tag with + | None -> empty + | Some st -> st + in + (** Use the merging of the latest tag and the one being currently pushed. + This may be useful if for instance the latest tag changes the background and + the current one the foreground, so that the two effects are additioned. *) + let style = Terminal.merge (peek ()) style in + style_stack := style :: !style_stack; + Terminal.eval style + in + let pop _ = match !style_stack with + | [] -> (** Something went wrong, we fallback *) + Terminal.eval default_tag + | _ :: rem -> style_stack := rem; + Terminal.eval (peek ()) + in + let clear () = style_stack := [] in + push, pop, clear + +let init_color_output () = + let push_tag, pop_tag, clear_tag = make_style_stack () in + std_logger_cleanup := clear_tag; + std_logger_tag := Some Ppstyle.to_format; + let tag_handler = { + Format.mark_open_tag = push_tag; + Format.mark_close_tag = pop_tag; + Format.print_open_tag = ignore; + Format.print_close_tag = ignore; + } 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 + +(* Rules for emacs: + - Debug/info: emacs_quote_info + - Warning/Error: emacs_quote_err + - Notice: unquoted + *) +let emacs_logger = gen_logger emacs_quote_info emacs_quote_err + +(* Output to file, used only in extraction so a candidate for removal *) +let ft_logger old_logger ft ?loc level mesg = + let id x = x in + match level with + | Debug -> msgnl_with ft (make_body id dbg_str mesg) + | Info -> msgnl_with ft (make_body id info_str mesg) + | Notice -> msgnl_with ft mesg + | Warning -> old_logger ?loc level mesg + | Error -> old_logger ?loc level mesg + +let with_output_to_file fname func input = + (* XXX FIXME: redirect std_ft *) + (* let old_logger = !logger in *) + let channel = open_out (String.concat "." [fname; "out"]) in + (* logger := ft_logger old_logger (Format.formatter_of_out_channel channel); *) + try + let output = func input in + (* logger := old_logger; *) + close_out channel; + output + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + (* logger := old_logger; *) + close_out channel; + Exninfo.iraise reraise diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli new file mode 100644 index 000000000..38a400cfd --- /dev/null +++ b/vernac/topfmt.mli @@ -0,0 +1,49 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Console printing options *) + +type pp_global_params = { + margin : int; + max_indent : int; + max_depth : int; + ellipsis : string } + +val dflt_gp : pp_global_params +val deep_gp : pp_global_params +val set_gp : Format.formatter -> pp_global_params -> unit +val set_dflt_gp : Format.formatter -> unit +val get_gp : Format.formatter -> pp_global_params + +(** {6 Output functions of pretty-printing. } *) + +val with_output_to : out_channel -> Format.formatter + +val std_ft : Format.formatter ref +val err_ft : Format.formatter ref +val deep_ft : Format.formatter ref + +(** {6 For parametrization through vernacular. } *) + +val set_depth_boxes : int option -> unit +val get_depth_boxes : unit -> int option + +val set_margin : int option -> unit +val get_margin : unit -> int option + +(** Console display of feedback *) +val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit + +val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit + +val init_color_output : unit -> unit + +(** [with_output_to_file file f x] executes [f x] with logging + redirected to a file [file] *) +val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b + diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 94ef54f70..283c095eb 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -14,4 +14,5 @@ Record Assumptions Vernacinterp Mltop +Topfmt Vernacentries diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3afe04b37..09c43f93e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1448,8 +1448,8 @@ let _ = optdepr = false; optname = "the printing depth"; optkey = ["Printing";"Depth"]; - optread = Pp_control.get_depth_boxes; - optwrite = Pp_control.set_depth_boxes } + optread = Topfmt.get_depth_boxes; + optwrite = Topfmt.set_depth_boxes } let _ = declare_int_option @@ -1457,8 +1457,8 @@ let _ = optdepr = false; optname = "the printing width"; optkey = ["Printing";"Width"]; - optread = Pp_control.get_margin; - optwrite = Pp_control.set_margin } + optread = Topfmt.get_margin; + optwrite = Topfmt.set_margin } let _ = declare_bool_option @@ -2193,7 +2193,7 @@ let with_fail b f = | e -> let e = CErrors.push e in raise (HasFailed (CErrors.iprint - (ExplainErr.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e)))) + (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))) () with e when CErrors.noncritical e -> let (e, _) = CErrors.push e in @@ -2226,7 +2226,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = current_timeout := Some n; aux ?locality ?polymorphism isprogcmd v | VernacRedirect (s, (_,v)) -> - Feedback.with_output_to_file s (aux false) v + Topfmt.with_output_to_file s (aux false) v | VernacTime (_,v) -> System.with_time !Flags.time (aux ?locality ?polymorphism isprogcmd) v; |