aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/aux_file.ml3
-rw-r--r--lib/cErrors.ml (renamed from lib/errors.ml)16
-rw-r--r--lib/cErrors.mli (renamed from lib/errors.mli)0
-rw-r--r--lib/cList.ml49
-rw-r--r--lib/cList.mli4
-rw-r--r--lib/cMap.ml6
-rw-r--r--lib/cMap.mli3
-rw-r--r--lib/cWarnings.ml188
-rw-r--r--lib/cWarnings.mli21
-rw-r--r--lib/feedback.ml153
-rw-r--r--lib/feedback.mli33
-rw-r--r--lib/flags.ml34
-rw-r--r--lib/flags.mli4
-rw-r--r--lib/future.ml18
-rw-r--r--lib/genarg.ml6
-rw-r--r--lib/hMap.ml101
-rw-r--r--lib/lib.mllib3
-rw-r--r--lib/minisys.ml8
-rw-r--r--lib/monad.ml11
-rw-r--r--lib/monad.mli3
-rw-r--r--lib/pp.ml92
-rw-r--r--lib/pp.mli11
-rw-r--r--lib/ppstyle.ml68
-rw-r--r--lib/ppstyle.mli9
-rw-r--r--lib/profile.ml2
-rw-r--r--lib/remoteCounter.ml4
-rw-r--r--lib/spawn.ml4
-rw-r--r--lib/stateid.ml2
-rw-r--r--lib/stateid.mli5
-rw-r--r--lib/system.ml60
-rw-r--r--lib/system.mli5
-rw-r--r--lib/unicode.ml8
-rw-r--r--lib/unicode.mli12
33 files changed, 619 insertions, 327 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index 096305b987..c6c7b42429 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -87,8 +87,7 @@ let load_aux_file_for vfile =
| End_of_file -> !h
| Sys_error s | Scanf.Scan_failure s
| Failure s | Invalid_argument s ->
- Flags.if_verbose
- Feedback.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s);
+ Flags.if_verbose Feedback.msg_info Pp.(str"Loading file "++str aux_fname++str": "++str s);
empty_aux_file
let set h loc k v = set h (Loc.unloc loc) k v
diff --git a/lib/errors.ml b/lib/cErrors.ml
index 1459141d1e..5c56192fc5 100644
--- a/lib/errors.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/errors.mli b/lib/cErrors.mli
index e5dad93fd0..e5dad93fd0 100644
--- a/lib/errors.mli
+++ b/lib/cErrors.mli
diff --git a/lib/cList.ml b/lib/cList.ml
index 3a792d4168..c8283e3c71 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -65,6 +65,7 @@ sig
val except : 'a eq -> 'a -> 'a list -> 'a list
val remove : 'a eq -> 'a -> 'a list -> 'a list
val remove_first : ('a -> bool) -> 'a list -> 'a list
+ val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val sep_last : 'a list -> 'a * 'a list
@@ -461,6 +462,14 @@ let rec remove_first p = function
| b::l -> b::remove_first p l
| [] -> raise Not_found
+let extract_first p li =
+ let rec loop rev_left = function
+ | [] -> raise Not_found
+ | x::right ->
+ if p x then List.rev_append rev_left right, x
+ else loop (x :: rev_left) right
+ in loop [] li
+
let insert p v l =
let rec insrec = function
| [] -> [v]
@@ -592,19 +601,35 @@ let filter2 f l1 l2 =
filter2_loop f c1 c2 l1 l2;
(c1.tail, c2.tail)
-let rec map_filter f = function
- | [] -> []
- | x::l ->
- let l' = map_filter f l in
- match f x with None -> l' | Some y -> y::l'
+let rec map_filter_loop f p = function
+ | [] -> ()
+ | x :: l ->
+ match f x with
+ | None -> map_filter_loop f p l
+ | Some y ->
+ let c = { head = y; tail = [] } in
+ p.tail <- cast c;
+ map_filter_loop f c l
+
+let map_filter f l =
+ let c = { head = Obj.magic 0; tail = [] } in
+ map_filter_loop f c l;
+ c.tail
-let map_filter_i f =
- let rec aux i = function
- | [] -> []
- | x::l ->
- let l' = aux (succ i) l in
- match f i x with None -> l' | Some y -> y::l'
- in aux 0
+let rec map_filter_i_loop f i p = function
+ | [] -> ()
+ | x :: l ->
+ match f i x with
+ | None -> map_filter_i_loop f (succ i) p l
+ | Some y ->
+ let c = { head = y; tail = [] } in
+ p.tail <- cast c;
+ map_filter_i_loop f (succ i) c l
+
+let map_filter_i f l =
+ let c = { head = Obj.magic 0; tail = [] } in
+ map_filter_i_loop f 0 c l;
+ c.tail
let rec filter_with filter l = match filter, l with
| [], [] -> []
diff --git a/lib/cList.mli b/lib/cList.mli
index b19d1a80fc..bc8749b4f8 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -125,6 +125,10 @@ sig
val remove_first : ('a -> bool) -> 'a list -> 'a list
(** Remove the first element satisfying a predicate, or raise [Not_found] *)
+ val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
+ (** Remove and return the first element satisfying a predicate,
+ or raise [Not_found] *)
+
val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
(** Insert at the (first) position so that if the list is ordered wrt to the
total order given as argument, the order is preserved *)
diff --git a/lib/cMap.ml b/lib/cMap.ml
index 4b058380c6..ba0873ffa7 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -34,6 +34,7 @@ sig
val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val smartmap : ('a -> 'a) -> 'a t -> 'a t
val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
+ val height : 'a t -> int
module Unsafe :
sig
val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
@@ -57,6 +58,7 @@ sig
val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
val smartmap : ('a -> 'a) -> 'a map -> 'a map
val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map
+ val height : 'a map -> int
module Unsafe :
sig
val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map
@@ -168,6 +170,10 @@ struct
if l == l' && r == r' && v == v' then s
else map_inj (MNode (l', k, v', r', h))
+ let height s = match map_prj s with
+ | MEmpty -> 0
+ | MNode (_, _, _, _, h) -> h
+
module Unsafe =
struct
diff --git a/lib/cMap.mli b/lib/cMap.mli
index 3ef7fa2c8a..2838b374ec 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -61,6 +61,9 @@ sig
val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
(** As [mapi] but tries to preserve sharing. *)
+ val height : 'a t -> int
+ (** An indication of the logarithmic size of a map *)
+
module Unsafe :
sig
val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
new file mode 100644
index 0000000000..cc2463e224
--- /dev/null
+++ b/lib/cWarnings.ml
@@ -0,0 +1,188 @@
+(************************************************************************)
+(* 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 Pp
+
+type status =
+ Disabled | Enabled | AsError
+
+type t = {
+ default : status;
+ category : string;
+ status : status;
+}
+
+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 ""
+
+let set_current_loc = (:=) current_loc
+
+let get_flags () = !flags
+
+let add_warning_in_category ~name ~category =
+ let ws =
+ try
+ Hashtbl.find categories category
+ with Not_found -> []
+ 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;
+ if default <> Disabled then
+ add_warning_in_category ~name ~category:"default";
+ fun ?loc x -> let w = Hashtbl.find warnings name in
+ match w.status with
+ | Disabled -> ()
+ | AsError ->
+ 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 = refine_loc loc in
+ Feedback.msg_warning ?loc msg
+
+let warn_unknown_warning =
+ create ~name:"unknown-warning" ~category:"toplevel"
+ (fun name -> strbrk "Unknown warning name: " ++ str name)
+
+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 -> ()
+
+let reset_default_warnings () =
+ Hashtbl.iter (fun name w ->
+ Hashtbl.replace warnings name { w with status = w.default })
+ warnings
+
+let set_all_warnings_status status =
+ Hashtbl.iter (fun name w ->
+ 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
+ | '+' -> (AsError, String.sub s 1 (String.length s - 1))
+ | '-' -> (Disabled, String.sub s 1 (String.length s - 1))
+ | _ -> (Enabled, s)
+ else CErrors.error "Invalid warnings flag"
+
+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 =
+ CList.iter (fun (status, name) -> set_status ~name status) items
+
+(* For compatibility, we accept "none" *)
+let parse_flags s =
+ if is_none_keyword s then begin
+ Flags.make_warn false;
+ set_all_warnings_status Disabled;
+ "none"
+ end
+ else begin
+ Flags.make_warn true;
+ 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 =
+ reset_default_warnings (); let s = parse_flags s in flags := s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
new file mode 100644
index 0000000000..3f6cee31b7
--- /dev/null
+++ b/lib/cWarnings.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+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 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 d6f580fd16..44b3ee35d7 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -9,7 +9,7 @@
open Xml_datatype
type level =
- | Debug of string
+ | Debug
| Info
| Notice
| Warning
@@ -24,7 +24,6 @@ type feedback_content =
| Processed
| Incomplete
| Complete
- | ErrorMsg of Loc.t * string
| ProcessingIn of string
| InProgress of int
| WorkerStatus of string * string
@@ -36,8 +35,8 @@ type feedback_content =
| FileLoaded of string * string
(* Extra metadata *)
| Custom of Loc.t * string * xml
- (* Old generic messages *)
- | Message of level * Richpp.richpp
+ (* Generic messages *)
+ | Message of level * Loc.t option * Richpp.richpp
type feedback = {
id : edit_or_state_id;
@@ -51,10 +50,9 @@ let default_route = 0
open Pp
open Pp_control
-type logger = level -> std_ppcmds -> unit
+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
@@ -76,56 +74,118 @@ 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 s = quoter (hov 0 (info ++ s))
+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 level msg = match level with
- | Debug _ -> msgnl (make_body dbg dbg_str msg)
- | Info -> msgnl (make_body dbg info_str msg)
- | 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 msg)) ()
- | Error -> msgnl_with !err_ft (make_body err err_str 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 level strm =
- let msg = Ppstyle.color_msg in
- match level with
- | Debug _ -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
- | Info -> msg !std_ft strm
- | Notice -> msg !std_ft strm
- | Warning ->
- let header = ("Warning", Ppstyle.warning_tag) in
- Flags.if_warn (fun () -> msg ~header !err_ft strm) ()
- | Error -> msg ~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
-let msg_info x = !logger Info x
-let msg_notice x = !logger Notice x
-let msg_warning x = !logger Warning x
-let msg_error x = !logger Error x
-let msg_debug x = !logger (Debug "_") x
+let msg_info ?loc x = !logger ?loc Info x
+let msg_notice ?loc x = !logger ?loc Notice x
+let msg_warning ?loc x = !logger ?loc Warning x
+let msg_error ?loc x = !logger ?loc Error x
+let msg_debug ?loc x = !logger ?loc Debug x
(** Feeders *)
-let feeder = ref ignore
-let set_feeder f = feeder := f
+let feeders = ref []
+let add_feeder f = feeders := f :: !feeders
+
+let debug_feeder = function
+ | { contents = Message (Debug, loc, pp) } ->
+ msg_debug ?loc (Pp.str (Richpp.raw_print pp))
+ | _ -> ()
let feedback_id = ref (Edit 0)
let feedback_route = ref default_route
@@ -134,25 +194,26 @@ let set_id_for_feedback ?(route=default_route) i =
feedback_id := i; feedback_route := route
let feedback ?id ?route what =
- !feeder {
+ let m = {
contents = what;
route = Option.default !feedback_route route;
id = Option.default !feedback_id id;
- }
+ } in
+ List.iter (fun f -> f m) !feeders
-let feedback_logger lvl msg =
+let feedback_logger ?loc lvl msg =
feedback ~route:!feedback_route ~id:!feedback_id
- (Message (lvl, Richpp.richpp_of_pp msg))
+ (Message (lvl, loc, Richpp.richpp_of_pp msg))
(* Output to file *)
-let ft_logger old_logger ft level mesg =
+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)
+ | 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 level mesg
- | Error -> old_logger level mesg
+ | Warning -> old_logger ?loc level mesg
+ | Error -> old_logger ?loc level mesg
let with_output_to_file fname func input =
let old_logger = !logger in
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 50ffd22db9..5160bd5bc1 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -10,7 +10,7 @@ open Xml_datatype
(* Old plain messages (used to be in Pp) *)
type level =
- | Debug of string
+ | Debug
| Info
| Notice
| Warning
@@ -31,7 +31,6 @@ type feedback_content =
| Processed
| Incomplete
| Complete
- | ErrorMsg of Loc.t * string
(* STM optional data *)
| ProcessingIn of string
| InProgress of int
@@ -45,8 +44,8 @@ type feedback_content =
| FileLoaded of string * string
(* Extra metadata *)
| Custom of Loc.t * string * xml
- (* Old generic messages *)
- | Message of level * Richpp.richpp
+ (* Generic messages *)
+ | Message of level * Loc.t option * Richpp.richpp
type feedback = {
id : edit_or_state_id; (* The document part concerned *)
@@ -65,7 +64,7 @@ type feedback = {
* Only one among state_id and edit_id can be provided. *)
(** A [logger] takes a level plus a pretty printing doc and logs it *)
-type logger = level -> Pp.std_ppcmds -> unit
+type logger = ?loc:Loc.t -> level -> Pp.std_ppcmds -> unit
(** [set_logger l] makes the [msg_*] to use [l] for logging *)
val set_logger : logger -> unit
@@ -73,19 +72,19 @@ 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
val emacs_logger : logger
-(** [set_feeder] A feeder processes the feedback, [ignore] by default *)
-val set_feeder : (feedback -> unit) -> unit
+(** [add_feeder] feeders observe the feedback *)
+val add_feeder : (feedback -> unit) -> unit
+
+(** Prints feedback messages of kind Message(Debug,_) using msg_debug *)
+val debug_feeder : feedback -> unit
(** [feedback ?id ?route fb] produces feedback fb, with [route] and
[id] set appropiatedly, if absent, it will use the defaults set by
@@ -110,22 +109,22 @@ relaxed. *)
(* Should we advertise these functions more? Should they be the ONLY
allowed way to output something? *)
-val msg_info : Pp.std_ppcmds -> unit
+val msg_info : ?loc:Loc.t -> Pp.std_ppcmds -> unit
(** Message that displays information, usually in verbose mode, such as [Foobar
is defined] *)
-val msg_notice : Pp.std_ppcmds -> unit
+val msg_notice : ?loc:Loc.t -> Pp.std_ppcmds -> unit
(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
-val msg_warning : Pp.std_ppcmds -> unit
+val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit
(** Message indicating that something went wrong, but without serious
consequences. *)
-val msg_error : Pp.std_ppcmds -> unit
+val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit
(** Message indicating that something went really wrong, though still
recoverable; otherwise an exception would have been raised. *)
-val msg_debug : Pp.std_ppcmds -> unit
+val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit
(** For debugging purposes *)
diff --git a/lib/flags.ml b/lib/flags.ml
index ba19c7a63b..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 *)
@@ -172,7 +175,7 @@ let make_polymorphic_flag b =
let program_mode = ref false
let is_program_mode () = !program_mode
-let warn = ref false
+let warn = ref true
let make_warn flag = warn := flag; ()
let if_warn f x = if !warn then f x
@@ -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/future.ml b/lib/future.ml
index 9cdc1c20e3..ea0382a63d 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -30,10 +30,10 @@ let customize_not_here_msg f = not_here_msg := f
exception NotReady of string
exception NotHere of string
-let _ = Errors.register_handler (function
+let _ = CErrors.register_handler (function
| NotReady name -> !not_ready_msg name
| NotHere name -> !not_here_msg name
- | _ -> raise Errors.Unhandled)
+ | _ -> raise CErrors.Unhandled)
type fix_exn = Exninfo.iexn -> Exninfo.iexn
let id x = prerr_endline "Future: no fix_exn.\nYou have probably created a Future.computation from a value without passing the ~fix_exn argument. You probably want to chain with an already existing future instead."; x
@@ -136,7 +136,7 @@ let rec compute ~pure ck : 'a value =
let state = if pure then None else Some (!freeze ()) in
c := Val (data, state); `Val data
with e ->
- let e = Errors.push e in
+ let e = CErrors.push e in
let e = fix_exn e in
match e with
| (NotReady _, _) -> `Exn e
@@ -156,9 +156,9 @@ let chain ~pure ck f =
| Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v)
| Val (v, None) ->
match !ck with
- | Finished _ -> Errors.anomaly(Pp.str
+ | Finished _ -> CErrors.anomaly(Pp.str
"Future.chain ~pure:false call on an already joined computation")
- | Ongoing _ -> Errors.anomaly(Pp.strbrk(
+ | Ongoing _ -> CErrors.anomaly(Pp.strbrk(
"Future.chain ~pure:false call on a pure computation. "^
"This can happen if the computation was initial created with "^
"Future.from_val or if it was Future.chain ~pure:true with a "^
@@ -170,7 +170,7 @@ let replace kx y =
let _, _, _, x = get kx in
match !x with
| Exn _ -> x := Closure (fun () -> force ~pure:false y)
- | _ -> Errors.anomaly
+ | _ -> CErrors.anomaly
(Pp.str "A computation can be replaced only if is_exn holds")
let purify f x =
@@ -180,13 +180,13 @@ let purify f x =
!unfreeze state;
v
with e ->
- let e = Errors.push e in !unfreeze state; Exninfo.iraise e
+ let e = CErrors.push e in !unfreeze state; Exninfo.iraise e
let transactify f x =
let state = !freeze () in
try f x
with e ->
- let e = Errors.push e in !unfreeze state; Exninfo.iraise e
+ let e = CErrors.push e in !unfreeze state; Exninfo.iraise e
let purify_future f x = if is_over x then f x else purify f x
let compute x = purify_future (compute ~pure:false) x
@@ -213,7 +213,7 @@ let map2 ?greedy f x l =
let xi = chain ?greedy ~pure:true x (fun x ->
try List.nth x i
with Failure _ | Invalid_argument _ ->
- Errors.anomaly (Pp.str "Future.map2 length mismatch")) in
+ CErrors.anomaly (Pp.str "Future.map2 length mismatch")) in
f xi y) 0 l
let print f kx =
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 69408fb1a5..05c828d5f9 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -159,7 +159,7 @@ let create_arg name =
match ArgT.name name with
| None -> ExtraArg (ArgT.create name)
| Some _ ->
- Errors.anomaly (str "generic argument already declared: " ++ str name)
+ CErrors.anomaly (str "generic argument already declared: " ++ str name)
let make0 = create_arg
@@ -181,7 +181,7 @@ struct
| ExtraArg s ->
if GenMap.mem s !arg0_map then
let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) in
- Errors.anomaly msg
+ CErrors.anomaly msg
else
arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map
| _ -> assert false
@@ -192,7 +192,7 @@ struct
with Not_found ->
match M.default (ExtraArg name) with
| None ->
- Errors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name))
+ CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name))
| Some obj -> obj
(** For now, the following function is quite dummy and should only be applied
diff --git a/lib/hMap.ml b/lib/hMap.ml
index 778c366fd5..ea76e74272 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -68,34 +68,91 @@ struct
Int.Map.update h m s
with Not_found -> s
+ let height s = Int.Map.height s
+
+ let is_smaller s1 s2 = height s1 <= height s2 + 3
+
+ (** Assumes s1 << s2 *)
+ let fast_union s1 s2 =
+ let fold h s accu =
+ try Int.Map.modify h (fun _ s' -> Set.fold Set.add s s') accu
+ with Not_found -> Int.Map.add h s accu
+ in
+ Int.Map.fold fold s1 s2
+
let union s1 s2 =
- let fu _ m1 m2 = match m1, m2 with
- | None, None -> None
- | (Some _ as m), None | None, (Some _ as m) -> m
- | Some m1, Some m2 -> Some (Set.union m1 m2)
+ if is_smaller s1 s2 then fast_union s1 s2
+ else if is_smaller s2 s1 then fast_union s2 s1
+ else
+ let fu _ m1 m2 = match m1, m2 with
+ | None, None -> None
+ | (Some _ as m), None | None, (Some _ as m) -> m
+ | Some m1, Some m2 -> Some (Set.union m1 m2)
+ in
+ Int.Map.merge fu s1 s2
+
+ (** Assumes s1 << s2 *)
+ let fast_inter s1 s2 =
+ let fold h s accu =
+ try
+ let s' = Int.Map.find h s2 in
+ let si = Set.filter (fun e -> Set.mem e s') s in
+ if Set.is_empty si then accu
+ else Int.Map.add h si accu
+ with Not_found -> accu
in
- Int.Map.merge fu s1 s2
+ Int.Map.fold fold s1 Int.Map.empty
let inter s1 s2 =
- let fu _ m1 m2 = match m1, m2 with
- | None, None -> None
- | Some _, None | None, Some _ -> None
- | Some m1, Some m2 ->
- let m = Set.inter m1 m2 in
- if Set.is_empty m then None else Some m
+ if is_smaller s1 s2 then fast_inter s1 s2
+ else if is_smaller s2 s1 then fast_inter s2 s1
+ else
+ let fu _ m1 m2 = match m1, m2 with
+ | None, None -> None
+ | Some _, None | None, Some _ -> None
+ | Some m1, Some m2 ->
+ let m = Set.inter m1 m2 in
+ if Set.is_empty m then None else Some m
+ in
+ Int.Map.merge fu s1 s2
+
+ (** Assumes s1 << s2 *)
+ let fast_diff_l s1 s2 =
+ let fold h s accu =
+ try
+ let s' = Int.Map.find h s2 in
+ let si = Set.filter (fun e -> not (Set.mem e s')) s in
+ if Set.is_empty si then accu
+ else Int.Map.add h si accu
+ with Not_found -> Int.Map.add h s accu
+ in
+ Int.Map.fold fold s1 Int.Map.empty
+
+ (** Assumes s2 << s1 *)
+ let fast_diff_r s1 s2 =
+ let fold h s accu =
+ try
+ let s' = Int.Map.find h accu in
+ let si = Set.filter (fun e -> not (Set.mem e s)) s' in
+ if Set.is_empty si then Int.Map.remove h accu
+ else Int.Map.update h si accu
+ with Not_found -> accu
in
- Int.Map.merge fu s1 s2
+ Int.Map.fold fold s2 s1
let diff s1 s2 =
- let fu _ m1 m2 = match m1, m2 with
- | None, None -> None
- | (Some _ as m), None -> m
- | None, Some _ -> None
- | Some m1, Some m2 ->
- let m = Set.diff m1 m2 in
- if Set.is_empty m then None else Some m
- in
- Int.Map.merge fu s1 s2
+ if is_smaller s1 s2 then fast_diff_l s1 s2
+ else if is_smaller s2 s2 then fast_diff_r s1 s2
+ else
+ let fu _ m1 m2 = match m1, m2 with
+ | None, None -> None
+ | (Some _ as m), None -> m
+ | None, Some _ -> None
+ | Some m1, Some m2 ->
+ let m = Set.diff m1 m2 in
+ if Set.is_empty m then None else Some m
+ in
+ Int.Map.merge fu s1 s2
let compare s1 s2 = Int.Map.compare Set.compare s1 s2
@@ -324,6 +381,8 @@ struct
let fs m = Map.smartmapi f m in
Int.Map.smartmap fs s
+ let height s = Int.Map.height s
+
module Unsafe =
struct
let map f s =
diff --git a/lib/lib.mllib b/lib/lib.mllib
index a6c09058dd..8791f07417 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,4 +1,5 @@
-Errors
+CErrors
+CWarnings
Bigint
Segmenttree
Unicodetable
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 d07f01b906..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
@@ -197,6 +186,25 @@ let strbrk s =
else if p = n then [] else [str (String.sub s p (n-p))]
in List.fold_left (++) Glue.empty (aux 0 0)
+let pr_loc_pos loc =
+ if Loc.is_ghost loc then (str"<unknown>")
+ else
+ let loc = Loc.unloc loc in
+ int (fst loc) ++ str"-" ++ int (snd loc)
+
+let pr_loc loc =
+ if Loc.is_ghost loc then str"<unknown>" ++ fnl ()
+ else
+ let fname = loc.Loc.fname in
+ if CString.equal fname "" then
+ Loc.(str"Toplevel input, characters " ++ int loc.bp ++
+ str"-" ++ int loc.ep ++ str":" ++ fnl ())
+ else
+ Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
+ str", line " ++ int loc.line_nb ++ str", characters " ++
+ int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
+ str":" ++ fnl())
+
let ismt = is_empty
(* boxing commands *)
@@ -235,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
@@ -279,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 -> ()
@@ -320,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
@@ -337,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
@@ -346,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 a18744c376..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} *)
@@ -166,13 +165,15 @@ val surround : std_ppcmds -> std_ppcmds
val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+val pr_loc : Loc.t -> std_ppcmds
+
(** {6 Low-level pretty-printing functions with and without flush} *)
(** 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 b068788c92..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,36 +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 ?header ft strm =
- let pptag = tag in
- let open Pp in
- let strm = match header with
- | None -> hov 0 strm
- | Some (h, t) ->
- let tag = Pp.Tag.inj t pptag in
- let h = Pp.tag tag (str h ++ str ":") in
- hov 0 (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 1cd701ed4e..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 : ?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 2350cd43ac..0910db3fe2 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -260,7 +260,7 @@ let time_overhead_B_C () =
let _dw = dummy_spent_alloc () in
let _dt = get_time () in
()
- with e when Errors.noncritical e -> assert false
+ with e when CErrors.noncritical e -> assert false
done;
let after = get_time () in
let beforeloop = get_time () in
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index 6cc48c8745..e7646fb796 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -25,7 +25,7 @@ let new_counter ~name a ~incr ~build =
(* - in the main process there is a race condition between slave
managers (that are threads) and the main thread, hence the mutex *)
if Flags.async_proofs_is_worker () then
- Errors.anomaly(Pp.str"Slave processes must install remote counters");
+ CErrors.anomaly(Pp.str"Slave processes must install remote counters");
Mutex.lock m; let x = f () in Mutex.unlock m;
build x in
let mk_thsafe_remote_getter f () =
@@ -33,7 +33,7 @@ let new_counter ~name a ~incr ~build =
let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in
let installer f =
if not (Flags.async_proofs_is_worker ()) then
- Errors.anomaly(Pp.str"Only slave processes can install a remote counter");
+ CErrors.anomaly(Pp.str"Only slave processes can install a remote counter");
getter := mk_thsafe_remote_getter f in
(fun () -> !getter ()), installer
diff --git a/lib/spawn.ml b/lib/spawn.ml
index 2b9c4ccac1..4791769735 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -43,7 +43,7 @@ module type MainLoopModel = sig
end
(* Common code *)
-let assert_ b s = if not b then Errors.anomaly (Pp.str s)
+let assert_ b s = if not b then CErrors.anomaly (Pp.str s)
(* According to http://caml.inria.fr/mantis/view.php?id=5325
* you can't use the same socket for both writing and reading (may change
@@ -192,7 +192,7 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
let live = callback cl ~read_all:(fun () -> ML.read_all gchan) in
if not live then kill p;
live
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
pr_err ("Async reader raised: " ^ (Printexc.to_string e));
kill p;
false) gchan
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 8b53a11d67..4b99de707b 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -9,7 +9,6 @@
(* $Id$ *)
open Pp
-open Errors
open Util
include Minisys
@@ -18,6 +17,10 @@ include Minisys
depth-first search, with sons ordered as on the file system;
warns if [root] does not exist *)
+let warn_cannot_open_dir =
+ CWarnings.create ~name:"cannot-open-dir" ~category:"filesystem"
+ (fun dir -> str ("Cannot open directory " ^ dir))
+
let all_subdirs ~unix_path:root =
let l = ref [] in
let add f rel = l := (f, rel) :: !l in
@@ -30,9 +33,8 @@ 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 Feedback.msg_warning (str ("Cannot open " ^ root));
+ else warn_cannot_open_dir root;
List.rev !l
(* Caching directory contents for efficient syntactic equality of file
@@ -85,19 +87,22 @@ let rec search paths test =
| [] -> []
| lpe :: rem -> test lpe @ search rem test
+let warn_ambiguous_file_name =
+ CWarnings.create ~name:"ambiguous-file-name" ~category:"filesystem"
+ (fun (filename,l,f) -> str filename ++ str " has been found in" ++ spc () ++
+ hov 0 (str "[ " ++
+ hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
+ (fun (lpe,_) -> str lpe) l)
+ ++ str " ];") ++ fnl () ++
+ str "loading " ++ str f)
+
+
let where_in_path ?(warn=true) path filename =
let check_and_warn l = match l with
| [] -> raise Not_found
| (lpe, f) :: l' ->
let () = match l' with
- | _ :: _ when warn ->
- Feedback.msg_warning
- (str filename ++ str " has been found in" ++ spc () ++
- hov 0 (str "[ " ++
- hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
- (fun (lpe,_) -> str lpe) l)
- ++ str " ];") ++ fnl () ++
- str "loading " ++ str f)
+ | _ :: _ when warn -> warn_ambiguous_file_name (filename,l,f)
| _ -> ()
in
(lpe, f)
@@ -126,7 +131,7 @@ let find_file_in_path ?(warn=true) paths filename =
let root = Filename.dirname filename in
root, filename
else
- errorlabstrm "System.find_file_in_path"
+ CErrors.errorlabstrm "System.find_file_in_path"
(hov 0 (str "Can't find file" ++ spc () ++ str filename))
else
(* the name is considered to be the transcription as a relative
@@ -134,7 +139,7 @@ let find_file_in_path ?(warn=true) paths filename =
to be locate respecting case *)
try where_in_path ~warn paths filename
with Not_found ->
- errorlabstrm "System.find_file_in_path"
+ CErrors.errorlabstrm "System.find_file_in_path"
(hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
str "on loadpath"))
@@ -142,27 +147,34 @@ let is_in_path lpath filename =
try ignore (where_in_path ~warn:false lpath filename); true
with Not_found -> false
+let warn_path_not_found =
+ CWarnings.create ~name:"path-not-found" ~category:"filesystem"
+ (fun () -> str "system variable PATH not found")
+
let is_in_system_path filename =
try
let lpath = CUnix.path_to_list (Sys.getenv "PATH") in
is_in_path lpath filename
with Not_found ->
- Feedback.msg_warning (str "system variable PATH not found");
+ warn_path_not_found ();
false
let open_trapping_failure name =
try open_out_bin name
- with e when Errors.noncritical e ->
- errorlabstrm "System.open" (str "Can't open " ++ str name)
+ with e when CErrors.noncritical e ->
+ CErrors.errorlabstrm "System.open" (str "Can't open " ++ str name)
+
+let warn_cannot_remove_file =
+ CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem"
+ (fun filename -> str"Could not remove file " ++ str filename ++ str" which is corrupted!")
let try_remove filename =
try Sys.remove filename
- with e when Errors.noncritical e ->
- Feedback.msg_warning
- (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
+ with e when CErrors.noncritical e ->
+ warn_cannot_remove_file filename
let error_corrupted file s =
- errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
+ CErrors.errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
let input_binary_int f ch =
try input_binary_int ch
@@ -235,11 +247,11 @@ let extern_state magic filename val_0 =
marshal_out channel val_0;
close_out channel
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
let () = try_remove filename in
iraise reraise
with Sys_error s ->
- errorlabstrm "System.extern_state" (str "System error: " ++ str s)
+ CErrors.errorlabstrm "System.extern_state" (str "System error: " ++ str s)
let intern_state magic filename =
try
@@ -248,12 +260,12 @@ let intern_state magic filename =
close_in channel;
v
with Sys_error s ->
- errorlabstrm "System.intern_state" (str "System error: " ++ str s)
+ CErrors.errorlabstrm "System.intern_state" (str "System error: " ++ str s)
let with_magic_number_check f a =
try f a
with Bad_magic_number {filename=fname;actual=actual;expected=expected} ->
- errorlabstrm "with_magic_number_check"
+ CErrors.errorlabstrm "with_magic_number_check"
(str"File " ++ str fname ++ strbrk" has bad magic number " ++
int actual ++ str" (expected " ++ int expected ++ str")." ++
spc () ++
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-01 05:37:38 +0000