author | wenzelm |
Sun, 24 Aug 2008 17:23:42 +0200 | |
changeset 27984 | b4dd58cff97c |
parent 27983 | 00e005cdceb0 |
child 27985 | fb774d10ea4c |
1.1 --- a/src/Pure/General/symbol_pos.ML Sun Aug 24 14:42:26 2008 +0200 1.2 +++ b/src/Pure/General/symbol_pos.ML Sun Aug 24 17:23:42 2008 +0200 1.3 @@ -55,7 +55,7 @@ 1.4 fun untabify ("\t", pos) = 1.5 (case Position.column_of pos of 1.6 SOME n => Symbol.spaces (tab_width - ((n - 1) mod tab_width)) 1.7 - | NONE => error "No column information -- cannot interpret tabulators") 1.8 + | NONE => Symbol.space) 1.9 | untabify (s, _) = s; 1.10 1.11 val untabify_content = implode o map untabify;