X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitacLib.ml;h=52ad776e71d3a2fe91a07c5107b28dea21baa3ff;hb=e3c1b393ff24fe15f01896bec715c8b8a0bc8b96;hp=ba9af1302402450a390e7f4bb0f7f2b5ae5d6b0d;hpb=1716dfe9afab861ad742a434e83e3bcad259dec4;p=helm.git

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index ba9af1302..52ad776e7 100644
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -31,6 +31,10 @@ open GrafiteTypes
 
 exception AttemptToInsertAnAlias
 
+let out = ref ignore 
+
+let set_callback f = out := f
+
 let pp_ast_statement =
   GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
     ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term)
@@ -126,8 +130,14 @@ let rec interactive_loop () =
         "matita.includes"))
   with 
   | GrafiteEngine.Drop -> pp_ocaml_mode ()
-  | GrafiteEngine.Macro (floc,_) ->
-     let x, y = HExtlib.loc_of_floc floc in
+  | GrafiteEngine.Macro (floc, f) ->
+      begin match snd (f []) with 
+       | GrafiteAst.Inline (_, style, suri, prefix) ->
+         let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
+         !out str
+       | _ -> ()
+      end;
+      let x, y = HExtlib.loc_of_floc floc in
       HLog.error
        (sprintf "A macro has been found in a script at %d-%d" x y);
       interactive_loop ()