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

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index aecf026aa6609a50d8359597e0638f449048ed0e..fb7ad27bf6244c2a914dfc418957e760feae75ce 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -134,10 +134,18 @@ let _ =
     in
     addDebugItem "dump aliases" (fun _ ->
       let status = script#lexicon_status in
+      LexiconEngine.dump_aliases HLog.debug "" status);
+(* FG: DEBUGGING   
+    addDebugItem "dump interpretations" (fun _ ->
+      let status = script#lexicon_status in
+      let filter = 
+       List.filter (function LexiconAst.Interpretation _ -> true | _ -> false)
+      in
       HLog.debug (String.concat "\n"
-       (DisambiguateTypes.Environment.fold
-         (fun _ x l -> (LexiconAstPp.pp_alias x)::l)
-         status.LexiconEngine.aliases [])));
+       (List.fold_right
+         (fun x l -> (LexiconAstPp.pp_command x)::l)
+         (filter status.LexiconEngine.lexicon_content_rev) [])));
+*)
     addDebugItem "dump environment to \"env.dump\"" (fun _ ->
       let oc = open_out "env.dump" in
       CicEnvironment.dump_to_channel oc;

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index 5468c863a97f8ac1af856d9f17b7cde2aa850257..cf8d6860b14608d60ef443ce01919a03c1483f8c 100644 (file)
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -119,7 +119,7 @@ let eval_ast ?do_heavy_checks lexicon_status
   ((new_grafite_status,new_lexicon_status),None)::intermediate_states
 
 exception TryingToAdd of string
-exception EnrichedWithLexiconStatus of exn * LexiconEngine.status
+exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status
 
 let out = ref ignore 
 
@@ -173,7 +173,7 @@ let eval_from_stream ~first_statement_only ~include_paths
              watch_statuses lexicon_status grafite_status ;
              false, lexicon_status, grafite_status, (new_statuses @ statuses))
    with exn when not matita_debug ->
-     raise (EnrichedWithLexiconStatus (exn, lexicon_status))
+     raise (EnrichedWithStatus (exn, lexicon_status, grafite_status))
   in
   if stop then s else loop l g s
  in

diff --git a/helm/software/matita/matitaEngine.mli b/helm/software/matita/matitaEngine.mli
index 032ee2c1e18ac904ad9c5ad0c244272a8de2b942..9429b00e6db022f8a4e0a3ed19cefa39e352cc6d 100644 (file)
--- a/helm/software/matita/matitaEngine.mli
+++ b/helm/software/matita/matitaEngine.mli
@@ -38,7 +38,7 @@ val eval_ast :
 (* heavy checks slow down the compilation process but give you some interesting
  * infos like if the theorem is a duplicate *)
 
-exception EnrichedWithLexiconStatus of exn * LexiconEngine.status
+exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status
 
 (* should be used only by the compiler since it looses the
    * disambiguation_context (text,prefix_len,_) *)

diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml
index 7579c3a562841a7da99e3e8280d3a841eb708355..d728fb0b301e0ee9c9b2cdb6b756e749fe8d78af 100644 (file)
--- a/helm/software/matita/matitaExcPp.ml
+++ b/helm/software/matita/matitaExcPp.ml
@@ -165,8 +165,8 @@ let rec to_string =
      None, "Already defined: " ^ UriManager.string_of_uri s
   | DisambiguateChoices.Choice_not_found msg ->
      None, ("Disambiguation choice not found: " ^ Lazy.force msg)
-  | MatitaEngine.EnrichedWithLexiconStatus (exn,_) ->
-     None, "EnrichedWithLexiconStatus "^snd(to_string exn)
+  | MatitaEngine.EnrichedWithStatus (exn,_,_) ->
+     None, "EnrichedWithStatus "^snd(to_string exn)
   | NTacStatus.Error msg ->
      None, "NTactic error: " ^ Lazy.force msg
   | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->

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