1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Dec 09 16:09:38 1996 +0100
     1.3 @@ -0,0 +1,119 @@
     1.4 +(*  Title:      Pure/ML-Systems/polyml.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +
     1.9 +Compatibility file for Poly/ML (versions 2.x, 3.x).
    1.10 +*)
    1.11 +
    1.12 +open PolyML ExtendedIO;
    1.13 +
    1.14 +use"basis.ML";
    1.15 +
    1.16 +
    1.17 +(*A conditional timing function: applies f to () and, if the flag is true,
    1.18 +  prints its runtime.*)
    1.19 +
    1.20 +fun cond_timeit flag f =
    1.21 +  if flag then
    1.22 +    let val before = System.processtime()
    1.23 +        val result = f()
    1.24 +        val both = real(System.processtime() - before) / 10.0
    1.25 +    in  output(std_out, "Process time (incl GC): "^
    1.26 +                         makestring both ^ " secs\n");
    1.27 +        result
    1.28 +    end
    1.29 +  else f();
    1.30 +
    1.31 +
    1.32 +(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
    1.33 +
    1.34 +fun make_pp _ pprint (str, blk, brk, en) obj =
    1.35 +  pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
    1.36 +    fn () => brk (99999, 0), en);
    1.37 +
    1.38 +
    1.39 +(*** File handling ***)
    1.40 +
    1.41 +local
    1.42 +
    1.43 +(*These are functions from library.ML *)
    1.44 +fun take_suffix _ [] = ([], [])
    1.45 +  | take_suffix pred (x :: xs) =
    1.46 +      (case take_suffix pred xs of
    1.47 +         ([], sffx) => if pred x then ([], x :: sffx)
    1.48 +                                 else ([x], sffx)
    1.49 +       | (prfx, sffx) => (x :: prfx, sffx));
    1.50 +
    1.51 +fun apr (f,y) x = f(x,y);
    1.52 +
    1.53 +fun seq (proc: 'a -> unit) : 'a list -> unit =
    1.54 +  let fun seqf [] = ()
    1.55 +        | seqf (x :: xs) = (proc x; seqf xs)
    1.56 +  in seqf end;
    1.57 +
    1.58 +fun radixpand num : int list =
    1.59 +  let fun radix (n, tail) =
    1.60 +    if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail)
    1.61 +  in radix (num, []) end;
    1.62 +
    1.63 +fun radixstring num =
    1.64 +  let fun chrof n = chr (ord "0" + n);
    1.65 +  in implode (map chrof (radixpand num)) end;
    1.66 +
    1.67 +in
    1.68 +
    1.69 +(*Get time of last modification; if file doesn't exist return an empty string*)
    1.70 +fun file_info "" = ""
    1.71 +  | file_info name = radixstring (System.filedate name)  handle _ => "";
    1.72 +
    1.73 +
    1.74 +structure OS =
    1.75 +  struct
    1.76 +  structure FileSys =
    1.77 +    struct
    1.78 +    val chDir = PolyML.cd
    1.79 +
    1.80 +    fun remove name =    (*Delete a file *)
    1.81 +      let val (is, os) = ExtendedIO.execute ("rm " ^ name)
    1.82 +      in close_in is; close_out os end;
    1.83 +
    1.84 +    (*Get pathname of current working directory *)
    1.85 +    fun getDir () =
    1.86 +      let val (is, os) = ExtendedIO.execute ("pwd")
    1.87 +	  val (path, _) = take_suffix (apr(op=,"\n")) (*remove newline*)
    1.88 +			   (explode (ExtendedIO.input_line is)) 
    1.89 +      in close_in is; close_out os; implode path end;
    1.90 +
    1.91 +    end
    1.92 +  end;
    1.93 +
    1.94 +
    1.95 +
    1.96 +(*** ML command execution ***)
    1.97 +
    1.98 +val use_string =
    1.99 +  let fun exec command =
   1.100 +    let val firstLine = ref true;
   1.101 +
   1.102 +        fun getLine () =
   1.103 +          if !firstLine
   1.104 +          then (firstLine := false; command)
   1.105 +          else raise Io "use_string: buffer exhausted"
   1.106 +    in PolyML.compiler (getLine, fn s => output (std_out, s)) () end
   1.107 +  in seq exec end;
   1.108 +
   1.109 +end;
   1.110 +
   1.111 +
   1.112 +(*** System command execution ***)
   1.113 +
   1.114 +(*Execute an Unix command which doesn't take any input from stdin and
   1.115 +  sends its output to stdout.*)
   1.116 +fun execute command =
   1.117 +  let val (is, os) =  ExtendedIO.execute command;
   1.118 +      val result = input (is, 999999);
   1.119 +  in close_out os;
   1.120 +     close_in is;
   1.121 +     result
   1.122 +  end;