src/Pure/ML-Systems/smlnj-1.09.ML
author wenzelm
Thu, 24 Apr 1997 19:46:24 +0200
changeset 3048 a4b609108712
parent 2425 4db9e4a150d6
child 3591 412c62dd43de
permissions -rw-r--r--
adapted for 1.09.27 (and later);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/smlnj-1.09.ML
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
     3
    Author:     Carsten Clasohm, TU Muenchen
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
     4
    Copyright   1996  TU Muenchen
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
     5
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
     6
Compatibility file for Standard ML of New Jersey, version 1.09.27 or later.
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
     7
*)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
     8
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
     9
(** Poly/ML emulation **)
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    10
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    11
fun quit () = exit 0;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    12
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    13
(*to limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    14
fun print_depth n =
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    15
 (Compiler.Control.Print.printDepth := n div 2;
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    16
  Compiler.Control.Print.printLength := n);
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    17
2425
4db9e4a150d6 Poly/ML style prompts;
wenzelm
parents: 2408
diff changeset
    18
Compiler.Control.primaryPrompt := "> ";
4db9e4a150d6 Poly/ML style prompts;
wenzelm
parents: 2408
diff changeset
    19
Compiler.Control.secondaryPrompt := "# ";
4db9e4a150d6 Poly/ML style prompts;
wenzelm
parents: 2408
diff changeset
    20
4db9e4a150d6 Poly/ML style prompts;
wenzelm
parents: 2408
diff changeset
    21
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    22
(* interface for toplevel pretty printers, see also Pure/install_pp.ML *)
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    23
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    24
fun make_pp path pprint =
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    25
  let
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    26
    open Compiler.PrettyPrint;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    27
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    28
    fun pp pps obj =
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    29
      pprint obj
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    30
        (add_string pps, begin_block pps INCONSISTENT,
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    31
          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    32
          fn () => end_block pps);
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    33
  in
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    34
    (path, pp)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    35
  end;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    36
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    37
fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    38
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    39
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    40
(** New Jersey ML parameters **)
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    41
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    42
val _ =
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    43
 (Compiler.Control.Print.printLength := 1000;
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    44
  Compiler.Control.Print.printDepth := 350;
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    45
  Compiler.Control.Print.stringDepth := 250;
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    46
  Compiler.Control.Print.signatures := 2);
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    47
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    48
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    49
(** Character / string functions which are compatible with 0.93 and Poly/ML **)
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    50
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    51
fun ord s = Char.ord (String.sub (s, 0));
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    52
val chr = str o Char.chr;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    53
val explode = (map str) o String.explode;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    54
val implode = String.concat;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    55
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    56
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    57
(** Timing functions **)
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    58
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    59
(*A conditional timing function: applies f to () and, if the flag is true,
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    60
  prints its runtime. *)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    61
fun cond_timeit flag f =
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    62
  if flag then
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    63
    let open Time  (*...for Time.toString, Time.+ and Time.- *)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    64
	val CPUtimer = Timer.startCPUTimer();
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    65
        val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer);
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    66
        val result = f();
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    67
        val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    68
    in  print("User " ^ toString (usrt2-usrt1) ^
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    69
              "  GC " ^ toString (gct2-gct1) ^
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    70
              "  All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    71
              " secs\n")
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    72
	  handle Time => ();
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    73
        result
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    74
    end
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    75
  else f ();
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    76
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    77
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    78
(** File handling **)
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    79
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    80
(*get time of last modification; if file doesn't exist return an empty string*)
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    81
fun file_info "" = ""
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    82
  | file_info name = Time.toString (OS.FileSys.modTime name) handle _ =>"";
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    83
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    84
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    85
(** ML command execution **)
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    86
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    87
val use_string = Compiler.Interact.useStream o TextIO.openString o implode;
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    88
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    89
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
    90
(** System command execution **)
2342
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    91
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    92
(*Execute an Unix command which doesn't take any input from stdin and
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    93
  sends its output to stdout.
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    94
  This could be done more easily by Unix.execute, but that function
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    95
  doesn't use the PATH.*)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    96
fun execute command =
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    97
  let val tmp_name = "isa_converted.tmp"
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    98
      val is = (OS.Process.system (command ^ " > " ^ tmp_name);
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    99
                TextIO.openIn tmp_name);
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   100
      val result = TextIO.inputAll is;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   101
  in TextIO.closeIn is;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   102
     OS.FileSys.remove tmp_name;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   103
     result
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   104
  end;
2408
acddf41dbbf7 added needs_filtered_use;
wenzelm
parents: 2342
diff changeset
   105
acddf41dbbf7 added needs_filtered_use;
wenzelm
parents: 2342
diff changeset
   106
3048
a4b609108712 adapted for 1.09.27 (and later);
wenzelm
parents: 2425
diff changeset
   107
(** non-ASCII input **)
2408
acddf41dbbf7 added needs_filtered_use;
wenzelm
parents: 2342
diff changeset
   108
acddf41dbbf7 added needs_filtered_use;
wenzelm
parents: 2342
diff changeset
   109
val needs_filtered_use = false;