src/Pure/ML-Systems/smlnj-0.93.ML
author paulson
Fri, 02 Jan 1998 11:17:06 +0100
changeset 4506 f21ec26b2265
parent 4494 7e5611945959
child 4977 6cec2c0ffdbf
permissions -rw-r--r--
Declared startTiming and endTiming
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
4506
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    59
f21ec26b2265 Declared startTiming and endTiming
paulson
parents: 4494
diff changeset
    60
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    61
(* toplevel pretty printing (see also Pure/install_pp.ML) *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    62
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    63
fun make_pp path pprint =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    64
  let
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    65
    open System.PrettyPrint;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    66
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    67
    fun pp pps obj =
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    68
      pprint obj
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    69
        (add_string pps, begin_block pps INCONSISTENT,
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    70
          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    71
          fn () => end_block pps);
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    72
  in
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    73
    (path, pp)
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    74
  end;
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
fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    77
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    78
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    79
(* ML command execution *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    80
3631
88a279998f90 renamed use_string to use_strings;
wenzelm
parents: 3595
diff changeset
    81
fun use_strings commands =
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    82
  System.Compile.use_stream (open_string (implode commands));
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    83
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    84
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    85
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    86
(** OS related **)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    87
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    88
(* system command execution *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    89
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    90
(*execute Unix command which doesn't take any input from stdin and
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    91
  sends its output to stdout; could be done more easily by IO.execute,
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    92
  but that function seems to be buggy in SML/NJ 0.93*)
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    93
fun execute command =
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    94
  let
4494
7e5611945959 fixed execute;
wenzelm
parents: 4428
diff changeset
    95
    val tmp_name = "/tmp/isabelle-execute";
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    96
    val is = (System.system (command ^ " > " ^ tmp_name); open_in tmp_name);
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    97
    val result = input (is, 999999);
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    98
  in
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
    99
    close_in is;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   100
    System.Unsafe.SysIO.unlink tmp_name;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   101
    result
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   102
  end;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   103
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   104
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   105
(* file handling *)
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
(*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
   108
local
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   109
  open System.Timer System.Unsafe.SysIO;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   110
in
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   111
  fun file_info "" = ""
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   112
    | file_info name = makestring (mtime (PATH name)) handle _ => "";
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   113
end;
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   114
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   115
structure OS =
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   116
struct
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   117
  structure FileSys =
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   118
  struct
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   119
    val chDir = System.Directory.cd;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   120
    val remove = System.Unsafe.SysIO.unlink;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   121
    val getDir = System.Directory.getWD;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   122
  end;
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   123
end;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   124
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   125
(*redefine to flush its output immediately -- temporary patch suggested
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   126
  by Kim Dam Petersen*)		(* FIXME !? *)
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   127
val output = fn (s, t) => (output (s, t); flush_out s);
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   128
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   129
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   130
(* getenv *)
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   131
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   132
local
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   133
  fun drop_last [] = []
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   134
    | drop_last [x] = []
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   135
    | drop_last (x :: xs) = x :: drop_last xs;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   136
3594
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   137
  val drop_last_char = implode o drop_last o explode;
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   138
in
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   139
  fun getenv var = drop_last_char
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   140
    (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
193cc37e6f60 tuned comments;
wenzelm
parents: 2413
diff changeset
   141
end;
2413
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   142
a00f0476e189 SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
   143
4428
5c26253b8a2e tuned comment;
wenzelm
parents: 4340
diff changeset
   144
(* non-ASCII input (see also Thy/use.ML) *)
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
val needs_filtered_use = false;