X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=ed739eefbebb8c9be4a9e5ab95f919166625a722;hb=112afe13b5aef27425d1a0bc9c71a70b491069bf;hp=a10493fca8588fd497e92b8a13a4911e3d1bee97;hpb=aa0d60227b785da3355b31519ba11cb4fbd2c925;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index a10493fca..ed739eefb 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -75,11 +75,17 @@ let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status =
   let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in
   let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
   let save () =
-    let metadata_fname= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
-    GrafiteMarshal.save_moo moo_fname
-     grafite_status.GrafiteTypes.moo_content_rev;
-    LibraryNoDb.save_metadata metadata_fname
-     lexicon_status.LexiconEngine.metadata
+    let metadata_fname =
+     LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
+    let lexicon_fname =
+     LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri
+    in
+     GrafiteMarshal.save_moo moo_fname
+      grafite_status.GrafiteTypes.moo_content_rev;
+     LibraryNoDb.save_metadata metadata_fname
+      lexicon_status.LexiconEngine.metadata;
+     LexiconMarshal.save_lexicon lexicon_fname
+      lexicon_status.LexiconEngine.lexicon_content_rev
   in
   if (MatitaScript.current ())#eos &&
      grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
@@ -601,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
@@ -719,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