cleaned up;
authorwenzelm
Tue Aug 05 16:14:23 1997 +0200 (1997-08-05)
changeset 3588e487bf0ed6c4
parent 3587 00ea30ea0734
child 3589 244daa75f890
cleaned up;
added getenv;
src/Pure/ML-Systems/polyml.ML
     1.1 --- a/src/Pure/ML-Systems/polyml.ML	Tue Aug 05 10:50:24 1997 +0200
     1.2 +++ b/src/Pure/ML-Systems/polyml.ML	Tue Aug 05 16:14:23 1997 +0200
     1.3 @@ -3,123 +3,119 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1991  University of Cambridge
     1.6  
     1.7 -Compatibility file for Poly/ML (versions 2.x, 3.x).
     1.8 +Compatibility file for Poly/ML (versions 2.x and 3.x).
     1.9  *)
    1.10  
    1.11  open PolyML ExtendedIO;
    1.12  
    1.13 -use"basis.ML";
    1.14 +(*needs the Basis Library emulation*)
    1.15 +use "basis.ML";
    1.16 +
    1.17  
    1.18  
    1.19 -(*A conditional timing function: applies f to () and, if the flag is true,
    1.20 -  prints its runtime.*)
    1.21 +(** ML system related **)
    1.22 +
    1.23 +(* timing *)
    1.24 +
    1.25 +(*a conditional timing function: applies f to () and, if the flag is true,
    1.26 +  prints its runtime*)
    1.27  
    1.28  fun cond_timeit flag f =
    1.29    if flag then
    1.30 -    let val before = System.processtime()
    1.31 -        val result = f()
    1.32 -        val both = real(System.processtime() - before) / 10.0
    1.33 -    in  output(std_out, "Process time (incl GC): "^
    1.34 -                         makestring both ^ " secs\n");
    1.35 -        result
    1.36 +    let
    1.37 +      val before = System.processtime ();
    1.38 +      val result = f ();
    1.39 +      val both = real (System.processtime () - before) / 10.0;
    1.40 +    in
    1.41 +      print ("Process time (incl GC): " ^ makestring both ^ " secs\n");
    1.42 +      result
    1.43      end
    1.44 -  else f();
    1.45 +  else f ();
    1.46  
    1.47  
    1.48 -(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
    1.49 +(* toplevel pretty printing (see also Pure/install_pp.ML) *)
    1.50  
    1.51  fun make_pp _ pprint (str, blk, brk, en) obj =
    1.52    pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
    1.53      fn () => brk (99999, 0), en);
    1.54  
    1.55  
    1.56 -(*** File handling ***)
    1.57 +(* ML command execution -- 'eval' *)
    1.58 +
    1.59 +val use_string =
    1.60 +  let
    1.61 +    fun exec line =
    1.62 +      let
    1.63 +        val is_first = ref true;
    1.64 +
    1.65 +        fun get_line () =
    1.66 +          if ! is_first then (is_first := false; line)
    1.67 +          else raise Io "use_string: buffer exhausted";
    1.68 +      in
    1.69 +        PolyML.compiler (get_line, print) ()
    1.70 +      end;
    1.71 +
    1.72 +    fun execs [] = ()
    1.73 +      | execs (line :: lines) = (exec line; execs lines);
    1.74 +  in execs end;
    1.75 +
    1.76 +
    1.77 +
    1.78 +(** OS related **)
    1.79  
    1.80  local
    1.81  
    1.82 -(*These are functions from library.ML *)
    1.83 -fun take_suffix _ [] = ([], [])
    1.84 -  | take_suffix pred (x :: xs) =
    1.85 -      (case take_suffix pred xs of
    1.86 -         ([], sffx) => if pred x then ([], x :: sffx)
    1.87 -                                 else ([x], sffx)
    1.88 -       | (prfx, sffx) => (x :: prfx, sffx));
    1.89 -
    1.90 -fun apr (f,y) x = f(x,y);
    1.91 +fun drop_last [] = []
    1.92 +  | drop_last [x] = []
    1.93 +  | drop_last (x :: xs) = x :: drop_last xs;
    1.94  
    1.95 -fun seq (proc: 'a -> unit) : 'a list -> unit =
    1.96 -  let fun seqf [] = ()
    1.97 -        | seqf (x :: xs) = (proc x; seqf xs)
    1.98 -  in seqf end;
    1.99 -
   1.100 -fun radixpand num : int list =
   1.101 -  let fun radix (n, tail) =
   1.102 -    if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail)
   1.103 -  in radix (num, []) end;
   1.104 -
   1.105 -fun radixstring num =
   1.106 -  let fun chrof n = chr (ord "0" + n);
   1.107 -  in implode (map chrof (radixpand num)) end;
   1.108 +val drop_last_char = implode o drop_last o explode;
   1.109  
   1.110  in
   1.111  
   1.112 -(*Get time of last modification; if file doesn't exist return an empty string*)
   1.113 -fun file_info "" = ""
   1.114 -  | file_info name = radixstring (System.filedate name)  handle _ => "";
   1.115  
   1.116 -
   1.117 -structure OS =
   1.118 -  struct
   1.119 -  structure FileSys =
   1.120 -    struct
   1.121 -    val chDir = PolyML.cd
   1.122 +(* system command execution *)
   1.123  
   1.124 -    fun remove name =    (*Delete a file *)
   1.125 -      let val (is, os) = ExtendedIO.execute ("rm " ^ name)
   1.126 -      in close_in is; close_out os end;
   1.127 -
   1.128 -    (*Get pathname of current working directory *)
   1.129 -    fun getDir () =
   1.130 -      let val (is, os) = ExtendedIO.execute ("pwd")
   1.131 -	  val (path, _) = take_suffix (apr(op=,"\n")) (*remove newline*)
   1.132 -			   (explode (ExtendedIO.input_line is)) 
   1.133 -      in close_in is; close_out os; implode path end;
   1.134 -
   1.135 -    end
   1.136 +(*execute Unix command which doesn't take any input from stdin and
   1.137 +  sends its output to stdout*)
   1.138 +fun execute command =
   1.139 +  let
   1.140 +    val (is, os) =  ExtendedIO.execute command;
   1.141 +    val result = input (is, 999999);
   1.142 +  in
   1.143 +    close_out os;
   1.144 +    close_in is;
   1.145 +    result
   1.146    end;
   1.147  
   1.148  
   1.149 -
   1.150 -(*** ML command execution ***)
   1.151 +(* file handling *)
   1.152  
   1.153 -val use_string =
   1.154 -  let fun exec command =
   1.155 -    let val firstLine = ref true;
   1.156 +(*get time of last modification; if file doesn't exist return an empty string*)
   1.157 +fun file_info "" = ""		(* FIXME !? *)
   1.158 +  | file_info name = Int.toString (System.filedate name) handle _ => "";
   1.159  
   1.160 -        fun getLine () =
   1.161 -          if !firstLine
   1.162 -          then (firstLine := false; command)
   1.163 -          else raise Io "use_string: buffer exhausted"
   1.164 -    in PolyML.compiler (getLine, fn s => output (std_out, s)) () end
   1.165 -  in seq exec end;
   1.166 +structure OS =
   1.167 +struct
   1.168 +  structure FileSys =
   1.169 +  struct
   1.170 +    val chDir = PolyML.cd;
   1.171 +    fun remove name = (execute ("rm " ^ name); ());
   1.172 +    fun getDir () = drop_last_char (execute "pwd");
   1.173 +  end;
   1.174 +end;
   1.175 +
   1.176 +
   1.177 +(* getenv *)
   1.178 +
   1.179 +fun getenv var = drop_last_char
   1.180 +  (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
   1.181 +
   1.182  
   1.183  end;
   1.184  
   1.185  
   1.186 -(*** System command execution ***)
   1.187 -
   1.188 -(*Execute an Unix command which doesn't take any input from stdin and
   1.189 -  sends its output to stdout.*)
   1.190 -fun execute command =
   1.191 -  let val (is, os) =  ExtendedIO.execute command;
   1.192 -      val result = input (is, 999999);
   1.193 -  in close_out os;
   1.194 -     close_in is;
   1.195 -     result
   1.196 -  end;
   1.197 -
   1.198 -
   1.199 -(* symbol input *)
   1.200 +(* non-ASCII input (see also Thy/symbol_input.ML) *)
   1.201  
   1.202  val needs_filtered_use =
   1.203    (case explode ml_system of