# HG changeset patch
# User wenzelm
# Date 1237493140 -3600
# Node ID 8f2682d3f48f7637395f72578623f968b3e33af0
# Parent  495672058d9761ecfb3ab8a405687c39aff68264
eval_antiquotes: joint scanning of ML tokens and antiquotations;

diff -r 495672058d97 -r 8f2682d3f48f src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Mar 19 21:04:53 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 19 21:05:40 2009 +0100
@@ -194,7 +194,7 @@
 fun eval_antiquotes (txt, pos) opt_context =
   let
     val syms = Symbol_Pos.explode (txt, pos);
-    val ants = Antiquote.read Antiquote.scan_text (syms, pos);
+    val ants = Antiquote.read ML_Lex.scan_antiq (syms, pos);
     val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
     val ((ml_env, ml_body), opt_ctxt') =
       if not (exists Antiquote.is_antiq ants)
@@ -210,8 +210,8 @@
           val lex = #1 (OuterKeyword.get_lexicons ());
           fun no_decl _ = ("", "");
 
-          fun expand (Antiquote.Text ss) state =
-                (K ("", Symbol.escape (Symbol_Pos.content ss)), state)
+          fun expand (Antiquote.Text tok) state =
+                (K ("", Symbol.escape (ML_Lex.content_of tok)), state)
             | expand (Antiquote.Antiq x) (scope, background) =
                 let
                   val context = Stack.top scope;