diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cErrors.ml | 4 | ||||
| -rw-r--r-- | lib/feedback.ml | 104 | ||||
| -rw-r--r-- | lib/feedback.mli | 7 | ||||
| -rw-r--r-- | lib/flags.ml | 32 | ||||
| -rw-r--r-- | lib/flags.mli | 4 | ||||
| -rw-r--r-- | lib/monad.ml | 11 | ||||
| -rw-r--r-- | lib/monad.mli | 3 | ||||
| -rw-r--r-- | lib/pp.ml | 24 | ||||
| -rw-r--r-- | lib/pp.mli | 9 | ||||
| -rw-r--r-- | lib/ppstyle.ml | 69 | ||||
| -rw-r--r-- | lib/ppstyle.mli | 9 | ||||
| -rw-r--r-- | lib/unicode.ml | 8 | ||||
| -rw-r--r-- | lib/unicode.mli | 12 |
13 files changed, 135 insertions, 161 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 1459141d1e..c69c7e4001 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -93,7 +93,9 @@ let print_backtrace e = match Backtrace.get_backtrace e with let print_anomaly askreport e = if askreport then - hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.") + hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ + strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++ + str ".") else hov 0 (raw_anomaly e) diff --git a/lib/feedback.ml b/lib/feedback.ml index dd1ca2af36..44b3ee35d7 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -52,8 +52,7 @@ open Pp_control type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit -let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) -let msgnl strm = msgnl_with !std_ft strm +let msgnl_with ?pp_tag fmt strm = msg_with ?pp_tag fmt (strm ++ fnl ()) (* XXX: This is really painful! *) module Emacs = struct @@ -75,45 +74,100 @@ end open Emacs -let dbg_str = str "Debug:" ++ spc () +let dbg_str = tag Ppstyle.(Tag.inj debug_tag tag) (str "Debug:") ++ spc () let info_str = mt () -let warn_str = str "Warning:" ++ spc () -let err_str = str "Error:" ++ spc () +let warn_str = tag Ppstyle.(Tag.inj warning_tag tag) (str "Warning:") ++ spc () +let err_str = tag Ppstyle.(Tag.inj error_tag 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 dbg err ?loc level msg = match level with - | Debug -> msgnl (make_body dbg dbg_str ?loc msg) - | Info -> msgnl (make_body dbg info_str ?loc msg) - (* XXX: What to do with loc here? *) - | Notice -> msgnl msg +let gen_logger dbg err ?pp_tag ?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) + | Notice -> msgnl_with ?pp_tag !std_ft msg | Warning -> Flags.if_warn (fun () -> - msgnl_with !err_ft (make_body err warn_str ?loc msg)) () - | Error -> msgnl_with !err_ft (make_body err err_str ?loc msg) + 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 *) -let std_logger = gen_logger (fun x -> x) (fun x -> x) +(* 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 () -> ()) -(* Color logger *) -let color_terminal_logger ?loc level strm = - let msg = Ppstyle.color_msg in - match level with - | Debug -> msg ?loc ~header:("Debug", Ppstyle.debug_tag) !std_ft strm - | Info -> msg ?loc !std_ft strm - | Notice -> msg ?loc !std_ft strm - | Warning -> Flags.if_warn (fun () -> - msg ?loc ~header:("Warning", Ppstyle.warning_tag) !err_ft strm) () - | Error -> msg ?loc ~header:("Error", Ppstyle.error_tag) !err_ft strm +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 () (* Rules for emacs: - Debug/info: emacs_quote_info - Warning/Error: emacs_quote_err - Notice: unquoted + + Note the inconsistency. *) -let emacs_logger = gen_logger emacs_quote_info emacs_quote_err +let emacs_logger = gen_logger emacs_quote_info emacs_quote_err ?pp_tag:None + +(** 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 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 open Pp_control in + let push_tag, pop_tag, clear_tag = make_style_stack () in + std_logger_cleanup := clear_tag; + std_logger_tag := Some Ppstyle.pp_tag; + 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 let logger = ref std_logger let set_logger l = logger := l diff --git a/lib/feedback.mli b/lib/feedback.mli index 48b1c19a67..5160bd5bc1 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -72,11 +72,8 @@ val set_logger : logger -> unit (** [std_logger] standard logger to [stdout/stderr] *) val std_logger : logger -val color_terminal_logger : logger -(* This logger will apply the proper {!Pp_style} tags, and in - particular use the formatters {!Pp_control.std_ft} and - {!Pp_control.err_ft} to display those messages. Be careful this is - not compatible with the Emacs mode! *) +(** [init_color_output ()] Enable color in the std_logger *) +val init_color_output : unit -> unit (** [feedback_logger] will produce feedback messages instead IO events *) val feedback_logger : logger diff --git a/lib/flags.ml b/lib/flags.ml index 13525165ab..0e2f7e5a62 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -70,7 +70,7 @@ let priority_of_string = function | "high" -> High | _ -> raise (Invalid_argument "priority_of_string") type tac_error_filter = [ `None | `Only of string list | `All ] -let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "curly" ]) +let async_proofs_tac_error_resilience = ref (`Only [ "curly" ]) let async_proofs_cmd_error_resilience = ref true let async_proofs_is_worker () = @@ -112,17 +112,22 @@ type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current let compat_version = ref Current -let version_strictly_greater v = match !compat_version, v with -| V8_2, (V8_2 | V8_3 | V8_4 | V8_5 | Current) -> false -| V8_3, (V8_3 | V8_4 | V8_5 | Current) -> false -| V8_4, (V8_4 | V8_5 | Current) -> false -| V8_5, (V8_5 | Current) -> false -| Current, Current -> false -| V8_3, V8_2 -> true -| V8_4, (V8_2 | V8_3) -> true -| V8_5, (V8_2 | V8_3 | V8_4) -> true -| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> true - +let version_compare v1 v2 = match v1, v2 with +| V8_2, V8_2 -> 0 +| V8_2, (V8_3 | V8_4 | V8_5 | Current) -> -1 +| V8_3, V8_2 -> 1 +| V8_3, V8_3 -> 0 +| V8_3, (V8_4 | V8_5 | Current) -> -1 +| V8_4, (V8_2 | V8_3) -> 1 +| V8_4, V8_4 -> 0 +| V8_4, (V8_5 | Current) -> -1 +| V8_5, (V8_2 | V8_3 | V8_4) -> 1 +| V8_5, V8_5 -> 0 +| V8_5, Current -> -1 +| Current, Current -> 0 +| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> 1 + +let version_strictly_greater v = version_compare !compat_version v > 0 let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function @@ -134,8 +139,6 @@ let pr_version = function (* Translate *) let beautify = ref false -let make_beautify f = beautify := f -let do_beautify () = !beautify let beautify_file = ref false (* Silent / Verbose *) @@ -226,6 +229,7 @@ let print_mod_uid = ref false let tactic_context_compat = ref false let profile_ltac = ref false +let profile_ltac_cutoff = ref 2.0 let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode diff --git a/lib/flags.mli b/lib/flags.mli index 8fe64d24fa..897602641c 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -64,13 +64,12 @@ val univ_print : bool ref type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current val compat_version : compat_version ref +val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool val pr_version : compat_version -> string val beautify : bool ref -val make_beautify : bool -> unit -val do_beautify : unit -> bool val beautify_file : bool ref val make_silent : bool -> unit @@ -149,6 +148,7 @@ val tactic_context_compat : bool ref context vs. appcontext) is set. *) val profile_ltac : bool ref +val profile_ltac_cutoff : float ref (** Dump the bytecode after compilation (for debugging purposes) *) val dump_bytecode : bool ref diff --git a/lib/monad.ml b/lib/monad.ml index a1714a41b3..2e55e9698c 100644 --- a/lib/monad.ml +++ b/lib/monad.ml @@ -64,6 +64,9 @@ module type ListS = sig its second argument in a tail position. *) val iter : ('a -> unit t) -> 'a list -> unit t + (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*) + val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t + (** {6 Two-list iterators} *) @@ -138,6 +141,14 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct | a::b::l -> f a >> f b >> iter f l + let rec map_filter f = function + | [] -> return [] + | a::l -> + f a >>= function + | None -> map_filter f l + | Some b -> + map_filter f l >>= fun filtered -> + return (b::filtered) let rec fold_left2 r f x l1 l2 = match l1,l2 with diff --git a/lib/monad.mli b/lib/monad.mli index c8655efa04..f7de71f53a 100644 --- a/lib/monad.mli +++ b/lib/monad.mli @@ -66,6 +66,9 @@ module type ListS = sig its second argument in a tail position. *) val iter : ('a -> unit t) -> 'a list -> unit t + (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*) + val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t + (** {6 Two-list iterators} *) @@ -77,17 +77,6 @@ open Pp_control \end{description} *) -let comments = ref [] - -let rec split_com comacc acc pos = function - [] -> comments := List.rev acc; comacc - | ((b,e),c as com)::coms -> - (* Take all comments that terminates before pos, or begin exactly - at pos (used to print comments attached after an expression) *) - if e<=pos || pos=b then split_com (c::comacc) acc pos coms - else split_com comacc (com::acc) pos coms - - type block_type = | Pp_hbox of int | Pp_vbox of int @@ -111,7 +100,7 @@ type 'a ppcmd_token = | Ppcmd_open_box of block_type | Ppcmd_close_box | Ppcmd_close_tbox - | Ppcmd_comment of int + | Ppcmd_comment of string list | Ppcmd_open_tag of Tag.t | Ppcmd_close_tag @@ -177,7 +166,7 @@ let tab () = Glue.atom(Ppcmd_set_tab) let fnl () = Glue.atom(Ppcmd_force_newline) let pifb () = Glue.atom(Ppcmd_print_if_broken) let ws n = Glue.atom(Ppcmd_white_space n) -let comment n = Glue.atom(Ppcmd_comment n) +let comment l = Glue.atom(Ppcmd_comment l) (* derived commands *) let mt () = Glue.empty @@ -321,8 +310,7 @@ let pp_dirs ?pp_tag ft = com_brk ft; Format.pp_force_newline ft () | Ppcmd_print_if_broken -> com_if ft (Lazy.from_fun(fun()->Format.pp_print_if_newline ft ())) - | Ppcmd_comment i -> - let coms = split_com [] [] i !comments in + | Ppcmd_comment coms -> (* Format.pp_open_hvbox ft 0;*) List.iter (pr_com ft) coms(*; Format.pp_close_box ft ()*) @@ -356,8 +344,8 @@ let pp_with ?pp_tag ft strm = pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm)) (* pretty printing functions WITH FLUSH *) -let msg_with ft strm = - pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush)) +let msg_with ?pp_tag ft strm = + pp_dirs ?pp_tag ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush)) (* If mixing some output and a goal display, please use msg_warning, so that interfaces (proofgeneral for example) can easily dispatch @@ -365,7 +353,7 @@ let msg_with ft strm = (** Output to a string formatter *) let string_of_ppcmds c = - Format.fprintf Format.str_formatter "@[%a@]" msg_with c; + Format.fprintf Format.str_formatter "@[%a@]" (msg_with ?pp_tag:None) c; Format.flush_str_formatter () (* Copy paste from Util *) diff --git a/lib/pp.mli b/lib/pp.mli index 3bd560812e..8342a983de 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -23,8 +23,7 @@ val ws : int -> std_ppcmds val mt : unit -> std_ppcmds val ismt : std_ppcmds -> bool -val comment : int -> std_ppcmds -val comments : ((int * int) * string) list ref +val comment : string list -> std_ppcmds (** {6 Manipulation commands} *) @@ -173,8 +172,8 @@ val pr_loc : Loc.t -> std_ppcmds (** FIXME: These ignore the logging settings and call [Format] directly *) type tag_handler = Tag.t -> Format.tag -(** [msg_with fmt pp] Print [pp] to [fmt] and flush [fmt] *) -val msg_with : Format.formatter -> std_ppcmds -> unit +(** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and flush [fmt] *) +val msg_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit -(** [msg_with fmt pp] Print [pp] to [fmt] and don't flush [fmt] *) +(** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and don't flush [fmt] *) val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml index ecfaa822c7..aa47c51671 100644 --- a/lib/ppstyle.ml +++ b/lib/ppstyle.ml @@ -56,41 +56,6 @@ let default = Terminal.({ let empty = Terminal.make () -let make_style_stack style_tags = - (** Not thread-safe. We should put a lock somewhere if we print from - different threads. Do we? *) - let style_stack = ref [] in - let peek () = match !style_stack with - | [] -> default (** Anomalous case, but for robustness *) - | st :: _ -> st - in - let push tag = - let style = - try - begin match String.Map.find tag style_tags with - | None -> empty - | Some st -> st - end - with Not_found -> empty - 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 - let () = style_stack := style :: !style_stack in - Terminal.eval style - in - let pop _ = match !style_stack with - | [] -> - (** Something went wrong, we fallback *) - Terminal.eval default - | _ :: rem -> - let () = style_stack := rem in - Terminal.eval (peek ()) - in - let clear () = style_stack := [] in - push, pop, clear - let error_tag = let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in make ~style ["message"; "error"] @@ -106,37 +71,3 @@ let debug_tag = let pp_tag t = match Pp.Tag.prj t tag with | None -> "" | Some key -> key - -let clear_tag_fn = ref (fun () -> ()) - -let init_color_output () = - let push_tag, pop_tag, clear_tag = make_style_stack !tags in - clear_tag_fn := clear_tag; - 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 - let open Pp_control 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 - -let color_msg ?loc ?header ft strm = - let pptag = tag in - let open Pp in - let ploc = Option.cata Pp.pr_loc (Pp.mt ()) loc in - let strm = match header with - | None -> hov 0 (ploc ++ strm) - | Some (h, t) -> - let tag = Pp.Tag.inj t pptag in - let h = Pp.tag tag (str h ++ str ":") in - hov 0 (ploc ++ h ++ spc () ++ strm) - in - pp_with ~pp_tag ft strm; - Format.pp_print_newline ft (); - Format.pp_print_flush ft (); - (** In case something went wrong, we reset the stack *) - !clear_tag_fn () diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli index b07fcd5d4c..d9fd757656 100644 --- a/lib/ppstyle.mli +++ b/lib/ppstyle.mli @@ -44,14 +44,7 @@ val parse_config : string -> unit val dump : unit -> (t * Terminal.style option) list (** Recover the list of known tags together with their current style. *) -(** {5 Setting color output} *) - -val init_color_output : unit -> unit - -val color_msg : ?loc:Loc.t -> ?header:string * Format.tag -> - Format.formatter -> Pp.std_ppcmds -> unit -(** {!color_msg ?header fmt pp} will format according to the tags - defined in this file *) +(** {5 Color output} *) val pp_tag : Pp.tag_handler (** Returns the name of a style tag that is understandable by the formatters diff --git a/lib/unicode.ml b/lib/unicode.ml index dc852d9819..ced5e258c2 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -8,9 +8,7 @@ (** Unicode utilities *) -type status = Letter | IdentPart | Symbol - -exception Unsupported +type status = Letter | IdentPart | Symbol | Unknown (* The following table stores classes of Unicode characters that are used by the lexer. There are 3 different classes so 2 bits are @@ -29,6 +27,7 @@ let mask i = function | Letter -> 1 lsl ((i land 7) lsl 1) (* 01 *) | IdentPart -> 2 lsl ((i land 7) lsl 1) (* 10 *) | Symbol -> 3 lsl ((i land 7) lsl 1) (* 11 *) + | Unknown -> 0 lsl ((i land 7) lsl 1) (* 00 *) (* Helper to reset 2 bits in a word. *) let reset_mask i = @@ -55,7 +54,7 @@ let lookup x = if v = 1 then Letter else if v = 2 then IdentPart else if v = 3 then Symbol - else raise Unsupported + else Unknown (* [classify] discriminates between 3 different kinds of symbols based on the standard unicode classification (extracted from @@ -215,7 +214,6 @@ let ident_refutation s = |x -> x with | End_of_input -> Some (true,"The empty string is not an identifier.") - | Unsupported -> Some (true,s^": unsupported character in utf8 sequence.") | Invalid_argument _ -> Some (true,s^": invalid utf8 sequence.") let lowercase_unicode = diff --git a/lib/unicode.mli b/lib/unicode.mli index 1f8bd44eee..2609e1968f 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -8,22 +8,16 @@ (** Unicode utilities *) -type status = Letter | IdentPart | Symbol +type status = Letter | IdentPart | Symbol | Unknown -(** This exception is raised when UTF-8 the input string contains unsupported UTF-8 characters. *) -exception Unsupported - -(** Classify a unicode char into 3 classes. - @raise Unsupported if the input string contains unsupported UTF-8 characters. *) +(** Classify a unicode char into 3 classes or unknown. *) val classify : int -> status (** Return [None] if a given string can be used as a (Coq) identifier. - Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity. - @raise Unsupported if the input string contains unsupported UTF-8 characters. *) + Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity. *) val ident_refutation : string -> (bool * string) option (** First char of a string, converted to lowercase - @raise Unsupported if the input string contains unsupported UTF-8 characters. @raise Assert_failure if the input string is empty. *) val lowercase_first_char : string -> string |