Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
scan: SymbolPos.tabify_content when creating tokens (for proper presentation output);
authorwenzelm
Wed, 13 Aug 2008 20:57:30 +0200
changeset 27856 b28b2baada06
parent 27855 b1bf607e06c2
child 27857 fdf43ffceae0
scan: SymbolPos.tabify_content when creating tokens (for proper presentation output);
src/Pure/Isar/outer_lex.ML file | annotate | diff | comparison | revisions 
--- 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 ||
isabelle