X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FnEstatus.ml;h=0c6e91095d4502bd0052afe6c89aa0d1b952ab44;hb=72cd94b68037956a70b98cfa54f316fd54e52bae;hp=a225f439d84df7f2ac76586806feabdde3a3736a;hpb=dcdbb979433a61e2ef2842d96604098728824416;p=helm.git diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml index a225f439d..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.refiner_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