helm/software/components/ng_refiner/nRstatus.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
  13
  14 class status =
  15  object
  16   inherit NCicUnifHint.status
  17   inherit NCicCoercion.status
  18   inherit NCicLibrary.status
  19  end
  20
  21 type sstatus = status
  22
  23 module Serializer =
  24  struct
  25   include NCicLibrary.Serializer(struct type status = sstatus end)
  26
  27   let require ~baseuri status =
  28    let rstatus = require ~baseuri (status : #status :> status) in
  29    let status = status#set_uhint_db (rstatus#uhint_db) in
  30    let status = status#set_coerc_db (rstatus#coerc_db) in
  31    let status = status#set_timestamp (rstatus#timestamp) in
  32     status
  33  end
  34
  35 class dumpable_status =
  36  object
  37   inherit status
  38   val dump = ([] : Serializer.obj list)
  39   method dump = dump
  40   method set_dump v = {< dump = v >}
  41  end