--- a/lib/scripts/run-mlworks Fri Jun 04 11:51:31 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-# License: GPL (GNU GENERAL PUBLIC LICENSE)
-#
-# MLWorks startup script (for 1.0r2 or later).
-
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail_out()
-{
- echo "Unable to create output heap file: \"$OUTFILE\"" >&2
- exit 2
-}
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
- EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
- MLWORKS="mlworks-basis -tty"
-else
- EXIT=""
- MLWORKS="mlimage -load $INFILE -tty"
-fi
-
-if [ -z "$OUTFILE" ]; then
- COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
-else
- COMMIT="fun commit () = (Shell.saveImage (\"$OUTFILE\", false); true);"
- [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-fi
-
-
-## run it!
-
-MLTEXT="$EXIT $COMMIT $MLTEXT"
-MLEXIT="commit();"
-
-if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
-else
- FEEDER_OPTS="-q"
-fi
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$ML_HOME"/$MLWORKS $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-RC="$?"
-
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
-exit "$RC"
--- a/lib/scripts/run-smlnj-0.93 Fri Jun 04 11:51:31 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-# License: GPL (GNU GENERAL PUBLIC LICENSE)
-#
-# SML/NJ startup script (for 0.93).
-
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail_out()
-{
- echo "Unable to create output heap file: \"$OUTFILE\"" >&2
- exit 2
-}
-
-function check_mlhome_file()
-{
- if [ ! -f "$1" ]; then
- echo "Unable to locate $1" >&2
- echo "Please check your ML_HOME setting!" >&2
- exit 2
- fi
-}
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
- INFILE="$ML_HOME/sml"
- check_mlhome_file "$INFILE"
- EXIT="val exit: int -> unit = System.Unsafe.CInterface.exit;"
-else
- EXIT=""
-fi
-
-MOVE=""
-
-if [ -z "$OUTFILE" ]; then
- COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);'
-else
- if [ "$INFILE" -ef "$OUTFILE" ]; then
- OUTDIR=$(dirname "$OUTFILE")/tmp
- OUTFILE="$OUTDIR"/$(basename "$OUTFILE")
- mkdir -p "$OUTDIR" || fail_out
- MOVE=true
- fi
- [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
- COMMIT="fun commit () = not (exportML\"$OUTFILE\");"
-fi
-
-
-## run it!
-
-MLTEXT="$EXIT $COMMIT $MLTEXT"
-MLEXIT="commit();"
-
-if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
-else
- FEEDER_OPTS="-q"
-fi
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$INFILE" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-RC="$?"
-
-
-## fix heap file
-
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
-if [ -n "$MOVE" -a -f "$OUTFILE" ]; then
- rm -f "$INFILE" || fail_out
- mv "$OUTFILE" "$INFILE" || fail_out
-fi
-
-exit "$RC"
--- a/src/Pure/ML-Systems/mlworks.ML Fri Jun 04 11:51:31 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,136 +0,0 @@
-(* Title: Pure/ML-Systems/mlworks.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Compatibility file for MLWorks version 1.0r2 or later.
-*)
-
-(** ML system related **)
-
-(* restore old-style character / string functions *)
-
-val ord = SML90.ord;
-val chr = SML90.chr;
-val explode = SML90.explode;
-val implode = SML90.implode;
-
-
-(* MLWorks parameters *)
-
-val _ =
- (MLWorks.Internal.Runtime.Event.stack_overflow_handler
- (fn () =>
- let val max_stack = MLWorks.Internal.Runtime.Memory.max_stack_blocks
- in max_stack := (!max_stack * 3) div 2 + 5;
- print ("#### Increasing stack to " ^ Int.toString (64 * !max_stack) ^
- "KB\n")
- end);
- MLWorks.Internal.Runtime.Memory.gc_message_level := 10;
- (*Is this of any use at all?*)
- Shell.Options.set (Shell.Options.ValuePrinter.showExnDetails, true));
-
-
-(* Poly/ML emulation *)
-
-(*To exit the system with an exit code -- an alternative to ^D *)
-fun exit 0 = (OS.Process.exit OS.Process.success): unit
- | exit _ = OS.Process.exit OS.Process.failure;
-fun quit () = exit 0;
-
-(*limit the printing depth*)
-fun print_depth n =
- let open Shell.Options
- in set (ValuePrinter.maximumDepth, n div 2);
- set (ValuePrinter.maximumSeqSize, n)
- end;
-
-(*interface for toplevel pretty printers, see also Pure/install_pp.ML*)
-(*n.a.*)
-fun make_pp path pprint = ();
-fun install_pp _ = ();
-
-(*prompts*)
-(*n.a.??*)
-fun ml_prompts p1 p2 = ();
-
-
-(** Compiler-independent timing functions **)
-
-use "ML-Systems/cpu-timer-gc.ML"
-
-(* bounded time execution *)
-
-(* FIXME proper implementation available? *)
-
-structure TimeLimit : sig
- exception TimeOut
- val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
-end = struct
- exception TimeOut
- fun timeLimit t f x =
- f x;
-end;
-
-(* ML command execution *)
-
-(*Can one redirect 'use' directly to an instream?*)
-fun use_text _ _ txt =
- let
- val tmp_name = OS.FileSys.tmpName ();
- val tmp_file = TextIO.openOut tmp_name;
- in
- TextIO.output (tmp_file, txt);
- TextIO.closeOut tmp_file;
- use tmp_name;
- OS.FileSys.remove tmp_name
- end;
-
-
-
-(** interrupts **) (*Note: may get into race conditions*)
-
-exception Interrupt;
-
-MLWorks.Internal.Runtime.Event.interrupt_handler (fn () => raise Interrupt);
-
-fun ignore_interrupt f x = f x;
-fun raise_interrupt f x = f x;
-
-
-
-(** OS related **)
-
-(* system command execution *)
-
-(*execute Unix command which doesn't take any input from stdin and
- sends its output to stdout; could be done more easily by Unix.execute,
- but that function doesn't use the PATH*)
-fun execute command =
- let
- val tmp_name = OS.FileSys.tmpName ();
- val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
- val result = TextIO.inputAll is;
- in
- TextIO.closeIn is;
- OS.FileSys.remove tmp_name;
- result
- end;
-
-(*plain version; with return code*)
-fun system cmd =
- if OS.Process.system cmd = OS.Process.success then 0 else 1;
-
-
-(* file handling *)
-
-(*get time of last modification*)
-fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
-
-
-(* getenv *)
-
-fun getenv var =
- (case OS.Process.getEnv var of
- NONE => ""
- | SOME txt => txt);
--- a/src/Pure/ML-Systems/polyml-3.x.ML Fri Jun 04 11:51:31 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,132 +0,0 @@
-(* Title: Pure/ML-Systems/polyml.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Compatibility file for Poly/ML (versions 2.x and 3.x).
-*)
-
-open PolyML ExtendedIO;
-
-(*needs the Basis Library emulation*)
-use "basis.ML";
-
-
-structure String =
-struct
- fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j)
- handle Substring => raise Subscript
- fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1))
- handle Subscript => false
- fun str (s : string) = s;
- fun translate f s = implode (map f (explode s));
-end;
-
-
-(** ML system related **)
-
-(** Compiler-independent timing functions **)
-
-(*Note start point for timing*)
-fun startTiming() = System.processtime ();
-
-(*Finish timing and return string*)
-fun endTiming before =
- "User + GC: " ^
- makestring (real (System.processtime () - before) / 10.0) ^
- " secs";
-
-
-(* prompts *)
-
-fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
-
-
-(* toplevel pretty printing (see also Pure/install_pp.ML) *)
-
-fun make_pp _ pprint (str, blk, brk, en) obj =
- pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
- fn () => brk (99999, 0), en);
-
-
-(* ML command execution -- 'eval' *)
-
-local
-
-fun drop_last [] = []
- | drop_last [x] = []
- | drop_last (x :: xs) = x :: drop_last xs;
-
-val drop_last_char = implode o drop_last o explode;
-
-in
-
-fun use_text (print, err) verbose txt =
- let
- val in_buffer = ref (explode txt);
- val out_buffer = ref ([]: string list);
- fun output () = drop_last_char (implode (rev (! out_buffer)));
-
- fun get () =
- (case ! in_buffer of
- [] => ""
- | c :: cs => (in_buffer := cs; c));
- fun put s = out_buffer := s :: ! out_buffer;
-
- fun exec () =
- (case ! in_buffer of
- [] => ()
- | _ => (PolyML.compiler (get, put) (); exec ()));
- in
- exec () handle exn => (err (output ()); raise exn);
- if verbose then print (output ()) else ()
- end;
-
-
-
-(** interrupts **) (*Note: may get into race conditions*)
-
-fun ignore_interrupt f x = f x;
-fun raise_interrupt f x = f x;
-
-
-
-(** OS related **)
-
-(* system command execution *)
-
-(*execute Unix command which doesn't take any input from stdin and
- sends its output to stdout*)
-fun execute command =
- let
- val (is, os) = ExtendedIO.execute command;
- val _ = close_out os;
- val result = input (is, 999999);
- in close_in is; result end;
-
-fun system cmd = (print (execute cmd); 0); (* FIXME rc not available *)
-
-
-(* file handling *)
-
-(*get time of last modification*)
-fun file_info name = Int.toString (System.filedate name) handle _ => "";
-
-structure OS =
-struct
- structure FileSys =
- struct
- val chDir = PolyML.cd;
- fun remove name = (execute ("rm " ^ name); ());
- fun getDir () = drop_last_char (execute "pwd");
- end;
-end;
-
-
-(* getenv *)
-
-fun getenv var = drop_last_char
- (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
-
-
-end;
--- a/src/Pure/ML-Systems/smlnj-0.93.ML Fri Jun 04 11:51:31 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,195 +0,0 @@
-(* Title: Pure/ML-Systems/smlnj-0.93.ML
- ID: $Id$
- Author: Carsten Clasohm, TU Muenchen
- Copyright 1996 TU Muenchen
-
-Compatibility file for Standard ML of New Jersey version 0.93.
-*)
-
-(*needs the Basis Library emulation*)
-use "basis.ML";
-
-structure String =
-struct
- fun substring args = String.substring args
- handle String.Substring => raise Subscript;
- fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1))
- handle Subscript => false;
- fun str (s : string) = s;
- fun translate f s = implode (map f (explode s));
-end;
-
-
-
-(** ML system related **)
-
-(* New Jersey ML parameters *)
-
-System.Control.Runtime.gcmessages := 0;
-
-
-(* Poly/ML emulation *)
-
-fun quit () = exit 0;
-
-(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
-fun print_depth n =
- (System.Control.Print.printDepth := n div 2;
- System.Control.Print.printLength := n);
-
-
-
-(* timing *)
-
-(*Note start point for timing*)
-fun startTiming() = System.Timer.start_timer();
-
-(*Finish timing and return string*)
-local
- (*print microseconds, suppressing trailing zeroes*)
- fun umakestring 0 = ""
- | umakestring n =
- chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
-
- fun string_of_time (System.Timer.TIME {sec, usec}) =
- makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
-
-in
-
-fun endTiming start =
- let val nongc = System.Timer.check_timer(start)
- and gc = System.Timer.check_timer_gc(start);
- val both = System.Timer.add_time(nongc, gc)
- in "Non GC " ^ string_of_time nongc ^
- " GC " ^ string_of_time gc ^
- " both "^ string_of_time both ^ " secs\n"
- end
-end;
-
-
-(* prompts *)
-
-fun ml_prompts p1 p2 = ();
-
-
-(* toplevel pretty printing (see also Pure/install_pp.ML) *)
-
-fun make_pp path pprint =
- let
- open System.PrettyPrint;
-
- fun pp pps obj =
- pprint obj
- (add_string pps, begin_block pps INCONSISTENT,
- fn wd => add_break pps (wd, 0), fn () => add_newline pps,
- fn () => end_block pps);
- in
- (path, pp)
- end;
-
-fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
-
-
-(* ML command execution *)
-
-fun use_text _ _ = System.Compile.use_stream o open_string;
-
-
-
-(** interrupts **)
-
-exception Interrupt;
-
-local
-
-fun capture f x = ((f x): unit; NONE) handle exn => SOME exn;
-
-fun release NONE = ()
- | release (SOME exn) = raise exn;
-
-structure Signals = System.Signals;
-
-in
-
-fun ignore_interrupt f x =
- let
- val old_handler = Signals.inqHandler Signals.SIGINT;
- val _ = Signals.setHandler (Signals.SIGINT, SOME #2);
- val result = capture f x;
- val _ = Signals.setHandler (Signals.SIGINT, old_handler);
- in release result end;
-
-fun raise_interrupt f x =
- let
- val interrupted = ref false;
- val result = ref NONE;
- val old_handler = Signals.inqHandler Signals.SIGINT;
- in
- callcc (fn cont =>
- (Signals.setHandler (Signals.SIGINT, SOME (fn _ => (interrupted := true; cont)));
- result := capture f x));
- Signals.setHandler (Signals.SIGINT, old_handler);
- if ! interrupted then raise Interrupt else release (! result)
- end;
-
-end;
-
-
-(** OS related **)
-
-(* system command execution *)
-
-(*execute Unix command which doesn't take any input from stdin and
- sends its output to stdout; could be done more easily by IO.execute,
- but that function seems to be buggy in SML/NJ 0.93*)
-fun execute command =
- let
- val tmp_name = "/tmp/isabelle-execute";
- val is = (System.system (command ^ " > " ^ tmp_name); open_in tmp_name);
- val result = input (is, 999999);
- in
- close_in is;
- System.Unsafe.SysIO.unlink tmp_name;
- result
- end;
-
-(*plain version; with return code*)
-fun system cmd = System.system cmd div 256;
-
-
-(* file handling *)
-
-(*get time of last modification*)
-local
- open System.Timer System.Unsafe.SysIO;
-in
- fun file_info name = makestring (mtime (PATH name)) handle _ => "";
-end;
-
-structure OS =
-struct
- structure FileSys =
- struct
- val chDir = System.Directory.cd;
- val remove = System.Unsafe.SysIO.unlink;
- val getDir = System.Directory.getWD;
- end;
-end;
-
-(*redefine to flush its output immediately -- temporary patch suggested
- by Kim Dam Petersen*) (* FIXME !? *)
-val output = fn (s, t) => (output (s, t); flush_out s);
-
-
-(* getenv *)
-
-local
- fun drop_last [] = []
- | drop_last [x] = []
- | drop_last (x :: xs) = x :: drop_last xs;
-
- val drop_last_char = implode o drop_last o explode;
-in
- fun getenv var = drop_last_char
- (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
-end;
--- a/src/Pure/basis.ML Fri Jun 04 11:51:31 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,192 +0,0 @@
-(* Title: Pure/basis.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Basis Library emulation. Needed for Poly/ML and Standard ML of New
-Jersey version 0.93 to 1.08. Full compatibility cannot be obtained
-using a file: what about char constants?
-*)
-
-exception Subscript;
-
-structure Bool =
- struct
- fun toString true = "true"
- | toString false = "false"
- end;
-
-
-structure Option =
- struct
- exception Option
-
- datatype 'a option = NONE | SOME of 'a
-
- fun getOpt (SOME v, _) = v
- | getOpt (NONE, a) = a
-
- fun isSome (SOME _) = true
- | isSome NONE = false
-
- fun valOf (SOME v) = v
- | valOf NONE = raise Option
- end;
-
-
-structure Int =
- struct
- type int = int
- fun toString (i: int) = makestring i;
- fun max (x, y) = if x < y then y else x : int;
- fun min (x, y) = if x < y then x else y : int;
- end;
-
-
-structure Real =
- struct
- fun toString (x: real) = makestring x;
- fun max (x, y) = if x < y then y else x : real;
- fun min (x, y) = if x < y then x else y : real;
- val real = real;
- val floor = floor;
- fun ceil x = ~1 - floor (~ (x + 1.0));
- fun round x = floor (x + 0.5); (*does not do round-to-nearest*)
- fun trunc x = if x < 0.0 then ceil x else floor x;
- end;
-
-
-structure List =
- struct
- exception Empty
-
- fun last [] = raise Empty
- | last [x] = x
- | last (x::xs) = last xs;
-
- fun nth (xs, n) =
- let fun h [] _ = raise Subscript
- | h (x::xs) n = if n=0 then x else h xs (n-1)
- in if n<0 then raise Subscript else h xs n end;
-
- fun drop (xs, n) =
- let fun h xs 0 = xs
- | h [] n = raise Subscript
- | h (x::xs) n = h xs (n-1)
- in if n<0 then raise Subscript else h xs n end;
-
- fun take (xs, n) =
- let fun h xs 0 = []
- | h [] n = raise Subscript
- | h (x::xs) n = x :: h xs (n-1)
- in if n<0 then raise Subscript else h xs n end;
-
- fun concat [] = []
- | concat (l::ls) = l @ concat ls;
-
- fun mapPartial f [] = []
- | mapPartial f (x::xs) =
- (case f x of Option.NONE => mapPartial f xs
- | Option.SOME y => y :: mapPartial f xs);
-
- fun find _ [] = Option.NONE
- | find p (x :: xs) = if p x then Option.SOME x else find p xs;
-
-
- (*copy the list preserving elements that satisfy the predicate*)
- fun filter p [] = []
- | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
-
- (*Partition list into elements that satisfy predicate and those that don't.
- Preserves order of elements in both lists.*)
- fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
- let fun part ([], answer) = answer
- | part (x::xs, (ys, ns)) = if p(x)
- then part (xs, (x::ys, ns))
- else part (xs, (ys, x::ns))
- in part (rev ys, ([], [])) end;
-
- end;
-
-
-structure ListPair =
- struct
- fun zip ([], []) = []
- | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
-
- fun unzip [] = ([],[])
- | unzip((x,y)::pairs) =
- let val (xs,ys) = unzip pairs
- in (x::xs, y::ys) end;
-
- fun map f ([], []) = []
- | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
-
- fun exists p =
- let fun boolf ([], []) = false
- | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
- in boolf end;
-
- fun all p =
- let fun boolf ([], []) = true
- | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
- in boolf end;
- end;
-
-
-structure TextIO =
- struct
- type instream = instream
- and outstream = outstream
- exception Io of {name: string, function: string, cause: exn}
- val stdIn = std_in
- val stdOut = std_out
- val stdErr = std_out
- val openIn = open_in
- val openAppend = open_append
- val openOut = open_out
- val closeIn = close_in
- val closeOut = close_out
- val inputN = input
- val inputAll = fn is => inputN (is, 999999)
- val inputLine = input_line
- val endOfStream = end_of_stream
- val output = output
- val flushOut = flush_out
- end;
-
-
-fun print s = (output (std_out, s); flush_out std_out);
-
-
-structure General =
-struct
-
-local
- fun raised name = "exception " ^ name ^ " raised";
- fun raised_msg name msg = raised name ^ ": " ^ msg;
-in
- fun exnMessage Match = raised_msg "Match" "nonexhaustive match failure"
- | exnMessage Bind = raised_msg "Bind" "nonexhaustive binding failure"
- | exnMessage (Io msg) = "I/O error: " ^ msg
- | exnMessage Neg = raised "Neg"
- | exnMessage Sum = raised "Sum"
- | exnMessage Diff = raised "Diff"
- | exnMessage Prod = raised "Prod"
- | exnMessage Quot = raised "Quot"
- | exnMessage Abs = raised "Abs"
- | exnMessage Div = raised "Div"
- | exnMessage Mod = raised "Mod"
- | exnMessage Floor = raised "Floor"
- | exnMessage Sqrt = raised "Sqrt"
- | exnMessage Exp = raised "Exp"
- | exnMessage Ln = raised "Ln"
- | exnMessage Ord = raised "Ord"
- | exnMessage Subscript = raised_msg "Subscript " "subscript out of bounds"
- | exnMessage Option.Option = raised "Option.Option"
- | exnMessage List.Empty = raised "List.Empty"
- | exnMessage (TextIO.Io {name, ...}) = raised_msg "TextIO.Io" name
- | exnMessage exn = raised "???";
-end;
-
-end;