diff options
author | 2018-03-04 17:10:23 +0100 | |
---|---|---|
committer | 2018-03-04 17:10:23 +0100 | |
commit | dffc6a20eb1a0636904164e00b5963ed96f774c4 (patch) | |
tree | 138b1c0a86f27cc3d29a65b77d7ca0335cd1dbcd /printing/pputils.ml | |
parent | b3a8761790c0905aad8e5d3102fab606fe5e7fd6 (diff) | |
parent | 2a64471512ee7dcd6d6c65cd5a792344628616f0 (diff) |
Merge PR #6736: [toplevel] Move beautify to its own pass.
Diffstat (limited to 'printing/pputils.ml')
-rw-r--r-- | printing/pputils.ml | 16 |
1 files changed, 14 insertions, 2 deletions
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 |