[parsing] Move `coq_parsable` custom logic to Grammar.

Latest refactorings allow us to make the signature Coq parser a
standard `Grammar.S` one; the only bit needed is to provide the extra
capabilities to the `Lexer` signature w.r.t. to comments state.

The handling of Lexer state is still a bit ad-hoc, in particular it is
global whereas it should be fully attached to the parsable. This may
work ok in batch mode but the current behavior may be buggy in the
interactive context.

This PR doesn't solve that but it is a step towards a more functional
solution.

4 files changed, 22 insertions, 103 deletions

diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index a39da96a53..85640cabba 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -392,22 +392,6 @@ let comments = ref []
 let current_comment = Buffer.create 8192
 let between_commands = ref true
 
-(* The state of the lexer visible from outside *)
-type lexer_state = int option * string * bool * ((int * int) * string) list
-
-let init_lexer_state () = (None,"",true,[])
-let set_lexer_state (o,s,b,c) =
-  comment_begin := o;
-  Buffer.clear current_comment; Buffer.add_string current_comment s;
-  between_commands := b;
-  comments := c
-let get_lexer_state () =
-  (!comment_begin, Buffer.contents current_comment, !between_commands, !comments)
-let drop_lexer_state () =
-    set_lexer_state (init_lexer_state ())
-
-let get_comment_state (_,_,_,c) = c
-
 let real_push_char c = Buffer.add_char current_comment c
 
 (* Add a char if it is between two commands, if it is a newline or
@@ -851,6 +835,24 @@ module MakeLexer (Diff : sig val mode : bool end) = struct
   let tok_removing = (fun _ -> ())
   let tok_match = Tok.match_pattern
   let tok_text = token_text
+
+  (* The state of the lexer visible from outside *)
+  module State = struct
+
+    type t = int option * string * bool * ((int * int) * string) list
+
+    let init () = (None,"",true,[])
+    let set (o,s,b,c) =
+      comment_begin := o;
+      Buffer.clear current_comment; Buffer.add_string current_comment s;
+      between_commands := b;
+      comments := c
+    let get () =
+      (!comment_begin, Buffer.contents current_comment, !between_commands, !comments)
+    let drop () = set (init ())
+    let get_comments (_,_,_,c) = c
+
+  end
 end
 
 module Lexer = MakeLexer (struct let mode = false end)
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 2c1284c4db..67b8310bde 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -63,15 +63,6 @@ module Error : sig
   val to_string : t -> string
 end
 
-(* Mainly for comments state, etc... *)
-type lexer_state
-
-val init_lexer_state : unit -> lexer_state
-val set_lexer_state : lexer_state -> unit
-val get_lexer_state : unit -> lexer_state
-val drop_lexer_state : unit -> unit
-val get_comment_state : lexer_state -> ((int * int) * string) list
-
 (** Create a lexer.  true enables alternate handling for computing diffs.
 It ensures that, ignoring white space, the concatenated tokens equal the input
 string.  Specifically:
@@ -81,5 +72,6 @@ as if it was unquoted, possibly becoming multiple tokens
 it was not in a comment, possibly becoming multiple tokens
 - return any unrecognized Ascii or UTF-8 character as a string
 *)
+
 module LexerDiff :
   Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8f3c1e029c..59f92e7790 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -14,77 +14,7 @@ open Genarg
 open Gramlib
 
 (** The parser of Coq *)
-
-module G : sig
-
-  include Grammar.S
-    with type te = Tok.t
-     and type 'c pattern = 'c Tok.p
-
-  val comment_state : Parsable.t -> ((int * int) * string) list
-
-end = struct
-
-  module G_ = Grammar.GMake(CLexer.Lexer)
-
-  type te = G_.te
-  type 'c pattern = 'c G_.pattern
-
-  type coq_parsable = G_.Parsable.t * CLexer.lexer_state ref
-
-  let coq_parsable ?loc c =
-    let state = ref (CLexer.init_lexer_state ()) in
-    CLexer.set_lexer_state !state;
-    let a = G_.Parsable.make ?loc c in
-    state := CLexer.get_lexer_state ();
-    (a,state)
-
-  let comment_state (p,state) =
-    CLexer.get_comment_state !state
-
-  module Parsable = struct
-    type t = coq_parsable
-    let make = coq_parsable
-    (* let comment_state = comment_state *)
-  end
-
-  let tokens = G_.tokens
-
-  type 'a single_extend_statement = 'a G_.single_extend_statement
-  type 'a extend_statement = 'a G_.extend_statement =
-    { pos : Gramlib.Gramext.position option
-    ; data : 'a single_extend_statement list
-    }
-
-  module Entry = struct
-    include G_.Entry
-
-    let parse e (p,state) =
-      CLexer.set_lexer_state !state;
-      try
-        let c = G_.Entry.parse e p in
-        state := CLexer.get_lexer_state ();
-        c
-      with Ploc.Exc (loc,e) ->
-        CLexer.drop_lexer_state ();
-        let loc' = Loc.get_loc (Exninfo.info e) in
-        let loc = match loc' with None -> loc | Some loc -> loc in
-        Loc.raise ~loc e
-
-  end
-
-  module Symbol = G_.Symbol
-  module Rule = G_.Rule
-  module Rules = G_.Rules
-  module Production = G_.Production
-  module Unsafe = G_.Unsafe
-
-  let safe_extend = G_.safe_extend
-  let safe_delete_rule = G_.safe_delete_rule
-  let level_of_nonterm = G_.level_of_nonterm
-  let generalize_symbol = G_.generalize_symbol
-  let mk_rule = G_.mk_rule
-end
+module G = Grammar.GMake(CLexer.Lexer)
 
 module Entry = struct
   include G.Entry
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 0352c1d55b..5d21b39dee 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -15,14 +15,9 @@ open Libnames
 
 (** The parser of Coq *)
 
-module G : sig
-
-  include Gramlib.Grammar.S
-
-  val comment_state : Parsable.t -> ((int * int) * string) list
-
-end with type te = Tok.t and type 'a pattern = 'a Tok.p
+module G : Gramlib.Grammar.S with type te = Tok.t and type 'a pattern = 'a Tok.p
 
+(** Compatibility module, please avoid  *)
 module Entry : sig
   type 'a t = 'a G.Entry.t
   val create : string -> 'a t