diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cErrors.ml | 7 | ||||
| -rw-r--r-- | lib/cErrors.mli | 11 | ||||
| -rw-r--r-- | lib/cSig.mli | 2 | ||||
| -rw-r--r-- | lib/dyn.ml | 43 | ||||
| -rw-r--r-- | lib/dyn.mli | 42 | ||||
| -rw-r--r-- | lib/exninfo.ml | 2 | ||||
| -rw-r--r-- | lib/feedback.ml | 38 | ||||
| -rw-r--r-- | lib/feedback.mli | 8 | ||||
| -rw-r--r-- | lib/flags.ml | 4 | ||||
| -rw-r--r-- | lib/flags.mli | 8 | ||||
| -rw-r--r-- | lib/genarg.ml | 2 | ||||
| -rw-r--r-- | lib/loc.ml | 6 | ||||
| -rw-r--r-- | lib/loc.mli | 11 | ||||
| -rw-r--r-- | lib/spawn.ml | 4 | ||||
| -rw-r--r-- | lib/spawn.mli | 4 | ||||
| -rw-r--r-- | lib/store.ml | 6 | ||||
| -rw-r--r-- | lib/store.mli | 7 |
17 files changed, 99 insertions, 106 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 3f4e8aa12f..eaffc28aca 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -91,7 +91,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with let print_anomaly askreport e = if askreport then - hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e) ++ spc ()) ++ + hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e)) ++ spc () ++ hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".") else hov 0 (raw_anomaly e) @@ -137,8 +137,3 @@ let handled e = let bottom _ = raise Bottom in try let _ = print_gen bottom !handle_stack e in true with Bottom -> false - -(* Deprecated functions *) -let error string = user_err (str string) -let user_err_loc (loc,hdr,msg) = user_err ~loc ~hdr msg -let errorlabstrm hdr msg = user_err ~hdr msg diff --git a/lib/cErrors.mli b/lib/cErrors.mli index f3253979f2..6fcc97a918 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -93,14 +93,3 @@ val noncritical : exn -> bool (** Check whether an exception is handled by some toplevel printer. The [Anomaly] exception is never handled. *) val handled : exn -> bool - -(** Deprecated functions *) -val error : string -> 'a - [@@ocaml.deprecated "use [user_err] instead"] - -val errorlabstrm : string -> Pp.t -> 'a - [@@ocaml.deprecated "use [user_err ~hdr] instead"] - -val user_err_loc : Loc.t * string * Pp.t -> 'a - [@@ocaml.deprecated "use [user_err ~loc] instead"] - diff --git a/lib/cSig.mli b/lib/cSig.mli index 151cfbdca5..6910cbbf03 100644 --- a/lib/cSig.mli +++ b/lib/cSig.mli @@ -48,8 +48,6 @@ end (** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml documentation for more information. *) -module type EmptyS = sig end - module type MapS = sig type key diff --git a/lib/dyn.ml b/lib/dyn.ml index 6bd43455f6..83e673d2c0 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -11,6 +11,26 @@ sig type 'a t end +module type MapS = +sig + type t + type 'a obj + type 'a key + val empty : t + val add : 'a key -> 'a obj -> t -> t + val remove : 'a key -> t -> t + val find : 'a key -> t -> 'a obj + val mem : 'a key -> t -> bool + + type any = Any : 'a key * 'a obj -> any + + type map = { map : 'a. 'a key -> 'a obj -> 'a obj } + val map : map -> t -> t + + val iter : (any -> unit) -> t -> unit + val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r +end + module type PreS = sig type 'a tag @@ -24,24 +44,7 @@ type any = Any : 'a tag -> any val name : string -> any option -module Map(M : TParam) : -sig - type t - val empty : t - val add : 'a tag -> 'a M.t -> t -> t - val remove : 'a tag -> t -> t - val find : 'a tag -> t -> 'a M.t - val mem : 'a tag -> t -> bool - - type any = Any : 'a tag * 'a M.t -> any - - type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } - val map : map -> t -> t - - val iter : (any -> unit) -> t -> unit - val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r - -end +module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag val dump : unit -> (int * string) list @@ -59,7 +62,7 @@ sig end -module Make(M : CSig.EmptyS) = struct +module Make () = struct module Self : PreS = struct (* Dynamics, programmed with DANGER !!! *) @@ -104,6 +107,8 @@ let dump () = Int.Map.bindings !dyntab module Map(M : TParam) = struct type t = Obj.t M.t Int.Map.t +type 'a obj = 'a M.t +type 'a key = 'a tag let cast : 'a M.t -> 'b M.t = Obj.magic let empty = Int.Map.empty let add tag v m = Int.Map.add tag (cast v) m diff --git a/lib/dyn.mli b/lib/dyn.mli index e43c8a9bcf..e0e1a9d140 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -13,6 +13,26 @@ sig type 'a t end +module type MapS = +sig + type t + type 'a obj + type 'a key + val empty : t + val add : 'a key -> 'a obj -> t -> t + val remove : 'a key -> t -> t + val find : 'a key -> t -> 'a obj + val mem : 'a key -> t -> bool + + type any = Any : 'a key * 'a obj -> any + + type map = { map : 'a. 'a key -> 'a obj -> 'a obj } + val map : map -> t -> t + + val iter : (any -> unit) -> t -> unit + val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r +end + module type S = sig type 'a tag @@ -26,24 +46,7 @@ type any = Any : 'a tag -> any val name : string -> any option -module Map(M : TParam) : -sig - type t - val empty : t - val add : 'a tag -> 'a M.t -> t -> t - val remove : 'a tag -> t -> t - val find : 'a tag -> t -> 'a M.t - val mem : 'a tag -> t -> bool - - type any = Any : 'a tag * 'a M.t -> any - - type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } - val map : map -> t -> t - - val iter : (any -> unit) -> t -> unit - val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r - -end +module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag val dump : unit -> (int * string) list @@ -59,5 +62,4 @@ end end -(** FIXME: use OCaml 4.02 generative functors when available *) -module Make(M : CSig.EmptyS) : S +module Make () : S diff --git a/lib/exninfo.ml b/lib/exninfo.ml index d049dc6cff..167d3d6dc8 100644 --- a/lib/exninfo.ml +++ b/lib/exninfo.ml @@ -10,7 +10,7 @@ containing a pair composed of the distinguishing [token] and the backtrace information. We discriminate the token by pointer equality. *) -module Store = Store.Make(struct end) +module Store = Store.Make () type 'a t = 'a Store.field diff --git a/lib/feedback.ml b/lib/feedback.ml index 7a126363cc..1007582e08 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -63,6 +63,7 @@ let set_id_for_feedback ?(route=default_route) d i = span_id := i; feedback_route := route +let warn_no_listeners = ref true let feedback ?did ?id ?route what = let m = { contents = what; @@ -70,6 +71,8 @@ let feedback ?did ?id ?route what = doc_id = Option.default !doc_id did; span_id = Option.default !span_id id; } in + if !warn_no_listeners && Hashtbl.length feeders = 0 then + Format.eprintf "Warning, feedback message received but no listener to handle it!@\n%!"; Hashtbl.iter (fun _ f -> f m) feeders (* Logging messages *) @@ -81,3 +84,38 @@ let msg_notice ?loc x = feedback_logger ?loc Notice x let msg_warning ?loc x = feedback_logger ?loc Warning x let msg_error ?loc x = feedback_logger ?loc Error x let msg_debug ?loc x = feedback_logger ?loc Debug x + +(* Helper for tools willing to understand only the messages *) +let console_feedback_listener fmt = + let open Format in + let pp_lvl fmt lvl = match lvl with + | Error -> fprintf fmt "Error: " + | Info -> fprintf fmt "Info: " + | Debug -> fprintf fmt "Debug: " + | Warning -> fprintf fmt "Warning: " + | Notice -> fprintf fmt "" + in + let pp_loc fmt loc = let open Loc in match loc with + | None -> fprintf fmt "" + | Some loc -> + let where = + match loc.fname with InFile f -> f | ToplevelInput -> "Toplevel input" in + fprintf fmt "\"%s\", line %d, characters %d-%d:@\n" + where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in + let checker_feed (fb : feedback) = + match fb.contents with + | Processed -> () + | Incomplete -> () + | Complete -> () + | ProcessingIn _ -> () + | InProgress _ -> () + | WorkerStatus (_,_) -> () + | AddedAxiom -> () + | GlobRef (_,_,_,_,_) -> () + | GlobDef (_,_,_,_) -> () + | FileDependency (_,_) -> () + | FileLoaded (_,_) -> () + | Custom (_,_,_) -> () + | Message (lvl,loc,msg) -> + fprintf fmt "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg + in checker_feed diff --git a/lib/feedback.mli b/lib/feedback.mli index 73b84614f1..62b909516f 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -99,3 +99,11 @@ val msg_error : ?loc:Loc.t -> Pp.t -> unit val msg_debug : ?loc:Loc.t -> Pp.t -> unit (** For debugging purposes *) + +val console_feedback_listener : Format.formatter -> feedback -> unit +(** Helper for tools willing to print to the feedback system *) + +val warn_no_listeners : bool ref +(** The library will print a warning to the console if no listener is + available by default; ML-clients willing to use Coq without a + feedback handler should set this to false. *) diff --git a/lib/flags.ml b/lib/flags.ml index a53a866aba..323b5492dd 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -140,10 +140,6 @@ let verbosely f x = without_option quiet f x let if_silent f x = if !quiet then f x let if_verbose f x = if not !quiet then f x -let make_silent flag = quiet := flag -let is_silent () = !quiet -let is_verbose () = not !quiet - let auto_intros = ref true let make_auto_intros flag = auto_intros := flag let is_auto_intros () = !auto_intros diff --git a/lib/flags.mli b/lib/flags.mli index 5233e72a25..0ff3e0a81d 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -87,14 +87,6 @@ val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit -(* Deprecated *) -val make_silent : bool -> unit -[@@ocaml.deprecated "Please use Flags.quiet"] -val is_silent : unit -> bool -[@@ocaml.deprecated "Please use Flags.quiet"] -val is_verbose : unit -> bool -[@@ocaml.deprecated "Please use Flags.quiet"] - (* Miscellaneus flags for vernac *) val make_auto_intros : bool -> unit val is_auto_intros : unit -> bool diff --git a/lib/genarg.ml b/lib/genarg.ml index b78fe40373..a3bfb405c8 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -11,7 +11,7 @@ open Util module ArgT = struct - module DYN = Dyn.Make(struct end) + module DYN = Dyn.Make () module Map = DYN.Map type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag type any = Any : ('a, 'b, 'c) tag -> any diff --git a/lib/loc.ml b/lib/loc.ml index 4a935a9d9c..2cf4d3960b 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -84,9 +84,3 @@ let raise ?loc e = let info = Exninfo.add Exninfo.null location loc in Exninfo.iraise (e, info) -(** Deprecated *) -let located_fold_left f x (_,a) = f x a -let located_iter2 f (_,a) (_,b) = f a b -let down_located f (_,a) = f a - - diff --git a/lib/loc.mli b/lib/loc.mli index fde490cc8a..800940f219 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -65,14 +65,3 @@ val tag : ?loc:t -> 'a -> 'a located val map : ('a -> 'b) -> 'a located -> 'b located (** Modify an object carrying a location *) - -(** Deprecated functions *) -val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a - [@@ocaml.deprecated "use pattern matching"] - -val down_located : ('a -> 'b) -> 'a located -> 'b - [@@ocaml.deprecated "use pattern matching"] - -val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit - [@@ocaml.deprecated "use pattern matching"] - diff --git a/lib/spawn.ml b/lib/spawn.ml index 0cf163e737..de31d87d0e 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -28,8 +28,6 @@ module type Control = sig end -module type Empty = sig end - module type MainLoopModel = sig type async_chan type condition @@ -216,7 +214,7 @@ let rec wait p = end -module Sync(T : Empty) = struct +module Sync () = struct type process = { cin : in_channel; diff --git a/lib/spawn.mli b/lib/spawn.mli index a131715e9d..fd2b92ae3e 100644 --- a/lib/spawn.mli +++ b/lib/spawn.mli @@ -34,8 +34,6 @@ module type Control = sig end (* Abstraction to work with both threads and main loop models *) -module type Empty = sig end - module type MainLoopModel = sig type async_chan type condition @@ -64,7 +62,7 @@ module Async(ML : MainLoopModel) : sig end (* spawn a process and read its output synchronously *) -module Sync(T : Empty) : sig +module Sync () : sig type process val spawn : diff --git a/lib/store.ml b/lib/store.ml index a1788f7da9..97a8fea085 100644 --- a/lib/store.ml +++ b/lib/store.ml @@ -14,10 +14,6 @@ stores, we might want something static to avoid troubles with plugins order. *) -module type T = -sig -end - module type S = sig type t @@ -30,7 +26,7 @@ sig val field : unit -> 'a field end -module Make (M : T) : S = +module Make () : S = struct let next = diff --git a/lib/store.mli b/lib/store.mli index 8eab314ed7..5cc5bb8593 100644 --- a/lib/store.mli +++ b/lib/store.mli @@ -9,11 +9,6 @@ (*** This module implements an "untyped store", in this particular case we see it as an extensible record whose fields are left unspecified. ***) -module type T = -sig -(** FIXME: Waiting for first-class modules... *) -end - module type S = sig type t @@ -42,5 +37,5 @@ sig end -module Make (M : T) : S +module Make () : S (** Create a new store type. *) |