diff options
| -rw-r--r-- | library/goptions.ml | 15 | ||||
| -rw-r--r-- | library/goptions.mli | 12 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 6 |
6 files changed, 31 insertions, 10 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 7c522022f..75fba89fe 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -27,11 +27,18 @@ let nickname table = String.concat " " table let error_undeclared_key key = error ((nickname key)^": no table or option of this type") -type value = +type 'a option_state = { + opt_sync : bool; + opt_name : string; + opt_key : option_name; + opt_value : 'a; +} + +type option_value = | BoolValue of bool | IntValue of int option | StringValue of string - | IdentValue of global_reference +(* | IdentValue of global_reference *) (****************************************************************************) (* 1- Tables *) @@ -204,7 +211,7 @@ type 'a option_sig = { optread : unit -> 'a; optwrite : 'a -> unit } -type option_type = bool * (unit -> value) -> (value -> unit) +type option_type = bool * (unit -> option_value) -> (option_value -> unit) module OptionMap = Map.Make (struct type t = option_name let compare = compare end) @@ -348,7 +355,7 @@ let msg_option_value (name,v) = | IntValue (Some n) -> int n | IntValue None -> str "undefined" | StringValue s -> str s - | IdentValue r -> pr_global_env Idset.empty r +(* | IdentValue r -> pr_global_env Idset.empty r *) let print_option_value key = let (name,(_,read,_,_,_)) = get_option key in diff --git a/library/goptions.mli b/library/goptions.mli index d3e0ac1a6..1a89961ac 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -135,6 +135,18 @@ val declare_string_option: string option_sig -> string write_function (** {6 Special functions supposed to be used only in vernacentries.ml } *) +type 'a option_state = { + opt_sync : bool; + opt_name : string; + opt_key : option_name; + opt_value : 'a; +} + +type option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + val get_string_table : option_name -> < add : string -> unit; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c9700cdf0..78e01afd9 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -799,7 +799,7 @@ GEXTEND Gram | IDENT "Ltac"; qid = global -> LocateTactic qid ] ] ; option_value: - [ [ n = integer -> IntValue n + [ [ n = integer -> IntValue (Some n) | s = STRING -> StringValue s ] ] ; option_ref_value: diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 950013013..6254d345f 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -164,7 +164,9 @@ let pr_printoption table b = let pr_set_option a b = let pr_opt_value = function - | IntValue n -> spc() ++ int n + | IntValue None -> assert false + (* This should not happen because of the grammar *) + | IntValue (Some n) -> spc() ++ int n | StringValue s -> spc() ++ str s | BoolValue b -> mt() in pr_printoption a None ++ pr_opt_value b diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cd30eaf5c..88b78a633 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -997,7 +997,7 @@ let vernac_set_opacity local str = let vernac_set_option locality key = function | StringValue s -> set_string_option_value_gen locality key s - | IntValue n -> set_int_option_value_gen locality key (Some n) + | IntValue n -> set_int_option_value_gen locality key n | BoolValue b -> set_bool_option_value_gen locality key b let vernac_unset_option locality key = diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 32ea70baf..bae6cfcdd 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -134,10 +134,10 @@ type onlyparsing_flag = bool (* true = Parse only; false = Print also *) type infer_flag = bool (* true = try to Infer record; false = nothing *) type full_locality_flag = bool option (* true = Local; false = Global *) -type option_value = - | StringValue of string - | IntValue of int +type option_value = Goptions.option_value = | BoolValue of bool + | IntValue of int option + | StringValue of string type option_ref_value = | StringRefValue of string |