src/Pure/ML-Systems/smlnj-0.93.ML
author wenzelm
Thu, 28 May 1998 12:21:05 +0200
changeset 4977 6cec2c0ffdbf
parent 4506 f21ec26b2265
child 5038 301c37df931d
permissions -rw-r--r--
added ml_prompts;
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
4506
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    30
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    31
(* timing *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    32
4506
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    33
(*Note start point for timing*)
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    34
fun startTiming() = System.Timer.start_timer();
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    35
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    36
(*Finish timing and return string*)
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    37
local
3631
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    38
  (*print microseconds, suppressing trailing zeroes*)
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    39
  fun umakestring 0 = ""
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    40
    | umakestring n =
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    41
        chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
4506
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    42
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    43
  fun string_of_time (System.Timer.TIME {sec, usec}) =
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    44
      makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    45
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    46
in
4506
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    47
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    48
fun endTiming start =
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    49
  let val nongc = System.Timer.check_timer(start)
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    50
      and gc    = System.Timer.check_timer_gc(start);
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    51
      val both  = System.Timer.add_time(nongc, gc)
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    52
  in  "Non GC " ^ string_of_time nongc ^
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    53
      "   GC " ^ string_of_time gc ^
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    54
      "  both "^ string_of_time both ^ " secs\n"
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    55
  end
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
4977
6cec2c0ffdbf added ml_prompts;
wenzelm
parents: 4506
diff changeset
    59
(* prompts *)
6cec2c0ffdbf added ml_prompts;
wenzelm
parents: 4506
diff changeset
    60
6cec2c0ffdbf added ml_prompts;
wenzelm
parents: 4506
diff changeset
    61
fun ml_prompts p1 p2 = ();
4506
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    62
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    63
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    64
(* toplevel pretty printing (see also Pure/install_pp.ML) *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    65
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    66
fun make_pp path pprint =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    67
  let
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    68
    open System.PrettyPrint;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    69
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    70
    fun pp pps obj =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    71
      pprint obj
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    72
        (add_string pps, begin_block pps INCONSISTENT,
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    73
          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    74
          fn () => end_block pps);
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    75
  in
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    76
    (path, pp)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    77
  end;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    78
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    79
fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    80
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    81
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    82
(* ML command execution *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    83
3631
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    84
fun use_strings commands =
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    85
  System.Compile.use_stream (open_string (implode commands));
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    86
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    87
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    88
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    89
(** OS related **)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    90
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    91
(* system command execution *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    92
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    93
(*execute Unix command which doesn't take any input from stdin and
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    94
  sends its output to stdout; could be done more easily by IO.execute,
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    95
  but that function seems to be buggy in SML/NJ 0.93*)
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    96
fun execute command =
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    97
  let
4494
7e5611945959 fixed execute;
wenzelm
parents: 4428
diff changeset
    98
    val tmp_name = "/tmp/isabelle-execute";
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    99
    val is = (System.system (command ^ " > " ^ tmp_name); open_in tmp_name);
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   100
    val result = input (is, 999999);
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   101
  in
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   102
    close_in is;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   103
    System.Unsafe.SysIO.unlink tmp_name;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   104
    result
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   105
  end;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   106
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   107
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   108
(* file handling *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   109
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   110
(*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
   111
local
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   112
  open System.Timer System.Unsafe.SysIO;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   113
in
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   114
  fun file_info "" = ""
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   115
    | file_info name = makestring (mtime (PATH name)) handle _ => "";
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   116
end;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   117
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   118
structure OS =
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   119
struct
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   120
  structure FileSys =
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   121
  struct
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   122
    val chDir = System.Directory.cd;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   123
    val remove = System.Unsafe.SysIO.unlink;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   124
    val getDir = System.Directory.getWD;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   125
  end;
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   126
end;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   127
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   128
(*redefine to flush its output immediately -- temporary patch suggested
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   129
  by Kim Dam Petersen*)		(* FIXME !? *)
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   130
val output = fn (s, t) => (output (s, t); flush_out s);
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   131
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   132
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   133
(* getenv *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   134
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   135
local
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   136
  fun drop_last [] = []
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   137
    | drop_last [x] = []
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   138
    | drop_last (x :: xs) = x :: drop_last xs;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   139
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   140
  val drop_last_char = implode o drop_last o explode;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   141
in
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   142
  fun getenv var = drop_last_char
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   143
    (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   144
end;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   145
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   146
4428
5c26253b8a2e tuned comment;
wenzelm
parents: 4340
diff changeset
   147
(* non-ASCII input (see also Thy/use.ML) *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   148
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   149
val needs_filtered_use = false;