diff options
| -rw-r--r-- | toplevel/coqloop.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 31 |
2 files changed, 17 insertions, 15 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 08c3fe205..ea7539fce 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -308,7 +308,6 @@ let do_vernac () = else Feedback.msg_error (str"There is no ML toplevel.") | any -> let any = CErrors.push any in - Format.set_formatter_out_channel stdout; let msg = print_toplevel_error any ++ fnl () in pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg; Format.pp_print_flush !Pp_control.std_ft () diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7ff93e44e..46c6c66aa 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -127,18 +127,23 @@ let pr_new_syntax_in_context loc chan_beautify ocom = let loc = Loc.unloc loc in if !beautify_file then set_formatter_translator chan_beautify; let fs = States.freeze ~marshallable:`No in - (* 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 !beautify_file then - Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after)) - else - Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); - States.unfreeze fs; - Format.set_formatter_out_channel stdout + (* 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 !beautify_file then + Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after)) + 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 po loc chan_beautify ocom = (* Reinstall the context of parsing which includes the bindings of comments to locations *) @@ -193,7 +198,6 @@ let rec vernac_com po chan_beautify checknav (loc,com) = interp com with reraise -> let (reraise, info) = CErrors.push reraise in - Format.set_formatter_out_channel stdout; let loc' = Option.default Loc.ghost (Loc.get_loc info) in if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc) else iraise (reraise, info) @@ -214,7 +218,6 @@ and read_vernac_file verbosely chan_beautify s = done with any -> (* whatever the exception *) let (e, info) = CErrors.push any in - Format.set_formatter_out_channel stdout; close_input in_chan input; (* we must close the file first *) match e with | End_of_input -> |