# HG changeset patch
# User wenzelm
# Date 1219591422 -7200
# Node ID b4dd58cff97c7954349c1d293cf614ae89fbb58e
# Parent  00e005cdceb0d34cb55069f78a3154346fc2caee
untabify: silently turn tab into space if column information is unavailable;

diff -r 00e005cdceb0 -r b4dd58cff97c src/Pure/General/symbol_pos.ML
--- 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;