1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Aug 14 19:52:35 2008 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 14 19:52:36 2008 +0200
     1.3 @@ -13,7 +13,8 @@
     1.4    val print_translation: bool * (string * Position.T) -> theory -> theory
     1.5    val typed_print_translation: bool * (string * Position.T) -> theory -> theory
     1.6    val print_ast_translation: bool * (string * Position.T) -> theory -> theory
     1.7 -  val oracle: bstring -> string -> string * Position.T -> theory -> theory
     1.8 +  val oracle: bstring -> SymbolPos.text * Position.T -> SymbolPos.text * Position.T ->
     1.9 +    theory -> theory
    1.10    val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
    1.11    val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
    1.12    val declaration: string * Position.T -> local_theory -> local_theory
    1.13 @@ -84,10 +85,10 @@
    1.14    val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
    1.15    val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
    1.16    val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
    1.17 -  val header_markup: string * Position.T -> Toplevel.transition -> Toplevel.transition
    1.18 -  val local_theory_markup: xstring option * (string * Position.T) ->
    1.19 +  val header_markup: SymbolPos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    1.20 +  val local_theory_markup: xstring option * (SymbolPos.text * Position.T) ->
    1.21      Toplevel.transition -> Toplevel.transition
    1.22 -  val proof_markup: string * Position.T -> Toplevel.transition -> Toplevel.transition
    1.23 +  val proof_markup: SymbolPos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    1.24  end;
    1.25  
    1.26  structure IsarCmd: ISAR_CMD =
    1.27 @@ -155,20 +156,23 @@
    1.28  
    1.29  (* oracles *)
    1.30  
    1.31 -fun oracle name typ (oracle, pos) =
    1.32 -  let val txt =
    1.33 -    "local\
    1.34 -    \  type T = " ^ typ ^ ";\
    1.35 -    \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
    1.36 -    \  val name = " ^ quote name ^ ";\n\
    1.37 -    \  exception Arg of T;\n\
    1.38 -    \  val _ = Context.>> (Context.map_theory\n\
    1.39 -    \    (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x)));\n\
    1.40 -    \  val thy = ML_Context.the_global_context ();\n\
    1.41 -    \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
    1.42 -    \in\n\
    1.43 -    \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
    1.44 -    \end;\n";
    1.45 +fun oracle name typ_pos (oracle_txt, pos) =
    1.46 +  let
    1.47 +    val typ = SymbolPos.content (SymbolPos.explode typ_pos);
    1.48 +    val oracle = SymbolPos.content (SymbolPos.explode (oracle_txt, pos));
    1.49 +    val txt =
    1.50 +      "local\
    1.51 +      \  type T = " ^ typ ^ ";\
    1.52 +      \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
    1.53 +      \  val name = " ^ quote name ^ ";\n\
    1.54 +      \  exception Arg of T;\n\
    1.55 +      \  val _ = Context.>> (Context.map_theory\n\
    1.56 +      \    (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x)));\n\
    1.57 +      \  val thy = ML_Context.the_global_context ();\n\
    1.58 +      \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
    1.59 +      \in\n\
    1.60 +      \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
    1.61 +      \end;\n";
    1.62    in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end;
    1.63  
    1.64