+ if first_statement_only then fun _ _ statuses -> statuses
+ else loop
+ in
+ let stop,l,g,s =
+ try
+ let cont =
+ try
+ Some (GrafiteParser.parse_statement ~include_paths str lexicon_status)
+ with
+ End_of_file -> None
+ in
+ match cont with
+ | None -> true, lexicon_status, grafite_status, statuses
+ | Some (lexicon_status,ast) ->
+ (match ast with
+ GrafiteParser.LNone _ ->
+ watch_statuses lexicon_status grafite_status ;
+ false, lexicon_status, grafite_status,
+ (((grafite_status,lexicon_status),None)::statuses)
+ | GrafiteParser.LSome ast ->
+ !out ast;
+ cb grafite_status ast;
+ let new_statuses =
+ eval_ast ?do_heavy_checks lexicon_status
+ grafite_status ("",0,ast) in
+ if enforce_no_new_aliases then
+ List.iter
+ (fun (_,alias) ->
+ match alias with
+ None -> ()
+ | Some (k,((v,_) as value)) ->
+ let newtxt =
+ DisambiguatePp.pp_environment
+ (DisambiguateTypes.Environment.add k value
+ DisambiguateTypes.Environment.empty)
+ in
+ raise (TryingToAdd newtxt)) new_statuses;
+ let grafite_status,lexicon_status =
+ match new_statuses with
+ [] -> assert false
+ | (s,_)::_ -> s
+ in
+ watch_statuses lexicon_status grafite_status ;
+ false, lexicon_status, grafite_status, (new_statuses @ statuses))
+ with exn when not matita_debug ->
+ raise (EnrichedWithLexiconStatus (exn, lexicon_status))