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