src/Pure/POLY.ML

Now uses type option instead of Fail/Subst

(*  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;