diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-08-04 18:28:31 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-11-01 08:05:37 +0100 |
| commit | f874a292c94b290a31af8e0f707ffd20ab31001b (patch) | |
| tree | eb8c4b67597cbf6adaee337717e9a09eaf9325eb /grammar | |
| parent | e5659c8ffe735c530a707a61c692a3af21a79a9a (diff) | |
provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules
Originally, it was not possible to define a new vernacular command
in the following way:
VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY
[ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ]
END
because "loc : Loc.t" was not bound.
This commit fixes that, i.e. the location of the custom Vernacular command
(within *.v file) is made available as "loc" variable bound on the right side
of "->" .
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/vernacextend.mlp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index a529185dd..874712124 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -59,7 +59,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = | None, Some cg -> (make_patt pt, ploc_vala None, - <:expr< fun () -> $cg$ $str:s$ >>) + <:expr< fun loc -> $cg$ $str:s$ >>) | None, None -> prerr_endline (("Vernac entry \""^s^"\" misses a classifier. "^ "A classifier is a function that returns an expression "^ @@ -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 () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) + <:expr< fun loc -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) let make_fun_clauses loc s l = let map c = @@ -165,16 +165,16 @@ EXTEND [ [ "["; 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 () -> $e$ >> in + let b = <:expr< fun loc -> $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 () -> $e$ >> in + let b = <:expr< fun loc -> $e$ >> in { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } ] ] ; classifier: - [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ] ] + [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun loc -> $c$>> ] ] ; args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> |