diff options
Diffstat (limited to 'grammar/vernacextend.mlp')
| -rw-r--r-- | grammar/vernacextend.mlp | 29 |
1 files changed, 23 insertions, 6 deletions
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 874712124..a561ea370 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -82,7 +82,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, ploc_vala None, - <:expr< fun loc -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) + <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>) let make_fun_clauses loc s l = let map c = @@ -136,6 +136,10 @@ EXTEND OPT "|"; l = LIST1 rule SEP "|"; "END" -> declare_command loc s c <:expr<None>> l + | "VERNAC"; "COMMAND"; "FUNCTIONAL"; "EXTEND"; s = UIDENT; c = OPT classification; + OPT "|"; l = LIST1 fun_rule SEP "|"; + "END" -> + declare_command loc s c <:expr<None>> l | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification; OPT "|"; l = LIST1 rule SEP "|"; "END" -> @@ -158,18 +162,31 @@ EXTEND deprecation: [ [ "DEPRECATED" -> () ] ] ; - (* spiwack: comment-by-guessing: it seems that the isolated string (which - otherwise could have been another argument) is not passed to the - VernacExtend interpreter function to discriminate between the clauses. *) + (* spiwack: comment-by-guessing: it seems that the isolated string + (which otherwise could have been another argument) is not passed + to the VernacExtend interpreter function to discriminate between + the clauses. *) rule: [ [ "["; s = STRING; l = LIST0 args; "]"; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> let () = if s = "" then failwith "Command name is empty." in - let b = <:expr< fun loc -> $e$ >> in + let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in + { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } + | "[" ; "-" ; l = LIST1 args ; "]" ; + d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> + let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in + { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } + ] ] + ; + fun_rule: + [ [ "["; s = STRING; l = LIST0 args; "]"; + d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> + let () = if s = "" then failwith "Command name is empty." in + let b = <:expr< $e$ >> in { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } | "[" ; "-" ; l = LIST1 args ; "]" ; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let b = <:expr< fun loc -> $e$ >> in + let b = <:expr< $e$ >> in { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } ] ] ; |