Attaching all extra imperative components of the lexer/parser state to

the state of parsable streams, so that different lexing/parsing
processes can be started independently without conflicting.

Note however that these different lexing/parsing processes cannot be
run concurrently as they still work on the same piece of global memory
(i.e. calls to entry_parse should remain atomic). To go further, one
would typically need to be able to functionally pass the lexing state
to each call to the lexer.

Note that currently the beautifier is also running in the context of a
lexer/parser state (for the mapping of location to comments).

In particular, this fixes #5102 (parsing/lexing of bullets depending on
the lexing state which was global).

3 files changed, 93 insertions, 46 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index bec891f7f1..777cdc9bf7 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -340,34 +340,35 @@ let comm_loc bp = match !comment_begin with
 | None -> comment_begin := Some bp
 | _ -> ()
 
-let current = Buffer.create 8192
-let between_com = ref true
+let current_comment = Buffer.create 8192
+let between_commands = ref true
 
-type com_state = int option * string * bool
-let restore_com_state (o,s,b) =
+type comments_state = int option * string * bool * ((int * int) * string) list
+let restore_comments_state (o,s,b,c) =
   comment_begin := o;
-  Buffer.clear current; Buffer.add_string current s;
-  between_com := b
-let dflt_com = (None,"",true)
-let com_state () =
-  let s = (!comment_begin, Buffer.contents current, !between_com) in
-  restore_com_state dflt_com; s
+  Buffer.clear current_comment; Buffer.add_string current_comment s;
+  between_commands := b;
+  Pp.comments := c
+let default_comments_state = (None,"",true,[])
+let comments_state () =
+  let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !Pp.comments) in
+  restore_comments_state default_comments_state; s
 
-let real_push_char c = Buffer.add_char current 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
    if the last char is not a space itself. *)
 let push_char c =
   if
