huge commit regarding the grafite_status:

[helm.git] / helm / software / matita / matitacLib.ml

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 1276300b10bd117d367ade15f9a95ab6c840cc44..a4e879a36e985432df1ac7c16e3914702e924735 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -226,18 +226,19 @@ let compile atstart options fname =
       if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
       else pp_ast_statement
     in
-    let lexicon_status, grafite_status =
-     let rec aux_for_dump x lexicon_status grafite_status =
+    let grafite_status =
+     let rec aux_for_dump x grafite_status =
      try
       match
        MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
-        lexicon_status grafite_status buf x
+        grafite_status buf x
       with
-      | [] -> lexicon_status, grafite_status
-      | ((grafite,lexicon),None)::_ -> lexicon, grafite
-      | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l)
+      | [] -> grafite_status
+      | (g,None)::_ -> g
+      | (g,Some _)::_ -> 
+            raise (AttemptToInsertAnAlias (GrafiteTypes.get_lexicon g))
      with MatitaEngine.EnrichedWithStatus 
-            (GrafiteEngine.Macro (floc, f), lexicon, grafite) as exn ->
+            (GrafiteEngine.Macro (floc, f), grafite) as exn ->
             match f (get_macro_context (Some grafite)) with 
             | _, GrafiteAst.Inline (_, _suri, _params) ->
 (*              
@@ -249,15 +250,15 @@ let compile atstart options fname =
              in
               !out str;
 *)
-              aux_for_dump x lexicon grafite
+              aux_for_dump x grafite
             |_-> raise exn
      in
-       aux_for_dump print_cb lexicon_status grafite_status
+       aux_for_dump print_cb grafite_status
     in
     let elapsed = Unix.time () -. time in
     let proof_status,moo_content_rev,lexicon_content_rev = 
       grafite_status.proof_status, grafite_status.moo_content_rev, 
-       lexicon_status.LexiconEngine.lexicon_content_rev
+       (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev
     in
     if proof_status <> GrafiteTypes.No_proof then
      (HLog.error
@@ -299,7 +300,7 @@ let compile atstart options fname =
        ~present:lexicon_status ~past:initial_lexicon_status;
 *)
      clean_exit baseuri false
-  | MatitaEngine.EnrichedWithStatus (exn, _lexicon, _grafite) as exn' ->
+  | MatitaEngine.EnrichedWithStatus (exn, _grafite) as exn' ->
       (match exn with
       | Sys.Break -> HLog.error "user break!"
       | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->