diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 8 | ||||
| -rw-r--r-- | library/goptions.ml | 15 | ||||
| -rw-r--r-- | library/libobject.ml | 2 | ||||
| -rw-r--r-- | library/library.ml | 12 | ||||
| -rw-r--r-- | library/loadpath.ml | 2 | ||||
| -rw-r--r-- | library/nametab.ml | 6 |
6 files changed, 23 insertions, 22 deletions
diff --git a/library/declare.ml b/library/declare.ml index c59d190a0..b0df32b8d 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -398,7 +398,7 @@ let declare_mind mie = let pr_rank i = pr_nth (i+1) let fixpoint_message indexes l = - Flags.if_verbose msg_info (match l with + Flags.if_verbose Feedback.msg_info (match l with | [] -> anomaly (Pp.str "no recursive definition") | [id] -> pr_id id ++ str " is recursively defined" ++ (match indexes with @@ -413,7 +413,7 @@ let fixpoint_message indexes l = | None -> mt ())) let cofixpoint_message l = - Flags.if_verbose msg_info (match l with + Flags.if_verbose Feedback.msg_info (match l with | [] -> anomaly (Pp.str "No corecursive definition.") | [id] -> pr_id id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ @@ -423,13 +423,13 @@ let recursive_message isfix i l = (if isfix then fixpoint_message i else cofixpoint_message) l let definition_message id = - Flags.if_verbose msg_info (pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined") let assumption_message id = (* Changing "assumed" to "declared", "assuming" referring more to the type of the object than to the name of the object (see discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) - Flags.if_verbose msg_info (pr_id id ++ str " is declared") + Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared") (** Global universe names, in a different summary *) diff --git a/library/goptions.ml b/library/goptions.ml index 5f6512e11..4aa3a2a21 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -108,7 +108,8 @@ module MakeTable = (fun c -> t := MySet.remove c !t)) let print_table table_name printer table = - pp (str table_name ++ + Feedback.msg_notice + (str table_name ++ (hov 0 (if MySet.is_empty table then str " None" ++ fnl () else MySet.fold @@ -122,7 +123,7 @@ module MakeTable = method mem x = let y = A.encode x in let answer = MySet.mem y !t in - msg_info (A.member_message y answer) + Feedback.msg_info (A.member_message y answer) method print = print_table A.title A.printer !t end @@ -271,7 +272,7 @@ let declare_option cast uncast in let warn () = if depr then - msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated") + Feedback.msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated") in let cread () = cast (read ()) in let cwrite v = warn (); write (uncast v) in @@ -346,12 +347,12 @@ let set_int_option_value_gen locality = set_option_value locality check_int_value let set_bool_option_value_gen locality key v = try set_option_value locality check_bool_value key v - with UserError (_,s) -> msg_warning s + with UserError (_,s) -> Feedback.msg_warning s let set_string_option_value_gen locality = set_option_value locality check_string_value let unset_option_value_gen locality key = try set_option_value locality check_unset_value key () - with UserError (_,s) -> msg_warning s + with UserError (_,s) -> Feedback.msg_warning s let set_int_option_value = set_int_option_value_gen None let set_bool_option_value = set_bool_option_value_gen None @@ -375,9 +376,9 @@ let print_option_value key = let s = read () in match s with | BoolValue b -> - msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) + Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) | _ -> - msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) + Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) let get_tables () = let tables = !value_tab in diff --git a/library/libobject.ml b/library/libobject.ml index c566840e4..b12d2038a 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -133,7 +133,7 @@ let apply_dyn_fun deflt f lobj = Failure "local to_apply_dyn_fun" -> if not (!relax_flag || Hashtbl.mem missing_tab tag) then begin - Pp.msg_warning + Feedback.msg_warning (Pp.str ("Cannot find library functions for an object with tag " ^ tag ^ " (a plugin may be missing)")); Hashtbl.add missing_tab tag () diff --git a/library/library.ml b/library/library.ml index 8e2402dda..192700be7 100644 --- a/library/library.ml +++ b/library/library.ml @@ -287,7 +287,7 @@ let locate_absolute_library dir = | [] -> raise LibNotFound | [file] -> file | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ + Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ str vo ++ str " because it is more recent"); vi | [vo;vi] -> vo @@ -311,7 +311,7 @@ let locate_qualified_library ?root ?(warn = true) qid = | [lpath, file] -> lpath, file | [lpath_vo, vo; lpath_vi, vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ + Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ str vo ++ str " because it is more recent"); lpath_vi, vi | [lpath_vo, vo; _ ] -> lpath_vo, vo @@ -370,7 +370,7 @@ let access_table what tables dp i = | Fetched t -> t | ToFetch f -> let dir_path = Names.DirPath.to_string dp in - Flags.if_verbose msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); + Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); let t = try fetch_delayed f with Faulty f -> @@ -448,7 +448,7 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) let rec intern_library (needed, contents) (dir, f) from = - Pp.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); + Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* Look if in the current logical environment *) try (find_library dir).libsum_digests, (needed, contents) with Not_found -> @@ -463,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from = (str "The file " ++ str f ++ str " contains library" ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); - Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f)); + Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); m.library_digests, intern_library_deps (needed, contents) dir m (Some f) and intern_library_deps libs dir m from = @@ -755,7 +755,7 @@ let save_library_to ?todo dir f otab = error "Could not compile the library to native code." with reraise -> let reraise = Errors.push reraise in - let () = msg_warning (str "Removed file " ++ str f') in + let () = Feedback.msg_warning (str "Removed file " ++ str f') in let () = close_out ch in let () = Sys.remove f' in iraise reraise diff --git a/library/loadpath.ml b/library/loadpath.ml index f8169576d..33c0f41e1 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -72,7 +72,7 @@ let add_load_path phys_path coq_path ~implicit = let () = (* Do not warn when overriding the default "-I ." path *) if not (DirPath.equal old_path Nameops.default_root_prefix) then - msg_warning + Feedback.msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath old_path ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path) in diff --git a/library/nametab.ml b/library/nametab.ml index bbae98fc0..db902d625 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -119,7 +119,7 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - msg_warning (str ("Trying to mask the absolute name \"" + Feedback.msg_warning (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")); tree.path | Nothing @@ -155,7 +155,7 @@ let rec push_exactly uname o level tree = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - msg_warning (str ("Trying to mask the absolute name \"" + Feedback.msg_warning (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")); tree.path | Nothing @@ -525,7 +525,7 @@ let shortest_qualid_of_tactic kn = let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) with Not_found as e -> - if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e + if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e let global_inductive r = match global r with |