X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaWiki.ml;h=52d18f42a3ea5d43caaf6856d02d5aabb8377900;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=268da7e51c32142d3305100f27194f3b0576ac40;hpb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;p=helm.git

diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index 268da7e51..52d18f42a 100644
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -64,7 +64,7 @@ let clean_exit n =
   match !grafite_status with
      [] -> exit n
    | grafite_status::_ ->
-       let baseuri = GrafiteTypes.get_baseuri grafite_status in
+       let baseuri = grafite_status#baseuri in
        LibraryClean.clean_baseuris ~verbose:false [baseuri];
        exit n
 
@@ -141,15 +141,14 @@ let rec interactive_loop () =
           grafite_status := drop (to_be_dropped, !grafite_status) ;
           let grafite_status = safe_hd !grafite_status in
            LexiconSync.time_travel
-            ~present:(GrafiteTypes.get_estatus cur_grafite_status)
-            ~past:(GrafiteTypes.get_estatus grafite_status);
-           GrafiteSync.time_travel
             ~present:cur_grafite_status ~past:grafite_status;
+           GrafiteSync.time_travel
+            ~present:cur_grafite_status ~past:grafite_status ();
            interactive_loop (Some n)
     | `Do command ->
         let str = Ulexing.from_utf8_string command in
         let watch_statuses grafite_status =
-         match grafite_status.GrafiteTypes.proof_status with
+         match grafite_status#proof_status with
             GrafiteTypes.Incomplete_proof
              {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
               GrafiteTypes.stack = stack } ->
@@ -225,9 +224,8 @@ let main () =
     let proof_status,moo_content_rev,lexicon_content_rev,dump = 
       match !grafite_status with
       |  s::_ ->
-         s.proof_status, s.moo_content_rev,
-          (GrafiteTypes.get_estatus s)#lstatus.LexiconEngine.lexicon_content_rev,
-          (GrafiteTypes.get_estatus s)#dump
+         s#proof_status, s#moo_content_rev,
+          s#lstatus.LexiconEngine.lexicon_content_rev, s#dump
       | _ -> assert false
     in
     if proof_status <> GrafiteTypes.No_proof then
@@ -239,10 +237,9 @@ let main () =
     else
      begin
        let baseuri =
-        GrafiteTypes.get_baseuri 
-           (match !grafite_status with
-             [] -> assert false
-           | s::_ -> s)
+        (match !grafite_status with
+           [] -> assert false
+         | s::_ -> s)#baseuri
        in
        let moo_fname = 
          LibraryMisc.obj_file_of_baseuri 
@@ -254,7 +251,7 @@ let main () =
        in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
-       NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
+       NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
        exit 0
      end
   with