File ZTheory.sml

 
(*  Title:      Pure/theory.ML
    ID:         $Id: ZTheory.sml,v 1.4 2002/09/20 12:44:18 wolff Exp $
    Author:     Burkhart Wolff,
    Copyright   2005 ETH Zürich *)

signature ZTHEORY =
  sig

  type  ztheory  

  exception IS_NOT_ZTHY of string

  val get_zenv           : ztheory -> ZEnv.Zenv
  val put_zenv           : ZEnv.Zenv -> theory -> ztheory

  val ZEnv_setup         : (theory -> theory) list


end;



structure ZTheory : ZTHEORY = 
struct

   structure ZEnvData : THEORY_DATA_ARGS =
   struct
     val name = "zenvironment" 
     type T = ZEnv.Zenv
     val empty = ZEnv.mt_zenv
     fun copy T = T
     fun prep_ext T = T
     fun extend T = T
     val merge  = (fn pp =>  ZEnv.merge)

     fun print thy T = ZEnv.prinzenv T
   end;

   structure ZEnv_DataManagement = TheoryDataFun(ZEnvData);
   val ZEnv_setup = [ZEnv_DataManagement.init]

   type      ztheory = theory

   exception IS_NOT_ZTHY of string;

   fun get_zenv thy = ZEnv_DataManagement.get thy 
                      handle _ => raise IS_NOT_ZTHY "NOT A Z THEORY";

   val put_zenv = ZEnv_DataManagement.put;

end;