diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 16 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 21 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 10 |
4 files changed, 16 insertions, 35 deletions
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 044e479aeb..3926b91a55 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1554,26 +1554,11 @@ let vernac_set_option ~locality table v = match v with vernac_set_option0 ~locality table v | _ -> vernac_set_option0 ~locality table v -let vernac_add_option key lv = - let f = function - | StringRefValue s -> (get_string_table key).add (Global.env()) s - | QualidRefValue locqid -> (get_ref_table key).add (Global.env()) locqid - in - try List.iter f lv with Not_found -> error_undeclared_key key +let vernac_add_option = iter_table { aux = fun table -> table.add } -let vernac_remove_option key lv = - let f = function - | StringRefValue s -> (get_string_table key).remove (Global.env()) s - | QualidRefValue locqid -> (get_ref_table key).remove (Global.env()) locqid - in - try List.iter f lv with Not_found -> error_undeclared_key key +let vernac_remove_option = iter_table { aux = fun table -> table.remove } -let vernac_mem_option key lv = - let f = function - | StringRefValue s -> (get_string_table key).mem (Global.env()) s - | QualidRefValue locqid -> (get_ref_table key).mem (Global.env()) locqid - in - try List.iter f lv with Not_found -> error_undeclared_key key +let vernac_mem_option = iter_table { aux = fun table -> table.mem } let vernac_print_option key = try (get_ref_table key).print () 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 |