# HG changeset patch
# User wenzelm
# Date 1237493093 -3600
# Node ID 495672058d9761ecfb3ab8a405687c39aff68264
# Parent  a66fe59e0a26cc4fbf87aea4a487d5bf6024b0b5
added scan_antiq;
more robust scan_ml: plain scanning without cut, regular Symbol_Pos.content instead of Symbol_Pos.implode (which contains spurious Symbol.DEL is used with proper positions);

diff -r a66fe59e0a26 -r 495672058d97 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Thu Mar 19 19:49:09 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML	Thu Mar 19 21:04:53 2009 +0100
@@ -17,6 +17,7 @@
   val kind_of: token -> token_kind
   val content_of: token -> string
   val keywords: string list
+  val scan_antiq: Symbol_Pos.T list -> token Antiquote.antiquote * Symbol_Pos.T list
   val source: (Symbol.symbol, 'a) Source.source ->
     (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
       Source.source) Source.source
@@ -185,9 +186,9 @@
 
 local
 
-fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.implode ss));
+fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss));
 
-val scan_ml = !!! "bad input"
+val scan_ml =
  (scan_char >> token Char ||
   scan_string >> token String ||
   scan_blanks1 >> token Space ||
@@ -207,9 +208,11 @@
 
 in
 
+val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
+
 fun source src =
   Symbol_Pos.source (Position.line 1) src
-  |> Source.source Symbol_Pos.stopper (Scan.bulk scan_ml) (SOME (false, recover));
+  |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
 
 val tokenize = Source.of_string #> source #> Source.exhaust;