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
(* 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
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