aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/cErrors.ml16
-rw-r--r--lib/cWarnings.ml130
-rw-r--r--lib/cWarnings.mli23
-rw-r--r--lib/feedback.ml104
-rw-r--r--lib/feedback.mli7
-rw-r--r--lib/flags.ml33
-rw-r--r--lib/flags.mli3
-rw-r--r--lib/minisys.ml8
-rw-r--r--lib/monad.ml11
-rw-r--r--lib/monad.mli3
-rw-r--r--lib/pp.ml73
-rw-r--r--lib/pp.mli9
-rw-r--r--lib/ppstyle.ml69
-rw-r--r--lib/ppstyle.mli9
-rw-r--r--lib/profile.ml6
-rw-r--r--lib/richpp.ml9
-rw-r--r--lib/stateid.ml2
-rw-r--r--lib/stateid.mli5
-rw-r--r--lib/system.ml8
-rw-r--r--lib/system.mli5
-rw-r--r--lib/unicode.ml8
-rw-r--r--lib/unicode.mli12
22 files changed, 278 insertions, 275 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 1459141d1e..5c56192fc5 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -16,6 +16,16 @@ let push = Backtrace.add_backtrace
exception Anomaly of string option * std_ppcmds (* System errors *)
+(* XXX: To move to common tagging functions in Pp, blocked on tag
+ * system cleanup as we cannot define generic error tags now.
+ *
+ * Anyways, tagging should not happen here, but in the specific
+ * listener to the msg_* stuff.
+ *)
+let tag_err_str s = tag Ppstyle.(Tag.inj error_tag tag) (str s) ++ spc ()
+let err_str = tag_err_str "Error:"
+let ann_str = tag_err_str "Anomaly:"
+
let _ =
let pr = function
| Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"")
@@ -93,7 +103,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 (ann_str ++ raw_anomaly e ++ spc () ++
+ strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
+ str ".")
else
hov 0 (raw_anomaly e)
@@ -113,7 +125,7 @@ let iprint_no_report (e, info) =
let _ = register_handler begin function
| UserError(s, pps) ->
- hov 0 (str "Error: " ++ where (Some s) ++ pps)
+ hov 0 (err_str ++ where (Some s) ++ pps)
| _ -> raise Unhandled
end
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 720f54606c..cc2463e224 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -21,7 +21,7 @@ let warnings : (string, t) Hashtbl.t = Hashtbl.create 97
let categories : (string, string list) Hashtbl.t = Hashtbl.create 97
let current_loc = ref Loc.ghost
-let flags = ref "default"
+let flags = ref ""
let set_current_loc = (:=) current_loc
@@ -35,6 +35,10 @@ let add_warning_in_category ~name ~category =
in
Hashtbl.replace categories category (name::ws)
+let refine_loc = function
+ | None when not (Loc.is_ghost !current_loc) -> Some !current_loc
+ | loc -> loc
+
let create ~name ~category ?(default=Enabled) pp =
Hashtbl.add warnings name { default; category; status = default };
add_warning_in_category ~name ~category;
@@ -44,15 +48,17 @@ let create ~name ~category ?(default=Enabled) pp =
match w.status with
| Disabled -> ()
| AsError ->
- let loc = Option.default !current_loc loc in
- CErrors.user_err_loc (loc,"_",pp x)
+ begin match refine_loc loc with
+ | Some loc -> CErrors.user_err_loc (loc,"_",pp x)
+ | None -> CErrors.errorlabstrm "_" (pp x)
+ end
| Enabled ->
let msg =
pp x ++ spc () ++ str "[" ++ str name ++ str "," ++
str category ++ str "]"
in
- let loc = Option.default !current_loc loc in
- Feedback.msg_warning ~loc msg
+ let loc = refine_loc loc in
+ Feedback.msg_warning ?loc msg
let warn_unknown_warning =
create ~name:"unknown-warning" ~category:"toplevel"
@@ -62,7 +68,7 @@ let set_warning_status ~name status =
try
let w = Hashtbl.find warnings name in
Hashtbl.replace warnings name { w with status = status }
- with Not_found -> warn_unknown_warning name
+ with Not_found -> ()
let reset_default_warnings () =
Hashtbl.iter (fun name w ->
@@ -74,6 +80,13 @@ let set_all_warnings_status status =
Hashtbl.replace warnings name { w with status })
warnings
+let set_category_status ~name status =
+ let names = Hashtbl.find categories name in
+ List.iter (fun name -> set_warning_status name status) names
+
+let is_all_keyword name = CString.equal name "all"
+let is_none_keyword s = CString.equal s "none"
+
let parse_flag s =
if String.length s > 1 then
match String.get s 0 with
@@ -82,39 +95,94 @@ let parse_flag s =
| _ -> (Enabled, s)
else CErrors.error "Invalid warnings flag"
-let rec do_all_keyword = function
- | [] -> []
- | (status, name as item) :: items ->
- if CString.equal name "all" then
- (set_all_warnings_status status; do_all_keyword items)
- else item :: do_all_keyword items
-
-let rec do_categories = function
- | [] -> []
- | (status, name as item) :: items ->
- try
- let names = Hashtbl.find categories name in
- List.iter (fun name -> set_warning_status name status) names;
- do_categories items
- with Not_found -> item :: do_categories items
+let string_of_flag (status,name) =
+ match status with
+ | AsError -> "+" ^ name
+ | Disabled -> "-" ^ name
+ | Enabled -> name
+
+let string_of_flags flags =
+ String.concat "," (List.map string_of_flag flags)
+
+let set_status ~name status =
+ if is_all_keyword name then
+ set_all_warnings_status status
+ else
+ try
+ set_category_status ~name status
+ with Not_found ->
+ try
+ set_warning_status ~name status
+ with Not_found -> ()
+
+let split_flags s =
+ let reg = Str.regexp "[ ,]+" in Str.split reg s
+
+let check_warning ~silent (_status,name) =
+ is_all_keyword name ||
+ Hashtbl.mem categories name ||
+ Hashtbl.mem warnings name ||
+ (if not silent then warn_unknown_warning name; false)
+
+(** [cut_before_all_rev] removes all flags subsumed by a later occurrence of the
+ "all" flag, and reverses the list. *)
+let rec cut_before_all_rev acc = function
+ | [] -> acc
+ | (_status,name as w) :: warnings ->
+ cut_before_all_rev (w :: if is_all_keyword name then [] else acc) warnings
+
+let cut_before_all_rev warnings = cut_before_all_rev [] warnings
+
+(** [uniquize_flags_rev] removes flags that are subsumed by later occurrences of
+ themselves or their categories, and reverses the list. *)
+let uniquize_flags_rev flags =
+ let rec aux acc visited = function
+ | (_,name as flag)::flags ->
+ if CString.Set.mem name visited then aux acc visited flags else
+ let visited =
+ try
+ let warnings = Hashtbl.find categories name in
+ List.fold_left (fun v w -> CString.Set.add w v) visited warnings
+ with Not_found ->
+ visited
+ in
+ aux (flag::acc) (CString.Set.add name visited) flags
+ | [] -> acc
+ in aux [] CString.Set.empty flags
+
+(** [normalize_flags] removes unknown or redundant warnings. If [silent] is
+ true, it emits a warning when an unknown warning is met. *)
+let normalize_flags ~silent warnings =
+ let warnings = List.filter (check_warning ~silent) warnings in
+ let warnings = cut_before_all_rev warnings in
+ uniquize_flags_rev warnings
+
+let flags_of_string s = List.map parse_flag (split_flags s)
+
+let normalize_flags_string s =
+ if is_none_keyword s then s
+ else
+ let flags = flags_of_string s in
+ let flags = normalize_flags ~silent:false flags in
+ string_of_flags flags
let rec parse_warnings items =
- List.iter (fun (status, name) -> set_warning_status ~name status) items
+ CList.iter (fun (status, name) -> set_status ~name status) items
(* For compatibility, we accept "none" *)
-let parse_flags s =
- if CString.equal s "none" then begin
+let parse_flags s =
+ if is_none_keyword s then begin
Flags.make_warn false;
- set_all_warnings_status Disabled
+ set_all_warnings_status Disabled;
+ "none"
end
else begin
Flags.make_warn true;
- let reg = Str.regexp "[ ,]+" in
- let items = List.map parse_flag (Str.split reg s) in
- let items = do_all_keyword items in
- let items = do_categories items in
- parse_warnings items
+ let flags = flags_of_string s in
+ let flags = normalize_flags ~silent:true flags in
+ parse_warnings flags;
+ string_of_flags flags
end
let set_flags s =
- flags := s; reset_default_warnings (); parse_flags s
+ reset_default_warnings (); let s = parse_flags s in flags := s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index 3515542840..3f6cee31b7 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -6,29 +6,16 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-type status =
- Disabled | Enabled | AsError
-
-(*
-type 'a repr = {
- print : 'a -> Pp.std_ppcmds;
- kind : string;
- enabled : bool;
-}
- *)
+type status = Disabled | Enabled | AsError
val set_current_loc : Loc.t -> unit
val create : name:string -> category:string -> ?default:status ->
('a -> Pp.std_ppcmds) -> ?loc:Loc.t -> 'a -> unit
-(*
-val emit : 'a t -> 'a -> unit
-
-type any = Any : string * string * 'a repr -> any
-
-val dump : unit -> any list
- *)
-
val get_flags : unit -> string
val set_flags : string -> unit
+
+(** Cleans up a user provided warnings status string, e.g. removing unknown
+ warnings (in which case a warning is emitted) or subsumed warnings . *)
+val normalize_flags_string : string -> string
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 d29064c97f..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,7 +229,7 @@ let print_mod_uid = ref false
let tactic_context_compat = ref false
let profile_ltac = ref false
-let profile_ltac_cutoff = ref 0.0
+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 839c252cbb..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
diff --git a/lib/minisys.ml b/lib/minisys.ml
index 25e4d79c4e..f15021c655 100644
--- a/lib/minisys.ml
+++ b/lib/minisys.ml
@@ -46,14 +46,6 @@ let ok_dirname f =
let exists_dir dir =
try Sys.is_directory dir with Sys_error _ -> false
-let check_unix_dir warn dir =
- if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
- (String.length dir > 2 && dir.[1] = ':' ||
- String.contains dir '\\' ||
- String.contains dir ';')
- then warn ("assuming " ^ dir ^
- " to be a Unix path even if looking like a Win32 path.")
-
let apply_subdir f path name =
(* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
(* as well as skipped files like CVS, ... *)
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} *)
diff --git a/lib/pp.ml b/lib/pp.ml
index 7f4bc149dc..f3bb475392 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -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
@@ -254,32 +243,15 @@ let qstring s = str "\"" ++ str (escape_string s) ++ str "\""
let qs = qstring
let quote s = h 0 (str "\"" ++ s ++ str "\"")
-(* This flag tells if the last printed comment ends with a newline, to
- avoid empty lines *)
-let com_eol = ref false
-
-let com_brk ft = com_eol := false
-let com_if ft f =
- if !com_eol then (com_eol := false; Format.pp_force_newline ft ())
- else Lazy.force f
-
let rec pr_com ft s =
let (s1,os) =
try
let n = String.index s '\n' in
String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1))
with Not_found -> s,None in
- com_if ft (Lazy.from_val());
-(* let s1 =
- if String.length s1 <> 0 && s1.[0] = ' ' then
- (Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1))
- else s1 in*)
Format.pp_print_as ft (utf8_length s1) s1;
match os with
- Some s2 ->
- if Int.equal (String.length s2) 0 then (com_eol := true)
- else
- (Format.pp_force_newline ft (); pr_com ft s2)
+ Some s2 -> Format.pp_force_newline ft (); pr_com ft s2
| None -> ()
type tag_handler = Tag.t -> Format.tag
@@ -298,34 +270,24 @@ let pp_dirs ?pp_tag ft =
begin match tok with
| Str_def s ->
let n = utf8_length s in
- com_if ft (Lazy.from_val()); Format.pp_print_as ft n s
+ Format.pp_print_as ft n s
| Str_len (s, n) ->
- com_if ft (Lazy.from_val()); Format.pp_print_as ft n s
+ Format.pp_print_as ft n s
end
| Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *)
- com_if ft (Lazy.from_val());
pp_open_box bty ;
if not (Format.over_max_boxes ()) then Glue.iter pp_cmd ss;
Format.pp_close_box ft ()
- | Ppcmd_open_box bty -> com_if ft (Lazy.from_val()); pp_open_box bty
+ | Ppcmd_open_box bty -> pp_open_box bty
| Ppcmd_close_box -> Format.pp_close_box ft ()
| Ppcmd_close_tbox -> Format.pp_close_tbox ft ()
- | Ppcmd_white_space n ->
- com_if ft (Lazy.from_fun (fun()->Format.pp_print_break ft n 0))
- | Ppcmd_print_break(m,n) ->
- com_if ft (Lazy.from_fun(fun()->Format.pp_print_break ft m n))
+ | Ppcmd_white_space n -> Format.pp_print_break ft n 0
+ | Ppcmd_print_break(m,n) -> Format.pp_print_break ft m n
| Ppcmd_set_tab -> Format.pp_set_tab ft ()
- | Ppcmd_print_tbreak(m,n) ->
- com_if ft (Lazy.from_fun(fun()->Format.pp_print_tbreak ft m n))
- | Ppcmd_force_newline ->
- 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
-(* Format.pp_open_hvbox ft 0;*)
- List.iter (pr_com ft) coms(*;
- Format.pp_close_box ft ()*)
+ | Ppcmd_print_tbreak(m,n) -> Format.pp_print_tbreak ft m n
+ | Ppcmd_force_newline -> Format.pp_force_newline ft ()
+ | Ppcmd_print_if_broken -> Format.pp_print_if_newline ft ()
+ | Ppcmd_comment coms -> List.iter (pr_com ft) coms
| Ppcmd_open_tag tag ->
begin match pp_tag with
| None -> ()
@@ -339,13 +301,12 @@ let pp_dirs ?pp_tag ft =
in
let pp_dir = function
| Ppdir_ppcmds cmdstream -> Glue.iter pp_cmd cmdstream
- | Ppdir_print_newline ->
- com_brk ft; Format.pp_print_newline ft ()
+ | Ppdir_print_newline -> Format.pp_print_newline ft ()
| Ppdir_print_flush -> Format.pp_print_flush ft ()
in
fun (dirstream : _ ppdirs) ->
try
- Glue.iter pp_dir dirstream; com_brk ft
+ Glue.iter pp_dir dirstream
with reraise ->
let reraise = Backtrace.add_backtrace reraise in
let () = Format.pp_print_flush ft () in
@@ -356,8 +317,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 +326,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/profile.ml b/lib/profile.ml
index 0910db3fe2..d620fe69c4 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -146,9 +146,9 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
number of allocated bytes may exceed the maximum integer capacity
(2^31 on 32-bits architectures); therefore, allocation is measured
by small steps, total allocations are computed by adding elementary
- measures and carries are controled from step to step *)
+ measures and carries are controlled from step to step *)
-(* Unix measure of time is approximative and shoitt delays are often
+(* Unix measure of time is approximate and short delays are often
unperceivable; therefore, total times are measured in one (big)
step to avoid rounding errors and to get the best possible
approximation.
@@ -358,7 +358,7 @@ let declare_profile name =
prof_table := (name,e)::!prof_table;
e
-(* Default initialisation, may be overriden *)
+(* Default initialization, may be overridden *)
let _ = init_profile ()
(******************************)
diff --git a/lib/richpp.ml b/lib/richpp.ml
index a98273edb2..d1c6d158e4 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -55,7 +55,7 @@ let rich_pp annotate ppcmds =
string_of_int index
in
- let pp_buffer = Buffer.create 13 in
+ let pp_buffer = Buffer.create 180 in
let push_pcdata () =
(** Push the optional PCData on the above node *)
@@ -113,6 +113,13 @@ let rich_pp annotate ppcmds =
pp_set_formatter_tag_functions ft tag_functions;
pp_set_mark_tags ft true;
+ (* Set formatter width. This is currently a hack and duplicate code
+ with Pp_control. Hopefully it will be fixed better in Coq 8.7 *)
+ let w = pp_get_margin str_formatter () in
+ let m = max (64 * w / 100) (w-30) in
+ pp_set_margin ft w;
+ pp_set_max_indent ft m;
+
(** The whole output must be a valid document. To that
end, we nest the document inside <pp> tags. *)
pp_open_tag ft "pp";
diff --git a/lib/stateid.ml b/lib/stateid.ml
index 500581a39e..ae25735c5f 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -22,7 +22,7 @@ let to_int id = id
let newer_than id1 id2 = id1 > id2
let state_id_info : (t * t) Exninfo.t = Exninfo.make ()
-let add exn ?(valid = initial) id =
+let add exn ~valid id =
Exninfo.add exn state_id_info (valid, id)
let get exn = Exninfo.get exn state_id_info
diff --git a/lib/stateid.mli b/lib/stateid.mli
index cd8fddf0ce..1d87a343b3 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -26,9 +26,8 @@ val newer_than : t -> t -> bool
(* Attaches to an exception the concerned state id, plus an optional
* state id that is a valid state id before the error.
- * Backtracking to the valid id is safe.
- * The initial_state_id is assumed to be safe. *)
-val add : Exninfo.info -> ?valid:t -> t -> Exninfo.info
+ * Backtracking to the valid id is safe. *)
+val add : Exninfo.info -> valid:t -> t -> Exninfo.info
val get : Exninfo.info -> (t * t) option
type ('a,'b) request = {
diff --git a/lib/system.ml b/lib/system.ml
index af9aa5c074..1817aed1fc 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -33,7 +33,6 @@ let all_subdirs ~unix_path:root =
| _ -> ()
in process_directory f path
in
- check_unix_dir (fun s -> Feedback.msg_warning (str s)) root;
if exists_dir root then traverse root []
else warn_cannot_open_dir root;
List.rev !l
@@ -310,6 +309,7 @@ let with_time time f x =
raise e
let process_id () =
- if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
- else Printf.sprintf "master:%d" (Thread.id (Thread.self ()))
-
+ Printf.sprintf "%d:%s:%d" (Unix.getpid ())
+ (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
+ else "master")
+ (Thread.id (Thread.self ()))
diff --git a/lib/system.mli b/lib/system.mli
index 4dbb3695d2..214369095c 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -20,11 +20,6 @@ val (//) : unix_path -> string -> unix_path
val exists_dir : unix_path -> bool
-(** [check_unix_dir warn path] calls [warn] with an appropriate
- message if [path] looks does not look like a Unix path on Windows *)
-
-val check_unix_dir : (string -> unit) -> unix_path -> unit
-
(** [exclude_search_in_dirname path] excludes [path] when processing
directories *)
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 21:22:25 +0000