-    !between_com || List.mem c ['\n';'\r'] ||
+    !between_commands || List.mem c ['\n';'\r'] ||
     (List.mem c [' ';'\t']&&
-     (Int.equal (Buffer.length current) 0 ||
-      not (let s = Buffer.contents current in
+     (Int.equal (Buffer.length current_comment) 0 ||
+      not (let s = Buffer.contents current_comment in
            List.mem s.[String.length s - 1] [' ';'\t';'\n';'\r'])))
   then
     real_push_char c
 
-let push_string s = Buffer.add_string current s
+let push_string s = Buffer.add_string current_comment s
 
 let null_comment s =
   let rec null i =
@@ -375,12 +376,12 @@ let null_comment s =
   null (String.length s - 1)
 
 let comment_stop ep =
-  let current_s = Buffer.contents current in
-  if !Flags.xml_export && Buffer.length current > 0 &&
-    (!between_com || not(null_comment current_s)) then
+  let current_s = Buffer.contents current_comment in
+  if !Flags.xml_export && Buffer.length current_comment > 0 &&
+    (!between_commands || not(null_comment current_s)) then
       Hook.get f_xml_output_comment current_s;
-  (if Flags.do_beautify() && Buffer.length current > 0 &&
-    (!between_com || not(null_comment current_s)) then
+  (if Flags.do_beautify() && Buffer.length current_comment > 0 &&
+    (!between_commands || not(null_comment current_s)) then
     let bp = match !comment_begin with
         Some bp -> bp
       | None ->
@@ -390,9 +391,9 @@ let comment_stop ep =
              ++ int ep);
           ep-1 in
     Pp.comments := ((bp,ep),current_s) :: !Pp.comments);
-  Buffer.clear current;
+  Buffer.clear current_comment;
   comment_begin := None;
-  between_com := false
+  between_commands := false
 
 (* Does not unescape!!! *)
 let rec comm_string loc bp = parser
@@ -548,16 +549,16 @@ let rec next_token loc = parser bp
       | KEYWORD ("." | "...") ->
         if not (blank_or_eof s) then
 	  err (set_loc_pos loc bp (ep+1)) Undefined_token;
-	between_com := true;
+	between_commands := true;
       | _ -> ()
       in
       (t, set_loc_pos loc bp ep)
   | [< ' ('-'|'+'|'*' as c); s >] ->
-      let t,new_between_com =
-        if !between_com then process_sequence loc bp c s, true
+      let t,new_between_commands =
+        if !between_commands then process_sequence loc bp c s, true
         else process_chars loc bp c s,false
       in
-      comment_stop bp; between_com := new_between_com; t
+      comment_stop bp; between_commands := new_between_commands; t
   | [< ''?'; s >] ep ->
       let t = parse_after_qmark loc bp s in
       comment_stop bp; (t, set_loc_pos loc ep bp)
@@ -590,9 +591,9 @@ let rec next_token loc = parser bp
             (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
         | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) ->
             let t = process_chars loc bp (Stream.next s) s in
-            let new_between_com = match t with
-              (KEYWORD ("{"|"}"),_) -> !between_com | _ -> false in
-            comment_stop bp; between_com := new_between_com; t
+            let new_between_commands = match t with
+              (KEYWORD ("{"|"}"),_) -> !between_commands | _ -> false in
+            comment_stop bp; between_commands := new_between_commands; t
         | EmptyStream ->
             comment_stop bp; (EOI, set_loc_pos loc bp (bp+1))
 
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 3b4891d9ac..2c05d6a95f 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -34,10 +34,6 @@ type frozen_t
 val freeze : unit -> frozen_t
 val unfreeze : frozen_t -> unit
 
-type com_state
-val com_state: unit -> com_state
-val restore_com_state: com_state -> unit
-
 val xml_output_comment : (string -> unit) Hook.t
 
 val terminal : string -> Tok.t
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 18bc8d664f..ecf515111c 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -138,12 +138,21 @@ module type LexerSig = sig
     exception E of t
     val to_string : t -> string
   end
+  type comments_state
+  val default_comments_state : comments_state
+  val comments_state : unit -> comments_state
+  val restore_comments_state : comments_state -> unit
 end
 
 ELSE
 
-module type LexerSig =
-  Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
+module type LexerSig = sig
+  include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
+  type comments_state
+  val default_comments_state : comments_state
+  val comments_state : unit -> comments_state
+  val restore_comments_state : comments_state -> unit
+end
 
 END
 
@@ -162,10 +171,13 @@ module type GrammarSig = sig
       string option * Gramext.g_assoc option * production_rule list
   type extend_statment =
       Gramext.position option * single_extend_statment list
+  type coq_parsable
+  val parsable : char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_parse : 'a entry -> coq_parsable -> 'a
   val entry_print : Format.formatter -> 'a entry -> unit
+  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
   val srules' : production_rule list -> symbol
   val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
 end
@@ -181,14 +193,33 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
       string option * Gramext.g_assoc option * production_rule list
   type extend_statment =
       Gramext.position option * single_extend_statment list
+  type coq_parsable = parsable * L.comments_state ref
+  let parsable c =
+    let state = ref L.default_comments_state in (parsable c, state)
   let action = Gramext.action
   let entry_create = Entry.create
-  let entry_parse e p =
-    try Entry.parse e p
+  let entry_parse e (p,state) =
+    L.restore_comments_state !state;
+    try
+      let c = Entry.parse e p in
+      state := L.comments_state ();
+      L.restore_comments_state L.default_comments_state;
+      c
     with Exc_located (loc,e) ->
+      L.restore_comments_state L.default_comments_state;
       let loc' = Loc.get_loc (Exninfo.info e) in
       let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
       Loc.raise loc e
+  let with_parsable (p,state) f x =
+    L.restore_comments_state !state;
+    try
+      let a = f x in
+      state := L.comments_state ();
+      L.restore_comments_state L.default_comments_state;
+      a
+    with e ->
+      L.restore_comments_state L.default_comments_state;
+      raise e
 
   let entry_print ft x = Entry.print ft x
   let srules' = Gramext.srules
@@ -202,12 +233,13 @@ module type GrammarSig = sig
     with module Loc = CompatLoc and type Token.t = Tok.t
   type 'a entry = 'a Entry.t
   type action = Action.t
-  type parsable
-  val parsable : char Stream.t -> parsable
+  type coq_parsable
+  val parsable : char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_parse : 'a entry -> coq_parsable -> 'a
   val entry_print : Format.formatter -> 'a entry -> unit
+  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
   val srules' : production_rule list -> symbol
 end
 
@@ -217,13 +249,31 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
   include Camlp4.Struct.Grammar.Static.Make (L)
   type 'a entry = 'a Entry.t
   type action = Action.t
-  type parsable = char Stream.t
-  let parsable s = s
+  type comments_state = int option * string * bool * ((int * int) * string) list
+  type coq_parsable = char Stream.t * L.comments_state ref
+  let parsable s = let state = ref L.default_comments_state in (s, state)
   let action = Action.mk
   let entry_create = Entry.mk
-  let entry_parse e s =
-    try parse e (*FIXME*)CompatLoc.ghost s
-    with Exc_located (loc,e) -> raise_coq_loc loc e
+  let entry_parse e (s,state) =
+    L.restore_comments_state !state;
+    try
+      let c = parse e (*FIXME*)CompatLoc.ghost s in
+      state := L.comments_state ();
+      L.restore_comments_state L.default_comments_state;
+      c
+    with Exc_located (loc,e) ->
+      L.restore_comments_state L.default_comments_state;
+      raise_coq_loc loc e
+  let with_parsable (p,state) f x =
+    L.restore_comments_state !state;
+    try
+      let a = f x in
+      state := L.comments_state ();
+      L.restore_comments_state L.default_comments_state;
+      a
+    with e ->
+      L.restore_comments_state L.default_comments_state;
+      raise e
   let entry_print ft x = Entry.print ft x
   let srules' = srules (entry_create "dummy")
 end