obsolete (see Pure/context.ML);
authorwenzelm
Wed Jun 22 19:41:15 2005 +0200 (2005-06-22)
changeset 165303e493fa130a3
parent 16529 d4de40568ab1
child 16531 9b442d0e5c0c
obsolete (see Pure/context.ML);
src/Pure/General/object.ML
src/Pure/Isar/ROOT.ML
src/Pure/Isar/proof_data.ML
     1.1 --- a/src/Pure/General/object.ML	Wed Jun 22 18:26:28 2005 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,42 +0,0 @@
     1.4 -(*  Title:      Pure/General/object.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Markus Wenzel, TU Muenchen
     1.7 -
     1.8 -Generic objects of arbitrary type -- fool the ML type system via
     1.9 -exception constructors.
    1.10 -*)
    1.11 -
    1.12 -signature OBJECT =
    1.13 -sig
    1.14 -  type T
    1.15 -  type kind
    1.16 -  val kind: string -> kind
    1.17 -  val name_of_kind: kind -> string
    1.18 -  val eq_kind: kind * kind -> bool
    1.19 -  val kind_error: kind -> 'a
    1.20 -end;
    1.21 -
    1.22 -structure Object: OBJECT =
    1.23 -struct
    1.24 -
    1.25 -
    1.26 -(* anytype values *)
    1.27 -
    1.28 -type T = exn;
    1.29 -
    1.30 -
    1.31 -(* kinds *)
    1.32 -
    1.33 -datatype kind = Kind of string * stamp;
    1.34 -
    1.35 -fun kind name = Kind (name, stamp ());
    1.36 -
    1.37 -fun name_of_kind (Kind (name, _)) = name;
    1.38 -
    1.39 -fun eq_kind (Kind (_, s1), Kind (_, s2)) = s1 = s2;
    1.40 -
    1.41 -fun kind_error k =
    1.42 -  error ("## RUNTIME TYPE ERROR ##\nFailed to access " ^ quote (name_of_kind k) ^ " object");
    1.43 -
    1.44 -
    1.45 -end;
     2.1 --- a/src/Pure/Isar/ROOT.ML	Wed Jun 22 18:26:28 2005 +0200
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Wed Jun 22 19:41:15 2005 +0200
     2.3 @@ -10,7 +10,6 @@
     2.4  use "auto_bind.ML";
     2.5  use "rule_cases.ML";
     2.6  use "proof_context.ML";
     2.7 -use "proof_data.ML";
     2.8  use "context_rules.ML";
     2.9  use "args.ML";
    2.10  use "attrib.ML";
     3.1 --- a/src/Pure/Isar/proof_data.ML	Wed Jun 22 18:26:28 2005 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,48 +0,0 @@
     3.4 -(*  Title:      Pure/Isar/proof_data.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Markus Wenzel, TU Muenchen
     3.7 -
     3.8 -Type-safe interface for proof context data.
     3.9 -*)
    3.10 -
    3.11 -signature PROOF_DATA_ARGS =
    3.12 -sig
    3.13 -  val name: string
    3.14 -  type T
    3.15 -  val init: theory -> T
    3.16 -  val print: ProofContext.context -> T -> unit
    3.17 -end;
    3.18 -
    3.19 -signature PROOF_DATA =
    3.20 -sig
    3.21 -  type T
    3.22 -  val init: theory -> theory
    3.23 -  val print: ProofContext.context -> unit
    3.24 -  val get: ProofContext.context -> T
    3.25 -  val put: T -> ProofContext.context -> ProofContext.context
    3.26 -  val map: (T -> T) -> ProofContext.context -> ProofContext.context
    3.27 -end;
    3.28 -
    3.29 -functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
    3.30 -struct
    3.31 -
    3.32 -(*object kind kept private!*)
    3.33 -val kind = Object.kind Args.name;
    3.34 -
    3.35 -type T = Args.T;
    3.36 -exception Data of T;
    3.37 -
    3.38 -val init =
    3.39 -  ProofContext.init_data kind
    3.40 -    (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
    3.41 -
    3.42 -val print = ProofContext.print_data kind;
    3.43 -val get = ProofContext.get_data kind (fn Data x => x);
    3.44 -val put = ProofContext.put_data kind Data;
    3.45 -fun map f ctxt = put (f (get ctxt)) ctxt;
    3.46 -
    3.47 -end;
    3.48 -
    3.49 -
    3.50 -(*hide private data access functions*)
    3.51 -structure ProofContext: PROOF_CONTEXT = ProofContext;