6 files changed, 19 insertions, 40 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index e9c6ebfa0..d65b35c46 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -386,16 +386,6 @@ let comments = ref []
 let current_comment = Buffer.create 8192
 let between_commands = ref true
 
-let rec split_comments comacc acc pos = function
-    [] -> comments := List.rev acc; comacc
-  | ((b,e),c as com)::coms ->
-      (* Take all comments that terminates before pos, or begin exactly
-         at pos (used to print comments attached after an expression) *)
-      if e<=pos || pos=b then split_comments (c::comacc) acc pos coms
-      else split_comments comacc (com::acc) pos coms
-
-let extract_comments pos = split_comments [] [] pos !comments
-
 (* The state of the lexer visible from outside *)
 type lexer_state = int option * string * bool * ((int * int) * string) list * Loc.source
 
@@ -406,11 +396,14 @@ let set_lexer_state (o,s,b,c,f) =
   between_commands := b;
   comments := c;
   current_file := f
-let release_lexer_state () =
+let get_lexer_state () =
   (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file)
+let release_lexer_state = get_lexer_state
 let drop_lexer_state () =
     set_lexer_state (init_lexer_state Loc.ToplevelInput)
 
+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
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 58673fefb..a14f08d91 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -53,9 +53,8 @@ type lexer_state
 
 val init_lexer_state : Loc.source -> lexer_state
 val set_lexer_state : lexer_state -> unit
+val get_lexer_state : unit -> lexer_state
 val release_lexer_state : unit -> lexer_state
+[@@ocaml.deprecated "Use get_lexer_state"]
 val drop_lexer_state : unit -> unit
-
-(* Retrieve the comments lexed at a given location of the stream
-   currently being processeed *)
-val extract_comments : int -> string list
+val get_comment_state : lexer_state -> ((int * int) * string) list
diff --git a/parsing/doc.tex b/parsing/doc.tex
deleted file mode 100644
index 68ab601cc..000000000
--- a/parsing/doc.tex
+++ /dev/null
@@ -1,9 +0,0 @@
-
-\newpage
-\section*{The Coq parsers and printers}
-
-\ocwsection \label{parsing}
-This chapter describes the implementation of the \Coq\ parsers and printers.
-
-\bigskip
-\begin{center}\epsfig{file=parsing.dep.ps}\end{center}
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d1abfbe44..595a60f33 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -58,9 +58,7 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function
   | "8.8" -> Current
   | "8.7" -> V8_7
   | "8.6" -> V8_6
-  | "8.5" -> V8_5
-  | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
-    if allow_old then VOld else
+  | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
     CErrors.user_err ~hdr:"get_compat_version"
       Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
   | s ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index bd4495fb4..9aae251f1 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -90,7 +90,9 @@ module type S =
   val entry_create : string -> 'a entry
   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 comment_state : coq_parsable -> ((int * int) * string) list
+
   val srules' : production_rule list -> symbol
   val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
 
@@ -107,13 +109,14 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
       string option * Gramext.g_assoc option * production_rule list
   type extend_statment =
       Gramext.position option * single_extend_statment list
+
   type coq_parsable = parsable * CLexer.lexer_state ref
 
   let parsable ?(file=Loc.ToplevelInput) c =
     let state = ref (CLexer.init_lexer_state file) in
     CLexer.set_lexer_state !state;
     let a = parsable c in
-    state := CLexer.release_lexer_state ();
+    state := CLexer.get_lexer_state ();
     (a,state)
 
   let action = Gramext.action
@@ -123,7 +126,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
     CLexer.set_lexer_state !state;
     try
       let c = Entry.parse e p in
-      state := CLexer.release_lexer_state ();
+      state := CLexer.get_lexer_state ();
       c
     with Ploc.Exc (loc,e) ->
       CLexer.drop_lexer_state ();
@@ -131,15 +134,8 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
       let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
       Loc.raise ~loc e
 
-  let with_parsable (p,state) f x =
-    CLexer.set_lexer_state !state;
-    try
-      let a = f x in
-      state := CLexer.release_lexer_state ();
-      a
-    with e ->
-      CLexer.drop_lexer_state ();
-      raise e
+  let comment_state (p,state) =
+    CLexer.get_comment_state !state
 
   let entry_print ft x = Entry.print ft x
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 9bb8bd31a..8592968dc 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -80,7 +80,9 @@ module type S =
   val entry_create : string -> 'a entry
   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
+
+  (* Get comment parsing information from the Lexer *)
+  val comment_state : coq_parsable -> ((int * int) * string) list
 
   (* Apparently not used *)
   val srules' : production_rule list -> symbol