diff options
| author | Pierre-Marie Pédrot | 2014-09-09 22:13:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-10 00:16:20 +0200 |
| commit | edfa5e986a25eb7a0719d20b43a618cb5bd4cd95 (patch) | |
| tree | e7af11e344a99b2496d22d2bc100f493bd701b96 /parsing | |
| parent | 0dd3f0d34873dcd126be8ec48724a310214f38ac (diff) | |
VernacExtend does not dispatch on type anymore.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramml.ml | 12 | ||||
| -rw-r--r-- | parsing/egramml.mli | 7 |
2 files changed, 13 insertions, 6 deletions
diff --git a/parsing/egramml.ml b/parsing/egramml.ml index 51dda26642..e7c5c4a480 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Compat open Names open Pcoq @@ -45,11 +46,18 @@ let make_rule mkact pt = (** Vernac grammar extensions *) let vernac_exts = ref [] -let get_extend_vernac_grammars () = !vernac_exts + +let get_extend_vernac_rule (s, i) = + try + let find ((name, j), _) = String.equal name s && Int.equal i j in + let (_, rules) = List.find find !vernac_exts in + rules + with + | Failure _ -> raise Not_found let extend_vernac_command_grammar s nt gl = let nt = Option.default Vernac_.command nt in vernac_exts := (s,gl) :: !vernac_exts; let mkact loc l = VernacExtend (s,List.map snd l) in - let rules = List.map (make_rule mkact) gl in + let rules = [make_rule mkact gl] in maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)]) diff --git a/parsing/egramml.mli b/parsing/egramml.mli index 9e2c29b98a..97bfbf682d 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -17,11 +17,10 @@ type grammar_prod_item = Pcoq.prod_entry_key * Names.Id.t option val extend_vernac_command_grammar : - string -> Vernacexpr.vernac_expr Pcoq.Gram.entry option -> - grammar_prod_item list list -> unit + Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Gram.entry option -> + grammar_prod_item list -> unit -val get_extend_vernac_grammars : - unit -> (string * grammar_prod_item list list) list +val get_extend_vernac_rule : Vernacexpr.extend_name -> grammar_prod_item list (** Utility function reused in Egramcoq : *) |