X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FnEstatus.ml;h=0c6e91095d4502bd0052afe6c89aa0d1b952ab44;hb=6f2f9693db45a2ef905123bc48cde9f04ddff54f;hp=2ae7d01e4ef639ca78dcbe2540ff68d15d602b7c;hpb=8bc5bc0e8375a85736f6a5df317d129d5efa8de4;p=helm.git diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml index 2ae7d01e4..0c6e91095 100644 --- a/helm/software/components/grafite_parser/nEstatus.ml +++ b/helm/software/components/grafite_parser/nEstatus.ml @@ -11,8 +11,16 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -type extra_status = { - lstatus : LexiconEngine.status; - rstatus : NRstatus.dumpable_status; -} - +class status = + object (self) + inherit LexiconEngine.status + inherit NRstatus.dumpable_status + method set_estatus + : 'status. + < coerc_db : NCicCoercion.db; + uhint_db : NCicUnifHint.db; + timestamp: NCicLibrary.timestamp; + dump: NRstatus.Serializer.obj list; + lstatus: LexiconEngine.lexicon_status; .. > as 'status -> 'self + = fun o -> (self#set_lexicon_engine_status o)#set_dumpable_status o + end