1.1 --- a/src/Pure/library.ML Wed Apr 04 00:11:12 2007 +0200
1.2 +++ b/src/Pure/library.ML Wed Apr 04 00:11:13 2007 +0200
1.3 @@ -239,7 +239,6 @@
1.4 val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
1.5 val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
1.6 val gensym: string -> string
1.7 - val scanwords: (string -> bool) -> string list -> string list
1.8 type stamp
1.9 val stamp: unit -> stamp
1.10 type serial
1.11 @@ -777,10 +776,11 @@
1.12 let
1.13 val tab_width = 8;
1.14
1.15 - fun untab pos [] ys = rev ys
1.16 + fun untab pos [] ys = rev ys
1.17 | untab pos ("\n" :: xs) ys = untab 0 xs ("\n" :: ys)
1.18 | untab pos ("\t" :: xs) ys =
1.19 - let val d = tab_width - (pos mod tab_width) in untab (pos + d) xs (replicate d " " @ ys) end
1.20 + let val d = tab_width - (pos mod tab_width)
1.21 + in untab (pos + d) xs (replicate d " " @ ys) end
1.22 | untab pos (c :: xs) ys = untab (pos + 1) xs (c :: ys);
1.23 in
1.24 if not (exists (fn c => c = "\t") chs) then chs
1.25 @@ -1131,7 +1131,7 @@
1.26 (** Freshly generated identifiers; supplied prefix MUST start with a letter **)
1.27 local
1.28 (*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
1.29 -fun gensym_char i =
1.30 +fun gensym_char i =
1.31 if i<26 then chr (ord "A" + i)
1.32 else if i<52 then chr (ord "a" + i - 26)
1.33 else chr (ord "0" + i - 52);
1.34 @@ -1146,18 +1146,6 @@
1.35 end;
1.36
1.37
1.38 -(* lexical scanning *)
1.39 -
1.40 -(*scan a list of characters into "words" composed of "letters" (recognized by
1.41 - is_let) and separated by any number of non-"letters"*)
1.42 -fun scanwords is_let cs =
1.43 - let fun scan1 [] = []
1.44 - | scan1 cs =
1.45 - let val (lets, rest) = take_prefix is_let cs
1.46 - in implode lets :: scanwords is_let rest end;
1.47 - in scan1 (#2 (take_prefix (not o is_let) cs)) end;
1.48 -
1.49 -
1.50 (* stamps and serial numbers *)
1.51
1.52 type stamp = unit ref;