# HG changeset patch # User wenzelm # Date 941112025 -7200 # Node ID d5c91c131070234be332ad6a90e253c49c28f667 # Parent 954e30918b86f294815567040b40fd8bd9004b14 improved IsarThy.init_context; diff -r 954e30918b86 -r d5c91c131070 src/Pure/Interface/proof_general.ML --- a/src/Pure/Interface/proof_general.ML Thu Oct 28 13:55:17 1999 +0200 +++ b/src/Pure/Interface/proof_general.ML Thu Oct 28 14:00:25 1999 +0200 @@ -201,7 +201,7 @@ val try_context_thy_onlyP = OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control - (P.name >> IsarThy.init_context try_update_thy_only); + (P.name >> (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)); val restartP = OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control diff -r 954e30918b86 -r d5c91c131070 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Thu Oct 28 13:55:17 1999 +0200 +++ b/src/Pure/Isar/isar_thy.ML Thu Oct 28 14:00:25 1999 +0200 @@ -158,7 +158,7 @@ val kill_theory: string -> unit val theory: string * string list * (string * bool) list -> Toplevel.transition -> Toplevel.transition - val init_context: (string -> unit) -> string -> Toplevel.transition -> Toplevel.transition + val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition val context: string -> Toplevel.transition -> Toplevel.transition end; @@ -537,8 +537,12 @@ (* context switch *) -fun init_context (f: string -> unit) name = - Toplevel.init_theory (fn _ => (the (#2 (Context.pass None f name)))) (K ()) (K ()); +fun fetch_context f x = + (case Context.pass None f x of + ((), None) => raise Toplevel.UNDEF + | ((), Some thy) => thy); + +fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ()); val context = init_context (ThyInfo.quiet_update_thy true);