diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-06 20:45:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-06 20:47:34 +0200 |
| commit | f4de78b048f6567f1e1fdd553b4f7ada0e0707b8 (patch) | |
| tree | d4c52d65d5d9cb55f98ed2710dc42344c0b93baf /parsing/g_vernac.ml4 | |
| parent | d180279aa934dfbb3fd97e707675b55f464f14ef (diff) | |
Do not add "Append" as a lexer keyword.
This was introduced to implement the Append feature on options. As usual when
messing with predefined keywords, this broke code in the wild. In order not
to create a new keyword, we do the string analysis on the production branch of
parsing.
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 96eede2b9..bc02a4621 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -850,9 +850,15 @@ GEXTEND Gram (* For acting on parameter tables *) | "Set"; table = option_table; v = option_value -> - VernacSetOption (table,v) - | "Set"; table = option_table; "Append"; v = STRING -> - VernacSetAppendOption (table,v) + begin match v with + | StringValue s -> + 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) | IDENT "Unset"; table = option_table -> |