1. matitaEngine splitted into disambiguation (now in grafite_parser) and

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index e4c1072425026c00b3889048fe0d61dddfd66635..6b4afa3cf3e549f9f484ed54c71d14504750965e 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -63,22 +63,22 @@ class console ~(buffer: GText.buffer) () =
         
 let clean_current_baseuri status = 
     try  
-      let baseuri = MatitaTypes.get_string_option status "baseuri" in
+      let baseuri = GrafiteTypes.get_string_option status "baseuri" in
       let basedir = Helm_registry.get "matita.basedir" in
       LibraryClean.clean_baseuris ~basedir [baseuri]
-    with MatitaTypes.Option_error _ -> ()
+    with GrafiteTypes.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 = MatitaMisc.obj_file_of_script ~basedir fname in
+    let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in
      GrafiteMarshal.save_moo moo_fname
-      status.MatitaTypes.moo_content_rev in
+      status.GrafiteTypes.moo_content_rev in
   if (MatitaScript.current ())#eos &&
-     status.MatitaTypes.proof_status = MatitaTypes.No_proof
+     status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
   then
     begin
-      let mooname = MatitaMisc.obj_file_of_script ~basedir fname in
+      let mooname = GrafiteMisc.obj_file_of_script ~basedir fname in
       let rc = 
         MatitaGtkMisc.ask_confirmation
         ~title:"A .moo can be generated"