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

6 files changed, 53 insertions, 45 deletions

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 072737dab..f79f71712 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -16,6 +16,7 @@ open Tok
 open Decl_expr
 open Names
 open Pcoq
+open Vernacexpr
 
 open Pcoq.Constr
 open Pcoq.Tactic
@@ -114,11 +115,13 @@ let wit_proof_instr =
 let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
   pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
 
+let classify_proof_instr _ = VtProofStep, VtLater
+
 (* We use the VERNAC EXTEND facility with a custom non-terminal
     to populate [proof_mode] with a new toplevel interpreter.
     The "-" indicates that the rule does not start with a distinguished
     string. *)
-VERNAC proof_mode EXTEND ProofInstr
+VERNAC proof_mode EXTEND ProofInstr CLASSIFIED BY classify_proof_instr
   [ - proof_instr(instr) ] -> [ vernac_proof_instr instr ]
 END
 
@@ -163,10 +166,13 @@ let _ =
 				   }
 
 (* Two new vernacular commands *)
-VERNAC COMMAND EXTEND DeclProof
+let classify_decl _ = VtProofStep, VtNow
+ 
+VERNAC COMMAND EXTEND DeclProof CLASSIFIED BY classify_decl
   [ "proof" ] -> [ vernac_decl_proof () ]
 END
-VERNAC COMMAND EXTEND  DeclReturn
+VERNAC COMMAND EXTEND  DeclReturn CLASSIFIED BY classify_decl
+
   [ "return" ] -> [ vernac_return () ]
 END
 
@@ -396,11 +402,3 @@ GLOBAL: proof_instr;
     [[ e=emphasis;i=bare_proof_instr;"." -> {emph=e;instr=i}]]
   ;
 END;;
-
-open Vernacexpr
-
-let () =
-  Vernac_classifier.declare_vernac_classifier "decl_mode" (function
-    | VernacExtend (("DeclProof"|"DeclReturn"), _) -> VtProofStep, VtNow
-    | VernacExtend ("ProofInstr", _) -> VtProofStep, VtLater
-    | _ -> VtUnknown, VtNow)
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 5295e2cf9..b0b8217b6 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -51,7 +51,7 @@ END
 
 (* Extraction commands *)
 
-VERNAC COMMAND EXTEND Extraction
+VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY
 (* Extraction in the Coq toplevel *)
 | [ "Extraction" global(x) ] -> [ simple_extraction x ]
 | [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ]
@@ -61,85 +61,85 @@ VERNAC COMMAND EXTEND Extraction
   -> [ full_extraction (Some f) l ]
 END
 
-VERNAC COMMAND EXTEND SeparateExtraction
+VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY
 (* Same, with content splitted in several files *)
 | [ "Separate" "Extraction" ne_global_list(l) ]
   -> [ separate_extraction l ]
 END
 
 (* Modular extraction (one Coq library = one ML module) *)
-VERNAC COMMAND EXTEND ExtractionLibrary
+VERNAC COMMAND EXTEND ExtractionLibrary CLASSIFIED AS QUERY
 | [ "Extraction" "Library" ident(m) ]
   -> [ extraction_library false m ]
 END
 
-VERNAC COMMAND EXTEND RecursiveExtractionLibrary
+VERNAC COMMAND EXTEND RecursiveExtractionLibrary CLASSIFIED AS QUERY
 | [ "Recursive" "Extraction" "Library" ident(m) ]
   -> [ extraction_library true m ]
 END
 
 (* Target Language *)
-VERNAC COMMAND EXTEND ExtractionLanguage
+VERNAC COMMAND EXTEND ExtractionLanguage CLASSIFIED AS SIDEFF
 | [ "Extraction" "Language" language(l) ]
   -> [ extraction_language l ]
 END
 
-VERNAC COMMAND EXTEND ExtractionInline
+VERNAC COMMAND EXTEND ExtractionInline CLASSIFIED AS SIDEFF
 (* Custom inlining directives *)
 | [ "Extraction" "Inline" ne_global_list(l) ]
   -> [ extraction_inline true l ]
 END
 
-VERNAC COMMAND EXTEND ExtractionNoInline
+VERNAC COMMAND EXTEND ExtractionNoInline CLASSIFIED AS SIDEFF
 | [ "Extraction" "NoInline" ne_global_list(l) ]
   -> [ extraction_inline false l ]
 END
 
-VERNAC COMMAND EXTEND PrintExtractionInline
+VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY
 | [ "Print" "Extraction" "Inline" ]
   -> [ msg_info (print_extraction_inline ()) ]
 END
 
-VERNAC COMMAND EXTEND ResetExtractionInline
+VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF
 | [ "Reset" "Extraction" "Inline" ]
   -> [ reset_extraction_inline () ]
 END
 
-VERNAC COMMAND EXTEND ExtractionImplicit
+VERNAC COMMAND EXTEND ExtractionImplicit CLASSIFIED AS SIDEFF
 (* Custom implicit arguments of some csts/inds/constructors *)
 | [ "Extraction" "Implicit" global(r) "[" int_or_id_list(l) "]" ]
   -> [ extraction_implicit r l ]
 END
 
