- matitacLib: lexicon status and grafite status where lost after handling a macro...

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

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index b33b103c1fcd66a40881e04c06c4f04ff81f0c99..7a6d48663927cf590837a30b3516b7677a5f11b8 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -185,7 +185,7 @@ let compile atstart options fname =
     CicNotation2.load_notation ~include_paths:[]
       BuildTimeConf.core_notation_script 
   in
-  atstart ();
+  atstart (); (* FG: do not invoke before loading the core notation script *)  
   let grafite_status = GrafiteSync.init lexicon_status baseuri in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
@@ -233,20 +233,20 @@ let compile atstart options fname =
       if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
       else pp_ast_statement
     in
-    let grafite_status, lexicon_status =
-     let rec aux_for_dump x =
+    let lexicon_status, grafite_status =
+     let rec aux_for_dump x lexicon_status grafite_status =
      try
       match
        MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
         lexicon_status grafite_status buf x
       with
-      | [] -> grafite_status, lexicon_status 
-      | ((grafite,lexicon),None)::_ -> grafite, lexicon
+      | [] -> lexicon_status, grafite_status
+      | ((grafite,lexicon),None)::_ -> lexicon, grafite
       | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l)
 
-     with MatitaEngine.EnrichedWithLexiconStatus 
-            (GrafiteEngine.Macro (floc, f), lex_status) as exn ->
-            match f (get_macro_context (Some grafite_status)) with 
+     with MatitaEngine.EnrichedWithStatus 
+            (GrafiteEngine.Macro (floc, f), lexicon, grafite) as exn ->
+            match f (get_macro_context (Some grafite)) with 
             | _, GrafiteAst.Inline (_, style, suri, prefix, flavour) ->
               let str =
                ApplyTransformation.txt_of_inline_macro style prefix suri
@@ -255,10 +255,10 @@ let compile atstart options fname =
                   "matita.paste_unicode_as_tex")
              in
               !out str;
-              aux_for_dump x
+              aux_for_dump x lexicon grafite
             |_-> raise exn
      in
-       aux_for_dump print_cb
+       aux_for_dump print_cb lexicon_status grafite_status
     in
     let elapsed = Unix.time () -. time in
     let proof_status,moo_content_rev,lexicon_content_rev = 
@@ -306,7 +306,7 @@ let compile atstart options fname =
        ~present:lexicon_status ~past:initial_lexicon_status;
 *)
      clean_exit baseuri false
-  | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) as exn' ->
+  | MatitaEngine.EnrichedWithStatus (exn, _lexicon, _grafite) as exn' ->
       (match exn with
       | Sys.Break -> HLog.error "user break!"
       | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
@@ -315,7 +315,7 @@ let compile atstart options fname =
       | exn when matita_debug -> raise exn'
       | exn -> HLog.error (snd (MatitaExcPp.to_string exn))
       );
-(*       LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status;
+(*       LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
  *       *)
       pp_times fname false big_bang big_bang_u big_bang_s;
       clean_exit baseuri false