--- a/lib/scripts/run-poplogml Sat Jun 14 17:26:09 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Makarius
-#
-# Poplog/PML startup script (version 15.6/2.1).
-
-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
-}
-
-function check_heap_file()
-{
- if [ ! -f "$1" ]; then
- echo "Expected to find ML heap file $1" >&2
- return 1
- else
- return 0
- fi
-}
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
- EXIT="fun exit (i: int) = OS.execve \"/bin/sh\" [\"sh\", \"-c\", \"exit \" ^ makestring i] (OS.envlist());"
- USE='pop11
-section $-ml;
-
-ml_exception Use of string;
-
-ml_val use : string -> unit =
-procedure(name) with_props use;
- lvars name, path;
- lconstant UseExn = exception("Use");
-
- define dlocal pop_exception_handler(n, msg, idstring, severity);
- returnunless(severity == `E` or severity == `R`)(false);
- erasenum(n);
- raise(UseExn(name));
- enddefine;
-
- unless sourcefile(name) ->> path then raise(UseExn(name)) endunless;
- ml_load(path);
- ml_unit;
-endprocedure;
-
-ml_val use_string : string -> unit =
-procedure(str) with_props use_string;
- lvars str;
- lconstant UseExn = exception("Use");
-
- define dlocal pop_exception_handler(n, msg, idstring, severity);
- [n ^n msg ^msg idstring ^idstring severity ^severity] ==>
- returnunless(severity == `E` or severity == `R`)(false);
- erasenum(n);
- raise(UseExn(str));
- enddefine;
-
- ml_compile(stringin(str));
- ml_unit;
-endprocedure;
-
-endsection;
-ml'
- DB=""
-else
- EXIT=""
- USE=""
- DB="+$INFILE"
-fi
-
-if [ -z "$OUTFILE" ]; then
- COMMIT='fun commit () = (StdIO.output (StdIO.std_err, "Error - Database is not opened for writing.\n"); false);'
-else
- ML_OPTIONS="$ML_OPTIONS -nort"
- if [ -z "$NOWRITE" ]; then
- COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = false, share = false, banner = false, init = false} then System.restart() else true;"
- else
- COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = true, share = true, banner = false, init = false} then System.restart() else true;"
- fi
- [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-fi
-
-
-## run it!
-
-POPLOG="$ML_HOME/poplog"
-check_mlhome_file "$POPLOG"
-
-INIT="$ISABELLE_TMP/init.ml"
-echo 'pop11
-section $-ml;
-false -> ml_quiet;
-endsection;
-ml' > "$INIT"
-
-echo "$EXIT $USE $COMMIT $MLTEXT" >> "$INIT"
-
-if [ -n "$TERMINATE" ]; then
- ML_OPTIONS="$ML_OPTIONS -nostdin"
- echo "commit();" >> "$INIT"
-fi
-
-"$POPLOG" pml "$DB" $ML_OPTIONS -load "$INIT" 2>&1
-RC="$?"
-
-rm -f "$INIT"
-
-if [ -n "$OUTFILE" ] && check_heap_file "$OUTFILE"; then
- [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
- rm -f "$OUTFILE-"
-fi
-
-exit "$RC"