src/Pure/NJ093.ML
author paulson
Fri May 30 15:14:59 1997 +0200 (1997-05-30)
changeset 3365 86c0d1988622
parent 3319 0206e7507737
permissions -rw-r--r--
flushOut ensures that no recent error message are lost (not certain this is
necessary)
clasohm@1480
     1
(*  Title:      Pure/NJ093.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 0.93.
clasohm@1480
     7
*)
clasohm@1480
     8
paulson@2190
     9
paulson@2242
    10
use"basis.ML";
paulson@2190
    11
clasohm@1480
    12
(*** Poly/ML emulation ***)
clasohm@1480
    13
clasohm@1480
    14
(*To exit the system with an exit code -- an alternative to ^D *)
clasohm@1480
    15
val exit = System.Unsafe.CInterface.exit;
clasohm@1480
    16
fun quit () = exit 0;
clasohm@1480
    17
clasohm@1480
    18
(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
clasohm@1480
    19
fun print_depth n = (System.Control.Print.printDepth := n div 2;
clasohm@1480
    20
                     System.Control.Print.printLength := n);
clasohm@1480
    21
clasohm@1480
    22
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
clasohm@1480
    23
clasohm@1480
    24
fun make_pp path pprint =
clasohm@1480
    25
  let
clasohm@1480
    26
    open System.PrettyPrint;
clasohm@1480
    27
clasohm@1480
    28
    fun pp pps obj =
clasohm@1480
    29
      pprint obj
clasohm@1480
    30
        (add_string pps, begin_block pps INCONSISTENT,
clasohm@1480
    31
          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
clasohm@1480
    32
          fn () => end_block pps);
clasohm@1480
    33
  in
clasohm@1480
    34
    (path, pp)
clasohm@1480
    35
  end;
clasohm@1480
    36
clasohm@1480
    37
fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
clasohm@1480
    38
clasohm@1480
    39
clasohm@1480
    40
(*** New Jersey ML parameters ***)
clasohm@1480
    41
clasohm@1480
    42
(* Suppresses Garbage Collection messages;  default was 2 *)
clasohm@1480
    43
System.Control.Runtime.gcmessages := 0;
clasohm@1480
    44
clasohm@1480
    45
clasohm@1480
    46
(*** Timing functions ***)
clasohm@1480
    47
clasohm@1480
    48
(*Print microseconds, suppressing trailing zeroes*)
clasohm@1480
    49
fun umakestring 0 = ""
clasohm@1480
    50
  | umakestring n = chr(ord "0" + n div 100000) ^
clasohm@1480
    51
                    umakestring(10 * (n mod 100000));
clasohm@1480
    52
clasohm@1480
    53
(*A conditional timing function: applies f to () and, if the flag is true,
clasohm@1480
    54
  prints its runtime. *)
clasohm@1480
    55
fun cond_timeit flag f =
clasohm@1480
    56
  if flag then
clasohm@1480
    57
    let fun string_of_time (System.Timer.TIME {sec, usec}) =
clasohm@1480
    58
            makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
clasohm@1480
    59
        open System.Timer;
clasohm@1480
    60
        val start = start_timer()
clasohm@1480
    61
        val result = f();
clasohm@1480
    62
        val nongc = check_timer(start)
clasohm@1480
    63
        and gc = check_timer_gc(start);
clasohm@1480
    64
        val both = add_time(nongc, gc)
clasohm@1480
    65
    in  print("Non GC " ^ string_of_time nongc ^
clasohm@1480
    66
               "   GC " ^ string_of_time gc ^
clasohm@1480
    67
               "  both "^ string_of_time both ^ " secs\n");
clasohm@1480
    68
        result
clasohm@1480
    69
    end
clasohm@1480
    70
  else f();
clasohm@1480
    71
clasohm@1480
    72
clasohm@1480
    73
(*** File handling ***)
clasohm@1480
    74
clasohm@1480
    75
(*Get time of last modification; if file doesn't exist return an empty string*)
clasohm@1480
    76
local
clasohm@1480
    77
    open System.Timer;
clasohm@1480
    78
    open System.Unsafe.SysIO;
clasohm@1480
    79
in
clasohm@1480
    80
  fun file_info "" = ""
clasohm@1480
    81
    | file_info name = makestring (mtime (PATH name))  handle _ => "";
clasohm@1480
    82
end;
clasohm@1480
    83
paulson@2242
    84
structure OS =
paulson@2242
    85
  struct
paulson@2242
    86
  structure FileSys =
paulson@2242
    87
    struct
wenzelm@3319
    88
    val chDir = System.Directory.cd
paulson@2242
    89
    val remove = System.Unsafe.SysIO.unlink       (*Delete a file *)
paulson@2242
    90
    val getDir = System.Directory.getWD           (*path of working directory*)
paulson@2242
    91
    end
paulson@2242
    92
  end;
clasohm@1480
    93
clasohm@1480
    94
clasohm@1480
    95
(*** ML command execution ***)
clasohm@1480
    96
clasohm@1480
    97
fun use_string commands = 
clasohm@1480
    98
  System.Compile.use_stream (open_string (implode commands));
clasohm@1480
    99
clasohm@1480
   100
clasohm@1480
   101
(*** System command execution ***)
clasohm@1480
   102
clasohm@1480
   103
(*Execute an Unix command which doesn't take any input from stdin and
clasohm@1480
   104
  sends its output to stdout.
clasohm@1480
   105
  This could be done more easily by IO.execute, but that function
clasohm@1480
   106
  seems to be buggy in SML/NJ 0.93.*)
clasohm@1480
   107
fun execute command =
clasohm@1480
   108
  let val tmp_name = "isa_converted.tmp"
clasohm@1480
   109
      val is = (System.system (command ^ " > " ^ tmp_name);
clasohm@1480
   110
                open_in tmp_name);
clasohm@1480
   111
      val result = input (is, 999999);
clasohm@1480
   112
  in close_in is;
wenzelm@3319
   113
     OS.FileSys.remove tmp_name;
clasohm@1480
   114
     result
clasohm@1480
   115
  end;
clasohm@1480
   116
paulson@2242
   117
(*redefine to flush its output immediately -- temporary patch suggested
paulson@2242
   118
  by Kim Dam Petersen*)
paulson@2242
   119
val output = fn(s, t) => (output(s, t); flush_out s);
clasohm@1480
   120
clasohm@1480
   121
(*For use in Makefiles -- saves space*)
clasohm@1480
   122
fun xML filename banner = (exportML filename;  print(banner^"\n"));
wenzelm@2408
   123
wenzelm@2408
   124
wenzelm@2408
   125
val needs_filtered_use = false;