added patch to allow agin "match sin ? = ?"

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index ed739eefbebb8c9be4a9e5ab95f919166625a722..7decc583c58ab4b8de1b7a0dab4b49867792bae9 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -66,19 +66,20 @@ 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 ~must_exist:false ~baseuri ~writable:true in
   let save () =
     let metadata_fname =
-     LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
+     LibraryMisc.metadata_file_of_baseuri 
+       ~must_exist:false ~baseuri ~writable:true in
     let lexicon_fname =
-     LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri
+     LibraryMisc.lexicon_file_of_baseuri 
+       ~must_exist:false ~baseuri ~writable:true
     in
      GrafiteMarshal.save_moo moo_fname
       grafite_status.GrafiteTypes.moo_content_rev;
@@ -206,6 +207,11 @@ class gui () =
         ~website:"http://helm.cs.unibo.it"
         ()
       in
+      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 () = 
@@ -467,6 +473,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 
@@ -608,7 +623,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
@@ -1133,7 +1148,7 @@ let interactive_uri_choice
   let gui = instance () in
   let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
   if (selection_mode <> `SINGLE) &&
-    (Helm_registry.get_bool "matita.auto_disambiguation")
+    (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
   then
     Lazy.force nonvars_uris
   else begin