beautified file_info a bit
authorclasohm
Mon Jan 15 14:56:38 1996 +0100 (1996-01-15)
changeset 14372ebbc23d49fa
parent 1436 88b73ad6b0da
child 1438 3cc22794ce71
beautified file_info a bit
src/Pure/POLY.ML
     1.1 --- a/src/Pure/POLY.ML	Mon Jan 15 14:47:56 1996 +0100
     1.2 +++ b/src/Pure/POLY.ML	Mon Jan 15 14:56:38 1996 +0100
     1.3 @@ -55,23 +55,21 @@
     1.4          | seqf (x :: xs) = (proc x; seqf xs)
     1.5    in seqf end;
     1.6  
     1.7 +fun radixpand num : int list =
     1.8 +  let fun radix (n, tail) =
     1.9 +    if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail)
    1.10 +  in radix (num, []) end;
    1.11 +
    1.12 +fun radixstring num =
    1.13 +  let fun chrof n = chr (ord "0" + n);
    1.14 +  in implode (map chrof (radixpand num)) end;
    1.15 +
    1.16  in
    1.17  
    1.18  (*Get a string containing the time of last modification, attributes, owner
    1.19    and size of file (but not the path) *)
    1.20  fun file_info "" = ""
    1.21 -  | file_info name =
    1.22 -    let fun radixpand num : int list =
    1.23 -          let fun radix (n, tail) =
    1.24 -            if n < 10 then n :: tail
    1.25 -            else radix (n div 10, (n mod 10) :: tail)
    1.26 -          in radix (num, []) end;
    1.27 -
    1.28 -        fun radixstring num =
    1.29 -          let val offset = ord "0";
    1.30 -              fun chrof n = chr (offset + n);
    1.31 -          in implode (map chrof (radixpand num)) end;
    1.32 -     in radixstring (System.filedate name) end;
    1.33 +  | file_info name = radixstring (System.filedate name);
    1.34  
    1.35  (*Delete a file *)
    1.36  fun delete_file name =