antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;

--- a/src/Pure/ML/ml_context.ML	Thu Aug 14 19:52:39 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu Aug 14 19:52:40 2008 +0200
@@ -124,9 +124,11 @@
 
 fun eval_antiquotes struct_name (txt, pos) opt_ctxt =
   let
-    val ants = Antiquote.read (txt, pos);
+    val syms = SymbolPos.explode (txt, pos);
+    val ants = Antiquote.read (syms, pos);
     val ((ml_env, ml_body), opt_ctxt') =
-      if not (exists Antiquote.is_antiq ants) then (("", Symbol.escape txt), opt_ctxt)
+      if not (exists Antiquote.is_antiq ants)
+      then (("", Symbol.escape (SymbolPos.content syms)), opt_ctxt)
       else
         let
           val ctxt =

--- a/src/Pure/Thy/latex.ML	Thu Aug 14 19:52:39 2008 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Aug 14 19:52:40 2008 +0200
@@ -87,15 +87,13 @@
 val output_known_symbols = implode oo (map o output_known_sym);
 val output_symbols = output_known_symbols (K true, K true);
 val output_syms = output_symbols o Symbol.explode;
-val output_syms' = output_symbols o map #1 o SymbolPos.explode;
 
-val output_syms_antiqs =
-  Antiquote.read #> map
+val output_syms_antiq =
   (fn Antiquote.Text s => output_syms s
-    | Antiquote.Antiq x => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms' x)
+    | Antiquote.Antiq (ss, _) =>
+        enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map SymbolPos.symbol ss))
     | Antiquote.Open _ => "{\\isaantiqopen}"
-    | Antiquote.Close _ => "{\\isaantiqclose}") #>
-  implode;
+    | Antiquote.Close _ => "{\\isaantiqclose}");
 
 end;
 
@@ -118,8 +116,11 @@
     else if T.is_kind T.AltString tok then
       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
     else if T.is_kind T.Verbatim tok then
-      enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
-        (output_syms_antiqs (s, T.position_of tok))
+      let
+        val (txt, pos) = T.source_of' tok;
+        val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
+        val out = implode (map output_syms_antiq ants);
+      in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
     else output_syms s
   end;
 

--- a/src/Pure/Thy/thy_output.ML	Thu Aug 14 19:52:39 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Aug 14 19:52:40 2008 +0200
@@ -22,7 +22,7 @@
     (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.node option -> string
   datatype markup = Markup | MarkupEnv | Verbatim
   val modes: string list ref
-  val eval_antiquote: Scan.lexicon -> Toplevel.node option -> string * Position.T -> string
+  val eval_antiquote: Scan.lexicon -> Toplevel.node option -> SymbolPos.text * Position.T -> string
   val process_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> Buffer.T
   val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
@@ -145,7 +145,7 @@
 
 val modes = ref ([]: string list);
 
-fun eval_antiquote lex node (str, pos) =
+fun eval_antiquote lex node (txt, pos) =
   let
     fun expand (Antiquote.Text s) = s
       | expand (Antiquote.Antiq x) =
@@ -156,7 +156,7 @@
           end
       | expand (Antiquote.Open _) = ""
       | expand (Antiquote.Close _) = "";
-    val ants = Antiquote.read (str, pos);
+    val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
   in
     if is_none node andalso exists Antiquote.is_antiq ants then
       error ("Unknown context -- cannot expand text antiquotations" ^ Position.str_of pos)
@@ -334,7 +334,7 @@
     fun markup mark mk flag = Scan.peek (fn d =>
       improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
       Scan.repeat tag --
-      P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
+      P.!!!! ((improper -- locale -- improper) |-- P.doc_source --| improper_end)
       >> (fn (((tok, pos), tags), txt) =>
         let val name = T.content_of tok
         in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
@@ -347,7 +347,7 @@
         in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
 
     val cmt = Scan.peek (fn d =>
-      P.$$$ "--" |-- P.!!!! (improper |-- P.position P.text)
+      P.$$$ "--" |-- P.!!!! (improper |-- P.doc_source)
       >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
 
     val other = Scan.peek (fn d =>