X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flexicon%2FlexiconEngine.ml;h=4aba86187b2ec388c4fa609d5ec3be55a2535ea9;hb=aab0401db0bedd941da96a32acd600af3fbe42e7;hp=a0dfb87cf227a375ebc2e3a59243b2a2e54bf0ea;hpb=3ce27112fe93ced5f67cc6af8fc63037eba3f322;p=helm.git

diff --git a/matita/components/lexicon/lexiconEngine.ml b/matita/components/lexicon/lexiconEngine.ml
index a0dfb87cf..4aba86187 100644
--- a/matita/components/lexicon/lexiconEngine.ml
+++ b/matita/components/lexicon/lexiconEngine.ml
@@ -49,16 +49,18 @@ let initial_status = {
 
 class type g_status =
  object
+  inherit Interpretations.g_status
   method lstatus: lexicon_status
  end
 
 class status =
  object(self)
+  inherit Interpretations.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_interp_status o
  end
 
 let dump_aliases out msg status =
@@ -151,7 +153,7 @@ let rec eval_command ?(mode=L.WithPreferences) sstatus cmd =
        (loc, dsc, (symbol, args), disambiguate cic_appl_pattern)
   | _-> cmd
  in
- let notation_ids' = CicNotation.process_notation cmd in
+ let sstatus,notation_ids' = CicNotation.process_notation sstatus cmd in
  let status =
    { status with notation_ids = notation_ids' @ status.notation_ids } in
  let sstatus = sstatus#set_lstatus status in