src/Pure/NJ1xx.ML
author paulson
Fri May 30 15:14:59 1997 +0200 (1997-05-30)
changeset 3365 86c0d1988622
parent 3084 9844abe1de72
permissions -rw-r--r--
flushOut ensures that no recent error message are lost (not certain this is
necessary)
clasohm@1480
     1
(*  Title:      Pure/NJ1xx.ML
clasohm@1480
     2
    ID:         $Id$
clasohm@1480
     3
    Author:     Carsten Clasohm, TU Muenchen
clasohm@1480
     4
    Copyright   1996  TU Muenchen
clasohm@1480
     5
clasohm@1480
     6
Compatibility file for Standard ML of New Jersey version 1.xx.
clasohm@1480
     7
*)
clasohm@1480
     8
clasohm@1480
     9
(*** Poly/ML emulation ***)
clasohm@1480
    10
clasohm@1480
    11
clasohm@1480
    12
(*To exit the system with an exit code -- an alternative to ^D *)
clasohm@1480
    13
fun exit 0 = OS.Process.exit OS.Process.success
clasohm@1480
    14
  | exit _ = OS.Process.exit OS.Process.failure;
clasohm@1480
    15
fun quit () = exit 0;
clasohm@1480
    16
clasohm@1480
    17
(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
clasohm@1480
    18
fun print_depth n = (Compiler.Control.Print.printDepth := n div 2;
clasohm@1480
    19
                     Compiler.Control.Print.printLength := n);
clasohm@1480
    20
clasohm@1480
    21
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
clasohm@1480
    22
clasohm@1480
    23
fun make_pp path pprint =
clasohm@1480
    24
  let
clasohm@1480
    25
    open Compiler.PrettyPrint;
clasohm@1480
    26
clasohm@1480
    27
    fun pp pps obj =
clasohm@1480
    28
      pprint obj
clasohm@1480
    29
        (add_string pps, begin_block pps INCONSISTENT,
clasohm@1480
    30
          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
clasohm@1480
    31
          fn () => end_block pps);
clasohm@1480
    32
  in
clasohm@1480
    33
    (path, pp)
clasohm@1480
    34
  end;
clasohm@1480
    35
clasohm@1480
    36
fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;
clasohm@1480
    37
clasohm@1480
    38
clasohm@1480
    39
(*** New Jersey ML parameters ***)
clasohm@1480
    40
clasohm@1480
    41
(* Suppresses Garbage Collection messages; doesn't work yet *)
clasohm@1480
    42
(*System.Runtime.gc 0;*)
clasohm@1480
    43
clasohm@1480
    44
val _ = (Compiler.Control.Print.printLength := 1000;
clasohm@1480
    45
         Compiler.Control.Print.printDepth := 350;
clasohm@1480
    46
         Compiler.Control.Print.stringDepth := 250;
clasohm@1480
    47
         Compiler.Control.Print.signatures := 2);
clasohm@1480
    48
paulson@2246
    49
(*** Character/string functions which are compatible with 0.93 and Poly/ML ***)
clasohm@1480
    50
paulson@2246
    51
fun ord s = Char.ord (String.sub(s,0));
clasohm@1480
    52
val chr = str o Char.chr;
clasohm@1480
    53
val explode = (map str) o String.explode;
clasohm@1480
    54
val implode = String.concat;
clasohm@1480
    55
clasohm@1480
    56
clasohm@1480
    57
(*** Timing functions ***)
clasohm@1480
    58
clasohm@1480
    59
(*A conditional timing function: applies f to () and, if the flag is true,
clasohm@1480
    60
  prints its runtime. *)
clasohm@1480
    61
fun cond_timeit flag f =
clasohm@1480
    62
  if flag then
paulson@2076
    63
    let open Time  (*...for Time.toString, Time.+ and Time.- *)
paulson@2101
    64
	val CPUtimer = Timer.startCPUTimer();
paulson@2101
    65
        val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer);
clasohm@1480
    66
        val result = f();
paulson@2076
    67
        val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer)
paulson@2076
    68
    in  print("User " ^ toString (usrt2-usrt1) ^
paulson@2076
    69
              "  GC " ^ toString (gct2-gct1) ^
paulson@2076
    70
              "  All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^
paulson@2076
    71
              " secs\n")
paulson@2076
    72
	  handle Time => ();
clasohm@1480
    73
        result
clasohm@1480
    74
    end
clasohm@1480
    75
  else f();
clasohm@1480
    76
clasohm@1480
    77
clasohm@1480
    78
(*** File handling ***)
clasohm@1480
    79
clasohm@1480
    80
(*Get time of last modification; if file doesn't exist return an empty string*)
paulson@2246
    81
fun file_info "" = ""
paulson@2304
    82
  | file_info name = Time.toString (OS.FileSys.modTime name) handle _ =>"";
clasohm@1480
    83
clasohm@1480
    84
clasohm@1480
    85
clasohm@1480
    86
(*** ML command execution ***)
clasohm@1480
    87
paulson@2288
    88
paulson@3084
    89
(*For version 109.21 and later:*)
paulson@2288
    90
val use_string = Compiler.Interact.useStream o TextIO.openString o implode;
paulson@2288
    91
paulson@3084
    92
(*For versions prior to 109.21:*****
clasohm@1480
    93
fun use_string commands = 
clasohm@1480
    94
   Compiler.Interact.use_stream (open_string (implode commands));
paulson@3084
    95
*)
clasohm@1480
    96
clasohm@1480
    97
(*** System command execution ***)
clasohm@1480
    98
clasohm@1480
    99
(*Execute an Unix command which doesn't take any input from stdin and
clasohm@1480
   100
  sends its output to stdout.
clasohm@1480
   101
  This could be done more easily by Unix.execute, but that function
clasohm@1480
   102
  doesn't use the PATH.*)
clasohm@1480
   103
fun execute command =
clasohm@1480
   104
  let val tmp_name = "isa_converted.tmp"
clasohm@1480
   105
      val is = (OS.Process.system (command ^ " > " ^ tmp_name);
paulson@2246
   106
                TextIO.openIn tmp_name);
paulson@2246
   107
      val result = TextIO.inputAll is;
paulson@2246
   108
  in TextIO.closeIn is;
paulson@2246
   109
     OS.FileSys.remove tmp_name;
clasohm@1480
   110
     result
clasohm@1480
   111
  end;
clasohm@1480
   112
paulson@2246
   113
(*For exporting images.  The short name saves space in Makefiles*)
clasohm@1480
   114
fun xML filename banner =
paulson@2246
   115
  let open SMLofNJ
paulson@2246
   116
      val runtime = hd (SMLofNJ.getAllArgs())
paulson@2246
   117
      and exec_file = TextIO.openOut filename
paulson@2246
   118
  in 
paulson@2246
   119
     TextIO.output  (*Write a shell script to invoke the actual image*)
paulson@2246
   120
       (exec_file,
paulson@2246
   121
	String.concat
paulson@2246
   122
	["#!/bin/sh\n", runtime, 
paulson@2246
   123
	 " @SMLdebug=/dev/null",  (*suppresses GC messages*)
paulson@2246
   124
	 " @SMLload=", filename, ".heap\n"]);
paulson@2246
   125
     TextIO.closeOut exec_file;
paulson@2246
   126
     OS.Process.system ("chmod a+x " ^ filename);
paulson@2246
   127
     exportML (filename^".heap");
paulson@2246
   128
     print(banner^"\n")
paulson@2246
   129
  end;
wenzelm@2408
   130
wenzelm@2408
   131
wenzelm@2408
   132
val needs_filtered_use = false;