From ab85be0ab41251ece3b583c3ff38f08f546f6414 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 8 Aug 2013 18:52:29 +0000 Subject: Vernac classification streamlined (handles VERNAC EXTEND) The warning output by vernacextend when the classifier is missing is the documentation of this commit: Warning: Vernac entry "Foo" misses a classifier. A classifier is a function that returns an expression of type vernac_classification (see Vernacexpr). You can: - Use '... EXTEND Foo CLASSIFIED AS QUERY ...' if the new vernacular command does not alter the system state; - Use '... EXTEND Foo CLASSIFIED AS SIDEFF ...' if the new vernacular command alters the system state but not the parser nor it starts a proof or ends one; - Use '... EXTEND Foo CLASSIFIED BY f ...' to specify a global function f. The function f will be called passing "Foo" as the only argument; - Add a specific classifier in each clause using the syntax: '[...] => [ f ] -> [...]'. Specific classifiers have precedence over global classifiers. Only one classifier is called. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16680 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/xml/xmlentries.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/xml') diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4 index 5ca6e155b..8cf3a0bdc 100644 --- a/plugins/xml/xmlentries.ml4 +++ b/plugins/xml/xmlentries.ml4 @@ -25,7 +25,7 @@ END (* Print XML and Show XML *) -VERNAC COMMAND EXTEND Xml +VERNAC COMMAND EXTEND Xml CLASSIFIED AS QUERY | [ "Print" "XML" filename(fn) global(qid) ] -> [ Xmlcommand.print_ref qid fn ] | [ "Show" "XML" filename(fn) "Proof" ] -> [ Xmlcommand.show fn ] -- cgit v1.2.3