X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitacLib.ml;h=cc0793c96b9d0f94f9d444affd72751c37f020fc;hb=bc1570da87ab07a65158b8216cb484bad04f576c;hp=7869482ba59543464c77798c99d5596e5bb2b0ef;hpb=0fde70bd19b8fdfa72b807b9713a02ad1bd91b5b;p=helm.git

diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml
index 7869482ba..cc0793c96 100644
--- a/matita/matita/matitacLib.ml
+++ b/matita/matita/matitacLib.ml
@@ -34,11 +34,8 @@ exception AttemptToInsertAnAlias of LexiconEngine.status
 let slash_n_RE = Pcre.regexp "\\n" ;;
 
 let pp_ast_statement grafite_status stm =
-  let stm = GrafiteAstPp.pp_statement
+  let stm = GrafiteAstPp.pp_statement stm
     ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
-    ~term_pp:CicNotationPp.pp_term
-    ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj
-    CicNotationPp.pp_term) stm
   in
   let stm = Pcre.replace ~rex:slash_n_RE stm in
   let stm =
@@ -59,25 +56,16 @@ let dump f =
    let floc = H.dummy_floc in
    let nl_ast = G.Comment (floc, G.Note (floc, "")) in
    let pp_statement stm =
-     GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+     GrafiteAstPp.pp_statement stm        
        ~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) stm
    in
    let pp_lexicon = LexiconAstPp.pp_command in
    let och = open_out f in
    let nl () =  output_string och (pp_statement nl_ast) in
    MatitaMisc.out_preamble och;
    let grafite_parser_cb = function
-      | G.Executable (_, G.Macro (_, G.Inline (_, uri, params))) ->
-         let str =
-            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, _, _))) -> ()
+      | G.Executable (loc, G.Command (_, G.Include (_,_))) -> ()
       | stm ->
          output_string och (pp_statement stm); nl (); nl ()
    in
@@ -147,6 +135,8 @@ let get_include_paths options =
 ;;
 
 let activate_extraction baseuri fname =
+  ()
+  (* MATITA 1.0
  if Helm_registry.get_bool "matita.extract" then
   let mangled_baseuri =
    let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in
@@ -159,6 +149,7 @@ let activate_extraction baseuri fname =
     (fun ~add_obj ~add_coercion _ obj ->
       output_string f (CicExportation.ppobj baseuri obj);
       flush f; []);
+      *)
 ;;
 
 let compile atstart options fname =
@@ -173,7 +164,8 @@ let compile atstart options fname =
       BuildTimeConf.core_notation_script 
   in
   atstart (); (* FG: do not invoke before loading the core notation script *)  
-  let grafite_status = GrafiteSync.init lexicon_status baseuri in
+  let grafite_status =
+   (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times () 
@@ -189,8 +181,7 @@ let compile atstart options fname =
        ~must_exist:false ~baseuri ~writable:true
     in
     (* cleanup of previously compiled objects *)
-    if (not (Http_getter_storage.is_empty ~local:true baseuri) ||
-        LibraryClean.db_uris_of_baseuri baseuri <> []) 
+    if (not (Http_getter_storage.is_empty ~local:true baseuri))
       then begin
       HLog.message ("baseuri " ^ baseuri ^ " is not empty");
       HLog.message ("cleaning baseuri " ^ baseuri);
@@ -222,7 +213,6 @@ let compile atstart options fname =
     in
     let grafite_status =
      let rec aux_for_dump x grafite_status =
-     try
       match
        MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
         grafite_status buf x
@@ -231,34 +221,17 @@ let compile atstart options fname =
       | (g,None)::_ -> g
       | (g,Some _)::_ ->
          raise (AttemptToInsertAnAlias (g :> LexiconEngine.status))
-     with MatitaEngine.EnrichedWithStatus 
-            (GrafiteEngine.Macro (floc, f), grafite) as exn ->
-            match f (get_macro_context (Some grafite)) with 
-            | _, GrafiteAst.Inline (_, _suri, _params) ->
-(*              
-	      let str =
-               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 grafite
-            |_-> raise exn
      in
        aux_for_dump print_cb grafite_status
     in
     let elapsed = Unix.time () -. time in
-    let moo_content_rev,lexicon_content_rev = 
-      grafite_status#moo_content_rev, 
-       grafite_status#lstatus.LexiconEngine.lexicon_content_rev
+    let lexicon_content_rev = 
+     grafite_status#lstatus.LexiconEngine.lexicon_content_rev
     in
      (if Helm_registry.get_bool "matita.moo" then begin
         (* 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;
-        NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+        GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
          grafite_status#dump
      end;
      let tm = Unix.gmtime elapsed in
@@ -359,16 +332,13 @@ module F =
       let matita_debug = Helm_registry.get_bool "matita.debug" in
       let compile atstart opts fname =
         try
-          GrafiteSync.push ();
           GrafiteParser.push ();
           let rc = compile atstart opts fname in
           GrafiteParser.pop ();
-          GrafiteSync.pop ();
           rc
         with 
         | Sys.Break ->
             GrafiteParser.pop ();
-            GrafiteSync.pop ();
             false
         | exn when not matita_debug ->
             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));