# HG changeset patch
# User wenzelm
# Date 1375392314 -7200
# Node ID cc425a7dc9adbcc95b7c6ed124466384e087275e
# Parent  591e76f2651e09082fb78ededf1ca1107a517bcf# Parent  fe1f6a1707f7eb9d7cfc333dd942e4964bafe354
merged

diff -r 591e76f2651e -r cc425a7dc9ad Admin/isatest/settings/at-poly-test
--- 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"
diff -r 591e76f2651e -r cc425a7dc9ad lib/scripts/recode.pl
--- /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 $_, " ";
+}
+
diff -r 591e76f2651e -r cc425a7dc9ad lib/scripts/run-polyml
--- 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
diff -r 591e76f2651e -r cc425a7dc9ad lib/scripts/run-polyml-5.5.1
--- /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:
diff -r 591e76f2651e -r cc425a7dc9ad src/Pure/ML-Systems/polyml.ML
--- 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);
 
diff -r 591e76f2651e -r cc425a7dc9ad src/Pure/ML/exn_trace_polyml-5.5.1.ML
--- /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);
+
diff -r 591e76f2651e -r cc425a7dc9ad src/Pure/ROOT
--- 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"
diff -r 591e76f2651e -r cc425a7dc9ad src/Pure/ROOT.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";
diff -r 591e76f2651e -r cc425a7dc9ad src/Tools/jEdit/src/isabelle_logic.scala
--- 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"))