diff options
| -rw-r--r-- | API/API.mli | 9 | ||||
| -rw-r--r-- | grammar/vernacextend.mlp | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml | 15 | ||||
| -rw-r--r-- | vernac/vernacinterp.mli | 13 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacstate.mli | 2 |
7 files changed, 35 insertions, 12 deletions
diff --git a/API/API.mli b/API/API.mli index 86c6f1415..f56509a70 100644 --- a/API/API.mli +++ b/API/API.mli @@ -5982,8 +5982,15 @@ sig type deprecation = bool + type atts = { + loc : Loc.t option; + locality : bool option; + } + type vernac_command = - Genarg.raw_generic_argument list -> Loc.t option -> Vernacstate.t -> Vernacstate.t + Genarg.raw_generic_argument list -> + atts:atts -> st:Vernacstate.t -> + Vernacstate.t val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 12308bede..ae8fe4da2 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -173,11 +173,11 @@ 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 loc -> ( let () = $e$ in fun st -> st ) >> 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 loc -> ( let () = $e$ in fun st -> st ) >> in + 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; } ] ] ; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 10c139e5a..358e965ec 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2078,7 +2078,7 @@ let interp ?proof ?loc locality poly st c = (* Extensions *) | VernacExtend (opn,args) -> (* XXX: Here we are returning the state! :) *) - let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) st in + let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) ~st in () (* Vernaculars that take a locality flag *) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 1d024386e..725436fef 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -11,8 +11,16 @@ open Pp open CErrors type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> - Vernacstate.t -> Vernacstate.t + +type atts = { + loc : Loc.t option; + locality : bool option; +} + +type vernac_command = + Genarg.raw_generic_argument list -> + atts:atts -> st:Vernacstate.t -> + Vernacstate.t (* Table of vernac entries *) let vernac_tab = @@ -67,7 +75,8 @@ let call ?locality ?loc (opn,converted_args) = let hunk = callback converted_args in phase := "Executing command"; Locality.LocalityFixme.set locality; - let res = hunk loc in + let atts = { loc; locality } in + let res = hunk ~atts in Locality.LocalityFixme.assert_consumed (); res with diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index 1c66b1c04..602ccba15 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -10,8 +10,15 @@ type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> - Vernacstate.t -> Vernacstate.t +type atts = { + loc : Loc.t option; + locality : bool option; +} + +type vernac_command = + Genarg.raw_generic_argument list -> + atts:atts -> st:Vernacstate.t -> + Vernacstate.t val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit @@ -21,4 +28,4 @@ val vinterp_init : unit -> unit val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> - Vernacstate.t -> Vernacstate.t + st:Vernacstate.t -> Vernacstate.t diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 9802a03ca..eb1359d52 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type t = { (* TODO: inline records in OCaml 4.03 *) +type t = { system : States.state; (* summary + libstack *) proof : Proof_global.state; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 63a5b3b1e..bcfa49aa3 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type t = { (* TODO: inline records in OCaml 4.03 *) +type t = { system : States.state; (* summary + libstack *) proof : Proof_global.state; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) |