X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;fp=helm%2Fmatita%2FmatitaGui.ml;h=57076910226043a5e7fe876e512c8394f9362257;hb=5b306342bf9befa57abd870527d6bd92b0a5ba50;hp=16712c4541b77047970d8530b69c165427021340;hpb=64e9baf5488aa0ad2e2d356ef6eb72b8ecb9fca0;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 16712c454..570769102 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -61,24 +61,26 @@ class console ~(buffer: GText.buffer) () =
       | `Warning -> self#warning (s ^ "\n")
   end
         
-let clean_current_baseuri status = 
+let clean_current_baseuri grafite_status = 
     try  
-      let baseuri = GrafiteTypes.get_string_option status "baseuri" in
+      let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
       let basedir = Helm_registry.get "matita.basedir" in
       LibraryClean.clean_baseuris ~basedir [baseuri]
     with GrafiteTypes.Option_error _ -> ()
 
-let ask_and_save_moo_if_needed parent fname status = 
+let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = 
   let basedir = Helm_registry.get "matita.basedir" in
-  let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths:[] fname in
+  let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in
   let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
   let save () =
     let metadata_fname= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
-    GrafiteMarshal.save_moo moo_fname status.GrafiteTypes.moo_content_rev;
-    LibraryNoDb.save_metadata metadata_fname status.GrafiteTypes.metadata
+    GrafiteMarshal.save_moo moo_fname
+     grafite_status.GrafiteTypes.moo_content_rev;
+    LibraryNoDb.save_metadata metadata_fname
+     lexicon_status.LexiconEngine.metadata
   in
   if (MatitaScript.current ())#eos &&
-     status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
+     grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
   then
     begin
       let rc = 
@@ -98,10 +100,10 @@ let ask_and_save_moo_if_needed parent fname status =
       if b then
           save ()
       else
-        clean_current_baseuri status
+        clean_current_baseuri grafite_status
     end
   else
-    clean_current_baseuri status 
+    clean_current_baseuri grafite_status 
     
 let ask_unsaved parent =
   MatitaGtkMisc.ask_confirmation 
@@ -544,7 +546,7 @@ class gui () =
         (* toolbar *)
       let module A = GrafiteAst in
       let hole = CicNotationPt.UserInput in
-      let loc = DisambiguateTypes.dummy_floc in
+      let loc = HExtlib.dummy_floc in
       let tac ast _ =
         if (MatitaScript.current ())#onGoingProof () then
           (MatitaScript.current ())#advance
@@ -664,7 +666,8 @@ class gui () =
               console#message ("'"^f^"' saved.\n");
       in
       let abandon_script () =
-        let status = (s ())#status in
+        let lexicon_status = (s ())#lexicon_status in
+        let grafite_status = (s ())#grafite_status in
         if source_view#buffer#modified then
           (match ask_unsaved main#toplevel with
           | `YES -> saveScript ()
@@ -672,7 +675,9 @@ class gui () =
           | `CANCEL -> raise MatitaTypes.Cancel);
         (match script_fname with
         | None -> ()
-        | Some fname -> ask_and_save_moo_if_needed main#toplevel fname status);
+        | Some fname ->
+           ask_and_save_moo_if_needed main#toplevel fname
+            lexicon_status grafite_status);
       in
       let loadScript () =
         let script = s () in 
@@ -720,7 +725,8 @@ class gui () =
       in
         (* quit *)
       self#setQuitCallback (fun () -> 
-        let status = (MatitaScript.current ())#status in
+        let lexicon_status = (MatitaScript.current ())#lexicon_status in
+        let grafite_status = (MatitaScript.current ())#grafite_status in
         if source_view#buffer#modified then
           begin
             let rc = ask_unsaved main#toplevel in 
@@ -732,8 +738,8 @@ class gui () =
                             (match script_fname with
                             | None -> ()
                             | Some fname -> 
-                               ask_and_save_moo_if_needed 
-                                 main#toplevel fname status);
+                               ask_and_save_moo_if_needed main#toplevel
+                                fname lexicon_status grafite_status);
                           GMain.Main.quit ()
                           end
               | `NO -> GMain.Main.quit ()
@@ -743,10 +749,11 @@ class gui () =
         else 
           begin  
             (match script_fname with
-            | None -> clean_current_baseuri status; GMain.Main.quit ()
+            | None -> clean_current_baseuri grafite_status; GMain.Main.quit ()
             | Some fname ->
                 try
-                  ask_and_save_moo_if_needed main#toplevel fname status;
+                  ask_and_save_moo_if_needed main#toplevel fname lexicon_status
+                   grafite_status;
                   GMain.Main.quit ()
                 with MatitaTypes.Cancel -> ())
           end);
@@ -1260,8 +1267,8 @@ let interactive_interp_choice () choices =
 
 let _ =
   (* disambiguator callbacks *)
-  MatitaDisambiguator.set_choose_uris_callback (interactive_uri_choice ());
-  MatitaDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
+  GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ());
+  GrafiteDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
   (* gtk initialization *)
   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
   GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;