datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;

--- a/src/Pure/General/antiquote.ML	Tue Mar 24 11:39:25 2009 +0100
+++ b/src/Pure/General/antiquote.ML	Tue Mar 24 11:57:41 2009 +0100
@@ -8,7 +8,7 @@
 sig
   datatype 'a antiquote =
     Text of 'a |
-    Antiq of Symbol_Pos.T list * Position.T |
+    Antiq of Symbol_Pos.T list * Position.range |
     Open of Position.T |
     Close of Position.T
   val is_text: 'a antiquote -> bool
@@ -26,7 +26,7 @@
 
 datatype 'a antiquote =
   Text of 'a |
-  Antiq of Symbol_Pos.T list * Position.T |
+  Antiq of Symbol_Pos.T list * Position.range |
   Open of Position.T |
   Close of Position.T;
 
@@ -39,7 +39,7 @@
 val report_antiq = Position.report Markup.antiq;
 
 fun report report_text (Text x) = report_text x
-  | report _ (Antiq (_, pos)) = report_antiq pos
+  | report _ (Antiq (_, (pos, _))) = report_antiq pos
   | report _ (Open pos) = report_antiq pos
   | report _ (Close pos) = report_antiq pos;
 
@@ -79,7 +79,7 @@
   Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
     Symbol_Pos.!!! "missing closing brace of antiquotation"
       (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
-  >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2)));
+  >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
 
 val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
 val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";

--- a/src/Pure/ML/ml_context.ML	Tue Mar 24 11:39:25 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Mar 24 11:57:41 2009 +0100
@@ -219,12 +219,12 @@
           fun no_decl _ = ([], []);
 
           fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
-            | expand (Antiquote.Antiq x) (scope, background) =
+            | expand (Antiquote.Antiq (ss, range)) (scope, background) =
                 let
                   val context = Stack.top scope;
-                  val (f, context') = antiquotation (T.read_antiq lex antiq x) context;
+                  val (f, context') = antiquotation (T.read_antiq lex antiq (ss, #1 range)) context;
                   val (decl, background') = f {background = background, struct_name = struct_name};
-                  val decl' = pairself ML_Lex.tokenize o decl;
+                  val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
                 in (decl', (Stack.map_top (K context') scope, background')) end
             | expand (Antiquote.Open _) (scope, background) =
                 (no_decl, (Stack.push scope, background))

--- a/src/Pure/ML/ml_lex.ML	Tue Mar 24 11:39:25 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML	Tue Mar 24 11:57:41 2009 +0100
@@ -13,6 +13,7 @@
   val stopper: token Scan.stopper
   val is_regular: token -> bool
   val is_improper: token -> bool
+  val set_range: Position.range -> token -> token
   val pos_of: token -> Position.T
   val kind_of: token -> token_kind
   val content_of: token -> string
@@ -42,6 +43,8 @@
 
 (* position *)
 
+fun set_range range (Token (_, x)) = Token (range, x);
+
 fun pos_of (Token ((pos, _), _)) = pos;
 fun end_pos_of (Token ((_, pos), _)) = pos;
 

--- a/src/Pure/Thy/thy_output.ML	Tue Mar 24 11:39:25 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Mar 24 11:57:41 2009 +0100
@@ -148,8 +148,8 @@
 fun eval_antiquote lex state (txt, pos) =
   let
     fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
-      | expand (Antiquote.Antiq x) =
-          let val (opts, src) = T.read_antiq lex antiq x in
+      | expand (Antiquote.Antiq (ss, (pos, _))) =
+          let val (opts, src) = T.read_antiq lex antiq (ss, pos) in
             options opts (fn () => command src state) ();  (*preview errors!*)
             PrintMode.with_modes (! modes @ Latex.modes)
               (Output.no_warnings (options opts (fn () => command src state))) ()