# HG changeset patch # User wenzelm # Date 1121362113 -7200 # Node ID a6cdb1ade95591dc3b488d199abb7a0ea5481326 # Parent 1c8a5bb7c6880955322807c310b735c8d7e01eb4 type-safe 'oracle' command; diff -r 1c8a5bb7c688 -r a6cdb1ade955 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Jul 14 19:28:32 2005 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Jul 14 19:28:33 2005 +0200 @@ -292,8 +292,9 @@ (* oracles *) val oracleP = - OuterSyntax.command "oracle" "install oracle" K.thy_decl - ((P.name --| P.$$$ "=") -- P.text >> (Toplevel.theory o IsarThy.add_oracle)); + OuterSyntax.command "oracle" "declare oracle" K.thy_decl + (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=") + -- P.text >> (Toplevel.theory o IsarThy.add_oracle o P.triple1)); (* locales *) diff -r 1c8a5bb7c688 -r a6cdb1ade955 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Thu Jul 14 19:28:32 2005 +0200 +++ b/src/Pure/Isar/isar_thy.ML Thu Jul 14 19:28:33 2005 +0200 @@ -153,7 +153,7 @@ val token_translation: string -> theory -> theory val generic_setup: string -> theory -> theory val method_setup: bstring * string * string -> theory -> theory - val add_oracle: bstring * string -> theory -> theory + val add_oracle: bstring * string * string -> theory -> theory val add_locale: bool * bstring * Locale.expr * Locale.element list -> theory -> theory val register_globally: ((string * Attrib.src list) * Locale.expr) * string option list -> @@ -615,11 +615,20 @@ (* add_oracle *) -fun add_oracle (name, txt) = - Context.use_let - "val oracle: bstring * (theory * Object.T -> term)" - "Theory.add_oracle oracle" - ("(" ^ Library.quote name ^ ", " ^ txt ^ ")"); +fun add_oracle (name, T, oracle) = + let val txt = + "local\n\ + \ type T = " ^ T ^ ";\n\ + \ val oracle: theory -> T -> term = " ^ oracle ^ ";\n\ + \ val name = " ^ quote name ^ ";\n\ + \ exception Arg of T;\n\ + \ val _ = Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\ + \ val thy = Context.the_context ();\n\ + \ val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\ + \in\n\ + \ fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\ + \end;\n"; + in Context.use_mltext_theory txt false end; (* add_locale *)