aliases: L.alias_spec DisambiguateTypes.Environment.t;
multi_aliases: L.alias_spec list DisambiguateTypes.Environment.t;
lexicon_content_rev: LexiconMarshal.lexicon;
- notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
}
let initial_status = {
aliases = DisambiguateTypes.Environment.empty;
multi_aliases = DisambiguateTypes.Environment.empty;
lexicon_content_rev = [];
- notation_ids = [];
}
class type g_status =
object
+ inherit CicNotation.g_status
method lstatus: lexicon_status
end
class status =
object(self)
+ inherit CicNotation.status
val lstatus = initial_status
method lstatus = lstatus
method set_lstatus v = {< lstatus = v >}
method set_lexicon_engine_status : 'status. #g_status as 'status -> 'self
- = fun o -> self#set_lstatus o#lstatus
+ = fun o -> (self#set_lstatus o#lstatus)#set_notation_status o
end
let dump_aliases out msg status =
(loc, dsc, (symbol, args), disambiguate cic_appl_pattern)
| _-> cmd
in
- let notation_ids' = CicNotation.process_notation cmd in
- let status =
- { status with notation_ids = notation_ids' @ status.notation_ids } in
+ let sstatus = CicNotation.process_notation sstatus cmd in
let sstatus = sstatus#set_lstatus status in
match cmd with
| L.Include (loc, baseuri, mode, fullpath) ->