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