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