lib/scripts/run-polyml

 #!/usr/bin/env bash
 #
 # $Id$
-# Author: Markus Wenzel, TU Muenchen
+# Author: Makarius
 #
-# Poly/ML startup script.
+# Poly/ML 5.1/5.2 startup script.
 
 export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
 
 
 ## diagnostics

     exit 2
   fi
 }
 
 
-## Poly/ML executable and database
-
-ML_DBASE_PREFIX=""
+## compiler executables and libraries
 
 POLY="$ML_HOME/poly"
 check_file "$POLY"
 
-if [ -z "$ML_DBASE" ]; then
-  if [ ! -e "$ML_HOME/ML_dbase" -a "$(basename "$ML_HOME")" = bin ]; then
-    ML_DBASE_HOME="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib/poly; pwd)"
-  else
-    ML_DBASE_HOME="$ML_HOME"
-  fi
-  if [ -z "$COPYDB" ]; then
-    ML_DBASE_PREFIX="$ML_DBASE_HOME/"
-    ML_DBASE="ML_dbase"
-  else
-    ML_DBASE="$ML_DBASE_HOME/ML_dbase"
-  fi
-  export POLYPATH="$ML_DBASE_HOME"
+if [ "$(basename "$ML_HOME")" = bin ]; then
+  POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)"
 else
-  export POLYPATH="$(dirname "$ML_DBASE")"
+  POLYLIB="$ML_HOME"
 fi
 
-DISCGARB_OPTIONS="-d -c"
-
-EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
+export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH"
+export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH"
 
 
 ## prepare databases
 
 if [ -z "$INFILE" ]; then
-  check_file "$ML_DBASE_PREFIX$ML_DBASE"
-  INFILE="$ML_DBASE"
-  MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
-  DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
+  INIT=""
+  EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
 else
-  COPYDB=true
+  check_file "$INFILE"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \"\\n\"); OS.Process.exit OS.Process.failure));"
+  EXIT=""
 fi
 
 if [ -z "$OUTFILE" ]; then
-  DB="$INFILE"
-  ML_OPTIONS="-r $ML_OPTIONS"
-elif [ "$INFILE" -ef "$OUTFILE" ]; then
-  DB="$INFILE"
-elif [ -n "$COPYDB" ]; then
-  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
-  cp "$INFILE" "$OUTFILE" || fail_out
-  chmod +w "$OUTFILE" || fail_out
-  DB="$OUTFILE"
+  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
 else
-  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
-  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
-  [ -f "$OUTFILE" ] || fail_out
-  DB="$OUTFILE"
+  if [ -z "$COMPRESS" ]; then
+    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
+  else
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
+  fi
+  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
 fi
 
 
 ## run it!
+
+MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
+MLEXIT="commit();"
 
 if [ -z "$TERMINATE" ]; then
   FEEDER_OPTS=""
 else
   FEEDER_OPTS="-q"
 fi
 
-DB_INFO="$(ls -l "$DB" 2>/dev/null)"
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | {
-  read FPID; "$POLY" $ML_OPTIONS "$DB";
-  RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
 RC="$?"
 
-NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)"
-[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
-  "$POLY" $DISCGARB_OPTIONS "$OUTFILE"
 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 
 exit "$RC"