removed obsolete untabify (superceded by SymbolPos.tabify_content);
authorwenzelm
Wed, 13 Aug 2008 20:57:20 +0200
changeset 27850 49503146b853
parent 27849 c74905423895
child 27851 b67974f24d0c
removed obsolete untabify (superceded by SymbolPos.tabify_content);
src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Aug 13 20:57:18 2008 +0200
+++ b/src/Pure/library.ML	Wed Aug 13 20:57:20 2008 +0200
@@ -152,7 +152,6 @@
   val space_explode: string -> string -> string list
   val split_lines: string -> string list
   val prefix_lines: string -> string -> string
-  val untabify: string list -> string list
   val prefix: string -> string -> string
   val suffix: string -> string -> string
   val unprefix: string -> string -> string
@@ -757,21 +756,6 @@
 fun prefix_lines "" txt = txt
   | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
 
-fun untabify chs =
-  let
-    val tab_width = 8;
-
-    fun untab pos [] ys = rev ys
-      | untab pos ("\n" :: xs) ys = untab 0 xs ("\n" :: ys)
-      | untab pos ("\t" :: xs) ys =
-          let val d = tab_width - (pos mod tab_width)
-          in untab (pos + d) xs (funpow d (cons " ") ys) end
-      | untab pos (c :: xs) ys = untab (pos + 1) xs (c :: ys);
-  in
-    if not (exists (fn c => c = "\t") chs) then chs
-    else untab 0 chs []
-  end;
-
 fun prefix prfx s = prfx ^ s;
 fun suffix sffx s = s ^ sffx;