src/Pure/POLY.ML
author wenzelm
Tue Aug 23 19:31:05 1994 +0200 (1994-08-23)
changeset 573 2fa5ef27bd0a
parent 396 18c9c28d0f7e
child 1289 2edd7a39d92a
permissions -rw-r--r--
removed constant _constrain from Pure sig;
     1 (*  Title:      Pure/POLY
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Compatibility file for Poly/ML (AHL release 1.88)
     7 *)
     8 
     9 open PolyML ExtendedIO;
    10 
    11 
    12 (*A conditional timing function: applies f to () and, if the flag is true,
    13   prints its runtime.*)
    14 
    15 fun cond_timeit flag f =
    16   if flag then
    17     let val before = System.processtime()
    18         val result = f()
    19         val both = real(System.processtime() - before) / 10.0
    20     in  output(std_out, "Process time (incl GC): "^
    21                          makestring both ^ " secs\n");
    22         result
    23     end
    24   else f();
    25 
    26 
    27 (*Save function: in Poly/ML, ignores filename and commits to present file*)
    28 
    29 fun xML filename banner = commit();
    30 
    31 
    32 (*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
    33 
    34 fun make_pp _ pprint (str, blk, brk, en) obj =
    35   pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
    36     fn () => brk (99999, 0), en);
    37 
    38 
    39 (*** File handling ***)
    40 
    41 local
    42 
    43 (*These are functions from library.ML *)
    44 fun take_suffix _ [] = ([], [])
    45   | take_suffix pred (x :: xs) =
    46       (case take_suffix pred xs of
    47          ([], sffx) => if pred x then ([], x :: sffx)
    48                                  else ([x], sffx)
    49        | (prfx, sffx) => (x :: prfx, sffx));
    50 
    51 fun apr (f,y) x = f(x,y);
    52 
    53 fun seq (proc: 'a -> unit) : 'a list -> unit =
    54   let fun seqf [] = ()
    55         | seqf (x :: xs) = (proc x; seqf xs)
    56   in seqf end;
    57 
    58 in
    59 
    60 (*Get a string containing the time of last modification, attributes, owner
    61   and size of file (but not the path) *)
    62 fun file_info "" = ""
    63   | file_info name =
    64       let
    65           val (is, os) = ExtendedIO.execute ("ls -l " ^ name)
    66           val (result, _) = take_suffix (apr(op<>," ")) 
    67                               (explode (ExtendedIO.input_line is))
    68              (*Remove the part after the last " " (i.e. the path/filename) *)
    69         in close_in is;
    70            close_out os;
    71            implode result
    72         end;
    73 
    74 (*Delete a file *)
    75 fun delete_file name =
    76   let val (is, os) = ExtendedIO.execute ("rm " ^ name)
    77   in close_in is;
    78      close_out os
    79   end;
    80 
    81 (*Get pathname of current working directory *)
    82 fun pwd () =
    83   let val (is, os) = ExtendedIO.execute ("pwd")
    84       val (path, _) = take_suffix (apr(op=,"\n"))
    85                        (explode (ExtendedIO.input_line is)) (*remove newline *)
    86   in close_in is;
    87      close_out os;
    88      implode path
    89   end;
    90 
    91 
    92 (*** ML command execution ***)
    93 
    94 val use_string =
    95   let fun exec command =
    96     let val firstLine = ref true;
    97 
    98         fun getLine () =
    99           if !firstLine
   100           then (firstLine := false; command)
   101           else raise Io "use_string: buffer exhausted"
   102     in PolyML.compiler (getLine, fn s => output (std_out, s)) () end
   103   in seq exec end;
   104 
   105 end;