1 files changed, 33 insertions, 5 deletions
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index a647b2ef73..0e46df2320 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -12,6 +12,27 @@ open Pcoq
 
 let uvernac = create_universe "vernac"
 
+type proof_mode = string
+
+(* Tactic parsing modes *)
+let register_proof_mode, find_proof_mode, lookup_proof_mode =
+  let proof_mode : (string, Vernacexpr.vernac_expr Entry.t) Hashtbl.t =
+    Hashtbl.create 19 in
+  let register_proof_mode ename e = Hashtbl.add proof_mode ename e; ename in
+  let find_proof_mode ename =
+    try Hashtbl.find proof_mode ename
+    with Not_found ->
+      CErrors.anomaly Pp.(str "proof mode not found: " ++ str ename) in
+  let lookup_proof_mode name =
+    if Hashtbl.mem proof_mode name then Some name
+    else None
+  in
+  register_proof_mode, find_proof_mode, lookup_proof_mode
+
+let proof_mode_to_string name = name
+
+let command_entry_ref = ref None
+
 module Vernac_ =
   struct
     let gec_vernac s = Entry.create ("vernac:" ^ s)
@@ -39,17 +60,24 @@ module Vernac_ =
       ] in
       Pcoq.grammar_extend main_entry None (None, [None, None, rule])
 
-    let command_entry_ref = ref noedit_mode
+    let select_tactic_entry spec =
+      match spec with
+      | None -> noedit_mode
+      | Some ename -> find_proof_mode ename
+
     let command_entry =
       Pcoq.Entry.of_parser "command_entry"
-        (fun strm -> Pcoq.Entry.parse_token_stream !command_entry_ref strm)
+        (fun strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
 
   end
 
-let main_entry = Vernac_.main_entry
+module Unsafe = struct
+  let set_tactic_entry oname = command_entry_ref := oname
+end
 
-let set_command_entry e = Vernac_.command_entry_ref := e
-let get_command_entry () = !Vernac_.command_entry_ref
+let main_entry proof_mode =
+  Unsafe.set_tactic_entry proof_mode;
+  Vernac_.main_entry
 
 let () =
   register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr);