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 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/ppconstr.ml') 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) -- cgit v1.2.3