From b8ae2de5be242bbd1e34ec974627c81f99b16d23 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Oct 2016 22:51:09 +0200
Subject: Moving Pp.comments to CLexer so that Pp is purer (no more side-effect
 done by the Ppcmd_comment token) and so that lexing/parsing side-effects are
 collected at the same place, i.e. in CLexer.

---
 printing/ppconstr.ml | 2 +-
 printing/pputils.ml  | 6 +++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index fa5a708995..c94650f1ee 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -129,7 +129,7 @@ end) = struct
     str "`" ++ str hd ++ c ++ str tl
 
   let pr_com_at n =
-    if Flags.do_beautify() && not (Int.equal n 0) then comment n
+    if Flags.do_beautify() && not (Int.equal n 0) then comment (CLexer.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 906b463a85..57a1d957e0 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -11,5 +11,9 @@ open Pp
 let pr_located pr (loc, x) =
   if Flags.do_beautify () && loc <> Loc.ghost then
     let (b, e) = Loc.unloc loc in
-    Pp.comment b ++ pr x ++ Pp.comment e
+    (* Side-effect: order matters *)
+    let before = Pp.comment (CLexer.extract_comments b) in
+    let x = pr x in
+    let after = Pp.comment (CLexer.extract_comments e) in
+    before ++ x ++ after
   else pr x
-- 
cgit v1.2.3