src/Pure/ML-Systems/MLWorks.ML
author paulson
Tue Aug 05 10:50:24 1997 +0200 (1997-08-05)
changeset 3587 00ea30ea0734
parent 3539 d4443afc8d28
child 3597 3ac6d6bcae42
permissions -rw-r--r--
Corrected a comment
     1 (*  Title:      Pure/MLWorks.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Compatibility file for MLWorks (??)
     7 
     8 NB: There is still no easy way of building Isabelle under MLWorks.  This file
     9     is just a start towards compatibility.  One problem is the peculiar
    10     behaviour of "use" in MLWorks.  Strange errors occur when loading theories,
    11     and ROOT.ML files on subdirectories are loaded incorrectly.
    12 *)
    13 
    14 (*** Poly/ML emulation ***)
    15 
    16 (**
    17 Shell.File.loadSource "system.__os";
    18 Shell.File.loadSource "basis.__timer";
    19 Shell.File.loadSource "system.__time";
    20 Shell.File.loadSource "unix.__os_file_sys";
    21 Shell.File.loadSource "basis.__list";
    22 Shell.File.loadSource "basis.__char";
    23 Shell.File.loadSource "basis.__string";
    24 Shell.File.loadSource "basis.__text_io";
    25 **)
    26 
    27 
    28 structure Option = General;
    29 
    30 (*To exit the system with an exit code -- an alternative to ^D *)
    31 fun exit 0 = OS.Process.exit OS.Process.success
    32   | exit _ = OS.Process.exit OS.Process.failure;
    33 fun quit () = exit 0;
    34 
    35 (*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
    36 fun print_depth n = ();
    37 
    38 (*Interface for toplevel pretty printers, see also Pure/install_pp.ML
    39   CURRENTLY UNAVAILABLE*)
    40 fun make_pp path pprint = ();
    41 fun install_pp _ = ();
    42 
    43 
    44 (*** New Jersey ML parameters ***)
    45 
    46 (*** Character/string functions which are compatible with 0.93 and Poly/ML ***)
    47 
    48 fun ord s = Char.ord (String.sub(s,0));
    49 val chr = str o Char.chr;
    50 val explode = (map str) o String.explode;
    51 val implode = String.concat;
    52 
    53 
    54 (*** Timing functions ***)
    55 
    56 (*A conditional timing function: applies f to () and, if the flag is true,
    57   prints its runtime. *)
    58 fun cond_timeit flag f =
    59   if flag then
    60     let open Time  (*...for Time.toString, Time.+ and Time.- *)
    61 	val CPUtimer = Timer.startCPUTimer();
    62         val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer);
    63         val result = f();
    64         val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer)
    65     in  print("User " ^ toString (usrt2-usrt1) ^
    66               "  GC " ^ toString (gct2-gct1) ^
    67               "  All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^
    68               " secs\n")
    69 	  handle Time => ();
    70         result
    71     end
    72   else f();
    73 
    74 
    75 (*** File handling ***)
    76 
    77 (*Get time of last modification; if file doesn't exist return an empty string*)
    78 fun file_info "" = ""
    79   | file_info name = Time.toString (OS.FileSys.modTime name) handle _ =>"";
    80 
    81 
    82 (*** ML command execution ***)
    83 
    84 val tmpName = OS.FileSys.tmpName();
    85 
    86 (*Can one redirect 'use' directly to an instream?*)
    87 fun use_string slist =
    88   let val tmpFile = TextIO.openOut tmpName
    89   in app (fn s => TextIO.output (tmpFile, s)) slist;
    90      TextIO.closeOut tmpFile;
    91      use tmpName
    92   end;
    93 
    94 
    95 (*** System command execution ***)
    96 
    97 (*Execute an Unix command which doesn't take any input from stdin and
    98   sends its output to stdout.
    99   This could be done more easily by Unix.execute, but that function
   100   doesn't use the PATH.*)
   101 fun execute command =
   102   let val is = (OS.Process.system (command ^ " > " ^ tmpName);
   103                 TextIO.openIn tmpName);
   104       val result = TextIO.inputAll is;
   105   in TextIO.closeIn is;
   106      OS.FileSys.remove tmpName;
   107      result
   108   end;
   109 
   110 
   111 (*"false" writes an image file that is executed via the MLWorks "mlimage" 
   112   script, while "true" would yield a larger, self-contained executable.*)
   113 fun xML filename = Shell.saveImage (filename, false);
   114 
   115 
   116 (*Non-printing and 8-bit chars are forbidden in string constants*)
   117 val needs_filtered_use = true;
   118