# HG changeset patch
# User wenzelm
# Date 1218653844 -7200
# Node ID 6454fef6a293aa5db18decdd9e13f8d5afcbccc9
# Parent  b67974f24d0c4b86f8f6c5b89516da9ac50771bd
added untabify_content;

diff -r b67974f24d0c -r 6454fef6a293 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);