aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-09-27 18:41:09 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-09-27 18:44:41 +0200
commitca9c0a1d3aa4a2c2dad3d5e5ff88b9bc324e71db (patch)
treeeffa9eda2dc2d3fc2bc502cd1256390def2a88a0 /toplevel/vernac.ml
parentfb0c6f696b769b1a7348a7c777947cbae5dea356 (diff)
Remove catch-all try with in the beautifier.
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r--toplevel/vernac.ml28
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 *)