src/Pure/context.ML
changeset 17060 cca2f3938443
parent 16894 40f80823b451
child 17221 6cd180204582
     1.1 --- a/src/Pure/context.ML	Tue Aug 16 13:42:30 2005 +0200
     1.2 +++ b/src/Pure/context.ML	Tue Aug 16 13:42:31 2005 +0200
     1.3 @@ -67,7 +67,9 @@
     1.4    val setup: unit -> (theory -> theory) list
     1.5    (*proof context*)
     1.6    type proof
     1.7 +  exception PROOF of string * proof
     1.8    val theory_of_proof: proof -> theory
     1.9 +  val transfer_proof: theory -> proof -> proof
    1.10    val init_proof: theory -> proof
    1.11    val proof_data_of: theory -> string list
    1.12    (*generic context*)
    1.13 @@ -472,10 +474,10 @@
    1.14  
    1.15  val ml_output = (writeln, error_msg);
    1.16  
    1.17 -fun use_output verb txt = use_text ml_output verb (Symbol.escape txt);
    1.18 +fun use_output verbose txt = use_text ml_output verbose (Symbol.escape txt);
    1.19  
    1.20 -fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) ();
    1.21 -fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt);
    1.22 +fun use_mltext txt verbose opt_thy = setmp opt_thy (fn () => use_output verbose txt) ();
    1.23 +fun use_mltext_theory txt verbose thy = #2 (pass_theory thy (use_output verbose) txt);
    1.24  
    1.25  fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
    1.26  
    1.27 @@ -498,11 +500,18 @@
    1.28  
    1.29  (* datatype proof *)
    1.30  
    1.31 -datatype proof = Proof of theory * Object.T Inttab.table;
    1.32 +datatype proof = Proof of theory_ref * Object.T Inttab.table;
    1.33 +
    1.34 +exception PROOF of string * proof;
    1.35  
    1.36 -fun theory_of_proof (Proof (thy, _)) = thy;
    1.37 +fun theory_of_proof (Proof (thy_ref, _)) = deref thy_ref;
    1.38  fun data_of_proof (Proof (_, data)) = data;
    1.39 -fun map_prf f (Proof (thy, data)) = Proof (thy, f data);
    1.40 +fun map_prf f (Proof (thy_ref, data)) = Proof (thy_ref, f data);
    1.41 +
    1.42 +fun transfer_proof thy' (prf as Proof (thy_ref, data)) =
    1.43 +  if not (subthy (deref thy_ref, thy')) then
    1.44 +    raise PROOF ("transfer proof context: no a super theory", prf)
    1.45 +  else Proof (self_ref thy', data);
    1.46  
    1.47  
    1.48  (* proof data kinds *)
    1.49 @@ -529,7 +538,7 @@
    1.50  val proof_data_of = dest_data invoke_name o #proof o data_of;
    1.51  
    1.52  fun init_proof thy =
    1.53 -  Proof (thy, Inttab.map' (fn k => fn _ => invoke_init k thy) (#proof (data_of thy)));
    1.54 +  Proof (self_ref thy, Inttab.map' (fn k => fn _ => invoke_init k thy) (#proof (data_of thy)));
    1.55  
    1.56  structure ProofData =
    1.57  struct