- if prompt then (print_string "matita> "; flush stdout);
- let cont =
- try
- Some (GrafiteParser.parse_statement ~include_paths str lexicon_status)
- with
- End_of_file -> None
- in
- match cont with
- | None -> statuses
- | Some (lexicon_status,ast) ->
- (match ast with
- GrafiteParser.LNone _ ->
- watch_statuses lexicon_status grafite_status ;
- loop 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 ?clean_baseuri 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 ;
- loop lexicon_status grafite_status (new_statuses @ statuses))