MLWorks compatibility: it sort of works
authorpaulson
Fri Dec 06 10:47:10 1996 +0100 (1996-12-06)
changeset 23303eea6b72bb4f
parent 2329 55060cfeda1b
child 2331 d6a56ff0d94e
MLWorks compatibility: it sort of works
src/Pure/MLWorks.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/MLWorks.ML	Fri Dec 06 10:47:10 1996 +0100
     1.3 @@ -0,0 +1,110 @@
     1.4 +(*  Title:      Pure/MLWorks.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Compatibility file for MLWorks (??)
    1.10 +
    1.11 +NB: There is still no easy way of building Isabelle under MLWorks.  This file
    1.12 +    is just a start towards compatibility.  One problem is the peculiar
    1.13 +    behaviour of "use" in MLWorks.  Strange errors occur when loading theories,
    1.14 +    and ROOT.ML files on subdirectories are loaded incorrectly.
    1.15 +*)
    1.16 +
    1.17 +(*** Poly/ML emulation ***)
    1.18 +
    1.19 +(**
    1.20 +require "system.__os";
    1.21 +require "basis.__timer";
    1.22 +require "system.__time";
    1.23 +require "unix.__os_file_sys";
    1.24 +require "basis.__list";
    1.25 +require "basis.__char";
    1.26 +require "basis.__string";
    1.27 +require "basis.__text_io";
    1.28 +**)
    1.29 +
    1.30 +
    1.31 +(*To exit the system with an exit code -- an alternative to ^D *)
    1.32 +fun exit 0 = OS.Process.exit OS.Process.success
    1.33 +  | exit _ = OS.Process.exit OS.Process.failure;
    1.34 +fun quit () = exit 0;
    1.35 +
    1.36 +(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
    1.37 +fun print_depth n = ();
    1.38 +
    1.39 +(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
    1.40 +
    1.41 +fun make_pp path pprint = ();
    1.42 +fun install_pp _ = ();
    1.43 +
    1.44 +
    1.45 +(*** New Jersey ML parameters ***)
    1.46 +
    1.47 +(*** Character/string functions which are compatible with 0.93 and Poly/ML ***)
    1.48 +
    1.49 +fun ord s = Char.ord (String.sub(s,0));
    1.50 +val chr = str o Char.chr;
    1.51 +val explode = (map str) o String.explode;
    1.52 +val implode = String.concat;
    1.53 +
    1.54 +
    1.55 +(*** Timing functions ***)
    1.56 +
    1.57 +(*A conditional timing function: applies f to () and, if the flag is true,
    1.58 +  prints its runtime. *)
    1.59 +fun cond_timeit flag f =
    1.60 +  if flag then
    1.61 +    let open Time  (*...for Time.toString, Time.+ and Time.- *)
    1.62 +	val CPUtimer = Timer.startCPUTimer();
    1.63 +        val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer);
    1.64 +        val result = f();
    1.65 +        val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer)
    1.66 +    in  print("User " ^ toString (usrt2-usrt1) ^
    1.67 +              "  GC " ^ toString (gct2-gct1) ^
    1.68 +              "  All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^
    1.69 +              " secs\n")
    1.70 +	  handle Time => ();
    1.71 +        result
    1.72 +    end
    1.73 +  else f();
    1.74 +
    1.75 +
    1.76 +(*** File handling ***)
    1.77 +
    1.78 +(*Get time of last modification; if file doesn't exist return an empty string*)
    1.79 +fun file_info "" = ""
    1.80 +  | file_info name = Time.toString (OS.FileSys.modTime name) handle _ =>"";
    1.81 +
    1.82 +
    1.83 +(*** ML command execution ***)
    1.84 +
    1.85 +val tmpName = OS.FileSys.tmpName();
    1.86 +
    1.87 +(*Can one redirect 'use' directly to an instream?*)
    1.88 +fun use_string slist =
    1.89 +  let val tmpFile = TextIO.openOut tmpName
    1.90 +  in app (fn s => TextIO.output (tmpFile, s)) slist;
    1.91 +     TextIO.closeOut tmpFile;
    1.92 +     use tmpName
    1.93 +  end;
    1.94 +
    1.95 +
    1.96 +(*** System command execution ***)
    1.97 +
    1.98 +(*Execute an Unix command which doesn't take any input from stdin and
    1.99 +  sends its output to stdout.
   1.100 +  This could be done more easily by Unix.execute, but that function
   1.101 +  doesn't use the PATH.*)
   1.102 +fun execute command =
   1.103 +  let val is = (OS.Process.system (command ^ " > " ^ tmpName);
   1.104 +                TextIO.openIn tmpName);
   1.105 +      val result = TextIO.inputAll is;
   1.106 +  in TextIO.closeIn is;
   1.107 +     OS.FileSys.remove tmpName;
   1.108 +     result
   1.109 +  end;
   1.110 +
   1.111 +
   1.112 +(*Don't know what the boolean is for*)
   1.113 +fun xML filename = Shell.saveImage (filename, false);