src/Pure/NJ.ML
author lcp
Tue, 18 Jan 1994 15:57:40 +0100
changeset 230 ec8a2b6aa8a7
parent 220 e50ea2471e06
child 378 85ff48546a05
permissions -rw-r--r--
Many other files modified as follows: s|Sign.cterm|cterm|g s|Sign.ctyp|ctyp|g s|Sign.rep_cterm|rep_cterm|g s|Sign.rep_ctyp|rep_ctyp|g s|Sign.pprint_cterm|pprint_cterm|g s|Sign.pprint_ctyp|pprint_ctyp|g s|Sign.string_of_cterm|string_of_cterm|g s|Sign.string_of_ctyp|string_of_ctyp|g s|Sign.term_of|term_of|g s|Sign.typ_of|typ_of|g s|Sign.read_cterm|read_cterm|g s|Sign.read_insts|read_insts|g s|Sign.cfun|cterm_fun|g
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title:      Pure/NJ
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Compatibility file for Standard ML of New Jersey.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
(*** Poly/ML emulation ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
(*To exit the system -- an alternative to ^D *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
fun quit () = System.Unsafe.CInterface.exit 0;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
(*To change the current directory*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
val cd = System.Directory.cd;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
fun print_depth n = (System.Control.Print.printDepth := n div 2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
                     System.Control.Print.printLength := n);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
fun make_pp path pprint =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
    open System.PrettyPrint;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
    fun pp pps obj =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
      pprint obj
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
        (add_string pps, begin_block pps INCONSISTENT,
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    31
          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    32
          fn () => end_block pps);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
    (path, pp)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
(*** New Jersey ML parameters ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
(* Suppresses Garbage Collection messages;  default was 2 *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
System.Control.Runtime.gcmessages := 0;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
(*redefine to flush its output immediately -- temporary patch suggested
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  by Kim Dam Petersen*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val output = fn(s, t) => (output(s, t); flush_out s);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
(*Dummy version of the Poly/ML function*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
fun commit() = ();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
(*For use in Makefiles -- saves space*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
fun xML filename banner = (exportML filename;  print(banner^"\n"));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
(*** Timing functions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
(*Print microseconds, suppressing trailing zeroes*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
fun umakestring 0 = ""
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  | umakestring n = chr(ord"0" + n div 100000) ^
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
                    umakestring(10 * (n mod 100000));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
(*A conditional timing function: applies f to () and, if the flag is true,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  prints its runtime. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
fun cond_timeit flag f =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
  if flag then
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
    let fun string_of_time (System.Timer.TIME {sec, usec}) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
            makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
        open System.Timer;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
        val start = start_timer()
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
        val result = f();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
        val nongc = check_timer(start)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
        and gc = check_timer_gc(start);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
        val both = add_time(nongc, gc)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
    in  print("Non GC " ^ string_of_time nongc ^
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
               "   GC " ^ string_of_time gc ^
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
               "  both "^ string_of_time both ^ " secs\n");
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
        result
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
    end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
  else f();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
66
1b14cd923772 /NJ,POLY/delete_file: new
lcp
parents: 19
diff changeset
    82
(*** File handling ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
(*Get time of last modification.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
local
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
    open System.Timer;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
    open System.Unsafe.SysIO;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
  fun file_info "" = ""
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
    | file_info name = makestring (mtime (PATH name));
220
e50ea2471e06 used unlink for delete_files instead of calling rm
clasohm
parents: 100
diff changeset
    91
e50ea2471e06 used unlink for delete_files instead of calling rm
clasohm
parents: 100
diff changeset
    92
  val delete_file = unlink;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
100
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    95
(*Get pathname of current working directory *)
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    96
fun pwd () = System.Directory.getWD ();