X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=e2274c387162f7b4830c104c0764706406058850;hb=bfb097be2d5aaad276ac8f7d4d82d05c244bc0e7;hp=9cde82b7535501fb100d9a3a121621fff0d1b301;hpb=bdb6fb19553a08101912c28ffb9c882393ccb11f;p=helm.git diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index 9cde82b75..e2274c387 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -66,19 +66,17 @@ class console ~(buffer: GText.buffer) () = let clean_current_baseuri grafite_status = try let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in - let basedir = Helm_registry.get "matita.basedir" in - LibraryClean.clean_baseuris ~basedir [baseuri] + LibraryClean.clean_baseuris [baseuri] with GrafiteTypes.Option_error _ -> () let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = - let basedir = Helm_registry.get "matita.basedir" in let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in - let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in + let moo_fname = LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true in let save () = let metadata_fname = - LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in + LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true in let lexicon_fname = - LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri + LibraryMisc.lexicon_file_of_baseuri ~baseuri ~writable:true in GrafiteMarshal.save_moo moo_fname grafite_status.GrafiteTypes.moo_content_rev; @@ -206,8 +204,11 @@ class gui () = ~website:"http://helm.cs.unibo.it" () in - connect_menu_item main#contentsMenuItem - (fun () -> ignore (Sys.command "gnome-help ghelp:///home/claudio/miohelm/matita/help/C/matita.xml &")); + connect_menu_item main#contentsMenuItem (fun () -> + let cmd = + sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir + in + ignore (Sys.command cmd)); connect_menu_item main#aboutMenuItem about_dialog#present; (* findRepl win *) let show_find_Repl () = @@ -469,6 +470,15 @@ class gui () = (fun () -> MatitamakeLib.clean_development_in_bg refresh d) in ignore(clean ()))); + connect_button develList#publishButton + (locker (fun () -> + match get_devel_selected () with + | None -> () + | Some d -> + let clean = locker + (fun () -> MatitamakeLib.publish_development_in_bg refresh d) + in + ignore(clean ()))); connect_button develList#closeButton (fun () -> develList#toplevel#misc#hide()); ignore(develList#toplevel#event#connect#delete @@ -610,7 +620,7 @@ class gui () = HLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := (function - | MatitaScript.ActionCancelled -> () + | MatitaScript.ActionCancelled s -> HLog.error s | exn -> if not (Helm_registry.get_bool "matita.debug") then let floc, msg = MatitaExcPp.to_string exn in