1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/mosml.ML	Thu Jul 06 00:09:45 2000 +0200
     1.3 @@ -0,0 +1,147 @@
     1.4 +(*  Title:      Pure/ML-Systems/mosml.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1999  University of Cambridge
     1.8 +
     1.9 +Compatibility file for Moscow ML 2.00
    1.10 +
    1.11 +NOTE: saving images does not work (yet!?), may run it interactively as follows:
    1.12 +
    1.13 +$ cd .../Pure
    1.14 +$ isabelle RAW_ML_SYSTEM
    1.15 +> val ml_system = "mosml";
    1.16 +> use "ML-Systems/mosml.ML";
    1.17 +> use "ROOT.ML";
    1.18 +*)
    1.19 +
    1.20 +(** ML system related **)
    1.21 +
    1.22 +
    1.23 +(* Poly/ML emulation *)
    1.24 +
    1.25 +load "Bool";
    1.26 +load "Int";
    1.27 +load "Real";
    1.28 +load "ListPair";
    1.29 +
    1.30 +load "OS";
    1.31 +load "Process";
    1.32 +load "FileSys";
    1.33 +
    1.34 +structure OS =
    1.35 +  struct
    1.36 +  open OS
    1.37 +  structure Process = Process
    1.38 +  structure FileSys = FileSys
    1.39 +  end;
    1.40 + 
    1.41 +(*To exit the system with an exit code -- an alternative to ^D *)
    1.42 +fun exit 0 = Process.exit Process.success
    1.43 +  | exit _ = Process.exit Process.failure;
    1.44 +
    1.45 +(*limit the printing depth*)
    1.46 +fun print_depth n =
    1.47 + (Meta.printDepth := n div 2;
    1.48 +  Meta.printLength := n);
    1.49 +
    1.50 +(*interface for toplevel pretty printers, see also Pure/install_pp.ML*)
    1.51 +(*the documentation refers to an installPP but I couldn't fine it!*)
    1.52 +fun make_pp path pprint = ();
    1.53 +fun install_pp _ = ();
    1.54 +
    1.55 +(*prompts*)
    1.56 +(*n.a.??*)
    1.57 +fun ml_prompts p1 p2 = ();
    1.58 +
    1.59 +
    1.60 +(** Compiler-independent timing functions **)
    1.61 +
    1.62 +load "Timer";
    1.63 +
    1.64 +(*Note start point for timing*)
    1.65 +fun startTiming() = 
    1.66 +  let val CPUtimer = Timer.startCPUTimer();
    1.67 +      val time = Timer.checkCPUTimer(CPUtimer)
    1.68 +  in  (CPUtimer,time)  end;
    1.69 +
    1.70 +(*Finish timing and return string*)
    1.71 +fun endTiming (CPUtimer, {gc,sys,usr}) =
    1.72 +  let open Time  (*...for Time.toString, Time.+ and Time.- *)
    1.73 +      val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    1.74 +  in  "User " ^ toString (usr2-usr) ^
    1.75 +      "  GC " ^ toString (gc2-gc) ^
    1.76 +      "  All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
    1.77 +      " secs"
    1.78 +      handle Time => ""
    1.79 +  end;
    1.80 +
    1.81 +
    1.82 +(* ML command execution *)
    1.83 +
    1.84 +(*Can one redirect 'use' directly to an instream?*)
    1.85 +fun use_text _ _ txt =
    1.86 +  let
    1.87 +    val tmp_name = FileSys.tmpName ();
    1.88 +    val tmp_file = TextIO.openOut tmp_name;
    1.89 +  in
    1.90 +    TextIO.output (tmp_file, txt);
    1.91 +    TextIO.closeOut tmp_file;
    1.92 +    use tmp_name;
    1.93 +    FileSys.remove tmp_name
    1.94 +  end;
    1.95 +
    1.96 +
    1.97 +
    1.98 +(** interrupts **)	(*Note: may get into race conditions*)
    1.99 +
   1.100 +(* FIXME proper implementation available? *)
   1.101 +
   1.102 +exception Interrupt;
   1.103 +
   1.104 +fun mask_interrupt f x = f x;           
   1.105 +fun unmask_interrupt f x = f x;
   1.106 +fun exhibit_interrupt f x = f x;
   1.107 +
   1.108 +
   1.109 +
   1.110 +(** OS related **)
   1.111 +
   1.112 +(* system command execution *)
   1.113 +
   1.114 +(*execute Unix command which doesn't take any input from stdin and
   1.115 +  sends its output to stdout; could be done more easily by Unix.execute,
   1.116 +  but that function doesn't use the PATH*)
   1.117 +fun execute command =
   1.118 +  let
   1.119 +    val tmp_name = FileSys.tmpName ();
   1.120 +    val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn 
   1.121 +tmp_name);
   1.122 +    val result = TextIO.inputAll is;
   1.123 +  in
   1.124 +    TextIO.closeIn is;
   1.125 +    FileSys.remove tmp_name;
   1.126 +    result
   1.127 +  end;
   1.128 +
   1.129 +(*plain version; with return code*)
   1.130 +fun system cmd =
   1.131 +  if Process.system cmd = Process.success then 0 else 1;
   1.132 +
   1.133 +
   1.134 +(* file handling *)
   1.135 +
   1.136 +(*get time of last modification*)
   1.137 +fun file_info name = Time.toString (FileSys.modTime name) handle _ => "";
   1.138 +
   1.139 +
   1.140 +(* getenv *)
   1.141 +
   1.142 +fun getenv var =
   1.143 +  (case Process.getEnv var of
   1.144 +    NONE => ""
   1.145 +  | SOME txt => txt);
   1.146 +
   1.147 +
   1.148 +(* non-ASCII input (see also Thy/use.ML) *)
   1.149 +
   1.150 +val needs_filtered_use = false;