and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
let matita_debug = Helm_registry.get_bool "matita.debug" in
- let rec loop asserted status =
- let asserted,stop,status =
+ let rec loop asserted status str =
+ let asserted,stop,status,str =
try
let cont =
try Some (get_ast status ~compiling ~asserted ~include_paths str)
with End_of_file -> None in
match cont with
- | None -> asserted, true, status
+ | None -> asserted, true, status, str
| Some (asserted,ast) ->
(* pp_ast_statement status ast; *)
cb status ast;
let status =
eval_ast ~include_paths ?do_heavy_checks status ("",0,ast)
in
- asserted, false, status
+ let str =
+ match ast with
+ (GrafiteAst.Executable
+ (_,GrafiteAst.NCommand
+ (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
+ GrafiteParser.parsable_statement status
+ (GrafiteParser.strm_of_parsable str)
+ | _ -> str
+ in
+ asserted, false, status, str
with exn when not matita_debug ->
prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn);
raise (EnrichedWithStatus (exn, status))
in
- if stop then asserted,status else loop asserted status
+ if stop then asserted,status else loop asserted status str
in
- loop asserted status
+ loop asserted status str
and compile ~compiling ~asserted ~include_paths ~outch ?uid fname =
if List.mem fname compiling then raise (CircularDependency fname);