added (placeholder) distribution stuff for matita

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 4ca67368fce43a6d4fe880ad2c75f956f5d518b5..ed739eefbebb8c9be4a9e5ab95f919166625a722 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -607,7 +607,9 @@ class gui () =
         (* log *)
       HLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=
-        (fun exn ->
+        (function 
+        | MatitaScript.ActionCancelled -> () 
+        | exn ->
           if not (Helm_registry.get_bool "matita.debug") then
            let floc, msg = MatitaExcPp.to_string exn in
             begin
@@ -725,12 +727,6 @@ class gui () =
       let top = locker (keep_focus top) in
       let bottom = locker (keep_focus bottom) in
       let jump = locker (keep_focus jump) in
-      let connect_key sym f =
-        connect_key main#mainWinEventBox#event
-          ~modifiers:[`CONTROL] ~stop:true sym f;
-        connect_key self#sourceView#event
-          ~modifiers:[`CONTROL] ~stop:true sym f
-      in
         (* quit *)
       self#setQuitCallback (fun () -> 
         let lexicon_status = (MatitaScript.current ())#lexicon_status in