# HG changeset patch
# User wenzelm
# Date 1218233374 -7200
# Node ID 52f07d5292cd34b34be9e95e459b936294995073
# Parent  b96c73f11a23bffd9c6e0185888f2aa77bcfb2fb
tuned SymbolPos interface;

diff -r b96c73f11a23 -r 52f07d5292cd src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Sat Aug 09 00:09:31 2008 +0200
+++ b/src/Pure/Isar/antiquote.ML	Sat Aug 09 00:09:34 2008 +0200
@@ -68,13 +68,13 @@
     T.!!! "missing closing brace of antiquotation"
       (Scan.repeat scan_ant -- ($$$ "}" |-- SymbolPos.scan_pos)))
   >> (fn (pos1, (body, pos2)) =>
-      let val (s, (pos, _)) = SymbolPos.implode_delim pos1 pos2 (flat body)
+      let val (s, (pos, _)) = SymbolPos.implode_range pos1 pos2 (flat body)
       in Antiq (s, pos) end);
 
 in
 
 val scan_antiquote =
- (Scan.repeat1 scan_txt >> (Text o implode o map symbol o flat) ||
+ (Scan.repeat1 scan_txt >> (Text o SymbolPos.content o flat) ||
   scan_antiq ||
   SymbolPos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
   SymbolPos.scan_pos --| $$$ "\\<rbrace>" >> Close);
diff -r b96c73f11a23 -r 52f07d5292cd src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Sat Aug 09 00:09:31 2008 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Sat Aug 09 00:09:34 2008 +0200
@@ -283,15 +283,17 @@
 
 fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
 
-fun token k ss = Token (SymbolPos.implode ss, (k, implode (map symbol ss)));
-fun token_delim k (pos1, (ss, pos2)) =
-  Token (SymbolPos.implode_delim pos1 pos2 ss, (k, implode (map symbol ss)));
+fun token k ss =
+  Token ((SymbolPos.implode ss, SymbolPos.range ss), (k, SymbolPos.content ss));
+
+fun token_range k (pos1, (ss, pos2)) =
+  Token (SymbolPos.implode_range pos1 pos2 ss, (k, SymbolPos.content ss));
 
 fun scan (lex1, lex2) = !!! "bad input"
-  (scan_string >> token_delim String ||
-    scan_alt_string >> token_delim AltString ||
-    scan_verbatim >> token_delim Verbatim ||
-    scan_comment >> token_delim Comment ||
+  (scan_string >> token_range String ||
+    scan_alt_string >> token_range AltString ||
+    scan_verbatim >> token_range Verbatim ||
+    scan_comment >> token_range Comment ||
     scan_space >> token Space ||
     scan_malformed >> token Malformed ||
     Scan.one (Symbol.is_sync o symbol) >> (token Sync o single) ||
diff -r b96c73f11a23 -r 52f07d5292cd src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sat Aug 09 00:09:31 2008 +0200
+++ b/src/Pure/ML/ml_lex.ML	Sat Aug 09 00:09:34 2008 +0200
@@ -184,9 +184,7 @@
 
 local
 
-fun token k s =
-  let val (x, range) = SymbolPos.implode s
-  in Token (range, (k, x)) end;
+fun token k ss = Token (SymbolPos.range ss, (k, SymbolPos.implode ss));
 
 val scan = !!! "bad input"
  (scan_char >> token Char ||