src/Pure/POLY.ML
author paulson
Fri May 30 15:14:59 1997 +0200 (1997-05-30)
changeset 3365 86c0d1988622
parent 2724 ddc6cf6b62e9
child 3406 131262e21ada
permissions -rw-r--r--
flushOut ensures that no recent error message are lost (not certain this is
necessary)
     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 fun radixpand num : int list =
    60   let fun radix (n, tail) =
    61     if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail)
    62   in radix (num, []) end;
    63 
    64 fun radixstring num =
    65   let fun chrof n = chr (ord "0" + n);
    66   in implode (map chrof (radixpand num)) end;
    67 
    68 in
    69 
    70 (*Get time of last modification; if file doesn't exist return an empty string*)
    71 fun file_info "" = ""
    72   | file_info name = radixstring (System.filedate name)  handle _ => "";
    73 
    74 
    75 structure OS =
    76   struct
    77   structure FileSys =
    78     struct
    79     val chDir = PolyML.cd
    80 
    81     fun remove name =    (*Delete a file *)
    82       let val (is, os) = ExtendedIO.execute ("rm " ^ name)
    83       in close_in is; close_out os end;
    84 
    85     (*Get pathname of current working directory *)
    86     fun getDir () =
    87       let val (is, os) = ExtendedIO.execute ("pwd")
    88 	  val (path, _) = take_suffix (apr(op=,"\n")) (*remove newline*)
    89 			   (explode (ExtendedIO.input_line is)) 
    90       in close_in is; close_out os; implode path end;
    91 
    92     end
    93   end;
    94 
    95 
    96 
    97 (*** ML command execution ***)
    98 
    99 val use_string =
   100   let fun exec command =
   101     let val firstLine = ref true;
   102 
   103         fun getLine () =
   104           if !firstLine
   105           then (firstLine := false; command)
   106           else raise Io "use_string: buffer exhausted"
   107     in PolyML.compiler (getLine, fn s => output (std_out, s)) () end
   108   in seq exec end;
   109 
   110 end;
   111 
   112 
   113 (*** System command execution ***)
   114 
   115 (*Execute an Unix command which doesn't take any input from stdin and
   116   sends its output to stdout.*)
   117 fun execute command =
   118   let val (is, os) =  ExtendedIO.execute command;
   119       val result = input (is, 999999);
   120   in close_out os;
   121      close_in is;
   122      result
   123   end;
   124 
   125 
   126 (*Non-printing and 8-bit chars are forbidden in string constants*)
   127 val needs_filtered_use = true;