Moving the proof mode parsing management to Pcoq.

3 files changed, 16 insertions, 11 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 49baeb556..2eb590132 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -35,7 +35,6 @@ let _ = List.iter Lexer.add_keyword vernac_kw
 let query_command = Gram.entry_create "vernac:query_command"
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
-let noedit_mode = Gram.entry_create "vernac:noedit_command"
 let subprf = Gram.entry_create "vernac:subprf"
 
 let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
@@ -48,11 +47,6 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
 let instance_name = Gram.entry_create "vernac:instance_name"
 let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
 
-let command_entry = ref noedit_mode
-let set_command_entry e = command_entry := e
-let get_command_entry () = !command_entry
-
-
 (* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
     proof editing and changes nothing else). Then sets it as the default proof mode. *)
 let set_tactic_mode () = set_command_entry tactic_mode
@@ -82,10 +76,6 @@ let test_bracket_ident =
 	      | _ -> raise Stream.Failure)
 	| _ -> raise Stream.Failure)
 
-let default_command_entry =
-  Gram.Entry.of_parser "command_entry"
-    (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
-
 GEXTEND Gram
   GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
   vernac: FIRST
@@ -129,7 +119,7 @@ GEXTEND Gram
     ] ]
   ;
   vernac_aux: LAST
-    [ [ prfcom = default_command_entry -> prfcom ] ]
+    [ [ prfcom = command_entry -> prfcom ] ]
   ;
   noedit_mode:
     [ [ c = subgoal_command -> c None] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 91f933987..9c2f09db8 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -383,6 +383,7 @@ module Vernac_ =
     let rec_definition = gec_vernac "Vernac.rec_definition"
     (* Main vernac entry *)
     let main_entry = Gram.entry_create "vernac"
+    let noedit_mode = gec_vernac "noedit_command"
 
     let () =
       let act_vernac = Gram.action (fun v loc -> Some (!@loc, v)) in
@@ -393,10 +394,18 @@ module Vernac_ =
       ] in
       maybe_uncurry (Gram.extend main_entry) (None, make_rule rule)
 
+    let command_entry_ref = ref noedit_mode
+    let command_entry =
+      Gram.Entry.of_parser "command_entry"
+        (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm)
+
   end
 
 let main_entry = Vernac_.main_entry
 
+let set_command_entry e = Vernac_.command_entry_ref := e
+let get_command_entry () = !Vernac_.command_entry_ref
+
 (**********************************************************************)
 (* This determines (depending on the associativity of the current
    level and on the expected associativity) if a reference to constr_n is
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d6bfe3eb3..7410d4e44 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -241,11 +241,17 @@ module Vernac_ :
     val vernac : vernac_expr Gram.entry
     val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
     val vernac_eoi : vernac_expr Gram.entry
+    val noedit_mode : vernac_expr Gram.entry
+    val command_entry : vernac_expr Gram.entry
   end
 
 (** The main entry: reads an optional vernac command *)
 val main_entry : (Loc.t * vernac_expr) option Gram.entry
 
+(** Handling of the proof mode entry *)
+val get_command_entry : unit -> vernac_expr Gram.entry
+val set_command_entry : vernac_expr Gram.entry -> unit
+
 (** Mapping formal entries into concrete ones *)
 
 (** Binding constr entry keys to entries and symbols *)