src/Pure/Isar/isar_cmd.ML
changeset 59029 c907cbe36713
parent 58991 92b6f4e68c5a
child 59064 a8bcb5a446c8
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 22 11:36:00 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Nov 22 13:38:15 2014 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    val print_ast_translation: Symbol_Pos.source -> theory -> theory
     1.5    val translations: (xstring * string) Syntax.trrule list -> theory -> theory
     1.6    val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
     1.7 -  val oracle: bstring * Position.T -> Symbol_Pos.source -> theory -> theory
     1.8 +  val oracle: bstring * Position.range -> Symbol_Pos.source -> theory -> theory
     1.9    val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
    1.10    val declaration: {syntax: bool, pervasive: bool} ->
    1.11      Symbol_Pos.source -> local_theory -> local_theory
    1.12 @@ -127,21 +127,25 @@
    1.13  
    1.14  (* oracles *)
    1.15  
    1.16 -fun oracle (name, pos) source =
    1.17 +fun oracle (name, range) source =
    1.18    let
    1.19 +    val body_range = #range source;
    1.20      val body = ML_Lex.read_source false source;
    1.21 +
    1.22 +    val hidden = ML_Lex.read Position.none;
    1.23 +    val visible = ML_Lex.read_set_range;
    1.24      val ants =
    1.25 -      ML_Lex.read Position.none
    1.26 +      hidden
    1.27         ("local\n\
    1.28 -        \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
    1.29 -        \  val body = ") @ body @ ML_Lex.read Position.none (";\n\
    1.30 +        \  val binding = " ^ ML_Syntax.make_binding (name, #1 range) ^ ";\n\
    1.31 +        \  val") @ visible body_range "oracle" @ hidden "=" @ body @ hidden (";\n\
    1.32          \in\n\
    1.33 -        \  val " ^ name ^
    1.34 -        " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
    1.35 -        \end;\n");
    1.36 +        \  val") @ visible range name @ hidden "=\
    1.37 +        \ snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\
    1.38 +        \end;\n";
    1.39    in
    1.40      Context.theory_map
    1.41 -      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#1 (#range source)) ants))
    1.42 +      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#1 body_range) ants))
    1.43    end;
    1.44  
    1.45