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