match href_callback with
| None -> ()
| Some f ->
- (match MatitaMisc.split href_value with
+ (match HExtlib.split href_value with
| [ uri ] -> f uri
| uris ->
let menu = GMenu.menu () in
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;
self#_showMath;
match self#script#status.proof_status with
| Proof (uri, metasenv, bo, ty) ->
- let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
+ let name = UriManager.name_of_uri (HExtlib.unopt uri) in
let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
self#_loadObj obj
| Incomplete_proof ((uri, metasenv, bo, ty), _) ->
- let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
+ let name = UriManager.name_of_uri (HExtlib.unopt uri) in
let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
self#_loadObj obj
| _ -> self#blank ()
(** this is what the browser does when you enter a string an hit enter *)
method loadInput txt =
- let txt = MatitaMisc.trim_blanks txt in
+ let txt = HExtlib.trim_blanks txt in
let fix_uri txt =
UriManager.string_of_uri
(UriManager.strip_xpointer (UriManager.uri_of_string txt))