;;
let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
- let lexicon_status_ref = ref (status :> LexiconTypes.status) in
let baseuri = status#baseuri in
- let new_status,new_objs =
- GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
- (text,prefix_len,ast)
- in
- let new_status =
- if !lexicon_status_ref#lstatus != status#lstatus then
- new_status#set_lstatus (!lexicon_status_ref#lstatus)
- else
- new_status in
- let new_status = LexiconSync.add_aliases_for_objs new_status new_objs in
- let new_aliases = LexiconSync.alias_diff ~from:status new_status in
+ let new_aliases,new_status =
+ GrafiteDisambiguate.eval_with_new_aliases status
+ (fun status ->
+ GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
+ (text,prefix_len,ast)) in
let _,intermediate_states =
List.fold_left
(fun (status,acc) (k,value) ->
if b then
status,acc
else
- let new_status =
- LexiconEngine.set_proof_aliases status
+ let status =
+ GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
GrafiteAst.WithPreferences [k,value]
in
- new_status, (new_status ,Some (k,value))::acc
- ) (status,[]) new_aliases
+ status, (status ,Some (k,value))::acc
+ ) (status,[]) new_aliases (* WARNING: this must be the old status! *)
in
- ((new_status),None)::intermediate_states
+ (new_status,None)::intermediate_states
;;
exception TryingToAdd of string
exception EnrichedWithStatus of exn * GrafiteTypes.status
-let eval_from_stream ~first_statement_only ~include_paths
- ?do_heavy_checks ?(enforce_no_new_aliases=true)
- ?(watch_statuses=fun _ -> ()) status str cb
+let eval_from_stream ~include_paths ?do_heavy_checks
+ ?(enforce_no_new_aliases=true) status str cb
=
let matita_debug = Helm_registry.get_bool "matita.debug" in
let rec loop status statuses =
- let loop =
- if first_statement_only then fun _ statuses -> statuses
- else loop
- in
let stop,g,s =
try
let cont =
match cont with
| None -> true, status, statuses
| Some ast ->
- (match ast with
- GrafiteParser.LNone _ ->
- watch_statuses status ;
- false, status, ((status,None)::statuses)
- | GrafiteParser.LSome ast ->
- cb status ast;
- let new_statuses =
- eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
- if enforce_no_new_aliases then
- List.iter
- (fun (_,alias) ->
- match alias with
- None -> ()
- | Some (k,value) ->
- let newtxt = GrafiteAstPp.pp_alias value in
- raise (TryingToAdd newtxt)) new_statuses;
- let status =
- match new_statuses with
- [] -> assert false
- | (s,_)::_ -> s
- in
- watch_statuses status ;
- false, status, (new_statuses @ statuses))
+ cb status ast;
+ let new_statuses =
+ eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
+ if enforce_no_new_aliases then
+ List.iter
+ (fun (_,alias) ->
+ match alias with
+ None -> ()
+ | Some (k,value) ->
+ let newtxt = GrafiteAstPp.pp_alias value in
+ raise (TryingToAdd newtxt)) new_statuses;
+ let status =
+ match new_statuses with
+ [] -> assert false
+ | (s,_)::_ -> s
+ in
+ false, status, (new_statuses @ statuses)
with exn when not matita_debug ->
raise (EnrichedWithStatus (exn, status))
in