src/Pure/POLY.ML
author paulson
Thu Jun 05 13:28:32 1997 +0200 (1997-06-05)
changeset 3406 131262e21ada
parent 2724 ddc6cf6b62e9
permissions -rw-r--r--
There was never need for another copy of radixstring...
     1 (*  Title:      Pure/POLY
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Compatibility file for Poly/ML (AHL release 1.88)
     7 *)
     8 
     9 open PolyML ExtendedIO;
    10 
    11 use"basis.ML";
    12 
    13 (*A conditional timing function: applies f to () and, if the flag is true,
    14   prints its runtime.*)
    15 
    16 fun cond_timeit flag f =
    17   if flag then
    18     let val before = System.processtime()
    19         val result = f()
    20         val both = real(System.processtime() - before) / 10.0
    21     in  output(std_out, "Process time (incl GC): "^
    22                          makestring both ^ " secs\n");
    23         result
    24     end
    25   else f();
    26 
    27 
    28 (*Save function: in Poly/ML, ignores filename and commits to present file*)
    29 
    30 fun xML filename banner = commit();
    31 
    32 
    33 (*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
    34 
    35 fun make_pp _ pprint (str, blk, brk, en) obj =
    36   pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
    37     fn () => brk (99999, 0), en);
    38 
    39 
    40 (*** File handling ***)
    41 
    42 local
    43 
    44 (*These are functions from library.ML *)
    45 fun take_suffix _ [] = ([], [])
    46   | take_suffix pred (x :: xs) =
    47       (case take_suffix pred xs of
    48          ([], sffx) => if pred x then ([], x :: sffx)
    49                                  else ([x], sffx)
    50        | (prfx, sffx) => (x :: prfx, sffx));
    51 
    52 fun apr (f,y) x = f(x,y);
    53 
    54 fun seq (proc: 'a -> unit) : 'a list -> unit =
    55   let fun seqf [] = ()
    56         | seqf (x :: xs) = (proc x; seqf xs)
    57   in seqf end;
    58 
    59 in
    60 
    61 (*Get time of last modification; if file doesn't exist return an empty string*)
    62 fun file_info "" = ""
    63   | file_info name = makestring (System.filedate name)  handle _ => "";
    64 
    65 
    66 structure OS =
    67   struct
    68   structure FileSys =
    69     struct
    70     val chDir = PolyML.cd
    71 
    72     fun remove name =    (*Delete a file *)
    73       let val (is, os) = ExtendedIO.execute ("rm " ^ name)
    74       in close_in is; close_out os end;
    75 
    76     (*Get pathname of current working directory *)
    77     fun getDir () =
    78       let val (is, os) = ExtendedIO.execute ("pwd")
    79 	  val (path, _) = take_suffix (apr(op=,"\n")) (*remove newline*)
    80 			   (explode (ExtendedIO.input_line is)) 
    81       in close_in is; close_out os; implode path end;
    82 
    83     end
    84   end;
    85 
    86 
    87 
    88 (*** ML command execution ***)
    89 
    90 val use_string =
    91   let fun exec command =
    92     let val firstLine = ref true;
    93 
    94         fun getLine () =
    95           if !firstLine
    96           then (firstLine := false; command)
    97           else raise Io "use_string: buffer exhausted"
    98     in PolyML.compiler (getLine, fn s => output (std_out, s)) () end
    99   in seq exec end;
   100 
   101 end;
   102 
   103 
   104 (*** System command execution ***)
   105 
   106 (*Execute an Unix command which doesn't take any input from stdin and
   107   sends its output to stdout.*)
   108 fun execute command =
   109   let val (is, os) =  ExtendedIO.execute command;
   110       val result = input (is, 999999);
   111   in close_out os;
   112      close_in is;
   113      result
   114   end;
   115 
   116 
   117 (*Non-printing and 8-bit chars are forbidden in string constants*)
   118 val needs_filtered_use = true;