1.1 --- a/src/Pure/context.ML Tue Oct 20 21:37:06 2009 +0200
1.2 +++ b/src/Pure/context.ML Tue Oct 20 22:46:24 2009 +0200
1.3 @@ -81,14 +81,14 @@
1.4 signature PRIVATE_CONTEXT =
1.5 sig
1.6 include CONTEXT
1.7 - structure TheoryData:
1.8 + structure Theory_Data:
1.9 sig
1.10 val declare: Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
1.11 (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
1.12 val get: serial -> (Object.T -> 'a) -> theory -> 'a
1.13 val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
1.14 end
1.15 - structure ProofData:
1.16 + structure Proof_Data:
1.17 sig
1.18 val declare: (theory -> Object.T) -> serial
1.19 val get: serial -> (Object.T -> 'a) -> Proof.context -> 'a
1.20 @@ -125,10 +125,10 @@
1.21
1.22 in
1.23
1.24 -fun invoke_empty k = invoke (K o #empty) k ();
1.25 -val invoke_copy = invoke #copy;
1.26 -val invoke_extend = invoke #extend;
1.27 -fun invoke_merge pp = invoke (fn kind => #merge kind pp);
1.28 +fun invoke_empty k = invoke (K o #empty) k ();
1.29 +val invoke_copy = invoke #copy;
1.30 +val invoke_extend = invoke #extend;
1.31 +fun invoke_merge pp = invoke (fn kind => #merge kind pp);
1.32
1.33 fun declare_theory_data empty copy extend merge =
1.34 let
1.35 @@ -176,9 +176,9 @@
1.36 fun rep_theory (Theory args) = args;
1.37
1.38 val identity_of = #1 o rep_theory;
1.39 -val data_of = #2 o rep_theory;
1.40 +val data_of = #2 o rep_theory;
1.41 val ancestry_of = #3 o rep_theory;
1.42 -val history_of = #4 o rep_theory;
1.43 +val history_of = #4 o rep_theory;
1.44
1.45 fun make_identity self draft id ids = {self = self, draft = draft, id = id, ids = ids};
1.46 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
1.47 @@ -254,12 +254,12 @@
1.48 theory in external data structures -- a plain theory value would
1.49 become stale as the self reference moves on*)
1.50
1.51 -datatype theory_ref = TheoryRef of theory Unsynchronized.ref;
1.52 +datatype theory_ref = Theory_Ref of theory Unsynchronized.ref;
1.53
1.54 -fun deref (TheoryRef (Unsynchronized.ref thy)) = thy;
1.55 +fun deref (Theory_Ref (Unsynchronized.ref thy)) = thy;
1.56
1.57 fun check_thy thy = (*thread-safe version*)
1.58 - let val thy_ref = TheoryRef (the_self thy) in
1.59 + let val thy_ref = Theory_Ref (the_self thy) in
1.60 if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
1.61 else thy_ref
1.62 end;
1.63 @@ -294,7 +294,8 @@
1.64 (* consistent ancestors *)
1.65
1.66 fun extend_ancestors thy thys =
1.67 - if member eq_thy thys thy then raise THEORY ("Duplicate theory node", thy :: thys)
1.68 + if member eq_thy thys thy then
1.69 + raise THEORY ("Duplicate theory node", thy :: thys)
1.70 else thy :: thys;
1.71
1.72 fun extend_ancestors_of thy = extend_ancestors thy (ancestors_of thy);
1.73 @@ -417,7 +418,7 @@
1.74
1.75 (* theory data *)
1.76
1.77 -structure TheoryData =
1.78 +structure Theory_Data =
1.79 struct
1.80
1.81 val declare = declare_theory_data;
1.82 @@ -481,7 +482,7 @@
1.83 fun init thy = Proof.Context (init_data thy, check_thy thy);
1.84 end;
1.85
1.86 -structure ProofData =
1.87 +structure Proof_Data =
1.88 struct
1.89
1.90 fun declare init =
1.91 @@ -592,19 +593,17 @@
1.92 functor TheoryDataFun(Data: THEORY_DATA_ARGS): THEORY_DATA =
1.93 struct
1.94
1.95 -structure TheoryData = Context.TheoryData;
1.96 -
1.97 type T = Data.T;
1.98 exception Data of T;
1.99
1.100 -val kind = TheoryData.declare
1.101 +val kind = Context.Theory_Data.declare
1.102 (Data Data.empty)
1.103 (fn Data x => Data (Data.copy x))
1.104 (fn Data x => Data (Data.extend x))
1.105 (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
1.106
1.107 -val get = TheoryData.get kind (fn Data x => x);
1.108 -val put = TheoryData.put kind Data;
1.109 +val get = Context.Theory_Data.get kind (fn Data x => x);
1.110 +val put = Context.Theory_Data.put kind Data;
1.111 fun map f thy = put (f (get thy)) thy;
1.112
1.113 fun init thy = map I thy;
1.114 @@ -632,15 +631,13 @@
1.115 functor ProofDataFun(Data: PROOF_DATA_ARGS): PROOF_DATA =
1.116 struct
1.117
1.118 -structure ProofData = Context.ProofData;
1.119 -
1.120 type T = Data.T;
1.121 exception Data of T;
1.122
1.123 -val kind = ProofData.declare (Data o Data.init);
1.124 +val kind = Context.Proof_Data.declare (Data o Data.init);
1.125
1.126 -val get = ProofData.get kind (fn Data x => x);
1.127 -val put = ProofData.put kind Data;
1.128 +val get = Context.Proof_Data.get kind (fn Data x => x);
1.129 +val put = Context.Proof_Data.put kind Data;
1.130 fun map f prf = put (f (get prf)) prf;
1.131
1.132 end;
1.133 @@ -668,16 +665,16 @@
1.134 functor GenericDataFun(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
1.135 struct
1.136
1.137 -structure ThyData = TheoryDataFun(open Data val copy = I);
1.138 -structure PrfData = ProofDataFun(type T = Data.T val init = ThyData.get);
1.139 +structure Thy_Data = TheoryDataFun(open Data val copy = I);
1.140 +structure Prf_Data = ProofDataFun(type T = Data.T val init = Thy_Data.get);
1.141
1.142 type T = Data.T;
1.143
1.144 -fun get (Context.Theory thy) = ThyData.get thy
1.145 - | get (Context.Proof prf) = PrfData.get prf;
1.146 +fun get (Context.Theory thy) = Thy_Data.get thy
1.147 + | get (Context.Proof prf) = Prf_Data.get prf;
1.148
1.149 -fun put x (Context.Theory thy) = Context.Theory (ThyData.put x thy)
1.150 - | put x (Context.Proof prf) = Context.Proof (PrfData.put x prf);
1.151 +fun put x (Context.Theory thy) = Context.Theory (Thy_Data.put x thy)
1.152 + | put x (Context.Proof prf) = Context.Proof (Prf_Data.put x prf);
1.153
1.154 fun map f ctxt = put (f (get ctxt)) ctxt;
1.155