X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitacLib.ml;h=b3b95325acc8a66ec7fc7e6c5237538975fb7078;hb=7477c3dbbc2fafe248d48302be0d6ba4cb38d062;hp=a4e879a36e985432df1ac7c16e3914702e924735;hpb=dcdbb979433a61e2ef2842d96604098728824416;p=helm.git

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index a4e879a36..b3b95325a 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -29,7 +29,7 @@ open Printf
 
 open GrafiteTypes
 
-exception AttemptToInsertAnAlias of LexiconEngine.status
+exception AttemptToInsertAnAlias of #LexiconEngine.status
 
 let slash_n_RE = Pcre.regexp "\\n" ;;
 
@@ -175,7 +175,7 @@ let compile atstart options fname =
   if Http_getter_storage.is_read_only baseuri then assert false;
   activate_extraction baseuri fname ;
   let lexicon_status = 
-    CicNotation2.load_notation ~include_paths:[]
+    CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status)
       BuildTimeConf.core_notation_script 
   in
   atstart (); (* FG: do not invoke before loading the core notation script *)  
@@ -236,7 +236,7 @@ let compile atstart options fname =
       | [] -> grafite_status
       | (g,None)::_ -> g
       | (g,Some _)::_ -> 
-            raise (AttemptToInsertAnAlias (GrafiteTypes.get_lexicon g))
+            raise (AttemptToInsertAnAlias (GrafiteTypes.get_estatus g))
      with MatitaEngine.EnrichedWithStatus 
             (GrafiteEngine.Macro (floc, f), grafite) as exn ->
             match f (get_macro_context (Some grafite)) with 
@@ -258,7 +258,7 @@ let compile atstart options fname =
     let elapsed = Unix.time () -. time in
     let proof_status,moo_content_rev,lexicon_content_rev = 
       grafite_status.proof_status, grafite_status.moo_content_rev, 
-       (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev
+       (GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev
     in
     if proof_status <> GrafiteTypes.No_proof then
      (HLog.error
@@ -274,6 +274,8 @@ let compile atstart options fname =
         (* FG: we do not generate .moo when dumping .mma files *)
         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)
+         (GrafiteTypes.get_estatus grafite_status)#dump
      end;
      let tm = Unix.gmtime elapsed in
      let sec = string_of_int tm.Unix.tm_sec ^ "''" in