Merge PR #6736: [toplevel] Move beautify to its own pass.

4 files changed, 12 insertions, 25 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 52a6fe16c..d7e3751fd 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -384,16 +384,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
 
@@ -410,6 +400,8 @@ 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 5f4e10f14..2d35571f1 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -55,7 +55,4 @@ 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/pcoq.ml b/parsing/pcoq.ml
index 7a51908d9..fec26f941 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -88,7 +88,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
 
@@ -105,6 +107,7 @@ 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 =
@@ -129,15 +132,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.get_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 f36250176..1b330aa04 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -78,7 +78,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