X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=a3d35c8e1129081de4c82de57706350f23b3cb74;hb=5a702cea95883f7095c16b450e065ccb1714fc5a;hp=153d474abe09b6a5e22baff307ebcaac3cc0283a;hpb=487210b76da19b0d2b3cea37aab7b71ad4e0abf2;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 153d474ab..a3d35c8e1 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -171,9 +171,7 @@ class gui () = (*~comments:"comments"*) ~copyright:"Copyright (C) 2005, the HELM team" ~license:(String.concat "\n" (parse_txt_file "LICENSE")) - ~logo: - (GdkPixbuf.from_file - (BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png")) + ~logo:(GdkPixbuf.from_file (MatitaMisc.image_path "/matita_medium.png")) ~name:"Matita" ~version:BuildTimeConf.version ~website:"http://helm.cs.unibo.it" @@ -606,19 +604,19 @@ class gui () = let script = s () in let status = script#status in try - if source_view#buffer#modified then - begin - match ask_unsaved main#toplevel with - | `YES -> saveScript () - | `NO -> () - | `CANCEL -> raise MatitaTypes.Cancel - end; - (match script_fname with - | None -> () - | Some fname -> - ask_and_save_moo_if_needed main#toplevel fname status); match self#chooseFile () with | Some f -> + if source_view#buffer#modified then + begin + match ask_unsaved main#toplevel with + | `YES -> saveScript () + | `NO -> () + | `CANCEL -> raise MatitaTypes.Cancel + end; + (match script_fname with + | None -> () + | Some fname -> + ask_and_save_moo_if_needed main#toplevel fname status); script#reset (); script#assignFileName f; source_view#source_buffer#begin_not_undoable_action ();