X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteSync.ml;h=999d961369324bd1c3be5df1661e244982cce0f1;hb=916c558005ed665c62699a7a4c5347870c8a3efb;hp=c1b23c9281697c18c3ac5d6ad8c0b5431fc0abf9;hpb=84e6cbe962c9a534be48542c098d7bb0d90be9a1;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml
index c1b23c928..999d96136 100644
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/components/grafite_engine/grafiteSync.ml
@@ -77,12 +77,13 @@ let add_obj ~pack_coercion_obj uri obj status =
  in
  let universe,status =
    List.fold_left add_to_universe 
-     (status.GrafiteTypes.universe,status) 
+     (status.GrafiteTypes.automation_cache.AutomationCache.univ,status) 
      uris_to_index 
  in
+ let cache = { status.GrafiteTypes.automation_cache with AutomationCache.univ = universe } in
   {status with 
      GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects;
-     GrafiteTypes.universe = universe},
+     GrafiteTypes.automation_cache = cache },
    lemmas
 
 let add_coercion ~pack_coercion_obj ~add_composites status uri arity
@@ -115,13 +116,14 @@ let time_travel ~present ~past =
   CoercDb.restore past.GrafiteTypes.coercions;
 ;;
 
-let initial_status baseuri = {
+let initial_status lexicon_status baseuri = {
     GrafiteTypes.moo_content_rev = [];
     proof_status = GrafiteTypes.No_proof;
     objects = [];
     coercions = CoercDb.empty_coerc_db;
-    universe = Universe.empty;
+    automation_cache = AutomationCache.empty;
     baseuri = baseuri;
+    ng_status = GrafiteTypes.CommandMode lexicon_status;
   }