aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--library/goptions.ml21
-rw-r--r--library/goptions.mli8
-rw-r--r--vernac/g_vernac.mlg16
-rw-r--r--vernac/ppvernac.ml4
-rw-r--r--vernac/vernacentries.ml17
-rw-r--r--vernac/vernacexpr.ml10
6 files changed, 41 insertions, 35 deletions
diff --git a/library/goptions.ml b/library/goptions.ml
index fbacd07226..666ba8ee2e 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -24,6 +24,10 @@ type option_value =
| StringValue of string
| StringOptValue of string option
+type table_value =
+ | StringRefValue of string
+ | QualidRefValue of qualid
+
(** Summary of an option status *)
type option_state = {
opt_depr : bool;
@@ -189,6 +193,23 @@ end
module MakeRefTable =
functor (A : RefConvertArg) -> MakeTable (RefConvert(A))
+type iter_table_aux = { aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit }
+
+let iter_table f key lv =
+ let aux = function
+ | StringRefValue s ->
+ begin
+ try f.aux (get_string_table key) (Global.env()) s
+ with Not_found -> error_no_table_of_this_type ~kind:"string" key
+ end
+ | QualidRefValue locqid ->
+ begin
+ try f.aux (get_ref_table key) (Global.env()) locqid
+ with Not_found -> error_no_table_of_this_type ~kind:"qualid" key
+ end
+ in
+ List.iter aux lv
+
(****************************************************************************)
(* 2- Flags. *)
diff --git a/library/goptions.mli b/library/goptions.mli
index 59b1667f5a..150954cbac 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -187,6 +187,10 @@ type option_value =
| StringValue of string
| StringOptValue of string option
+type table_value =
+ | StringRefValue of string
+ | QualidRefValue of qualid
+
val set_option_value : ?locality:option_locality ->
('a -> option_value -> option_value) -> option_name -> 'a -> unit
(** [set_option_value ?locality f name v] sets [name] to the result of
@@ -204,5 +208,7 @@ type option_state = {
val get_tables : unit -> option_state OptionMap.t
val print_tables : unit -> Pp.t
-val error_no_table_of_this_type : kind:string -> option_name -> 'a
+type iter_table_aux = { aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit }
+val iter_table : iter_table_aux -> option_name -> table_value list -> unit
+
val error_undeclared_key : option_name -> 'a
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 08ba49f92b..13145d3757 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -938,23 +938,23 @@ GRAMMAR EXTEND Gram
| IDENT "Print"; IDENT "Table"; table = option_table ->
{ VernacPrintOption table }
- | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
+ | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 table_value
-> { VernacAddOption ([table;field], v) }
(* A global value below will be hidden by a field above! *)
(* In fact, we give priority to secondary tables *)
(* No syntax for tertiary tables due to conflict *)
(* (but they are unused anyway) *)
- | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value ->
+ | IDENT "Add"; table = IDENT; v = LIST1 table_value ->
{ VernacAddOption ([table], v) }
- | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value
+ | IDENT "Test"; table = option_table; "for"; v = LIST1 table_value
-> { VernacMemOption (table, v) }
| IDENT "Test"; table = option_table ->
{ VernacPrintOption table }
- | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
+ | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 table_value
-> { VernacRemoveOption ([table;field], v) }
- | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
+ | IDENT "Remove"; table = IDENT; v = LIST1 table_value ->
{ VernacRemoveOption ([table], v) } ]]
;
query_command: (* TODO: rapprocher Eval et Check *)
@@ -1047,9 +1047,9 @@ GRAMMAR EXTEND Gram
| n = integer -> { OptionSetInt n }
| s = STRING -> { OptionSetString s } ] ]
;
- option_ref_value:
- [ [ id = global -> { QualidRefValue id }
- | s = STRING -> { StringRefValue s } ] ]
+ table_value:
+ [ [ id = global -> { Goptions.QualidRefValue id }
+ | s = STRING -> { Goptions.StringRefValue s } ] ]
;
option_table:
[ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 7a2e6d8b03..36d79bfdb1 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -168,8 +168,8 @@ open Pputils
keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search sl ++ pr_in_out_modules b
let pr_option_ref_value = function
- | QualidRefValue id -> pr_qualid id
- | StringRefValue s -> qs s
+ | Goptions.QualidRefValue id -> pr_qualid id
+ | Goptions.StringRefValue s -> qs s
let pr_printoption table b =
prlist_with_sep spc str table ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 07a9272336..3926b91a55 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1554,23 +1554,6 @@ let vernac_set_option ~locality table v = match v with
vernac_set_option0 ~locality table v
| _ -> vernac_set_option0 ~locality table v
-type iter_table_aux = { aux : 'a. 'a Goptions.table_of_A -> Environ.env -> 'a -> unit }
-
-let iter_table f key lv =
- let aux = function
- | StringRefValue s ->
- begin
- try f.aux (get_string_table key) (Global.env()) s
- with Not_found -> error_no_table_of_this_type ~kind:"string" key
- end
- | QualidRefValue locqid ->
- begin
- try f.aux (get_ref_table key) (Global.env()) locqid
- with Not_found -> error_no_table_of_this_type ~kind:"qualid" key
- end
- in
- List.iter aux lv
-
let vernac_add_option = iter_table { aux = fun table -> table.add }
let vernac_remove_option = iter_table { aux = fun table -> table.remove }
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index c32ac414ba..e46186288e 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -121,10 +121,6 @@ type option_setting =
| OptionSetInt of int
| OptionSetString of string
-type option_ref_value =
- | StringRefValue of string
- | QualidRefValue of qualid
-
(** Identifier and optional list of bound universes and constraints. *)
type sort_expr = Sorts.family
@@ -406,9 +402,9 @@ type nonrec vernac_expr =
| VernacSetStrategy of
(Conv_oracle.level * qualid or_by_notation list) list
| VernacSetOption of bool (* Export modifier? *) * Goptions.option_name * option_setting
- | VernacAddOption of Goptions.option_name * option_ref_value list
- | VernacRemoveOption of Goptions.option_name * option_ref_value list
- | VernacMemOption of Goptions.option_name * option_ref_value list
+ | VernacAddOption of Goptions.option_name * Goptions.table_value list
+ | VernacRemoveOption of Goptions.option_name * Goptions.table_value list
+ | VernacMemOption of Goptions.option_name * Goptions.table_value list
| VernacPrintOption of Goptions.option_name
| VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr
| VernacGlobalCheck of constr_expr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:53:27 +0000