# HG changeset patch
# User wenzelm
# Date 850121983 -3600
# Node ID 008ce88c9913f2416980c63e8b1ed55d1349dfc0
# Parent  e965156e84e3ffaa086ce88a69154bd327663258
renamed from POLY.ML;

diff -r e965156e84e3 -r 008ce88c9913 src/Pure/ML-Systems/polyml-2.07.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-2.07.ML	Mon Dec 09 09:59:43 1996 +0100
@@ -0,0 +1,123 @@
+(*  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;
diff -r e965156e84e3 -r 008ce88c9913 src/Pure/ML-Systems/polyml-3.1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-3.1.ML	Mon Dec 09 09:59:43 1996 +0100
@@ -0,0 +1,123 @@
+(*  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;