X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitacLib.ml;h=eb4ed69915f1e17cbc4b36639ed7500f1ef5d164;hb=729e08f5fb86b3ffee460fda4577b024ab5888aa;hp=114ed59372654e54133df235a17e4d56adf6f528;hpb=bfcde2b08d72f1392ed61164c67d199360f0397f;p=helm.git

diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml
index 114ed5937..eb4ed6991 100644
--- a/matita/matita/matitacLib.ml
+++ b/matita/matita/matitacLib.ml
@@ -36,9 +36,9 @@ let slash_n_RE = Pcre.regexp "\\n" ;;
 let pp_ast_statement grafite_status stm =
   let stm = GrafiteAstPp.pp_statement
     ~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
+    ~term_pp:NotationPp.pp_term
+    ~lazy_term_pp:NotationPp.pp_term ~obj_pp:(NotationPp.pp_obj
+    NotationPp.pp_term) stm
   in
   let stm = Pcre.replace ~rex:slash_n_RE stm in
   let stm =
@@ -59,11 +59,11 @@ 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 ~term_pp:NotationPp.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) stm
+       ~lazy_term_pp:NotationPp.pp_term 
+       ~obj_pp:(NotationPp.pp_obj NotationPp.pp_term) stm
    in
    let pp_lexicon = LexiconAstPp.pp_command in
    let och = open_out f in
@@ -185,8 +185,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);
@@ -218,7 +217,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
@@ -227,21 +225,6 @@ 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