Moved MLWorks.ML to its proper place, directory ML-Systems.
authorpaulson
Fri Jul 04 11:56:18 1997 +0200 (1997-07-04)
changeset 3493124103119f1c
parent 3492 88e786024079
child 3494 f7ac2d1e2051
Moved MLWorks.ML to its proper place, directory ML-Systems.
Note that MLWorks does not quite work yet, especially top-level pretty
printing
src/Pure/ML-Systems/MLWorks.ML
src/Pure/MLWorks.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/MLWorks.ML	Fri Jul 04 11:56:18 1997 +0200
     1.3 @@ -0,0 +1,115 @@
     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 +Shell.File.loadSource "system.__os";
    1.21 +Shell.File.loadSource "basis.__timer";
    1.22 +Shell.File.loadSource "system.__time";
    1.23 +Shell.File.loadSource "unix.__os_file_sys";
    1.24 +Shell.File.loadSource "basis.__list";
    1.25 +Shell.File.loadSource "basis.__char";
    1.26 +Shell.File.loadSource "basis.__string";
    1.27 +Shell.File.loadSource "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 +  CURRENTLY UNAVAILABLE*)
    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);
   1.114 +
   1.115 +
   1.116 +(*Non-printing and 8-bit chars are forbidden in string constants*)
   1.117 +val needs_filtered_use = true;
   1.118 +
     2.1 --- a/src/Pure/MLWorks.ML	Fri Jul 04 11:54:43 1997 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,115 +0,0 @@
     2.4 -(*  Title:      Pure/MLWorks.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1996  University of Cambridge
     2.8 -
     2.9 -Compatibility file for MLWorks (??)
    2.10 -
    2.11 -NB: There is still no easy way of building Isabelle under MLWorks.  This file
    2.12 -    is just a start towards compatibility.  One problem is the peculiar
    2.13 -    behaviour of "use" in MLWorks.  Strange errors occur when loading theories,
    2.14 -    and ROOT.ML files on subdirectories are loaded incorrectly.
    2.15 -*)
    2.16 -
    2.17 -(*** Poly/ML emulation ***)
    2.18 -
    2.19 -(**
    2.20 -Shell.File.loadSource "system.__os";
    2.21 -Shell.File.loadSource "basis.__timer";
    2.22 -Shell.File.loadSource "system.__time";
    2.23 -Shell.File.loadSource "unix.__os_file_sys";
    2.24 -Shell.File.loadSource "basis.__list";
    2.25 -Shell.File.loadSource "basis.__char";
    2.26 -Shell.File.loadSource "basis.__string";
    2.27 -Shell.File.loadSource "basis.__text_io";
    2.28 -**)
    2.29 -
    2.30 -
    2.31 -(*To exit the system with an exit code -- an alternative to ^D *)
    2.32 -fun exit 0 = OS.Process.exit OS.Process.success
    2.33 -  | exit _ = OS.Process.exit OS.Process.failure;
    2.34 -fun quit () = exit 0;
    2.35 -
    2.36 -(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
    2.37 -fun print_depth n = ();
    2.38 -
    2.39 -(*Interface for toplevel pretty printers, see also Pure/install_pp.ML
    2.40 -  CURRENTLY UNAVAILABLE*)
    2.41 -fun make_pp path pprint = ();
    2.42 -fun install_pp _ = ();
    2.43 -
    2.44 -
    2.45 -(*** New Jersey ML parameters ***)
    2.46 -
    2.47 -(*** Character/string functions which are compatible with 0.93 and Poly/ML ***)
    2.48 -
    2.49 -fun ord s = Char.ord (String.sub(s,0));
    2.50 -val chr = str o Char.chr;
    2.51 -val explode = (map str) o String.explode;
    2.52 -val implode = String.concat;
    2.53 -
    2.54 -
    2.55 -(*** Timing functions ***)
    2.56 -
    2.57 -(*A conditional timing function: applies f to () and, if the flag is true,
    2.58 -  prints its runtime. *)
    2.59 -fun cond_timeit flag f =
    2.60 -  if flag then
    2.61 -    let open Time  (*...for Time.toString, Time.+ and Time.- *)
    2.62 -	val CPUtimer = Timer.startCPUTimer();
    2.63 -        val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer);
    2.64 -        val result = f();
    2.65 -        val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer)
    2.66 -    in  print("User " ^ toString (usrt2-usrt1) ^
    2.67 -              "  GC " ^ toString (gct2-gct1) ^
    2.68 -              "  All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^
    2.69 -              " secs\n")
    2.70 -	  handle Time => ();
    2.71 -        result
    2.72 -    end
    2.73 -  else f();
    2.74 -
    2.75 -
    2.76 -(*** File handling ***)
    2.77 -
    2.78 -(*Get time of last modification; if file doesn't exist return an empty string*)
    2.79 -fun file_info "" = ""
    2.80 -  | file_info name = Time.toString (OS.FileSys.modTime name) handle _ =>"";
    2.81 -
    2.82 -
    2.83 -(*** ML command execution ***)
    2.84 -
    2.85 -val tmpName = OS.FileSys.tmpName();
    2.86 -
    2.87 -(*Can one redirect 'use' directly to an instream?*)
    2.88 -fun use_string slist =
    2.89 -  let val tmpFile = TextIO.openOut tmpName
    2.90 -  in app (fn s => TextIO.output (tmpFile, s)) slist;
    2.91 -     TextIO.closeOut tmpFile;
    2.92 -     use tmpName
    2.93 -  end;
    2.94 -
    2.95 -
    2.96 -(*** System command execution ***)
    2.97 -
    2.98 -(*Execute an Unix command which doesn't take any input from stdin and
    2.99 -  sends its output to stdout.
   2.100 -  This could be done more easily by Unix.execute, but that function
   2.101 -  doesn't use the PATH.*)
   2.102 -fun execute command =
   2.103 -  let val is = (OS.Process.system (command ^ " > " ^ tmpName);
   2.104 -                TextIO.openIn tmpName);
   2.105 -      val result = TextIO.inputAll is;
   2.106 -  in TextIO.closeIn is;
   2.107 -     OS.FileSys.remove tmpName;
   2.108 -     result
   2.109 -  end;
   2.110 -
   2.111 -
   2.112 -(*Don't know what the boolean is for*)
   2.113 -fun xML filename = Shell.saveImage (filename, false);
   2.114 -
   2.115 -
   2.116 -(*Non-printing and 8-bit chars are forbidden in string constants*)
   2.117 -val needs_filtered_use = true;
   2.118 -