src/Pure/ML-Systems/smlnj-0.93.ML
author wenzelm
Tue, 02 Dec 1997 12:38:39 +0100
changeset 4340 f5d7fbb73103
parent 3631 88a279998f90
child 4428 5c26253b8a2e
permissions -rw-r--r--
ISABELLE_TMP;
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
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
     9
(*needs the Basis Library emulation*)
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    10
use "basis.ML";
2413
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
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    13
(** ML system related **)
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    14
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    15
(* New Jersey ML parameters *)
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    16
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    17
System.Control.Runtime.gcmessages := 0;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    18
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    19
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    20
(* Poly/ML emulation *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    21
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    22
fun quit () = exit 0;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    23
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    24
(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    25
fun print_depth n =
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    26
 (System.Control.Print.printDepth := n div 2;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    27
  System.Control.Print.printLength := n);
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    28
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    29
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    30
(* timing *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    31
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    32
local
3631
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    33
  (*print microseconds, suppressing trailing zeroes*)
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    34
  fun umakestring 0 = ""
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    35
    | umakestring n =
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    36
        chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    37
in
3631
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    38
  (*a conditional timing function: applies f to () and, if the flag is true,
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    39
    prints its runtime*)
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    40
  fun cond_timeit flag f =
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    41
    if flag then
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    42
      let fun string_of_time (System.Timer.TIME {sec, usec}) =
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    43
              makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    44
          open System.Timer;
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    45
          val start = start_timer()
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    46
          val result = f();
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    47
          val nongc = check_timer(start)
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    48
          and gc = check_timer_gc(start);
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    49
          val both = add_time(nongc, gc)
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    50
      in  print("Non GC " ^ string_of_time nongc ^
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    51
                 "   GC " ^ string_of_time gc ^
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    52
                 "  both "^ string_of_time both ^ " secs\n");
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    53
          result
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    54
      end
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    55
    else f();
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    56
end;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    57
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    58
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    59
(* toplevel pretty printing (see also Pure/install_pp.ML) *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    60
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    61
fun make_pp path pprint =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    62
  let
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    63
    open System.PrettyPrint;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    64
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    65
    fun pp pps obj =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    66
      pprint obj
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    67
        (add_string pps, begin_block pps INCONSISTENT,
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    68
          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    69
          fn () => end_block pps);
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    70
  in
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    71
    (path, pp)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    72
  end;
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
fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    75
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    76
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    77
(* ML command execution *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    78
3631
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    79
fun use_strings commands =
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    80
  System.Compile.use_stream (open_string (implode commands));
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    81
2413
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
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    84
(** OS related **)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    85
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    86
(* system command execution *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    87
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    88
(*execute Unix command which doesn't take any input from stdin and
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    89
  sends its output to stdout; could be done more easily by IO.execute,
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    90
  but that function seems to be buggy in SML/NJ 0.93*)
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    91
fun execute command =
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    92
  let
4340
f5d7fbb73103 ISABELLE_TMP;
wenzelm
parents: 3631
diff changeset
    93
    val tmp_name = getenv "$ISABELLE_TMP" ^ "/isabelle-execute";
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    94
    val is = (System.system (command ^ " > " ^ tmp_name); open_in tmp_name);
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    95
    val result = input (is, 999999);
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    96
  in
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    97
    close_in is;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    98
    System.Unsafe.SysIO.unlink tmp_name;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    99
    result
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   100
  end;
2413
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
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   103
(* file handling *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   104
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   105
(*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
   106
local
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   107
  open System.Timer System.Unsafe.SysIO;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   108
in
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   109
  fun file_info "" = ""
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   110
    | file_info name = makestring (mtime (PATH name)) handle _ => "";
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   111
end;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   112
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   113
structure OS =
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   114
struct
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   115
  structure FileSys =
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   116
  struct
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   117
    val chDir = System.Directory.cd;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   118
    val remove = System.Unsafe.SysIO.unlink;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   119
    val getDir = System.Directory.getWD;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   120
  end;
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   121
end;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   122
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   123
(*redefine to flush its output immediately -- temporary patch suggested
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   124
  by Kim Dam Petersen*)		(* FIXME !? *)
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   125
val output = fn (s, t) => (output (s, t); flush_out s);
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   126
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   127
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   128
(* getenv *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   129
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   130
local
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   131
  fun drop_last [] = []
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   132
    | drop_last [x] = []
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   133
    | drop_last (x :: xs) = x :: drop_last xs;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   134
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   135
  val drop_last_char = implode o drop_last o explode;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   136
in
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   137
  fun getenv var = drop_last_char
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   138
    (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   139
end;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   140
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   141
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   142
(* non-ASCII input (see also Thy/symbol_input.ML) *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   143
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   144
val needs_filtered_use = false;