-VERNAC COMMAND EXTEND ExtractionBlacklist
+VERNAC COMMAND EXTEND ExtractionBlacklist CLASSIFIED AS SIDEFF
 (* Force Extraction to not use some filenames *)
 | [ "Extraction" "Blacklist" ne_ident_list(l) ]
   -> [ extraction_blacklist l ]
 END
 
-VERNAC COMMAND EXTEND PrintExtractionBlacklist
+VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY
 | [ "Print" "Extraction" "Blacklist" ]
   -> [ msg_info (print_extraction_blacklist ()) ]
 END
 
-VERNAC COMMAND EXTEND ResetExtractionBlacklist
+VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
 | [ "Reset" "Extraction" "Blacklist" ]
   -> [ reset_extraction_blacklist () ]
 END
 
 
 (* Overriding of a Coq object by an ML one *)
-VERNAC COMMAND EXTEND ExtractionConstant
+VERNAC COMMAND EXTEND ExtractionConstant CLASSIFIED AS SIDEFF
 | [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ]
   -> [ extract_constant_inline false x idl y ]
 END
 
-VERNAC COMMAND EXTEND ExtractionInlinedConstant
+VERNAC COMMAND EXTEND ExtractionInlinedConstant CLASSIFIED AS SIDEFF
 | [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ]
   -> [ extract_constant_inline true x [] y ]
 END
 
-VERNAC COMMAND EXTEND ExtractionInductive
+VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF
 | [ "Extract" "Inductive" global(x) "=>"
     mlname(id) "[" mlname_list(idl) "]" string_opt(o) ]
   -> [ extract_inductive x id idl o ]
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index bdea8b1a9..84060dc9d 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -53,14 +53,14 @@ let _=
 let (set_default_solver, default_solver, print_default_solver) = 
   Tactic_option.declare_tactic_option ~default:(<:tactic<auto with *>>) "Firstorder default solver"
 
-VERNAC COMMAND EXTEND Firstorder_Set_Solver
+VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
 | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
     set_default_solver 
       (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
       (Tacintern.glob_tactic t) ]
 END
 
-VERNAC COMMAND EXTEND Firstorder_Print_Solver
+VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
 | [ "Print" "Firstorder" "Solver" ] -> [
     Pp.msg_info
       (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 7ab9488de..7e229fbd2 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -155,12 +155,21 @@ type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexp
 
 let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) =
   Genarg.create_arg None "function_rec_definition_loc"
-VERNAC COMMAND EXTEND Function
-   ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] ->
-	[
-	  do_generate_principle false (List.map snd recsl);
 
-	]
+(* TASSI: n'importe quoi ! *)
+VERNAC COMMAND EXTEND Function
+   ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+    => [ let hard = List.exists (function
+           | _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true
+           | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
+         match
+           Vernac_classifier.classify_vernac
+             (Vernacexpr.VernacFixpoint(None, List.map snd recsl))
+         with
+         | Vernacexpr.VtSideff ids, _ when hard ->
+             Vernacexpr.VtStartProof ("Classic", ids), Vernacexpr.VtLater
+         | x -> x ]
+    -> [ do_generate_principle false (List.map snd recsl) ]
 END
 
 let pr_fun_scheme_arg (princ_name,fun_name,s) =
@@ -191,7 +200,9 @@ let warning_error names e =
 
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
-   ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] ->
+   ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
+   => [ Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater ]
+   ->
     [
       begin
 	try
@@ -225,14 +236,13 @@ END
 (***** debug only ***)
 
 VERNAC COMMAND EXTEND NewFunctionalCase
-   ["Functional" "Case" fun_scheme_arg(fas) ] ->
-    [
-      Functional_principles_types.build_case_scheme fas
-    ]
+  ["Functional" "Case" fun_scheme_arg(fas) ]
+  => [ Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater ]
+  -> [ Functional_principles_types.build_case_scheme fas ]
 END
 
 (***** debug only ***)
-VERNAC COMMAND EXTEND GenerateGraph
+VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
 ["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ]
 END
 
@@ -449,11 +459,11 @@ TACTIC EXTEND poseq
       [ poseq x c ]
 END
 
-VERNAC COMMAND EXTEND Showindinfo
+VERNAC COMMAND EXTEND Showindinfo CLASSIFIED AS QUERY
   [ "showindinfo" ident(x) ] -> [ Merge.showind x ]
 END
 
-VERNAC COMMAND EXTEND MergeFunind
+VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF
   [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")"
       "with" "(" ident(id2) ne_ident_list(cl2)  ")" "using" ident(id) ] ->
      [
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index be661587a..7e4fc7277 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -768,7 +768,7 @@ let process_ring_mods l =
   let k = match !kind with Some k -> ic_coeff_spec k | None -> Abstract in
   (k, !set, !cst_tac, !pre, !post, !power, !sign, !div)
 
-VERNAC COMMAND EXTEND AddSetoidRing
+VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
   | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] ->
     [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
       add_theory id (ic t) set k cst (pre,post) power sign div]
@@ -1095,7 +1095,7 @@ let process_field_mods l =
   let k = match !kind with Some k -> ic_coeff_spec k | None -> Abstract in
   (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
 
-VERNAC COMMAND EXTEND AddSetoidField
+VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
 | [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] ->
   [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
     add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
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 ]