src/Pure/General/symbol_pos.ML

--- a/src/Pure/General/symbol_pos.ML	Wed Aug 13 20:57:22 2008 +0200
+++ b/src/Pure/General/symbol_pos.ML	Wed Aug 13 20:57:24 2008 +0200
@@ -17,6 +17,7 @@
 sig
   include BASIC_SYMBOL_POS
   val content: T list -> string
+  val untabify_content: T list -> string
   val is_eof: T -> bool
   val stopper: T Scan.stopper
   val !!! : string -> (T list -> 'a) -> T list -> 'a
@@ -42,9 +43,24 @@
 type T = Symbol.symbol * Position.T;
 
 fun symbol ((s, _): T) = s;
+
+
+(* content *)
+
 val content = implode o map symbol;
 
 
+val tab_width = 8;
+
+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")
+  | untabify (s, _) = s;
+
+val untabify_content = implode o map untabify;
+
+
 (* stopper *)
 
 fun mk_eof pos = (Symbol.eof, pos);