~disambiguate_command:(wrap (disambiguate_command lexicon_status_ref))
~disambiguate_macro:(wrap (disambiguate_macro lexicon_status_ref))
?do_heavy_checks grafite_status (text,prefix_len,ast) in
- let lexicon_status =
+ let new_lexicon_status =
if !changed_lexicon then
!lexicon_status_ref
else
| GrafiteTypes.ProofMode s -> s.NTacStatus.istatus.NTacStatus.lstatus
in
let new_lexicon_status =
- LexiconSync.add_aliases_for_objs lexicon_status new_objs in
+ LexiconSync.add_aliases_for_objs new_lexicon_status new_objs in
let new_aliases =
LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in
let _,intermediate_states =
((new_grafite_status,new_lexicon_status),None)::intermediate_states
exception TryingToAdd of string
-exception EnrichedWithLexiconStatus of exn * LexiconEngine.status
+exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status
let out = ref ignore
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))
+ raise (EnrichedWithStatus (exn, lexicon_status, grafite_status))
in
if stop then s else loop l g s
in