X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=e9a84c9b475179cd4b588388a511bda3959ebddb;hb=a89868740968d139dd4e1d621663bcd4d69d0265;hp=34406a3cd147908ef96d76a9804ecafc3064815f;hpb=d39571d4fed32b6db8c355189bb099e2837eaf9c;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 34406a3cd..e9a84c9b4 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/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
@@ -875,11 +890,12 @@ class gui () =
     method private nextLigature () =
       let iter = source_buffer#get_iter_at_mark `INSERT in
       let write_ligature len s =
+        assert(Glib.Utf8.validate s);
         source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars len);
         source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s
       in
       let get_ligature word =
-        let len = String.length word in
+        let len = MatitaGtkMisc.utf8_string_length word in
         let aux_tex () =
           try
             for i = len - 1 downto 0 do
@@ -918,7 +934,7 @@ class gui () =
           (match CicNotationLexer.lookup_ligatures ligature with
           | [] -> ()
           | hd :: tl ->
-              write_ligature (String.length ligature) hd;
+              write_ligature (MatitaGtkMisc.utf8_string_length ligature) hd;
               next_ligatures <- tl @ [ hd ])
       | hd :: tl ->
           write_ligature 1 hd;