changeset 27984 | b4dd58cff97c |
parent 27864 | 827730aea9e8 |
child 29606 | fedb8be05f24 |
--- 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;