summaryrefslogtreecommitdiff
path: root/library/goptions.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/goptions.ml')
-rw-r--r--library/goptions.ml155
1 files changed, 68 insertions, 87 deletions
diff --git a/library/goptions.ml b/library/goptions.ml
index 9dc0f405..eb7bb5b4 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* This module manages customization parameters at the vernacular level *)
@@ -24,7 +26,6 @@ type option_value =
(** Summary of an option status *)
type option_state = {
- opt_sync : bool;
opt_depr : bool;
opt_name : string;
opt_value : option_value;
@@ -36,7 +37,7 @@ type option_state = {
let nickname table = String.concat " " table
let error_undeclared_key key =
- errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type")
+ user_err ~hdr:"Goptions" (str (nickname key) ++ str ": no table or option of this type")
(****************************************************************************)
(* 1- Tables *)
@@ -58,11 +59,10 @@ module MakeTable =
val table : (string * key table_of_A) list ref
val encode : key -> t
val subst : substitution -> t -> t
- val printer : t -> std_ppcmds
+ val printer : t -> Pp.t
val key : option_name
val title : string
- val member_message : t -> bool -> std_ppcmds
- val synchronous : bool
+ val member_message : t -> bool -> Pp.t
end) ->
struct
type option_mark =
@@ -73,17 +73,13 @@ module MakeTable =
let _ =
if String.List.mem_assoc nick !A.table then
- error "Sorry, this table name is already used."
+ user_err Pp.(str "Sorry, this table name is already used.")
module MySet = Set.Make (struct type t = A.t let compare = A.compare end)
- let t =
- if A.synchronous
- then Summary.ref MySet.empty ~name:nick
- else ref MySet.empty
+ let t = Summary.ref MySet.empty ~name:nick
let (add_option,remove_option) =
- if A.synchronous then
let cache_options (_,(f,p)) = match f with
| GOadd -> t := MySet.add p !t
| GOrmv -> t := MySet.remove p !t in
@@ -103,9 +99,6 @@ module MakeTable =
in
((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
(fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c))))
- else
- ((fun c -> t := MySet.add c !t),
- (fun c -> t := MySet.remove c !t))
let print_table table_name printer table =
Feedback.msg_notice
@@ -140,8 +133,7 @@ module type StringConvertArg =
sig
val key : option_name
val title : string
- val member_message : string -> bool -> std_ppcmds
- val synchronous : bool
+ val member_message : string -> bool -> Pp.t
end
module StringConvert = functor (A : StringConvertArg) ->
@@ -156,7 +148,6 @@ struct
let key = A.key
let title = A.title
let member_message = A.member_message
- let synchronous = A.synchronous
end
module MakeStringTable =
@@ -172,11 +163,10 @@ sig
val compare : t -> t -> int
val encode : reference -> t
val subst : substitution -> t -> t
- val printer : t -> std_ppcmds
+ val printer : t -> Pp.t
val key : option_name
val title : string
- val member_message : t -> bool -> std_ppcmds
- val synchronous : bool
+ val member_message : t -> bool -> Pp.t
end
module RefConvert = functor (A : RefConvertArg) ->
@@ -191,7 +181,6 @@ struct
let key = A.key
let title = A.title
let member_message = A.member_message
- let synchronous = A.synchronous
end
module MakeRefTable =
@@ -201,14 +190,13 @@ module MakeRefTable =
(* 2- Flags. *)
type 'a option_sig = {
- optsync : bool;
optdepr : bool;
optname : string;
optkey : option_name;
optread : unit -> 'a;
optwrite : 'a -> unit }
-type option_locality = OptLocal | OptDefault | OptGlobal
+type option_locality = OptDefault | OptLocal | OptExport | OptGlobal
type option_mod = OptSet | OptAppend
@@ -228,31 +216,24 @@ let get_option key = OptionMap.find key !value_tab
let check_key key = try
let _ = get_option key in
- error "Sorry, this option name is already used."
+ user_err Pp.(str "Sorry, this option name is already used.")
with Not_found ->
if String.List.mem_assoc (nickname key) !string_table
|| String.List.mem_assoc (nickname key) !ref_table
- then error "Sorry, this option name is already used."
+ then user_err Pp.(str "Sorry, this option name is already used.")
open Libobject
-open Lib
let warn_deprecated_option =
CWarnings.create ~name:"deprecated-option" ~category:"deprecated"
(fun key -> str "Option" ++ spc () ++ str (nickname key) ++
strbrk " is deprecated")
-let get_locality = function
- | Some true -> OptLocal
- | Some false -> OptGlobal
- | None -> OptDefault
-
let declare_option cast uncast append ?(preprocess = fun x -> x)
- { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
+ { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
check_key key;
let default = read() in
let change =
- if sync then
let _ = Summary.declare_summary (nickname key)
{ Summary.freeze_function = (fun _ -> read ());
Summary.unfreeze_function = write;
@@ -261,33 +242,41 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
match m with
| OptSet -> write v
| OptAppend -> write (append (read ()) v) in
- let load_options i o = cache_options o in
+ let load_options i (_, (l, _, _) as o) = match l with
+ | OptGlobal -> cache_options o
+ | OptExport -> ()
+ | OptLocal | OptDefault ->
+ (** Ruled out by classify_function *)
+ assert false
+ in
+ let open_options i (_, (l, _, _) as o) = match l with
+ | OptExport -> if Int.equal i 1 then cache_options o
+ | OptGlobal -> ()
+ | OptLocal | OptDefault ->
+ (** Ruled out by classify_function *)
+ assert false
+ in
let subst_options (subst,obj) = obj in
let discharge_options (_,(l,_,_ as o)) =
- match l with OptLocal -> None | _ -> Some o in
+ match l with OptLocal -> None | (OptExport | OptGlobal | OptDefault) -> Some o in
let classify_options (l,_,_ as o) =
- match l with OptGlobal -> Substitute o | _ -> Dispose in
+ match l with (OptExport | OptGlobal) -> Substitute o | (OptLocal | OptDefault) -> Dispose in
let options : option_locality * option_mod * _ -> obj =
declare_object
{ (default_object (nickname key)) with
load_function = load_options;
+ open_function = open_options;
cache_function = cache_options;
subst_function = subst_options;
discharge_function = discharge_options;
classify_function = classify_options } in
(fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v)))
- else
- (fun _ m v ->
- let v = preprocess v in
- match m with
- | OptSet -> write v
- | OptAppend -> write (append (read ()) v))
in
let warn () = if depr then warn_deprecated_option key in
let cread () = cast (read ()) in
let cwrite l v = warn (); change l OptSet (uncast v) in
let cappend l v = warn (); change l OptAppend (uncast v) in
- value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,cappend)) !value_tab;
+ value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab;
write
type 'a write_function = 'a -> unit
@@ -295,23 +284,23 @@ type 'a write_function = 'a -> unit
let declare_int_option =
declare_option
(fun v -> IntValue v)
- (function IntValue v -> v | _ -> anomaly (Pp.str "async_option"))
- (fun _ _ -> anomaly (Pp.str "async_option"))
+ (function IntValue v -> v | _ -> anomaly (Pp.str "async_option."))
+ (fun _ _ -> anomaly (Pp.str "async_option."))
let declare_bool_option =
declare_option
(fun v -> BoolValue v)
- (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option"))
- (fun _ _ -> anomaly (Pp.str "async_option"))
+ (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option."))
+ (fun _ _ -> anomaly (Pp.str "async_option."))
let declare_string_option =
declare_option
(fun v -> StringValue v)
- (function StringValue v -> v | _ -> anomaly (Pp.str "async_option"))
+ (function StringValue v -> v | _ -> anomaly (Pp.str "async_option."))
(fun x y -> x^","^y)
let declare_stringopt_option =
declare_option
(fun v -> StringOptValue v)
- (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option"))
- (fun _ _ -> anomaly (Pp.str "async_option"))
+ (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option."))
+ (fun _ _ -> anomaly (Pp.str "async_option."))
(* 3- User accessible commands *)
@@ -322,14 +311,14 @@ let warn_unknown_option =
(fun key -> strbrk "There is no option " ++
str (nickname key) ++ str ".")
-let set_option_value locality check_and_cast key v =
+let set_option_value ?(locality = OptDefault) check_and_cast key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> warn_unknown_option key
- | Some (name, depr, (_,read,write,append)) ->
- write (get_locality locality) (check_and_cast v (read ()))
+ | Some (name, depr, (read,write,append)) ->
+ write locality (check_and_cast v (read ()))
-let bad_type_error () = error "Bad type of value for this option."
+let bad_type_error () = user_err Pp.(str "Bad type of value for this option.")
let check_int_value v = function
| IntValue _ -> IntValue v
@@ -354,25 +343,25 @@ let check_unset_value v = function
warning. This allows a script to refer to an option that doesn't
exist anymore *)
-let set_int_option_value_gen locality =
- set_option_value locality check_int_value
-let set_bool_option_value_gen locality key v =
- set_option_value locality check_bool_value key v
-let set_string_option_value_gen locality =
- set_option_value locality check_string_value
-let unset_option_value_gen locality key =
- set_option_value locality check_unset_value key ()
+let set_int_option_value_gen ?locality =
+ set_option_value ?locality check_int_value
+let set_bool_option_value_gen ?locality key v =
+ set_option_value ?locality check_bool_value key v
+let set_string_option_value_gen ?locality =
+ set_option_value ?locality check_string_value
+let unset_option_value_gen ?locality key =
+ set_option_value ?locality check_unset_value key ()
-let set_string_option_append_value_gen locality key v =
+let set_string_option_append_value_gen ?(locality = OptDefault) key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> warn_unknown_option key
- | Some (name, depr, (_,read,write,append)) ->
- append (get_locality locality) (check_string_value v (read ()))
+ | Some (name, depr, (read,write,append)) ->
+ append locality (check_string_value v (read ()))
-let set_int_option_value = set_int_option_value_gen None
-let set_bool_option_value = set_bool_option_value_gen None
-let set_string_option_value = set_string_option_value_gen None
+let set_int_option_value opt v = set_int_option_value_gen opt v
+let set_bool_option_value opt v = set_bool_option_value_gen opt v
+let set_string_option_value opt v = set_string_option_value_gen opt v
(* Printing options/tables *)
@@ -382,13 +371,13 @@ let msg_option_value (name,v) =
| BoolValue false -> str "off"
| IntValue (Some n) -> int n
| IntValue None -> str "undefined"
- | StringValue s -> str "\"" ++ str s ++ str "\""
+ | StringValue s -> quote (str s)
| StringOptValue None -> str"undefined"
- | StringOptValue (Some s) -> str "\"" ++ str s ++ str "\""
+ | StringOptValue (Some s) -> quote (str s)
(* | IdentValue r -> pr_global_env Id.Set.empty r *)
let print_option_value key =
- let (name, depr, (_,read,_,_)) = get_option key in
+ let (name, depr, (read,_,_)) = get_option key in
let s = read () in
match s with
| BoolValue b ->
@@ -398,9 +387,8 @@ let print_option_value key =
let get_tables () =
let tables = !value_tab in
- let fold key (name, depr, (sync,read,_,_)) accu =
+ let fold key (name, depr, (read,_,_)) accu =
let state = {
- opt_sync = sync;
opt_name = name;
opt_depr = depr;
opt_value = read ();
@@ -415,17 +403,10 @@ let print_tables () =
if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
else msg ++ fnl ()
in
- str "Synchronous options:" ++ fnl () ++
- OptionMap.fold
- (fun key (name, depr, (sync,read,_,_)) p ->
- if sync then p ++ print_option key name (read ()) depr
- else p)
- !value_tab (mt ()) ++
- str "Asynchronous options:" ++ fnl () ++
+ str "Options:" ++ fnl () ++
OptionMap.fold
- (fun key (name, depr, (sync,read,_,_)) p ->
- if sync then p
- else p ++ print_option key name (read ()) depr)
+ (fun key (name, depr, (read,_,_)) p ->
+ p ++ print_option key name (read ()) depr)
!value_tab (mt ()) ++
str "Tables:" ++ fnl () ++
List.fold_right
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 19:12:23 +0000