(*  Title:      Pure/POLY

     ID:         $Id$

     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     Copyright   1991  University of Cambridge

 Compatibility file for Poly/ML (AHL release 1.88)

 *)

 open PolyML ExtendedIO;

 use"basis.ML";

 (*A conditional timing function: applies f to () and, if the flag is true,

   prints its runtime.*)

 fun cond_timeit flag f =

   if flag then

     let val before = System.processtime()

         val result = f()

         val both = real(System.processtime() - before) / 10.0

     in  output(std_out, "Process time (incl GC): "^

                          makestring both ^ " secs\n");

         result

     end

   else f();

 (*Save function: in Poly/ML, ignores filename and commits to present file*)

 fun xML filename banner = commit();

 (*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)

 fun make_pp _ pprint (str, blk, brk, en) obj =

   pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),

     fn () => brk (99999, 0), en);

 (*** File handling ***)

 local

 (*These are functions from library.ML *)

 fun take_suffix _ [] = ([], [])

   | take_suffix pred (x :: xs) =

       (case take_suffix pred xs of

          ([], sffx) => if pred x then ([], x :: sffx)

                                  else ([x], sffx)

        | (prfx, sffx) => (x :: prfx, sffx));

 fun apr (f,y) x = f(x,y);

 fun seq (proc: 'a -> unit) : 'a list -> unit =

   let fun seqf [] = ()

         | seqf (x :: xs) = (proc x; seqf xs)

   in seqf end;

 fun radixpand num : int list =

   let fun radix (n, tail) =

     if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail)

   in radix (num, []) end;

 fun radixstring num =

   let fun chrof n = chr (ord "0" + n);

   in implode (map chrof (radixpand num)) end;

 in

 (*Get time of last modification; if file doesn't exist return an empty string*)

 fun file_info "" = ""

   | file_info name = radixstring (System.filedate name)  handle _ => "";

 structure OS =

   struct

   structure FileSys =

     struct

     val chDir = PolyML.cd

     fun remove name =    (*Delete a file *)

       let val (is, os) = ExtendedIO.execute ("rm " ^ name)

       in close_in is; close_out os end;

     (*Get pathname of current working directory *)

     fun getDir () =

       let val (is, os) = ExtendedIO.execute ("pwd")

 	  val (path, _) = take_suffix (apr(op=,"\n")) (*remove newline*)

 			   (explode (ExtendedIO.input_line is)) 

       in close_in is; close_out os; implode path end;

     end

   end;

 (*** ML command execution ***)

 val use_string =

   let fun exec command =

     let val firstLine = ref true;

         fun getLine () =

           if !firstLine

           then (firstLine := false; command)

           else raise Io "use_string: buffer exhausted"

     in PolyML.compiler (getLine, fn s => output (std_out, s)) () end

   in seq exec end;

 end;

 (*** System command execution ***)

 (*Execute an Unix command which doesn't take any input from stdin and

   sends its output to stdout.*)

 fun execute command =

   let val (is, os) =  ExtendedIO.execute command;

       val result = input (is, 999999);

   in close_out os;

      close_in is;

      result

   end;

 (*Non-printing and 8-bit chars are forbidden in string constants*)

 val needs_filtered_use = true;