diff options
| author | Emilio Jesus Gallego Arias | 2020-03-01 02:49:04 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-08 00:44:58 -0500 |
| commit | 4ba8fabb14256cdc65e8440362d6697d9e97b7f4 (patch) | |
| tree | 6dc6168679e8b48127decd32823afa39ac77355c /vernac | |
| parent | dbd3a4c4213b3d56908a8387de93e27aaec501a4 (diff) | |
[exn] [nit] Remove not very useful re-raises.
Cleanup: IMHO most of the re-raises here are not worth it.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacextend.ml | 24 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 9 |
2 files changed, 10 insertions, 23 deletions
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index e0afb7f483..5d38ea32be 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -92,28 +92,18 @@ let warn_deprecated_command = (* Interpretation of a vernac command *) let type_vernac opn converted_args ~atts = - let phase = ref "Looking up command" in - try - let depr, callback = vinterp_map opn in - let () = if depr then + let depr, callback = vinterp_map opn in + let () = if depr then let rules = Egramml.get_extend_vernac_rule opn in let pr_gram = function - | Egramml.GramTerminal s -> str s - | Egramml.GramNonTerminal _ -> str "_" + | Egramml.GramTerminal s -> str s + | Egramml.GramNonTerminal _ -> str "_" in let pr = pr_sequence pr_gram rules in warn_deprecated_command pr; - in - phase := "Checking arguments"; - let hunk = callback converted_args in - phase := "Executing command"; - hunk ~atts - with - | reraise -> - let reraise = Exninfo.capture reraise in - if !Flags.debug then - Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); - Exninfo.iraise reraise + in + let hunk = callback converted_args in + hunk ~atts (** VERNAC EXTEND registering *) diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 59557a60a6..280343f315 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -18,12 +18,9 @@ module Parser = struct let parse ps entry pa = Pcoq.unfreeze ps; - Flags.with_option Flags.we_are_parsing (fun () -> - try Pcoq.Entry.parse entry pa - with e when CErrors.noncritical e -> - let (e, info) = Exninfo.capture e in - Exninfo.iraise (e, info)) - () + Flags.with_option Flags.we_are_parsing + (fun () -> Pcoq.Entry.parse entry pa) + () end |
