1.1 --- a/etc/settings Sat Feb 06 22:06:18 2010 +0100
1.2 +++ b/etc/settings Sat Feb 06 22:54:53 2010 +0100
1.3 @@ -50,12 +50,6 @@
1.4 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
1.5 #SMLNJ_CYGWIN_RUNTIME=1
1.6
1.7 -# Moscow ML 2.00 (experimental!)
1.8 -#ML_SYSTEM=mosml
1.9 -#ML_HOME="/usr/local/mosml/bin"
1.10 -#ML_OPTIONS=""
1.11 -#ML_PLATFORM=""
1.12 -
1.13
1.14 ###
1.15 ### JVM components (Scala or Java)
2.1 --- a/lib/scripts/run-mosml Sat Feb 06 22:06:18 2010 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,57 +0,0 @@
2.4 -#!/usr/bin/env bash
2.5 -#
2.6 -# Author: Markus Wenzel, TU Muenchen
2.7 -#
2.8 -# Moscow ML 2.00 startup script
2.9 -
2.10 -export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
2.11 -
2.12 -
2.13 -## diagnostics
2.14 -
2.15 -function fail_out()
2.16 -{
2.17 - echo "Unable to create output heap file: \"$OUTFILE\"" >&2
2.18 - exit 2
2.19 -}
2.20 -
2.21 -
2.22 -## prepare databases
2.23 -
2.24 -MOSML="mosml -P sml90"
2.25 -
2.26 -if [ -z "$INFILE" ]; then
2.27 - EXIT='load "OS"; fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;'
2.28 -else
2.29 - EXIT=""
2.30 - echo "Cannot load images yet!" >&2
2.31 - exit 2
2.32 -fi
2.33 -
2.34 -if [ -z "$OUTFILE" ]; then
2.35 - COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
2.36 -else
2.37 - COMMIT="fun commit () = true;"
2.38 - echo "WARNING: cannot save images yet!" >&2
2.39 - [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
2.40 -fi
2.41 -
2.42 -
2.43 -## run it!
2.44 -
2.45 -MLTEXT="$EXIT $COMMIT $MLTEXT"
2.46 -MLEXIT="commit();"
2.47 -
2.48 -if [ -z "$TERMINATE" ]; then
2.49 - FEEDER_OPTS=""
2.50 -else
2.51 - FEEDER_OPTS="-q"
2.52 -fi
2.53 -
2.54 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
2.55 - { read FPID; "$ML_HOME"/$MOSML $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
2.56 -RC="$?"
2.57 -
2.58 -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
2.59 -
2.60 -exit "$RC"
3.1 --- a/src/Pure/IsaMakefile Sat Feb 06 22:06:18 2010 +0100
3.2 +++ b/src/Pure/IsaMakefile Sat Feb 06 22:54:53 2010 +0100
3.3 @@ -24,13 +24,12 @@
3.4 BOOTSTRAP_FILES = ML-Systems/bash.ML ML-Systems/compiler_polyml-5.0.ML \
3.5 ML-Systems/compiler_polyml-5.2.ML ML-Systems/compiler_polyml-5.3.ML \
3.6 ML-Systems/ml_name_space.ML ML-Systems/ml_pretty.ML \
3.7 - ML-Systems/mosml.ML ML-Systems/multithreading.ML \
3.8 - ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML \
3.9 - ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML \
3.10 - ML-Systems/polyml-5.2.ML ML-Systems/polyml-5.2.1.ML \
3.11 - ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
3.12 - ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML \
3.13 - ML-Systems/single_assignment.ML \
3.14 + ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \
3.15 + ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \
3.16 + ML-Systems/polyml-5.1.ML ML-Systems/polyml-5.2.ML \
3.17 + ML-Systems/polyml-5.2.1.ML ML-Systems/polyml.ML \
3.18 + ML-Systems/polyml_common.ML ML-Systems/pp_polyml.ML \
3.19 + ML-Systems/proper_int.ML ML-Systems/single_assignment.ML \
3.20 ML-Systems/single_assignment_polyml.ML ML-Systems/smlnj.ML \
3.21 ML-Systems/thread_dummy.ML ML-Systems/timing.ML \
3.22 ML-Systems/time_limit.ML ML-Systems/universal.ML \
4.1 --- a/src/Pure/ML-Systems/mosml.ML Sat Feb 06 22:06:18 2010 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,259 +0,0 @@
4.4 -(* Title: Pure/ML-Systems/mosml.ML
4.5 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4.6 - Author: Makarius
4.7 -
4.8 -Compatibility file for Moscow ML 2.01
4.9 -
4.10 -NOTE: saving images does not work; may run it interactively as follows:
4.11 -
4.12 -$ cd Isabelle/src/Pure
4.13 -$ isabelle-process RAW_ML_SYSTEM
4.14 -> val ml_system = "mosml";
4.15 -> use "ML-Systems/mosml.ML";
4.16 -> use "ROOT.ML";
4.17 -> Session.finish ();
4.18 -> cd "../FOL";
4.19 -> use "ROOT.ML";
4.20 -> Session.finish ();
4.21 -> cd "../ZF";
4.22 -> use "ROOT.ML";
4.23 -*)
4.24 -
4.25 -(** ML system related **)
4.26 -
4.27 -val ml_system_fix_ints = false;
4.28 -
4.29 -fun forget_structure _ = ();
4.30 -
4.31 -load "Obj";
4.32 -load "Word";
4.33 -load "Bool";
4.34 -load "Int";
4.35 -load "Real";
4.36 -load "ListPair";
4.37 -load "OS";
4.38 -load "Process";
4.39 -load "FileSys";
4.40 -load "IO";
4.41 -load "CharVector";
4.42 -
4.43 -exception Interrupt;
4.44 -fun reraise exn = raise exn;
4.45 -
4.46 -use "ML-Systems/unsynchronized.ML";
4.47 -use "General/exn.ML";
4.48 -use "ML-Systems/universal.ML";
4.49 -use "ML-Systems/thread_dummy.ML";
4.50 -use "ML-Systems/multithreading.ML";
4.51 -use "ML-Systems/time_limit.ML";
4.52 -use "ML-Systems/ml_name_space.ML";
4.53 -use "ML-Systems/ml_pretty.ML";
4.54 -use "ML-Systems/use_context.ML";
4.55 -
4.56 -
4.57 -(*low-level pointer equality*)
4.58 -local val cast : 'a -> int = Obj.magic
4.59 -in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end;
4.60 -
4.61 -(*proper implementation available?*)
4.62 -structure IntInf =
4.63 -struct
4.64 - fun divMod (x, y) = (x div y, x mod y);
4.65 -
4.66 - local
4.67 - fun log 1 a = a
4.68 - | log n a = log (n div 2) (a + 1);
4.69 - in
4.70 - fun log2 n = if n > 0 then log n 0 else raise Domain;
4.71 - end;
4.72 -
4.73 - open Int;
4.74 -end;
4.75 -
4.76 -structure Substring =
4.77 -struct
4.78 - open Substring;
4.79 - val full = all;
4.80 -end;
4.81 -
4.82 -structure Real =
4.83 -struct
4.84 - open Real;
4.85 - val realFloor = real o floor;
4.86 -end;
4.87 -
4.88 -structure String =
4.89 -struct
4.90 - fun isSuffix s1 s2 =
4.91 - let val n1 = size s1 and n2 = size s2
4.92 - in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
4.93 - open String;
4.94 -end;
4.95 -
4.96 -structure Time =
4.97 -struct
4.98 - open Time;
4.99 - fun toString t = Time.toString t
4.100 - handle Overflow => Real.toString (Time.toReal t); (*workaround Y2004 bug*)
4.101 -end;
4.102 -
4.103 -structure OS =
4.104 -struct
4.105 - open OS
4.106 - structure Process =
4.107 - struct
4.108 - open Process
4.109 - fun sleep _ = raise Fail "OS.Process.sleep undefined"
4.110 - end;
4.111 - structure FileSys = FileSys
4.112 -end;
4.113 -
4.114 -exception Option = Option.Option;
4.115 -
4.116 -
4.117 -(*limit the printing depth*)
4.118 -local
4.119 - val depth = ref 10;
4.120 -in
4.121 - fun get_print_depth () = ! depth;
4.122 - fun print_depth n =
4.123 - (depth := n;
4.124 - Meta.printDepth := n div 2;
4.125 - Meta.printLength := n);
4.126 -end;
4.127 -
4.128 -(*dummy implementation*)
4.129 -fun toplevel_pp _ _ _ = ();
4.130 -
4.131 -(*dummy implementation*)
4.132 -fun ml_prompts p1 p2 = ();
4.133 -
4.134 -(*dummy implementation*)
4.135 -fun profile (n: int) f x = f x;
4.136 -
4.137 -(*dummy implementation*)
4.138 -fun exception_trace f = f ();
4.139 -
4.140 -
4.141 -
4.142 -(** Compiler-independent timing functions **)
4.143 -
4.144 -load "Timer";
4.145 -
4.146 -fun start_timing () =
4.147 - let
4.148 - val timer = Timer.startCPUTimer ();
4.149 - val time = Timer.checkCPUTimer timer;
4.150 - in (timer, time) end;
4.151 -
4.152 -fun end_timing (timer, {gc, sys, usr}) =
4.153 - let
4.154 - open Time; (*...for Time.toString, Time.+ and Time.- *)
4.155 - val {gc = gc2, sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
4.156 - val user = usr2 - usr + gc2 - gc;
4.157 - val all = user + sys2 - sys;
4.158 - val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => "";
4.159 - in {message = message, user = user, all = all} end;
4.160 -
4.161 -
4.162 -(* SML basis library fixes *)
4.163 -
4.164 -structure TextIO =
4.165 -struct
4.166 - fun canInput _ = raise IO.Io {cause = Fail "undefined", function = "canInput", name = ""};
4.167 - open TextIO;
4.168 - fun inputLine is =
4.169 - let val s = TextIO.inputLine is
4.170 - in if s = "" then NONE else SOME s end;
4.171 - fun getOutstream _ = ();
4.172 - structure StreamIO =
4.173 - struct
4.174 - fun setBufferMode _ = ();
4.175 - end
4.176 -end;
4.177 -
4.178 -structure IO =
4.179 -struct
4.180 - open IO;
4.181 - val BLOCK_BUF = ();
4.182 -end;
4.183 -
4.184 -
4.185 -(* ML command execution *)
4.186 -
4.187 -(*Can one redirect 'use' directly to an instream?*)
4.188 -fun use_text ({tune_source, ...}: use_context) _ _ txt =
4.189 - let
4.190 - val tmp_name = FileSys.tmpName ();
4.191 - val tmp_file = TextIO.openOut tmp_name;
4.192 - in
4.193 - TextIO.output (tmp_file, tune_source txt);
4.194 - TextIO.closeOut tmp_file;
4.195 - use tmp_name;
4.196 - FileSys.remove tmp_name
4.197 - end;
4.198 -
4.199 -fun use_file _ _ name = use name;
4.200 -
4.201 -
4.202 -
4.203 -(** interrupts **) (*Note: may get into race conditions*)
4.204 -
4.205 -(* FIXME proper implementation available? *)
4.206 -
4.207 -fun interruptible f x = f x;
4.208 -fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
4.209 -
4.210 -
4.211 -
4.212 -(** OS related **)
4.213 -
4.214 -(*dummy implementation*)
4.215 -structure Posix =
4.216 -struct
4.217 - structure ProcEnv =
4.218 - struct
4.219 - fun getpid () = 0;
4.220 - end;
4.221 -end;
4.222 -
4.223 -local
4.224 -
4.225 -fun read_file name =
4.226 - let val is = TextIO.openIn name
4.227 - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
4.228 -
4.229 -fun write_file name txt =
4.230 - let val os = TextIO.openOut name
4.231 - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
4.232 -
4.233 -in
4.234 -
4.235 -fun bash_output script =
4.236 - let
4.237 - val script_name = OS.FileSys.tmpName ();
4.238 - val _ = write_file script_name script;
4.239 -
4.240 - val output_name = OS.FileSys.tmpName ();
4.241 -
4.242 - val status =
4.243 - OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
4.244 - script_name ^ " /dev/null " ^ output_name);
4.245 - val rc = if status = OS.Process.success then 0 else 1;
4.246 -
4.247 - val output = read_file output_name handle IO.Io _ => "";
4.248 - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
4.249 - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
4.250 - in (output, rc) end;
4.251 -
4.252 -end;
4.253 -
4.254 -val cd = OS.FileSys.chDir;
4.255 -val pwd = OS.FileSys.getDir;
4.256 -
4.257 -val process_id = Int.toString o Posix.ProcEnv.getpid;
4.258 -
4.259 -fun getenv var =
4.260 - (case Process.getEnv var of
4.261 - NONE => ""
4.262 - | SOME txt => txt);