# HG changeset patch
# User wenzelm
# Date 1237473854 -3600
# Node ID cbe27c4ef41709c6bb300ccf4a133fea5cf90b04
# Parent  05f81bbb2614a95d1eff5a793d75f92d66dd4185
Antiquote.Text: keep full position information;

diff -r 05f81bbb2614 -r cbe27c4ef417 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Thu Mar 19 15:22:53 2009 +0100
+++ b/src/Pure/General/antiquote.ML	Thu Mar 19 15:44:14 2009 +0100
@@ -7,7 +7,7 @@
 signature ANTIQUOTE =
 sig
   datatype antiquote =
-    Text of string | Antiq of Symbol_Pos.T list * Position.T |
+    Text of Symbol_Pos.T list | Antiq of Symbol_Pos.T list * Position.T |
     Open of Position.T | Close of Position.T
   val is_antiq: antiquote -> bool
   val read: Symbol_Pos.T list * Position.T -> antiquote list
@@ -19,7 +19,7 @@
 (* datatype antiquote *)
 
 datatype antiquote =
-  Text of string |
+  Text of Symbol_Pos.T list |
   Antiq of Symbol_Pos.T list * Position.T |
   Open of Position.T |
   Close of Position.T;
@@ -68,7 +68,7 @@
 in
 
 val scan_antiquote =
- (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
+ (Scan.repeat1 scan_txt >> (Text o flat) ||
   scan_antiq ||
   Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
   Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
diff -r 05f81bbb2614 -r cbe27c4ef417 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Mar 19 15:22:53 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 19 15:44:14 2009 +0100
@@ -210,7 +210,8 @@
           val lex = #1 (OuterKeyword.get_lexicons ());
           fun no_decl _ = ("", "");
 
-          fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state)
+          fun expand (Antiquote.Text ss) state =
+                (K ("", Symbol.escape (Symbol_Pos.content ss)), state)
             | expand (Antiquote.Antiq x) (scope, background) =
                 let
                   val context = Stack.top scope;
diff -r 05f81bbb2614 -r cbe27c4ef417 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Thu Mar 19 15:22:53 2009 +0100
+++ b/src/Pure/Thy/latex.ML	Thu Mar 19 15:44:14 2009 +0100
@@ -88,7 +88,7 @@
 val output_syms = output_symbols o Symbol.explode;
 
 val output_syms_antiq =
-  (fn Antiquote.Text s => output_syms s
+  (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
     | Antiquote.Antiq (ss, _) =>
         enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss))
     | Antiquote.Open _ => "{\\isaantiqopen}"
diff -r 05f81bbb2614 -r cbe27c4ef417 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Mar 19 15:22:53 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Mar 19 15:44:14 2009 +0100
@@ -147,7 +147,7 @@
 
 fun eval_antiquote lex state (txt, pos) =
   let
-    fun expand (Antiquote.Text s) = s
+    fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
       | expand (Antiquote.Antiq x) =
           let val (opts, src) = T.read_antiq lex antiq x in
             options opts (fn () => command src state) ();  (*preview errors!*)