diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-09-27 18:41:09 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-09-27 18:44:41 +0200 |
commit | ca9c0a1d3aa4a2c2dad3d5e5ff88b9bc324e71db (patch) | |
tree | effa9eda2dc2d3fc2bc502cd1256390def2a88a0 /toplevel/vernac.ml | |
parent | fb0c6f696b769b1a7348a7c777947cbae5dea356 (diff) |
Remove catch-all try with in the beautifier.
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r-- | toplevel/vernac.ml | 28 |
1 files changed, 12 insertions, 16 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 6864618dd..bc536ddec 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -54,22 +54,18 @@ let set_formatter_translator ch = let pr_new_syntax_in_context ?loc ft_beautify ocom = let loc = Option.cata Loc.unloc (0,0) loc in 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 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 - with any -> - States.unfreeze fs + (* 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 *) |