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)
in
let matita_debug = Helm_registry.get_bool "matita.debug" in
try
- let grafite_status'', lexicon_status'' =
- match eval_function lexicon_status' grafite_status' is cb with
- [] -> assert false
- | (s,None)::_ -> s
- | (s,Some _)::_ -> raise AttemptToInsertAnAlias
- in
- lexicon_status := Some lexicon_status'';
- grafite_status := Some grafite_status''
+ match eval_function lexicon_status' grafite_status' is cb with
+ [] -> raise End_of_file
+ | ((grafite_status'',lexicon_status''),None)::_ ->
+ lexicon_status := Some lexicon_status'';
+ grafite_status := Some grafite_status''
+ | (s,Some _)::_ -> raise AttemptToInsertAnAlias
with
| GrafiteEngine.Drop
| End_of_file
"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 ()