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 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 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 From 96ed527472c38e92727d8fb6bfc41770c43b762b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 11 Oct 2016 22:11:16 +0200 Subject: Fixing a few confusions on the name of the beautify flag. (It should apply also interactively.) --- interp/constrextern.ml | 2 +- printing/ppvernac.ml | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'printing') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e71daef99..afc1c4caf 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -481,7 +481,7 @@ let explicitize loc inctx impl (cf,f) args = (!print_implicits && !print_implicits_explicit_args) || (is_needed_for_correct_partial_application tail imp) || (!print_implicits_defensive && - (not (is_inferable_implicit inctx n imp) || !Flags.beautify_file) && + (not (is_inferable_implicit inctx n imp) || !Flags.beautify) && is_significant_implicit (Lazy.force a)) in if visible then diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f4a112a4c..cfb4e79f0 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -263,7 +263,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 = @@ -383,7 +383,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_ @@ -678,7 +678,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)) @@ -760,7 +760,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() -- cgit v1.2.3