X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitacLib.ml;h=99c132c11d27cf2a6f951ef71087bc26aadaf172;hb=6a5e51c1cf9a56c74a8b53a9b8bc5aa686c9780e;hp=9c836d9b87a777298fa697fe0196ef338a6ddf91;hpb=c0731d1fa3ae894da2473541a759d48e9b76613a;p=helm.git

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 9c836d9b8..99c132c11 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -34,6 +34,7 @@ exception AttemptToInsertAnAlias of LexiconEngine.status
 let out = ref ignore 
 let set_callback f = out := f
 
+
 let slash_n_RE = Pcre.regexp "\\n" ;;
 
 let pp_ast_statement grafite_status stm =
@@ -55,6 +56,67 @@ let clean_exit baseuri rc =
   LibraryClean.clean_baseuris ~verbose:false [baseuri]; rc
 ;;
 
+let dump f =
+   let module G = GrafiteAst in
+   let module L = LexiconAst in
+   let module H = HExtlib in
+   Helm_registry.set_bool "matita.moo" false;
+   let floc = H.dummy_floc in
+   let nl_ast = G.Comment (floc, G.Note (floc, "")) in
+   let och = open_out f in
+   let out_comment och s =
+      let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in 
+      Printf.fprintf och "%s%s%s\n\n" "(*" s "*)"
+   in
+   let out_line_comment och s =
+      let l = 70 - String.length s in
+      let s = Printf.sprintf " %s %s" s (String.make l '*') in
+      out_comment och s
+   in
+   let out_preamble och (path, lines) =
+      let ich = open_in path in
+      let rec print i =
+         if i > 0 then 
+            let s = input_line ich in
+            begin Printf.fprintf och "%s\n" s; print (pred i) end
+      in 
+      print lines;
+      out_line_comment och "This file was automatically generated: do not edit"
+   in
+   let pp_ast_statement st =
+     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
+   in
+   let nl () =  output_string och (pp_ast_statement nl_ast) in
+   let rt_base_dir = Filename.dirname Sys.argv.(0) in
+   let path = Filename.concat rt_base_dir "matita.ma.templ" in
+   let lines = 14 in
+   out_preamble och (path, lines);
+   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 ()
+   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 ->
+      close_out och;
+      GrafiteParser.set_callback ignore;
+      MatitaEngine.set_callback ignore;
+      set_callback ignore; x
+;;
+
 let get_macro_context = function
    | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> []
    | Some status                ->
@@ -197,11 +259,13 @@ let compile options fname =
      with MatitaEngine.EnrichedWithLexiconStatus 
             (GrafiteEngine.Macro (floc, f), lex_status) as exn ->
             match f (get_macro_context (Some grafite_status)) with 
-            | _, GrafiteAst.Inline (_, style, suri, prefix) ->
+            | _, GrafiteAst.Inline (_, style, suri, prefix, flavour) ->
               let str =
-               ApplyTransformation.txt_of_inline_macro style suri prefix
-                ~map_unicode_to_tex:(Helm_registry.get_bool
-                  "matita.paste_unicode_as_tex") in
+               ApplyTransformation.txt_of_inline_macro style prefix suri
+                ?flavour
+		~map_unicode_to_tex:(Helm_registry.get_bool
+                  "matita.paste_unicode_as_tex")
+	      in
               !out str;
               aux_for_dump x
             |_-> raise exn
@@ -259,7 +323,7 @@ let compile options fname =
       LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status;
       pp_times fname false big_bang big_bang_u big_bang_s;
       clean_exit baseuri false
-  | Sys.Break as exn when not matita_debug ->
+  | Sys.Break when not matita_debug ->
      HLog.error "user break!";
      pp_times fname false big_bang big_bang_u big_bang_s;
      clean_exit baseuri false
@@ -286,8 +350,14 @@ module F =
         let root,baseuri,_,_ =
           Librarian.baseuri_of_script ~include_paths mafile 
         in
-        Some root, LibraryMisc.obj_file_of_baseuri 
-          ~must_exist:false ~baseuri ~writable:true 
+	let obj =
+	   if Filename.check_suffix mafile ".mma" then 
+	      Filename.chop_suffix mafile ".mma" ^ ".ma"
+	   else
+	      LibraryMisc.obj_file_of_baseuri 
+                 ~must_exist:false ~baseuri ~writable:true
+	in
+        Some root, obj 
       with Librarian.NoRootFor x -> None, ""
 
     let mtime_of_source_object s =
@@ -298,9 +368,16 @@ module F =
       try Some (Unix.stat s).Unix.st_mtime
       with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
 
-    let build = compile;;
+    let build options fname =
+       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
+	  atexit res
+       else
+          compile options fname
 
-    let load_deps_file = Librarian.load_deps_file;;
+    let load_deps_file = Librarian.load_deps_file
 
   end