aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml2
-rw-r--r--printing/pputils.ml6
-rw-r--r--printing/ppvernac.ml8
3 files changed, 10 insertions, 6 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index fa5a70899..c94650f1e 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 33382fe83..491688913 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -17,7 +17,11 @@ open Genredexpr
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
let pr_or_var pr = function
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 7c00106e2..5d7249aff 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -261,7 +261,7 @@ module Make
let pr_decl_notation prc ((loc,ntn),c,scopt) =
fnl () ++ keyword "where " ++ qs ntn ++ str " := "
- ++ Flags.without_option Flags.beautify_file prc c ++
+ ++ Flags.without_option Flags.beautify prc c ++
pr_opt (fun sc -> str ": " ++ str sc) scopt
let pr_binders_arg =
@@ -381,7 +381,7 @@ module Make
| Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}"
let pr_rec_definition ((((loc,id),pl),ro,bl,type_,def),ntn) =
- let pr_pure_lconstr c = Flags.without_option Flags.beautify_file pr_lconstr c in
+ let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
let annot = pr_guard_annot pr_lconstr_expr bl ro in
pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
@@ -676,7 +676,7 @@ module Make
| VernacNotation (_,c,((_,s),l),opt) ->
return (
hov 2 (keyword "Notation" ++ spc() ++ qs s ++
- str " :=" ++ Flags.without_option Flags.beautify_file pr_constrarg c ++ pr_syntax_modifiers l ++
+ str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
(match opt with
| None -> mt()
| Some sc -> str" :" ++ spc() ++ str sc))
@@ -758,7 +758,7 @@ module Make
let pr_constructor (coe,(id,c)) =
hov 2 (pr_lident id ++ str" " ++
(if coe then str":>" else str":") ++
- Flags.without_option Flags.beautify_file pr_spc_lconstr c)
+ Flags.without_option Flags.beautify pr_spc_lconstr c)
in
let pr_constructor_list b l = match l with
| Constructors [] -> mt()