src/Pure/General/symbol_pos.ML
changeset 43709 717e96cf9527
parent 42503 27514b6fbe93
child 43773 e8ba493027a3
     1.1 --- a/src/Pure/General/symbol_pos.ML	Fri Jul 08 16:01:14 2011 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Fri Jul 08 16:13:34 2011 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4    val $$$ : Symbol.symbol -> T list -> T list * T list
     1.5    val ~$$$ : Symbol.symbol -> T list -> T list * T list
     1.6    val content: T list -> string
     1.7 -  val untabify_content: T list -> string
     1.8    val is_eof: T -> bool
     1.9    val stopper: T Scan.stopper
    1.10    val !!! : string -> (T list -> 'a) -> T list -> 'a
    1.11 @@ -42,23 +41,9 @@
    1.12  
    1.13  fun symbol ((s, _): T) = s;
    1.14  
    1.15 -
    1.16 -(* content *)
    1.17 -
    1.18  val content = implode o map symbol;
    1.19  
    1.20  
    1.21 -val tab_width = (8: int);
    1.22 -
    1.23 -fun untabify ("\t", pos) =
    1.24 -      (case Position.column_of pos of
    1.25 -        SOME n => Symbol.spaces (tab_width - ((n - 1) mod tab_width))
    1.26 -      | NONE => Symbol.space)
    1.27 -  | untabify (s, _) = s;
    1.28 -
    1.29 -val untabify_content = implode o map untabify;
    1.30 -
    1.31 -
    1.32  (* stopper *)
    1.33  
    1.34  fun mk_eof pos = (Symbol.eof, pos);