fixed bug in file_info
authorclasohm
Mon Jan 15 14:47:56 1996 +0100 (1996-01-15)
changeset 143688b73ad6b0da
parent 1435 aefcd255ed4a
child 1437 2ebbc23d49fa
fixed bug in file_info
src/Pure/POLY.ML
     1.1 --- a/src/Pure/POLY.ML	Thu Jan 11 10:29:31 1996 +0100
     1.2 +++ b/src/Pure/POLY.ML	Mon Jan 15 14:47:56 1996 +0100
     1.3 @@ -60,7 +60,18 @@
     1.4  (*Get a string containing the time of last modification, attributes, owner
     1.5    and size of file (but not the path) *)
     1.6  fun file_info "" = ""
     1.7 -  | file_info name = string_of_int (System.filedate name);
     1.8 +  | file_info name =
     1.9 +    let fun radixpand num : int list =
    1.10 +          let fun radix (n, tail) =
    1.11 +            if n < 10 then n :: tail
    1.12 +            else radix (n div 10, (n mod 10) :: tail)
    1.13 +          in radix (num, []) end;
    1.14 +
    1.15 +        fun radixstring num =
    1.16 +          let val offset = ord "0";
    1.17 +              fun chrof n = chr (offset + n);
    1.18 +          in implode (map chrof (radixpand num)) end;
    1.19 +     in radixstring (System.filedate name) end;
    1.20  
    1.21  (*Delete a file *)
    1.22  fun delete_file name =