diff options
Diffstat (limited to 'toplevel/toplevel.ml')
| -rw-r--r-- | toplevel/toplevel.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index d5321623..cc659e36 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -180,7 +180,7 @@ let print_location_in_file s inlibrary fname loc = str", line " ++ int line ++ str", characters " ++ Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++ fnl () - with e -> + with e when Errors.noncritical e -> (close_in ic; hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ()) @@ -208,7 +208,7 @@ let valid_buffer_loc ib dloc loc = let make_prompt () = try (Names.string_of_id (Pfedit.get_current_proof_name ())) ^ " < " - with _ -> + with Proof_global.NoCurrentProof -> "Coq < " (*let build_pending_list l = @@ -340,7 +340,7 @@ let process_error = function discard_to_dot (); e with | End_of_input -> End_of_input - | de -> if is_pervasive_exn de then de else e + | any -> if is_pervasive_exn any then any else e (* do_vernac reads and executes a toplevel phrase, and print error messages when an exception is raised, except for the following: @@ -354,8 +354,8 @@ let do_vernac () = begin try raw_do_vernac top_buffer.tokens - with e -> - msgnl (print_toplevel_error (process_error e)) + with any -> + msgnl (print_toplevel_error (process_error any)) end; flush_all() @@ -374,6 +374,6 @@ let rec loop () = | Vernacexpr.Drop -> () | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0 | Vernacexpr.Quit -> exit 0 - | e -> + | any -> msgerrnl (str"Anomaly. Please report."); loop () |