let handle_error f =
try
f ()
- with exn -> fail (MatitaExcPp.to_string exn)
+ with exn ->
+ if Helm_registry.get_bool "matita.catch_top_level_exn" then
+ fail (MatitaExcPp.to_string exn)
+ else raise exn
in
let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
let load_easter_egg = lazy (
(* loads a uri which can be a cic uri or an about:* uri
* @param uri string *)
method private _load ?(force=false) entry =
- try
+ handle_error (fun () ->
if entry <> current_entry || entry = `About `Current_proof || force then
begin
(match entry with
self#_loadList (List.map (fun r -> "obj",
UriManager.string_of_uri r) results));
self#setEntry entry
- end
- with exn -> fail (MatitaExcPp.to_string exn)
+ end)
method private blank () =
self#_showMath;