From b8ae2de5be242bbd1e34ec974627c81f99b16d23 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
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/pputils.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'printing/pputils.ml')

diff --git a/printing/pputils.ml b/printing/pputils.ml
index 906b463a8..57a1d957e 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