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

3 files changed, 21 insertions, 3 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index dedad1990..da1fe6d3d 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -149,7 +149,7 @@ let tag_var = tag Tag.variable
     str "`" ++ str hd ++ c ++ str tl
 
   let pr_com_at n =
-    if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n)
+    if !Flags.beautify && not (Int.equal n 0) then comment (Pputils.extract_comments n)
     else mt()
 
   let pr_with_comments ?loc pp = pr_located (fun x -> x) (loc, pp)
diff --git a/printing/pputils.ml b/printing/pputils.ml
index e779fc5fc..3d72c8da3 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -13,14 +13,26 @@ open Misctypes
 open Locus
 open Genredexpr
 
+let beautify_comments = ref []
+
+let rec split_comments comacc acc pos = function
+  | [] -> beautify_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 !beautify_comments
+
 let pr_located pr (loc, x) =
   match loc with
   | Some loc when !Flags.beautify ->
     let (b, e) = Loc.unloc loc in
     (* Side-effect: order matters *)
-    let before = Pp.comment (CLexer.extract_comments b) in
+    let before = Pp.comment (extract_comments b) in
     let x = pr x in
-    let after = Pp.comment (CLexer.extract_comments e) in
+    let after = Pp.comment (extract_comments e) in
     before ++ x ++ after
   | _ -> pr x
 
diff --git a/printing/pputils.mli b/printing/pputils.mli
index ec5c32fc4..483bd0ae3 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -37,3 +37,9 @@ val pr_red_expr_env : Environ.env -> Evd.evar_map ->
 
 val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t
 val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t
+
+(* The comments interface is imperative due to the printer not
+   threading it, this could be solved using a better data
+   structure. *)
+val beautify_comments : ((int * int) * string) list ref
+val extract_comments : int -> string list