# HG changeset patch
# User wenzelm
# Date 939129935 -7200
# Node ID c522ec2adc37cbc7f45fdb63d6013258c3f4256c
# Parent  4dae7a4fceaf3ed0c1eb3995766f544897a79a14
added untabify;

diff -r 4dae7a4fceaf -r c522ec2adc37 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Oct 05 15:24:58 1999 +0200
+++ b/src/Pure/library.ML	Tue Oct 05 15:25:35 1999 +0200
@@ -138,6 +138,7 @@
   val std_output: string -> unit
   val prefix_lines: string -> string -> string
   val split_lines: string -> string list
+  val untabify: string list -> string list
   val suffix: string -> string -> string
   val unsuffix: string -> string -> string
 
@@ -712,6 +713,19 @@
 
 val split_lines = space_explode "\n";
 
+(*untabify*)
+fun untabify chs =
+  let
+    val tab_width = 8;
+
+    fun untab (_, "\n") = (0, ["\n"])
+      | untab (pos, "\t") = let val d = tab_width - (pos mod tab_width) in (pos + d, replicate d " ") end
+      | untab (pos, c) = (pos + 1, [c]);
+  in
+    if not (exists (equal "\t") chs) then chs
+    else flat (#2 (foldl_map untab (0, chs)))
+  end;
+
 (*append suffix*)
 fun suffix sfx s = s ^ sfx;