# HG changeset patch
# User wenzelm
# Date 1218736356 -7200
# Node ID 4ef76f8788ad145a342b2695b8a1aa6a61df1937
# Parent  643673ebe06513492c5dd7c78b8b630e543ac936
oracle, header/local_theory/proof_markup: pass SymbolPos.text;

diff -r 643673ebe065 -r 4ef76f8788ad src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Aug 14 19:52:35 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 14 19:52:36 2008 +0200
@@ -13,7 +13,8 @@
   val print_translation: bool * (string * Position.T) -> theory -> theory
   val typed_print_translation: bool * (string * Position.T) -> theory -> theory
   val print_ast_translation: bool * (string * Position.T) -> theory -> theory
-  val oracle: bstring -> string -> string * Position.T -> theory -> theory
+  val oracle: bstring -> SymbolPos.text * Position.T -> SymbolPos.text * Position.T ->
+    theory -> theory
   val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
   val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
   val declaration: string * Position.T -> local_theory -> local_theory
@@ -84,10 +85,10 @@
   val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
   val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
   val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
-  val header_markup: string * Position.T -> Toplevel.transition -> Toplevel.transition
-  val local_theory_markup: xstring option * (string * Position.T) ->
+  val header_markup: SymbolPos.text * Position.T -> Toplevel.transition -> Toplevel.transition
+  val local_theory_markup: xstring option * (SymbolPos.text * Position.T) ->
     Toplevel.transition -> Toplevel.transition
-  val proof_markup: string * Position.T -> Toplevel.transition -> Toplevel.transition
+  val proof_markup: SymbolPos.text * Position.T -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure IsarCmd: ISAR_CMD =
@@ -155,20 +156,23 @@
 
 (* oracles *)
 
-fun oracle name typ (oracle, pos) =
-  let val txt =
-    "local\
-    \  type T = " ^ typ ^ ";\
-    \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
-    \  val name = " ^ quote name ^ ";\n\
-    \  exception Arg of T;\n\
-    \  val _ = Context.>> (Context.map_theory\n\
-    \    (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x)));\n\
-    \  val thy = ML_Context.the_global_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";
+fun oracle name typ_pos (oracle_txt, pos) =
+  let
+    val typ = SymbolPos.content (SymbolPos.explode typ_pos);
+    val oracle = SymbolPos.content (SymbolPos.explode (oracle_txt, pos));
+    val txt =
+      "local\
+      \  type T = " ^ typ ^ ";\
+      \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
+      \  val name = " ^ quote name ^ ";\n\
+      \  exception Arg of T;\n\
+      \  val _ = Context.>> (Context.map_theory\n\
+      \    (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x)));\n\
+      \  val thy = ML_Context.the_global_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.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end;