# HG changeset patch
# User wenzelm
# Date 1218653850 -7200
# Node ID b28b2baada0651f78fde175ad023c6e772f63bc2
# Parent  b1bf607e06c295ca4fb15ff181d1b4220edeadba
scan: SymbolPos.tabify_content when creating tokens (for proper presentation output);

diff -r b1bf607e06c2 -r b28b2baada06 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Wed Aug 13 20:57:30 2008 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Wed Aug 13 20:57:30 2008 +0200
@@ -358,10 +358,10 @@
 fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
 
 fun token k ss =
-  Token ((SymbolPos.implode ss, SymbolPos.range ss), (k, SymbolPos.content ss), Slot);
+  Token ((SymbolPos.implode ss, SymbolPos.range ss), (k, SymbolPos.untabify_content ss), Slot);
 
 fun token_range k (pos1, (ss, pos2)) =
-  Token (SymbolPos.implode_range pos1 pos2 ss, (k, SymbolPos.content ss), Slot);
+  Token (SymbolPos.implode_range pos1 pos2 ss, (k, SymbolPos.untabify_content ss), Slot);
 
 fun scan (lex1, lex2) = !!! "bad input"
   (scan_string >> token_range String ||