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