src/Pure/ML-Systems/smlnj-1.09.ML
author wenzelm
Mon, 09 Dec 1996 16:33:57 +0100
changeset 2342 859d72636ce7
child 2408 acddf41dbbf7
permissions -rw-r--r--
Compatibility file for Standard ML of New Jersey, version 1.09.
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
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
     6
Compatibility file for Standard ML of New Jersey, version 1.09.
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
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
     9
(*** Poly/ML emulation ***)
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
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    13
(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    14
fun print_depth n = (Compiler.Control.Print.printDepth := n div 2;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    15
                     Compiler.Control.Print.printLength := n);
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    16
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    17
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    18
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    19
fun make_pp path pprint =
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    20
  let
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    21
    open Compiler.PrettyPrint;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    22
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    23
    fun pp pps obj =
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    24
      pprint obj
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    25
        (add_string pps, begin_block pps INCONSISTENT,
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    26
          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
    27
          fn () => end_block pps);
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    28
  in
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    29
    (path, pp)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    30
  end;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    31
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    32
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
    33
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    34
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    35
(*** New Jersey ML parameters ***)
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
(* Suppresses Garbage Collection messages; doesn't work yet *)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    38
(*System.Runtime.gc 0;*)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    39
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    40
val _ = (Compiler.Control.Print.printLength := 1000;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    41
         Compiler.Control.Print.printDepth := 350;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    42
         Compiler.Control.Print.stringDepth := 250;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    43
         Compiler.Control.Print.signatures := 2);
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    44
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    45
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    46
(*** Character/string functions which are compatible with 0.93 and Poly/ML ***)
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
fun ord s = Char.ord (String.sub(s,0));
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    49
val chr = str o Char.chr;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    50
val explode = (map str) o String.explode;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    51
val implode = String.concat;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    52
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    53
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    54
(*** Timing functions ***)
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
(*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
    57
  prints its runtime. *)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    58
fun cond_timeit flag f =
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    59
  if flag then
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    60
    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
    61
	val CPUtimer = Timer.startCPUTimer();
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    62
        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
    63
        val result = f();
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    64
        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
    65
    in  print("User " ^ toString (usrt2-usrt1) ^
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    66
              "  GC " ^ toString (gct2-gct1) ^
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    67
              "  All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    68
              " secs\n")
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    69
	  handle Time => ();
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    70
        result
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    71
    end
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    72
  else f();
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    73
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    74
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    75
(*** File handling ***)
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
(*Get time of last modification; if file doesn't exist return an empty string*)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    78
fun file_info "" = ""
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    79
  | 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
    80
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    81
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    82
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    83
(*** ML command execution ***)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    84
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    85
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    86
(*For version 109.21 and later:
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    87
val use_string = Compiler.Interact.useStream o TextIO.openString o implode;
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
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    90
(*For versions prior to 109.21:*)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    91
fun use_string commands = 
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    92
   Compiler.Interact.use_stream (open_string (implode commands));
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    93
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    94
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    95
(*** System command execution ***)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    96
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    97
(*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
    98
  sends its output to stdout.
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
    99
  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
   100
  doesn't use the PATH.*)
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   101
fun execute command =
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   102
  let val tmp_name = "isa_converted.tmp"
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   103
      val is = (OS.Process.system (command ^ " > " ^ tmp_name);
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   104
                TextIO.openIn tmp_name);
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   105
      val result = TextIO.inputAll is;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   106
  in TextIO.closeIn is;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   107
     OS.FileSys.remove tmp_name;
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   108
     result
859d72636ce7 Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff changeset
   109
  end;