From 2a64471512ee7dcd6d6c65cd5a792344628616f0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sun, 11 Feb 2018 19:42:14 +0100
Subject: [toplevel] Move beautify to its own pass.

We first load the file, then we print it as a post-processing
step. This is both more flexible and clearer.

We also refactor the comments handling to minimize the logic that is
living in the Lexer. Indeed, the main API is now living in the
printer, and complex interactions with the state are not possible
anymore, including the removal of messing with low-level summary and
state setting!
---
 printing/ppconstr.ml |  2 +-
 printing/pputils.ml  | 16 ++++++++++++++--
 printing/pputils.mli |  6 ++++++
 3 files changed, 21 insertions(+), 3 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 3c7095505..0d84e1b9e 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
-- 
cgit v1.2.3