src/Pure/General/symbol_pos.ML
changeset 43709 717e96cf9527
parent 42503 27514b6fbe93
child 43773 e8ba493027a3
--- a/src/Pure/General/symbol_pos.ML	Fri Jul 08 16:01:14 2011 +0200
+++ b/src/Pure/General/symbol_pos.ML	Fri Jul 08 16:13:34 2011 +0200
@@ -11,7 +11,6 @@
   val $$$ : Symbol.symbol -> T list -> T list * T list
   val ~$$$ : Symbol.symbol -> T list -> T list * T list
   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,23 +41,9 @@
 
 fun symbol ((s, _): T) = s;
 
-
-(* content *)
-
 val content = implode o map symbol;
 
 
-val tab_width = (8: int);
-
-fun untabify ("\t", pos) =
-      (case Position.column_of pos of
-        SOME n => Symbol.spaces (tab_width - ((n - 1) mod tab_width))
-      | NONE => Symbol.space)
-  | untabify (s, _) = s;
-
-val untabify_content = implode o map untabify;
-
-
 (* stopper *)
 
 fun mk_eof pos = (Symbol.eof, pos);