X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;fp=helm%2Fmatita%2FmatitaGui.ml;h=e4c1072425026c00b3889048fe0d61dddfd66635;hb=0ac236dda6f80f6dc86a7f12d8c88b25e64e3251;hp=3ea6b4f87f8f33d2d1953d305473a8b1254ae681;hpb=7703897d2b14dd101c763a4aa6d99b7cc95011d1;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 3ea6b4f87..e4c107242 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -53,7 +53,7 @@ class console ~(buffer: GText.buffer) () =
     method debug s   = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s
     method clear () =
       buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
-    method log_callback (tag: MatitaLog.log_tag) s =
+    method log_callback (tag: HLog.log_tag) s =
       match tag with
       | `Debug -> self#debug (s ^ "\n")
       | `Error -> self#error (s ^ "\n")
@@ -64,20 +64,21 @@ class console ~(buffer: GText.buffer) () =
 let clean_current_baseuri status = 
     try  
       let baseuri = MatitaTypes.get_string_option status "baseuri" in
-      MatitacleanLib.clean_baseuris [baseuri]
+      let basedir = Helm_registry.get "matita.basedir" in
+      LibraryClean.clean_baseuris ~basedir [baseuri]
     with MatitaTypes.Option_error _ -> ()
 
 let ask_and_save_moo_if_needed parent fname status = 
+  let basedir = Helm_registry.get "matita.basedir" in
   let save () =
-    let moo_fname = MatitacleanLib.obj_file_of_script fname in
-    MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in
+    let moo_fname = MatitaMisc.obj_file_of_script ~basedir fname in
+     GrafiteMarshal.save_moo moo_fname
+      status.MatitaTypes.moo_content_rev in
   if (MatitaScript.current ())#eos &&
      status.MatitaTypes.proof_status = MatitaTypes.No_proof
   then
     begin
-      let mooname = 
-        MatitacleanLib.obj_file_of_script fname
-      in
+      let mooname = MatitaMisc.obj_file_of_script ~basedir fname in
       let rc = 
         MatitaGtkMisc.ask_confirmation
         ~title:"A .moo can be generated"
@@ -471,7 +472,7 @@ class gui () =
               newDevel#toplevel#misc#hide()
             end
           else
-            MatitaLog.error ("The selected root does not contain " ^ 
+            HLog.error ("The selected root does not contain " ^ 
               match next_devel_must_contain with 
               | Some x -> x 
               | _ -> assert false));
@@ -569,7 +570,7 @@ class gui () =
         ~check:main#fullscreenMenuItem;
       main#fullscreenMenuItem#set_active false;
         (* log *)
-      MatitaLog.set_log_callback self#console#log_callback;
+      HLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=
         (fun exn ->
           if not (Helm_registry.get_bool "matita.debug") then
@@ -601,14 +602,14 @@ class gui () =
                  source_buffer#place_cursor
                   (source_buffer#get_iter (`OFFSET x'));
             end;
-            MatitaLog.error msg
+            HLog.error msg
           else raise exn);
         (* script *)
       ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
       let _ =
         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
         | None ->
-            MatitaLog.warn (sprintf "can't load language file %s"
+            HLog.warn (sprintf "can't load language file %s"
               BuildTimeConf.lang_file)
         | Some matita_lang ->
             source_buffer#set_language matita_lang;