Merge PR #1106: Fix beautifier

1 files changed, 30 insertions, 31 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b0f021cdc..1b020bc87 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -47,35 +47,29 @@ let beautify_suffix = ".beautified"
 
 let set_formatter_translator ch =
   let out s b e = output_substring ch s b e in
-  Format.set_formatter_output_functions out (fun () -> flush ch);
-  Format.set_max_boxes max_int
+  let ft = Format.make_formatter out (fun () -> flush ch) in
+  Format.pp_set_max_boxes ft max_int;
+  ft
 
-let pr_new_syntax_in_context ?loc chan_beautify ocom =
+let pr_new_syntax_in_context ?loc ft_beautify ocom =
   let loc = Option.cata Loc.unloc (0,0) loc in
-  if !Flags.beautify_file then set_formatter_translator chan_beautify;
   let fs = States.freeze ~marshallable:`No in
-  (* The content of this is not supposed to fail, but if ever *)
-  try
-    (* Side-effect: order matters *)
-    let before = comment (CLexer.extract_comments (fst loc)) in
-    let com = match ocom with
-      | Some com -> Ppvernac.pr_vernac com
-      | None -> mt() in
-    let after = comment (CLexer.extract_comments (snd loc)) in
-    if !Flags.beautify_file then
-      (Pp.pp_with !Topfmt.std_ft (hov 0 (before ++ com ++ after));
-       Format.pp_print_flush !Topfmt.std_ft ())
-    else
-      Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
-    States.unfreeze fs;
-    Format.set_formatter_out_channel stdout
-  with any ->
-    States.unfreeze fs;
-    Format.set_formatter_out_channel stdout
-
-let pr_new_syntax ?loc po chan_beautify ocom =
+  (* Side-effect: order matters *)
+  let before = comment (CLexer.extract_comments (fst loc)) in
+  let com = match ocom with
+    | Some com -> Ppvernac.pr_vernac com
+    | None -> mt() in
+  let after = comment (CLexer.extract_comments (snd loc)) in
+  if !Flags.beautify_file then
+    (Pp.pp_with ft_beautify (hov 0 (before ++ com ++ after));
+     Format.pp_print_flush ft_beautify ())
+  else
+    Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
+  States.unfreeze fs
+
+let pr_new_syntax ?loc po ft_beautify ocom =
   (* Reinstall the context of parsing which includes the bindings of comments to locations *)
-  Pcoq.Gram.with_parsable po (pr_new_syntax_in_context ?loc chan_beautify) ocom
+  Pcoq.Gram.with_parsable po (pr_new_syntax_in_context ?loc ft_beautify) ocom
 
 (* For coqtop -time, we display the position in the file,
    and a glimpse of the executed command *)
@@ -183,8 +177,13 @@ let rec interp_vernac sid (loc,com) =
 
 (* Load a vernac file. CErrors are annotated with file and location *)
 and load_vernac verbosely sid file =
-  let chan_beautify =
-    if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in
+  let ft_beautify, close_beautify =
+    if !Flags.beautify_file then
+      let chan_beautify = open_out (file^beautify_suffix) in
+      set_formatter_translator chan_beautify, fun () -> close_out chan_beautify;
+    else
+      !Topfmt.std_ft, fun () -> ()
+  in
   let in_chan = open_utf8_file_in file in
   let in_echo = if verbosely then Some (open_utf8_file_in file) else None in
   let in_pa   = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
@@ -214,7 +213,7 @@ and load_vernac verbosely sid file =
        *)
       in
       (* Printing of vernacs *)
-      if !Flags.beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast);
+      if !Flags.beautify then pr_new_syntax ?loc in_pa ft_beautify (Some ast);
       Option.iter (vernac_echo ?loc) in_echo;
 
       checknav_simple (loc, ast);
@@ -230,11 +229,11 @@ and load_vernac verbosely sid file =
       | Stm.End_of_input ->
           (* Is this called so comments at EOF are printed? *)
           if !Flags.beautify then
-            pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa chan_beautify None;
-          if !Flags.beautify_file then close_out chan_beautify;
+            pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa ft_beautify None;
+          if !Flags.beautify_file then close_beautify ();
           !rsid
       | reraise ->
-         if !Flags.beautify_file then close_out chan_beautify;
+         if !Flags.beautify_file then close_beautify ();
 	 iraise (disable_drop e, info)
 
 (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit]