diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-28 13:45:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-09 10:17:21 -0300 |
| commit | 25b07a6f824654be2041152d904507bc62102986 (patch) | |
| tree | 82f9d96e40911f85347ed4e5bc273cc6a15627f9 /parsing | |
| parent | 38a671f74857aec8e285a6a0bfcab876e3b9a133 (diff) | |
Implement the Export Set/Unset feature.
This feature has been asked many times by different people, and allows to
have options in a module that are performed when this module is imported.
This supersedes the well-numbered cursed PR #313.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 35 |
1 files changed, 14 insertions, 21 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index feaef3161..f1ec49623 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -822,7 +822,14 @@ GEXTEND Gram END GEXTEND Gram - GLOBAL: command query_command class_rawexpr; + GLOBAL: command query_command class_rawexpr gallina_ext; + + gallina_ext: + [ [ IDENT "Export"; "Set"; table = option_table; v = option_value -> + VernacSetOption (true, table, v) + | IDENT "Export"; IDENT "Unset"; table = option_table -> + VernacUnsetOption (true, table) + ] ]; command: [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l @@ -887,24 +894,9 @@ GEXTEND Gram (* For acting on parameter tables *) | "Set"; table = option_table; v = option_value -> - begin match v with - | StringValue s -> - (* We make a special case for warnings because appending is their - natural semantics *) - if CString.List.equal table ["Warnings"] then - VernacSetAppendOption (table, s) - else - let (last, prefix) = List.sep_last table in - if String.equal last "Append" && not (List.is_empty prefix) then - VernacSetAppendOption (prefix, s) - else - VernacSetOption (table, v) - | _ -> VernacSetOption (table, v) - end - | "Set"; table = option_table -> - VernacSetOption (table,BoolValue true) + VernacSetOption (false, table, v) | IDENT "Unset"; table = option_table -> - VernacUnsetOption table + VernacUnsetOption (false, table) | IDENT "Print"; IDENT "Table"; table = option_table -> VernacPrintOption table @@ -1010,7 +1002,8 @@ GEXTEND Gram | IDENT "Module"; qid = global -> LocateModule qid ] ] ; option_value: - [ [ n = integer -> IntValue (Some n) + [ [ -> BoolValue true + | n = integer -> IntValue (Some n) | s = STRING -> StringValue s ] ] ; option_ref_value: @@ -1081,10 +1074,10 @@ GEXTEND Gram (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> - VernacSetOption (["Ltac";"Debug"], BoolValue true) + VernacSetOption (false, ["Ltac";"Debug"], BoolValue true) | IDENT "Debug"; IDENT "Off" -> - VernacSetOption (["Ltac";"Debug"], BoolValue false) + VernacSetOption (false, ["Ltac";"Debug"], BoolValue false) (* registration of a custom reduction *) |