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))) ()