X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitacLib.ml;h=36f7cda6dc9d059bb22a14324dfbdd3febdc00f5;hb=779859f7a9e317e378d258897c289f447adea7ad;hp=5a14b2703bc8a24843bb25ff9f3ddda91b6b99a1;hpb=c81b4f59a7f58dc1e6c3ea1fc792bcce6234f866;p=helm.git

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 5a14b2703..36f7cda6d 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" ;;
 
@@ -69,19 +69,19 @@ let dump f =
    let och = open_out f in
    let nl () =  output_string och (pp_statement nl_ast) in
    MatitaMisc.out_preamble och;
-   let grafite_parser_cb status = function
-      | G.Executable (_, G.Macro (_, G.Inline (_, style, uri, prefix, flavour))) ->
+   let grafite_parser_cb = function
+      | G.Executable (_, G.Macro (_, G.Inline (_, uri, params))) ->
          let str =
-            ApplyTransformation.txt_of_inline_macro style prefix uri
-               ?flavour
+            ApplyTransformation.txt_of_inline_macro params uri
 	       ~map_unicode_to_tex:
 	          (Helm_registry.get_bool "matita.paste_unicode_as_tex")
 	 in
          output_string och str
+      | G.Executable (loc, G.Command (_, G.Include (_, false, _))) -> ()
       | stm ->
          output_string och (pp_statement stm); nl (); nl ()
    in
-   let lexicon_parser_cb status cmd =
+   let lexicon_parser_cb cmd =
          output_string och (pp_lexicon cmd); nl (); nl ()
    in
    begin fun () ->
@@ -91,15 +91,15 @@ let dump f =
    end, 
    begin fun x ->
       close_out och;
-      GrafiteParser.set_grafite_callback (fun _ _ -> ());
-      GrafiteParser.set_lexicon_callback (fun _ _ -> ());
+      GrafiteParser.set_grafite_callback (fun _ -> ());
+      GrafiteParser.set_lexicon_callback (fun _ -> ());
       Helm_registry.set_bool "matita.moo" true;
       x
    end
 ;;
 
 let get_macro_context = function
-   | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> []
+   | Some status when status#proof_status = GrafiteTypes.No_proof -> []
    | Some status                ->
       let stack = GrafiteTypes.get_stack status in
       let goal = Continuationals.Stack.find_goal stack in
@@ -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 *)  
@@ -226,20 +226,20 @@ 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 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 (_, style, suri, prefix, flavour) ->
+            | _, GrafiteAst.Inline (_, _suri, _params) ->
 (*              
 	      let str =
                ApplyTransformation.txt_of_inline_macro style prefix suri
@@ -249,15 +249,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
+      grafite_status#proof_status, grafite_status#moo_content_rev, 
+       grafite_status#lstatus.LexiconEngine.lexicon_content_rev
     in
     if proof_status <> GrafiteTypes.No_proof then
      (HLog.error
@@ -273,6 +273,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)
+         grafite_status#dump
      end;
      let tm = Unix.gmtime elapsed in
      let sec = string_of_int tm.Unix.tm_sec ^ "''" in
@@ -299,7 +301,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) ->
@@ -397,7 +399,7 @@ module F =
             Printf.printf "rm %s\n" generated; flush stdout; r
          end
       else
-         compile ignore options fname
+         compact (compile ignore options fname)
     ;;
 
     let load_deps_file = Librarian.load_deps_file;;