clasohm@1480: (*  Title:      Pure/NJ093.ML
clasohm@1480:     ID:         $Id$
clasohm@1480:     Author:     Carsten Clasohm, TU Muenchen
clasohm@1480:     Copyright   1996  TU Muenchen
clasohm@1480: 
clasohm@1480: Compatibility file for Standard ML of New Jersey version 0.93.
clasohm@1480: *)
clasohm@1480: 
paulson@2190: 
paulson@2242: use"basis.ML";
paulson@2190: 
clasohm@1480: (*** Poly/ML emulation ***)
clasohm@1480: 
clasohm@1480: (*To exit the system with an exit code -- an alternative to ^D *)
clasohm@1480: val exit = System.Unsafe.CInterface.exit;
clasohm@1480: fun quit () = exit 0;
clasohm@1480: 
clasohm@1480: (*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
clasohm@1480: fun print_depth n = (System.Control.Print.printDepth := n div 2;
clasohm@1480:                      System.Control.Print.printLength := n);
clasohm@1480: 
clasohm@1480: (*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
clasohm@1480: 
clasohm@1480: fun make_pp path pprint =
clasohm@1480:   let
clasohm@1480:     open System.PrettyPrint;
clasohm@1480: 
clasohm@1480:     fun pp pps obj =
clasohm@1480:       pprint obj
clasohm@1480:         (add_string pps, begin_block pps INCONSISTENT,
clasohm@1480:           fn wd => add_break pps (wd, 0), fn () => add_newline pps,
clasohm@1480:           fn () => end_block pps);
clasohm@1480:   in
clasohm@1480:     (path, pp)
clasohm@1480:   end;
clasohm@1480: 
clasohm@1480: fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
clasohm@1480: 
clasohm@1480: 
clasohm@1480: (*** New Jersey ML parameters ***)
clasohm@1480: 
clasohm@1480: (* Suppresses Garbage Collection messages;  default was 2 *)
clasohm@1480: System.Control.Runtime.gcmessages := 0;
clasohm@1480: 
clasohm@1480: 
clasohm@1480: (*** Timing functions ***)
clasohm@1480: 
clasohm@1480: (*Print microseconds, suppressing trailing zeroes*)
clasohm@1480: fun umakestring 0 = ""
clasohm@1480:   | umakestring n = chr(ord "0" + n div 100000) ^
clasohm@1480:                     umakestring(10 * (n mod 100000));
clasohm@1480: 
clasohm@1480: (*A conditional timing function: applies f to () and, if the flag is true,
clasohm@1480:   prints its runtime. *)
clasohm@1480: fun cond_timeit flag f =
clasohm@1480:   if flag then
clasohm@1480:     let fun string_of_time (System.Timer.TIME {sec, usec}) =
clasohm@1480:             makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
clasohm@1480:         open System.Timer;
clasohm@1480:         val start = start_timer()
clasohm@1480:         val result = f();
clasohm@1480:         val nongc = check_timer(start)
clasohm@1480:         and gc = check_timer_gc(start);
clasohm@1480:         val both = add_time(nongc, gc)
clasohm@1480:     in  print("Non GC " ^ string_of_time nongc ^
clasohm@1480:                "   GC " ^ string_of_time gc ^
clasohm@1480:                "  both "^ string_of_time both ^ " secs\n");
clasohm@1480:         result
clasohm@1480:     end
clasohm@1480:   else f();
clasohm@1480: 
clasohm@1480: 
clasohm@1480: (*** File handling ***)
clasohm@1480: 
clasohm@1480: (*Get time of last modification; if file doesn't exist return an empty string*)
clasohm@1480: local
clasohm@1480:     open System.Timer;
clasohm@1480:     open System.Unsafe.SysIO;
clasohm@1480: in
clasohm@1480:   fun file_info "" = ""
clasohm@1480:     | file_info name = makestring (mtime (PATH name))  handle _ => "";
clasohm@1480: end;
clasohm@1480: 
paulson@2242: structure OS =
paulson@2242:   struct
paulson@2242:   structure FileSys =
paulson@2242:     struct
wenzelm@3319:     val chDir = System.Directory.cd
paulson@2242:     val remove = System.Unsafe.SysIO.unlink       (*Delete a file *)
paulson@2242:     val getDir = System.Directory.getWD           (*path of working directory*)
paulson@2242:     end
paulson@2242:   end;
clasohm@1480: 
clasohm@1480: 
clasohm@1480: (*** ML command execution ***)
clasohm@1480: 
clasohm@1480: fun use_string commands = 
clasohm@1480:   System.Compile.use_stream (open_string (implode commands));
clasohm@1480: 
clasohm@1480: 
clasohm@1480: (*** System command execution ***)
clasohm@1480: 
clasohm@1480: (*Execute an Unix command which doesn't take any input from stdin and
clasohm@1480:   sends its output to stdout.
clasohm@1480:   This could be done more easily by IO.execute, but that function
clasohm@1480:   seems to be buggy in SML/NJ 0.93.*)
clasohm@1480: fun execute command =
clasohm@1480:   let val tmp_name = "isa_converted.tmp"
clasohm@1480:       val is = (System.system (command ^ " > " ^ tmp_name);
clasohm@1480:                 open_in tmp_name);
clasohm@1480:       val result = input (is, 999999);
clasohm@1480:   in close_in is;
wenzelm@3319:      OS.FileSys.remove tmp_name;
clasohm@1480:      result
clasohm@1480:   end;
clasohm@1480: 
paulson@2242: (*redefine to flush its output immediately -- temporary patch suggested
paulson@2242:   by Kim Dam Petersen*)
paulson@2242: val output = fn(s, t) => (output(s, t); flush_out s);
clasohm@1480: 
clasohm@1480: (*For use in Makefiles -- saves space*)
clasohm@1480: fun xML filename banner = (exportML filename;  print(banner^"\n"));
wenzelm@2408: 
wenzelm@2408: 
wenzelm@2408: val needs_filtered_use = false;