From 29a5b18f3da1a3ed648f23709384b7789cb099bf Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 19 Sep 2005 12:42:27 +0000 Subject: [PATCH] - avoid catching top level exceptions when the relevant setting in the registry is set - removed some ancient debugging prints --- helm/matita/matitaGui.ml | 9 +++++---- helm/matita/matitaMathView.ml | 10 ++++++---- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index a3d35c8e1..e0ca8c681 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -566,7 +566,10 @@ class gui () = (* log *) MatitaLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := - (fun exn -> MatitaLog.error (MatitaExcPp.to_string exn)); + (fun exn -> + if Helm_registry.get_bool "matita.catch_top_level_exn" then + MatitaLog.error (MatitaExcPp.to_string exn) + else raise exn); (* script *) let _ = match GSourceView.source_language_from_file BuildTimeConf.lang_file with @@ -1055,9 +1058,7 @@ let interactive_interp_choice () choices = let selection = dialog#interpChoiceTreeView#selection in ignore (selection#connect#changed (fun _ -> match selection#get_selected_rows with - | [path] -> - MatitaLog.debug (sprintf "selection: %d" (model#get_interp_no path)); - interp_no := Some (model#get_interp_no path) + | [path] -> interp_no := Some (model#get_interp_no path) | _ -> assert false)); dialog#interpChoiceDialog#show (); GtkThread.main (); diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 43547b8ff..28bd1caaa 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -590,7 +590,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 ( @@ -701,7 +704,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (* 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 @@ -717,8 +720,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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; -- 2.39.2