--- a/Admin/isatest/settings/at-poly-test Thu Aug 01 22:37:04 2013 +0200
+++ b/Admin/isatest/settings/at-poly-test Thu Aug 01 23:25:14 2013 +0200
@@ -3,7 +3,7 @@
init_components /home/isabelle/contrib "$HOME/admin/components/main"
POLYML_HOME="/home/polyml/polyml-svn"
- ML_SYSTEM="polyml-5.5.0"
+ ML_SYSTEM="polyml-5.5.1"
ML_PLATFORM="x86-linux"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 500 --gcthreads 1"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/recode.pl Thu Aug 01 23:25:14 2013 +0200
@@ -0,0 +1,12 @@
+#
+# Author: Makarius
+#
+# recode.pl - recode utf8 for ML
+#
+
+for (@ARGV) {
+ utf8::upgrade($_);
+ s/([\x80-\xff])/\\${\(ord($1))}/g;
+ print $_, " ";
+}
+
--- a/lib/scripts/run-polyml Thu Aug 01 22:37:04 2013 +0200
+++ b/lib/scripts/run-polyml Thu Aug 01 23:25:14 2013 +0200
@@ -2,7 +2,7 @@
#
# Author: Makarius
#
-# Poly/ML 5.1/5.2 startup script.
+# Startup script for Poly/ML 5.1 ... 5.5.
export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
@@ -33,13 +33,8 @@
POLY="$ML_HOME/poly"
check_file "$POLY"
-if [ "$(basename "$ML_HOME")" = bin ]; then
- POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)"
-else
- POLYLIB="$ML_HOME"
-fi
+librarypath "$ML_HOME"
-librarypath "$POLYLIB"
## prepare databases
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/run-polyml-5.5.1 Thu Aug 01 23:25:14 2013 +0200
@@ -0,0 +1,86 @@
+#!/usr/bin/env bash
+# :mode=shellscript:
+#
+# Author: Makarius
+#
+# Startup script for Poly/ML 5.5.1.
+
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
+
+
+## diagnostics
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+function fail_out()
+{
+ fail "Unable to create output heap file: \"$OUTFILE\""
+}
+
+function check_file()
+{
+ [ ! -f "$1" ] && fail "Unable to locate \"$1\""
+}
+
+
+## compiler executables and libraries
+
+[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
+
+POLY="$ML_HOME/poly"
+check_file "$POLY"
+
+librarypath "$ML_HOME"
+
+
+
+## prepare databases
+
+if [ -z "$INFILE" ]; then
+ INIT=""
+ EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
+else
+ check_file "$INFILE"
+ INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
+ EXIT=""
+fi
+
+if [ -z "$OUTFILE" ]; then
+ COMMIT='fun commit () = false;'
+ MLEXIT=""
+else
+ COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+ [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+ MLEXIT="commit();"
+fi
+
+
+## run it!
+
+MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
+
+if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
+ "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
+ --error-exit </dev/null
+ RC="$?"
+else
+ if [ -z "$TERMINATE" ]; then
+ FEEDER_OPTS=""
+ else
+ FEEDER_OPTS="-q"
+ ML_OPTIONS="$ML_OPTIONS --error-exit"
+ fi
+ "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+ { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+ RC="$?"
+fi
+
+[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+
+exit "$RC"
+
+#:wrap=soft:maxLineLen=100:
--- a/src/Pure/ML-Systems/polyml.ML Thu Aug 01 22:37:04 2013 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Thu Aug 01 23:25:14 2013 +0200
@@ -105,6 +105,7 @@
PolyML.Compiler.reportUnreferencedIds := true;
PolyML.Compiler.printInAlphabeticalOrder := false;
PolyML.Compiler.maxInlineSize := 80;
+(*PolyML.Compiler.reportExhaustiveHandlers := true;*)
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_trace_polyml-5.5.1.ML Thu Aug 01 23:25:14 2013 +0200
@@ -0,0 +1,14 @@
+(* Title: Pure/ML/exn_trace_polyml-5.5.1.ML
+ Author: Makarius
+
+Exception trace for Poly/ML 5.5.1, using regular Isabelle output.
+*)
+
+fun exception_trace e =
+ PolyML.Exception.traceException
+ (e, fn (trace, exn) =>
+ let
+ val title = "Exception trace - " ^ ML_Compiler.exn_message exn;
+ val _ = tracing (cat_lines (title :: trace));
+ in reraise exn end);
+
--- a/src/Pure/ROOT Thu Aug 01 22:37:04 2013 +0200
+++ b/src/Pure/ROOT Thu Aug 01 23:25:14 2013 +0200
@@ -138,6 +138,7 @@
"Isar/typedecl.ML"
"ML/exn_properties_dummy.ML"
"ML/exn_properties_polyml.ML"
+ "ML/exn_trace_polyml-5.5.1.ML"
"ML/install_pp_polyml.ML"
"ML/ml_antiquote.ML"
"ML/ml_compiler.ML"
--- a/src/Pure/ROOT.ML Thu Aug 01 22:37:04 2013 +0200
+++ b/src/Pure/ROOT.ML Thu Aug 01 23:25:14 2013 +0200
@@ -183,6 +183,7 @@
use "Isar/runtime.ML";
use "ML/ml_compiler.ML";
if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
+if ML_System.name = "polyml-5.5.1" then use "ML/exn_trace_polyml-5.5.1.ML" else ();
use "skip_proof.ML";
use "goal.ML";
--- a/src/Tools/jEdit/src/isabelle_logic.scala Thu Aug 01 22:37:04 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Thu Aug 01 23:25:14 2013 +0200
@@ -61,7 +61,7 @@
def session_args(): List[String] =
{
val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
- modes ::: List(jedit_logic())
+ modes ::: List("-r", "-q", jedit_logic())
}
def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))