- matitacLib: better handling of the callbacks for the dump operation

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

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index aff7895172e705f82c68fe3d71ee38bff21e185a..b33b103c1fcd66a40881e04c06c4f04ff81f0c99 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -63,36 +63,46 @@ let dump f =
    Helm_registry.set_bool "matita.moo" false;
    let floc = H.dummy_floc in
    let nl_ast = G.Comment (floc, G.Note (floc, "")) in
-   let pp_ast_statement st =
+   let pp_statement stm =
      GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
        ~map_unicode_to_tex:(Helm_registry.get_bool
          "matita.paste_unicode_as_tex")
        ~lazy_term_pp:CicNotationPp.pp_term 
-       ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st
+       ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) stm
    in
+   let pp_lexicon = LexiconAstPp.pp_command in
    let och = open_out f in
-   let nl () =  output_string och (pp_ast_statement nl_ast) in
+   let nl () =  output_string och (pp_statement nl_ast) in
    MatitaMisc.out_preamble och;
-   let grafite_parser_cb fname = 
-      let ast = G.Executable 
-        (floc, G.Command (floc, G.Include (floc, fname))) in
-      output_string och (pp_ast_statement ast); nl (); nl ()
+   let grafite_parser_cb status = function
+      | G.Executable (_, G.Macro (_, G.Inline _)) -> ()
+      | stm                                       ->
+         output_string och (pp_statement stm); nl (); nl ()
    in
+   let lexicon_parser_cb status cmd =
+         output_string och (pp_lexicon cmd); nl (); nl ()
+   in
+(*
    let matita_engine_cb = function
       | G.Executable (_, G.Macro (_, G.Inline _)) 
       | G.Executable (_, G.Command (_, G.Include _)) -> ()
       | ast                                          ->
-         output_string och (pp_ast_statement ast); nl (); nl ()
-   in
+*)
    let matitac_lib_cb = output_string och in
-   GrafiteParser.set_callback grafite_parser_cb;
-   MatitaEngine.set_callback matita_engine_cb;
-   set_callback matitac_lib_cb;
-   fun x ->
+   begin fun () ->
+      GrafiteParser.set_grafite_callback grafite_parser_cb;
+      GrafiteParser.set_lexicon_callback lexicon_parser_cb;
+(*   
+      MatitaEngine.set_callback matita_engine_cb;
+*)   
+      set_callback matitac_lib_cb
+   end, 
+   begin fun x ->
       close_out och;
-      GrafiteParser.set_callback ignore;
-      MatitaEngine.set_callback ignore;
+      GrafiteParser.set_grafite_callback (fun _ _ -> ());
+      GrafiteParser.set_lexicon_callback (fun _ _ -> ());
       set_callback ignore; x
+   end
 ;;
 
 let get_macro_context = function
@@ -164,7 +174,7 @@ let activate_extraction baseuri fname =
       flush f; []);
 ;;
 
-let compile options fname =
+let compile atstart options fname =
   let matita_debug = Helm_registry.get_bool "matita.debug" in
   let include_paths = get_include_paths options in
   let root,baseuri,fname,_tgt = 
@@ -175,6 +185,7 @@ let compile options fname =
     CicNotation2.load_notation ~include_paths:[]
       BuildTimeConf.core_notation_script 
   in
+  atstart ();
   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} = 
@@ -302,7 +313,8 @@ let compile options fname =
           let (x, y) = HExtlib.loc_of_floc floc in
           HLog.error (sprintf "Parse error at %d-%d: %s" x y err)
       | exn when matita_debug -> raise exn'
-      | exn -> HLog.error (snd (MatitaExcPp.to_string exn)));
+      | exn -> HLog.error (snd (MatitaExcPp.to_string exn))
+      );
 (*       LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status;
  *       *)
       pp_times fname false big_bang big_bang_u big_bang_s;
@@ -365,11 +377,11 @@ module F =
 
     let build options fname =
       let matita_debug = Helm_registry.get_bool "matita.debug" in
-      let compile opts fname =
+      let compile atstart opts fname =
         try
           GrafiteSync.push ();
           GrafiteParser.push ();
-          let rc = compile opts fname in
+          let rc = compile atstart opts fname in
           GrafiteParser.pop ();
           GrafiteSync.pop ();
           rc
@@ -384,15 +396,15 @@ module F =
       in
       if Filename.check_suffix fname ".mma" then 
          let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
-         let atexit = dump generated in
-         let res = compile options fname in
+         let atstart, atexit = dump generated in
+         let res = compile atstart options fname in
          let r = compact (atexit res) in
          if r then r else begin
-            Sys.remove generated;
+(*            Sys.remove generated; *)
             Printf.printf "rm %s\n" generated; flush stdout; r
          end
       else
-         compile options fname
+         compile ignore options fname
     ;;
 
     let load_deps_file = Librarian.load_deps_file;;