diff options
| author | Pierre-Marie Pédrot | 2018-07-11 15:11:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-12 13:53:22 +0200 |
| commit | 270ceed48217797e99ec845cc5d1c599b5729bc2 (patch) | |
| tree | dbeb209fe008c07e020f544cd95c051c4a575145 /stm | |
| parent | 31fce698ec8c3186dc6af49961e8572e81cab50b (diff) | |
Export a wrapper simplifying the registration of vernacular commands.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/vernac_classifier.ml | 9 | ||||
| -rw-r--r-- | stm/vernac_classifier.mli | 5 |
2 files changed, 1 insertions, 13 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 6be80d29a5..eca0c6674b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -42,13 +42,6 @@ let string_of_vernac_when = function let string_of_vernac_classification (t,w) = string_of_vernac_type t ^ " " ^ string_of_vernac_when w -let classifiers = ref [] -let declare_vernac_classifier - (s : Vernacexpr.extend_name) - (f : Genarg.raw_generic_argument list -> unit -> vernac_classification) -= - classifiers := !classifiers @ [s,f] - let idents_of_name : Names.Name.t -> Names.Id.t list = function | Names.Anonymous -> [] @@ -194,7 +187,7 @@ let classify_vernac e = | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> - try List.assoc s !classifiers l () + try Vernacentries.get_vernac_classifier s l with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier ~poly = function diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index 45fbfb42af..e82b191418 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -9,17 +9,12 @@ (************************************************************************) open Vernacexpr -open Genarg val string_of_vernac_classification : vernac_classification -> string (** What does a vernacular do *) val classify_vernac : vernac_control -> vernac_classification -(** Install a vernacular classifier for VernacExtend *) -val declare_vernac_classifier : - Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit - (** Standard constant classifiers *) val classify_as_query : vernac_classification val classify_as_sideeff : vernac_classification |