src/Pure/ML-Systems/smlnj-0.93.ML
author wenzelm
Mon, 16 Dec 1996 10:35:51 +0100
changeset 2413 a00f0476e189
child 3594 193cc37e6f60
permissions -rw-r--r--
SML/NJ startup script (for 0.93).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/smlnj-0.93.ML
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     3
    Author:     Carsten Clasohm, TU Muenchen
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     4
    Copyright   1996  TU Muenchen
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     5
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     6
Compatibility file for Standard ML of New Jersey version 0.93.
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     7
*)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     8
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     9
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    10
use"basis.ML";
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    11
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    12
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    13
(*** Poly/ML emulation ***)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    14
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    15
fun quit () = exit 0;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    16
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    17
(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    18
fun print_depth n = (System.Control.Print.printDepth := n div 2;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    19
                     System.Control.Print.printLength := n);
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    20
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    21
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    22
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    23
fun make_pp path pprint =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    24
  let
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    25
    open System.PrettyPrint;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    26
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    27
    fun pp pps obj =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    28
      pprint obj
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    29
        (add_string pps, begin_block pps INCONSISTENT,
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    30
          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    31
          fn () => end_block pps);
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    32
  in
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    33
    (path, pp)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    34
  end;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    35
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    36
fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    37
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    38
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    39
(*** New Jersey ML parameters ***)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    40
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    41
(* Suppresses Garbage Collection messages;  default was 2 *)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    42
System.Control.Runtime.gcmessages := 0;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    43
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    44
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    45
(*** Timing functions ***)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    46
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    47
(*Print microseconds, suppressing trailing zeroes*)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    48
fun umakestring 0 = ""
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    49
  | umakestring n = chr(ord "0" + n div 100000) ^
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    50
                    umakestring(10 * (n mod 100000));
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    51
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    52
(*A conditional timing function: applies f to () and, if the flag is true,
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    53
  prints its runtime. *)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    54
fun cond_timeit flag f =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    55
  if flag then
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    56
    let fun string_of_time (System.Timer.TIME {sec, usec}) =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    57
            makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    58
        open System.Timer;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    59
        val start = start_timer()
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    60
        val result = f();
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    61
        val nongc = check_timer(start)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    62
        and gc = check_timer_gc(start);
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    63
        val both = add_time(nongc, gc)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    64
    in  print("Non GC " ^ string_of_time nongc ^
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    65
               "   GC " ^ string_of_time gc ^
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    66
               "  both "^ string_of_time both ^ " secs\n");
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    67
        result
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    68
    end
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    69
  else f();
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    70
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    71
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    72
(*** File handling ***)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    73
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    74
(*Get time of last modification; if file doesn't exist return an empty string*)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    75
local
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    76
    open System.Timer;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    77
    open System.Unsafe.SysIO;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    78
in
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    79
  fun file_info "" = ""
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    80
    | file_info name = makestring (mtime (PATH name))  handle _ => "";
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    81
end;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    82
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    83
structure OS =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    84
  struct
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    85
  structure FileSys =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    86
    struct
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    87
    val chDir = System.Directory.cd
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    88
    val remove = System.Unsafe.SysIO.unlink       (*Delete a file *)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    89
    val getDir = System.Directory.getWD           (*path of working directory*)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    90
    end
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    91
  end;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    92
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    93
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    94
(*** ML command execution ***)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    95
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    96
fun use_string commands = 
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    97
  System.Compile.use_stream (open_string (implode commands));
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    98
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    99
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   100
(*** System command execution ***)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   101
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   102
(*Execute an Unix command which doesn't take any input from stdin and
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   103
  sends its output to stdout.
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   104
  This could be done more easily by IO.execute, but that function
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   105
  seems to be buggy in SML/NJ 0.93.*)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   106
fun execute command =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   107
  let val tmp_name = "isa_converted.tmp"
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   108
      val is = (System.system (command ^ " > " ^ tmp_name);
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   109
                open_in tmp_name);
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   110
      val result = input (is, 999999);
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   111
  in close_in is;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   112
     OS.FileSys.remove tmp_name;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   113
     result
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   114
  end;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   115
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   116
(*redefine to flush its output immediately -- temporary patch suggested
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   117
  by Kim Dam Petersen*)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   118
val output = fn(s, t) => (output(s, t); flush_out s);
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   119
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   120
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   121
(* symbol input *)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   122
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   123
val needs_filtered_use = false;