From d94a8b2024497e11ff9392a7fa4401ffcc131cc0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 10 Mar 2016 15:20:47 +0100
Subject: Moving the proof mode parsing management to Pcoq.

---
 parsing/pcoq.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 91f933987b..9c2f09db84 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
-- 
cgit v1.2.3