# HG changeset patch
# User wenzelm
# Date 1416659895 -3600
# Node ID c907cbe36713db29e38e9be7efc60654475bbca3
# Parent  df7476e7955808b02f2829ffbf484e417442580f
more careful ML source positions, for improved PIDE markup;

diff -r df7476e79558 -r c907cbe36713 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 22 11:36:00 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Nov 22 13:38:15 2014 +0100
@@ -15,7 +15,7 @@
   val print_ast_translation: Symbol_Pos.source -> theory -> theory
   val translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
-  val oracle: bstring * Position.T -> Symbol_Pos.source -> theory -> theory
+  val oracle: bstring * Position.range -> Symbol_Pos.source -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
   val declaration: {syntax: bool, pervasive: bool} ->
     Symbol_Pos.source -> local_theory -> local_theory
@@ -127,21 +127,25 @@
 
 (* oracles *)
 
-fun oracle (name, pos) source =
+fun oracle (name, range) source =
   let
+    val body_range = #range source;
     val body = ML_Lex.read_source false source;
+
+    val hidden = ML_Lex.read Position.none;
+    val visible = ML_Lex.read_set_range;
     val ants =
-      ML_Lex.read Position.none
+      hidden
        ("local\n\
-        \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
-        \  val body = ") @ body @ ML_Lex.read Position.none (";\n\
+        \  val binding = " ^ ML_Syntax.make_binding (name, #1 range) ^ ";\n\
+        \  val") @ visible body_range "oracle" @ hidden "=" @ body @ hidden (";\n\
         \in\n\
-        \  val " ^ name ^
-        " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
-        \end;\n");
+        \  val") @ visible range name @ hidden "=\
+        \ snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\
+        \end;\n";
   in
     Context.theory_map
-      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#1 (#range source)) ants))
+      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#1 body_range) ants))
   end;
 
 
diff -r df7476e79558 -r c907cbe36713 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Nov 22 11:36:00 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 22 13:38:15 2014 +0100
@@ -326,7 +326,7 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "oracle"} "declare oracle"
-    (Parse.position Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
+    (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
       (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
 
 
diff -r df7476e79558 -r c907cbe36713 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sat Nov 22 11:36:00 2014 +0100
+++ b/src/Pure/Isar/parse.ML	Sat Nov 22 13:38:15 2014 +0100
@@ -14,6 +14,7 @@
   val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
   val not_eof: Token.T parser
   val token: 'a parser -> Token.T parser
+  val range: 'a parser -> ('a * Position.range) parser
   val position: 'a parser -> ('a * Position.T) parser
   val source_position: 'a parser -> Symbol_Pos.source parser
   val inner_syntax: 'a parser -> string parser
@@ -172,6 +173,7 @@
 
 fun token atom = Scan.ahead not_eof --| atom;
 
+fun range scan = (Scan.ahead not_eof >> (Token.range_of o single)) -- scan >> Library.swap;
 fun position scan = (Scan.ahead not_eof >> Token.pos_of) -- scan >> Library.swap;
 fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
 fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;