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