src/Pure/NJ.ML
author lcp
Tue Jul 25 17:03:16 1995 +0200 (1995-07-25 ago)
changeset 1194 563ecd14c1d8
parent 907 61fcac0e50fc
child 1289 2edd7a39d92a
permissions -rw-r--r--
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
clasohm@0
     1
(*  Title:      Pure/NJ
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Compatibility file for Standard ML of New Jersey.
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
(*** Poly/ML emulation ***)
clasohm@0
    10
lcp@907
    11
(*To exit the system with an exit code -- an alternative to ^D *)
lcp@907
    12
val exit = System.Unsafe.CInterface.exit;
lcp@907
    13
fun quit () = exit 0;
clasohm@0
    14
clasohm@0
    15
(*To change the current directory*)
clasohm@0
    16
val cd = System.Directory.cd;
clasohm@0
    17
clasohm@0
    18
(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
clasohm@0
    19
fun print_depth n = (System.Control.Print.printDepth := n div 2;
clasohm@0
    20
                     System.Control.Print.printLength := n);
clasohm@0
    21
clasohm@0
    22
clasohm@0
    23
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
clasohm@0
    24
clasohm@0
    25
fun make_pp path pprint =
clasohm@0
    26
  let
clasohm@0
    27
    open System.PrettyPrint;
clasohm@0
    28
clasohm@0
    29
    fun pp pps obj =
clasohm@0
    30
      pprint obj
clasohm@0
    31
        (add_string pps, begin_block pps INCONSISTENT,
wenzelm@19
    32
          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
wenzelm@19
    33
          fn () => end_block pps);
clasohm@0
    34
  in
clasohm@0
    35
    (path, pp)
clasohm@0
    36
  end;
clasohm@0
    37
clasohm@0
    38
fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
clasohm@0
    39
clasohm@0
    40
clasohm@0
    41
(*** New Jersey ML parameters ***)
clasohm@0
    42
clasohm@0
    43
(* Suppresses Garbage Collection messages;  default was 2 *)
clasohm@0
    44
System.Control.Runtime.gcmessages := 0;
clasohm@0
    45
clasohm@0
    46
(*redefine to flush its output immediately -- temporary patch suggested
clasohm@0
    47
  by Kim Dam Petersen*)
clasohm@0
    48
val output = fn(s, t) => (output(s, t); flush_out s);
clasohm@0
    49
clasohm@0
    50
(*Dummy version of the Poly/ML function*)
clasohm@0
    51
fun commit() = ();
clasohm@0
    52
clasohm@0
    53
(*For use in Makefiles -- saves space*)
clasohm@0
    54
fun xML filename banner = (exportML filename;  print(banner^"\n"));
clasohm@0
    55
clasohm@0
    56
(*** Timing functions ***)
clasohm@0
    57
clasohm@0
    58
(*Print microseconds, suppressing trailing zeroes*)
clasohm@0
    59
fun umakestring 0 = ""
clasohm@0
    60
  | umakestring n = chr(ord"0" + n div 100000) ^
clasohm@0
    61
                    umakestring(10 * (n mod 100000));
clasohm@0
    62
clasohm@0
    63
(*A conditional timing function: applies f to () and, if the flag is true,
clasohm@0
    64
  prints its runtime. *)
clasohm@0
    65
fun cond_timeit flag f =
clasohm@0
    66
  if flag then
clasohm@0
    67
    let fun string_of_time (System.Timer.TIME {sec, usec}) =
clasohm@0
    68
            makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
clasohm@0
    69
        open System.Timer;
clasohm@0
    70
        val start = start_timer()
clasohm@0
    71
        val result = f();
clasohm@0
    72
        val nongc = check_timer(start)
clasohm@0
    73
        and gc = check_timer_gc(start);
clasohm@0
    74
        val both = add_time(nongc, gc)
clasohm@0
    75
    in  print("Non GC " ^ string_of_time nongc ^
clasohm@0
    76
               "   GC " ^ string_of_time gc ^
clasohm@0
    77
               "  both "^ string_of_time both ^ " secs\n");
clasohm@0
    78
        result
clasohm@0
    79
    end
clasohm@0
    80
  else f();
clasohm@0
    81
clasohm@0
    82
lcp@66
    83
(*** File handling ***)
clasohm@0
    84
clasohm@0
    85
(*Get time of last modification.*)
clasohm@0
    86
local
clasohm@0
    87
    open System.Timer;
clasohm@0
    88
    open System.Unsafe.SysIO;
clasohm@0
    89
in
clasohm@0
    90
  fun file_info "" = ""
clasohm@0
    91
    | file_info name = makestring (mtime (PATH name));
clasohm@220
    92
clasohm@220
    93
  val delete_file = unlink;
clasohm@0
    94
end;
clasohm@0
    95
clasohm@100
    96
(*Get pathname of current working directory *)
clasohm@100
    97
fun pwd () = System.Directory.getWD ();
clasohm@378
    98
clasohm@378
    99
clasohm@378
   100
(*** ML command execution ***)
clasohm@378
   101
clasohm@396
   102
fun use_string commands = 
clasohm@396
   103
  System.Compile.use_stream (open_string (implode commands));
clasohm@378
   104