]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/nEstatus.ml
debug pps removed
[helm.git] / helm / software / components / grafite_parser / nEstatus.ml
index a49174b11d3a2b13102d57835957c983cc37a134..d7737cde959fdc382b4e927c287a51519d18579b 100644 (file)
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-type extra_status = {
-        lstatus : LexiconEngine.status;
-        rstatus : NRstatus.dumpable_refiner_status;
-}
+class type ctstatus =
+ object ('self)
+  inherit LexiconEngine.status
+  inherit NRstatus.dumpable_status
+  method set_estatus: ctstatus -> 'self
+ end
 
+class status : ctstatus =
+ object (self)
+  inherit LexiconEngine.status
+  inherit NRstatus.dumpable_status
+  method set_estatus o =
+   (self#set_lexicon_engine_status (o :> LexiconEngine.status))
+        #set_dumpable_status       (o :> NRstatus.dumpable_status)
+ end