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

diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml
index 7869482ba..d9ce848d5 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,24 +59,17 @@ 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
    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, _, _))) -> ()
       | stm ->
          output_string och (pp_statement stm); nl (); nl ()
@@ -147,6 +140,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 +154,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 =