# HG changeset patch
# User wenzelm
# Date 1457044421 -3600
# Node ID 922e702ae8ca967f4b1a293e65933cd65cea2ab9
# Parent  ff99681b3fd818a28af586490c0cdd3d1e6d8103# Parent  93fa1efc7219c3b61b5de5e4c01fe0c775df5576
merged

diff -r ff99681b3fd8 -r 922e702ae8ca Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Thu Mar 03 17:03:09 2016 +0100
+++ b/Admin/Release/CHECKLIST	Thu Mar 03 23:33:41 2016 +0100
@@ -5,8 +5,6 @@
 
 - check Admin/components;
 
-- test polyml-5.3.0;
-
 - test 'display_drafts' command;
 
 - test "#!/usr/bin/env isabelle_scala_script";
diff -r ff99681b3fd8 -r 922e702ae8ca Admin/isatest/settings/at-poly
--- a/Admin/isatest/settings/at-poly	Thu Mar 03 17:03:09 2016 +0100
+++ b/Admin/isatest/settings/at-poly	Thu Mar 03 23:33:41 2016 +0100
@@ -2,11 +2,7 @@
 
 init_components /home/isabelle/contrib "$HOME/admin/components/main"
 
-  POLYML_HOME="/home/polyml/polyml-5.3.0"
-  ML_SYSTEM="polyml-5.3.0"
-  ML_PLATFORM="x86-linux"
-  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-H 1000"
+ML_OPTIONS="-H 1000 --gcthreads 1"
 
 ISABELLE_GHC=/usr/bin/ghc
 
@@ -35,4 +31,3 @@
 ISABELLE_POLYML="$ML_HOME/poly"
 ISABELLE_SCALA="$SCALA_HOME/bin"
 ISABELLE_SMLNJ="/home/smlnj/bin/sml"
-
diff -r ff99681b3fd8 -r 922e702ae8ca NEWS
--- a/NEWS	Thu Mar 03 17:03:09 2016 +0100
+++ b/NEWS	Thu Mar 03 23:33:41 2016 +0100
@@ -205,7 +205,7 @@
 discontinued. INCOMPATIBILITY, use operations from the modules "XML" and
 "YXML" in Isabelle/ML or Isabelle/Scala.
 
-* SML/NJ is no longer supported.
+* SML/NJ and old versions of Poly/ML are no longer supported.
 
 
 New in Isabelle2016 (February 2016)
@@ -998,7 +998,15 @@
 
 *** System ***
 
-* Command-line tool "isabelle console" enables print mode "ASCII".
+* Command-line tool "isabelle_process" supports ML evaluation of literal
+expressions (option -e) or files (option -f). Errors lead to premature
+exit of the ML process with return code 1.
+
+* Command-line tool "isabelle console -r" helps to bootstrap
+Isabelle/Pure interactively.
+
+* Command-line tool "isabelle console" enables print mode "ASCII" for
+regular logic sessions.
 
 * Command-line tool "isabelle update_then" expands old Isar command
 conflations:
diff -r ff99681b3fd8 -r 922e702ae8ca bin/isabelle_process
--- a/bin/isabelle_process	Thu Mar 03 17:03:09 2016 +0100
+++ b/bin/isabelle_process	Thu Mar 03 23:33:41 2016 +0100
@@ -29,7 +29,8 @@
   echo "    -O           system options from given YXML file"
   echo "    -P SOCKET    startup process wrapper via TCP socket"
   echo "    -S           secure mode -- disallow critical operations"
-  echo "    -e ML_TEXT   pass ML_TEXT to the ML session"
+  echo "    -e ML_EXPR   evaluate ML expression on startup"
+  echo "    -f ML_FILE   evaluate ML file on startup"
   echo "    -m MODE      add print mode for output"
   echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
   echo "    -q           non-interactive session"
@@ -47,6 +48,11 @@
   exit 2
 }
 
+function check_file()
+{
+  [ ! -f "$1" ] && fail "Bad file: \"$1\""
+}
+
 
 ## process command line
 
@@ -55,12 +61,12 @@
 OPTIONS_FILE=""
 PROCESS_SOCKET=""
 SECURE=""
-ML_TEXT=""
+declare -a LAST_ML_OPTIONS=()
 MODES=""
 declare -a SYSTEM_OPTIONS=()
 TERMINATE=""
 
-while getopts "O:P:Se:m:o:q" OPT
+while getopts "O:P:Se:f:m:o:q" OPT
 do
   case "$OPT" in
     O)
@@ -73,7 +79,12 @@
       SECURE=true
       ;;
     e)
-      ML_TEXT="$ML_TEXT $OPTARG"
+      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
+      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG"
+      ;;
+    f)
+      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--use"
+      LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG"
       ;;
     m)
       if [ -z "$MODES" ]; then
@@ -116,6 +127,8 @@
 
 ## heap file
 
+declare -a FIRST_ML_OPTIONS=()
+
 [ -z "$HEAP" ] && HEAP="$ISABELLE_LOGIC"
 
 case "$HEAP" in
@@ -146,6 +159,31 @@
     ;;
 esac
 
+if [ -z "$HEAP_FILE" ]; then
+  case "$ML_PLATFORM" in
+    *-windows)
+      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
+      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
+      ;;
+    *)
+      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
+      FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="fun exit rc = Posix.Process.exit (Word8.fromInt rc)"
+      ;;
+  esac
+else
+  check_file "$HEAP_FILE"
+  case "$ML_PLATFORM" in
+    *-windows)
+      PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")"
+      ;;
+    *)
+      PLATFORM_HEAP_FILE="$HEAP_FILE"
+      ;;
+  esac
+  PLATFORM_HEAP_FILE="$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$PLATFORM_HEAP_FILE")"
+  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
+  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.failure)"
+fi
 
 
 ## prepare tmp directory
@@ -157,16 +195,21 @@
 chmod $(umask -S) "$ISABELLE_TMP"
 
 
-## run it!
-
-ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
+## ML text
 
-[ -n "$MODES" ] && ML_TEXT="Unsynchronized.change print_mode (append [$MODES]); $ML_TEXT"
+if [ -n "$MODES" ]; then
+  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
+  FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Unsynchronized.change print_mode (append [$MODES])"
+fi
 
-[ -n "$SECURE" ] && ML_TEXT="$ML_TEXT; Secure.set_secure ();"
+if [ -n "$SECURE" ]; then
+  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
+  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Secure.set_secure ()"
+fi
 
 if [ -n "$PROCESS_SOCKET" ]; then
-  ML_TEXT="$ML_TEXT; Isabelle_Process.init \"$PROCESS_SOCKET\";"
+  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
+  LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Isabelle_Process.init \"$PROCESS_SOCKET\""
 else
   ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
   if [ -n "$OPTIONS_FILE" ]; then
@@ -179,18 +222,33 @@
       fail "Failed to retrieve Isabelle system options"
   fi
   if [ "$HEAP" != RAW_ML_SYSTEM -a "$HEAP" != RAW ]; then
-    ML_TEXT="Exn.capture_exit 2 Options.load_default (); $ML_TEXT"
+    FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
+    FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Exn.capture_exit 2 Options.load_default ()"
   fi
 fi
 
-export HEAP_FILE ML_TEXT TERMINATE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
+
+## ML process
+
+check_file "$ML_HOME/poly"
+librarypath "$ML_HOME"
+
+export ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
 
-if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
-  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
+if [ -n "$TERMINATE" ]; then
+  "$ML_HOME/poly" --error-exit -q -i $ML_OPTIONS \
+    "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}" </dev/null
+  RC="$?"
 else
-  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
+  "$ISABELLE_HOME/lib/scripts/feeder" -p | \
+    {
+      read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}"
+      RC="$?"
+      kill -TERM "$FPID"
+      exit "$RC"
+    }
+  RC="$?"
 fi
-RC="$?"
 
 [ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
 rmdir "$ISABELLE_TMP"
diff -r ff99681b3fd8 -r 922e702ae8ca lib/Tools/console
--- a/lib/Tools/console	Thu Mar 03 17:03:09 2016 +0100
+++ b/lib/Tools/console	Thu Mar 03 23:33:41 2016 +0100
@@ -31,6 +31,7 @@
   echo "    -m MODE      add print mode for output"
   echo "    -n           no build of session image on startup"
   echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
+  echo "    -r           logic session is RAW_ML_SYSTEM"
   echo "    -s           system build mode for session image"
   echo
   echo "  Run Isabelle process with raw ML console and line editor"
@@ -52,7 +53,7 @@
 declare -a SYSTEM_OPTIONS=()
 SYSTEM_MODE="false"
 
-while getopts "d:l:m:no:s" OPT
+while getopts "d:l:m:no:rs" OPT
 do
   case "$OPT" in
     d)
@@ -71,6 +72,9 @@
     o)
       SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
       ;;
+    r)
+      LOGIC="RAW_ML_SYSTEM"
+      ;;
     s)
       SYSTEM_MODE="true"
       ;;
@@ -97,14 +101,15 @@
 mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
 OPTIONS_FILE="$ISABELLE_TMP_PREFIX/options$$"
 
-"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Console \
-  "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" "$OPTIONS_FILE" \
-  "${INCLUDE_DIRS[@]}" $'\n' "${SYSTEM_OPTIONS[@]}" || {
-  rm -f "$OPTIONS_FILE"
-  exit "$?"
-}
-
-if [ "$LOGIC" != "RAW" ]; then
+if [ "$LOGIC" = "RAW_ML_SYSTEM" ]; then
+  "$ISABELLE_TOOL" options -x "$OPTIONS_FILE"
+else
+  "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Console \
+    "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" "$OPTIONS_FILE" \
+    "${INCLUDE_DIRS[@]}" $'\n' "${SYSTEM_OPTIONS[@]}" || {
+    rm -f "$OPTIONS_FILE"
+    exit "$?"
+  }
   ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
   ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="ASCII"
 fi
diff -r ff99681b3fd8 -r 922e702ae8ca lib/scripts/recode.pl
--- a/lib/scripts/recode.pl	Thu Mar 03 17:03:09 2016 +0100
+++ b/lib/scripts/recode.pl	Thu Mar 03 23:33:41 2016 +0100
@@ -7,6 +7,5 @@
 for (@ARGV) {
   utf8::upgrade($_);
   s/([\x80-\xff])/\\${\(ord($1))}/g;
-  print $_, " ";
+  print $_;
 }
-
diff -r ff99681b3fd8 -r 922e702ae8ca lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-#!/usr/bin/env bash
-# :mode=shellscript:
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.6.
-
-export -n HEAP_FILE ML_TEXT TERMINATE
-
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-function check_file()
-{
-  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## heap file
-
-if [ -z "$HEAP_FILE" ]; then
-  case "$ML_PLATFORM" in
-    *-windows)
-      INIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));"
-      ;;
-    *)
-      INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-      ;;
-  esac
-else
-  check_file "$HEAP_FILE"
-  case "$ML_PLATFORM" in
-    *-windows)
-      PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")"
-      ;;
-    *)
-      PLATFORM_HEAP_FILE="$HEAP_FILE"
-      ;;
-  esac
-  INIT="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.success);"
-fi
-
-
-## poly process
-
-ML_TEXT="$INIT $ML_TEXT"
-
-check_file "$ML_HOME/poly"
-librarypath "$ML_HOME"
-
-if [ -n "$TERMINATE" ]; then
-  "$ML_HOME/poly" -q -i $ML_OPTIONS \
-    --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$ML_TEXT")" \
-    --error-exit </dev/null
-  RC="$?"
-else
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" | \
-    { read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-  RC="$?"
-fi
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100:
diff -r ff99681b3fd8 -r 922e702ae8ca lib/scripts/run-polyml-5.3.0
--- a/lib/scripts/run-polyml-5.3.0	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.3.0.
-
-export -n HEAP_FILE ML_TEXT TERMINATE
-
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-function check_file()
-{
-  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## prepare databases
-
-if [ -z "$HEAP_FILE" ]; then
-  INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-else
-  check_file "$HEAP_FILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); Posix.Process.exit 0w1));"
-fi
-
-
-## poly process
-
-ML_TEXT="$INIT $ML_TEXT"
-
-check_file "$ML_HOME/poly"
-librarypath "$ML_HOME"
-
-if [ -z "$TERMINATE" ]; then
-  FEEDER_OPTS=""
-else
-  FEEDER_OPTS="-q"
-fi
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" $FEEDER_OPTS | \
-  { read FPID; "$ML_HOME/poly" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-RC="$?"
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100:
diff -r ff99681b3fd8 -r 922e702ae8ca src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Doc/Implementation/ML.thy	Thu Mar 03 23:33:41 2016 +0100
@@ -1154,7 +1154,7 @@
   @{index_ML_exception ERROR: string} \\
   @{index_ML_exception Fail: string} \\
   @{index_ML Exn.is_interrupt: "exn -> bool"} \\
-  @{index_ML reraise: "exn -> 'a"} \\
+  @{index_ML Exn.reraise: "exn -> 'a"} \\
   @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
   \end{mldecls}
 
@@ -1176,7 +1176,7 @@
   concrete exception constructors in user code. Handled interrupts need to be
   re-raised promptly!
 
-  \<^descr> @{ML reraise}~\<open>exn\<close> raises exception \<open>exn\<close> while preserving its implicit
+  \<^descr> @{ML Exn.reraise}~\<open>exn\<close> raises exception \<open>exn\<close> while preserving its implicit
   position information (if possible, depending on the ML platform).
 
   \<^descr> @{ML Runtime.exn_trace}~@{ML_text "(fn () =>"}~\<open>e\<close>@{ML_text ")"} evaluates
diff -r ff99681b3fd8 -r 922e702ae8ca src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Doc/System/Basics.thy	Thu Mar 03 23:33:41 2016 +0100
@@ -300,7 +300,8 @@
     -O           system options from given YXML file
     -P SOCKET    startup process wrapper via TCP socket
     -S           secure mode -- disallow critical operations
-    -e ML_TEXT   pass ML_TEXT to the ML session
+    -e ML_EXPR   evaluate ML expression on startup
+    -f ML_FILE   evaluate ML file on startup
     -m MODE      add print mode for output
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -q           non-interactive session
@@ -323,10 +324,10 @@
 subsubsection \<open>Options\<close>
 
 text \<open>
-  Using the \<^verbatim>\<open>-e\<close> option, arbitrary ML code may be passed to the Isabelle
-  session from the command line. Multiple \<^verbatim>\<open>-e\<close> options are evaluated in the
-  given order. Strange things may happen when erroneous ML code is provided.
-  Also make sure that the ML commands are terminated properly by semicolon.
+  Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is
+  started. The source is either given literally or taken from a file. Multiple
+  \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to
+  premature exit of the ML process with return code 1.
 
   \<^medskip>
   The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
@@ -368,7 +369,7 @@
   The next example demonstrates batch execution of Isabelle. We retrieve the
   \<^verbatim>\<open>Main\<close> theory value from the theory loader within ML (observe the delicate
   quoting rules for the Bash shell vs.\ ML):
-  @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main";' -q HOL\<close>}
+  @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' -q HOL\<close>}
 
   Note that the output text will be interspersed with additional junk messages
   by the ML runtime environment.
diff -r ff99681b3fd8 -r 922e702ae8ca src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Doc/System/Misc.thy	Thu Mar 03 23:33:41 2016 +0100
@@ -65,10 +65,11 @@
 
   Options are:
     -d DIR       include session directory
-    -l NAME      logic session name (default ISABELLE_LOGIC)
+    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
     -m MODE      add print mode for output
     -n           no build of session image on startup
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -r           logic session is RAW_ML_SYSTEM
     -s           system build mode for session image
 
   Run Isabelle process with raw ML console and line editor
@@ -77,6 +78,9 @@
   The \<^verbatim>\<open>-l\<close> option specifies the logic session name. By default, its heap
   image is checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
 
+  Option \<^verbatim>\<open>-r\<close> abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
+  Isabelle/Pure interactively.
+
   Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close> are passed directly to @{tool build}
   (\secref{sec:tool-build}).
 
diff -r ff99681b3fd8 -r 922e702ae8ca src/HOL/Matrix_LP/Cplex_tools.ML
--- a/src/HOL/Matrix_LP/Cplex_tools.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -1158,7 +1158,7 @@
         result
     end
     handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
-         | exn => if Exn.is_interrupt exn then reraise exn else raise (Execute answer)
+         | exn => if Exn.is_interrupt exn then Exn.reraise exn else raise (Execute answer)
     end
 
 fun solve_cplex prog =
diff -r ff99681b3fd8 -r 922e702ae8ca src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -71,11 +71,11 @@
 
 fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
   handle exn =>
-    if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; ())
+    if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; ())
 
 fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
   handle exn =>
-    if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; d)
+    if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; d)
 
 fun register (init, run, done) thy =
   let val id = length (Actions.get thy) + 1
diff -r ff99681b3fd8 -r 922e702ae8ca src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Mar 03 23:33:41 2016 +0100
@@ -159,7 +159,7 @@
 
 my $cmd =
   "\"$ENV{'ISABELLE_PROCESS'}\" " .
-  "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;' -q $mirabelle_logic" .
+  "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\"' -q $mirabelle_logic" .
   $quiet;
 my $result = system "bash", "-c", $cmd;
 
diff -r ff99681b3fd8 -r 922e702ae8ca src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/HOL/Nat.thy	Thu Mar 03 23:33:41 2016 +0100
@@ -1876,7 +1876,6 @@
   moreover from \<open>n < j\<close> have "Suc n \<le> j"
     by (simp add: Suc_le_eq)
   ultimately have "P (Suc n)"
-  thm Suc.hyps TrueI Suc.prems
   proof (rule Suc.hyps)
     fix q
     assume "Suc n \<le> q"
diff -r ff99681b3fd8 -r 922e702ae8ca src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Mar 03 23:33:41 2016 +0100
@@ -171,7 +171,7 @@
   end
   handle TimeLimit.TimeOut => "TIMEOUT"
        | NOT_SUPPORTED _ => "UNSUP"
-       | exn => if Exn.is_interrupt exn then reraise exn else "UNKNOWN"
+       | exn => if Exn.is_interrupt exn then Exn.reraise exn else "UNKNOWN"
 
 fun check_theory thy =
   let
diff -r ff99681b3fd8 -r 922e702ae8ca src/HOL/TPTP/TPTP_Interpret_Test.thy
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu Mar 03 23:33:41 2016 +0100
@@ -129,7 +129,7 @@
       val t1 = (parse_timed file |> fst)
       val t2 = (interpret_timed timeout file thy |> fst)
         handle exn => (*FIXME*)
-          if Exn.is_interrupt exn then reraise exn
+          if Exn.is_interrupt exn then Exn.reraise exn
           else
             (warning (" test: file " ^ Path.print file ^
              " raised exception: " ^ Runtime.exn_message exn);
diff -r ff99681b3fd8 -r 922e702ae8ca src/HOL/TPTP/TPTP_Test.thy
--- a/src/HOL/TPTP/TPTP_Test.thy	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Test.thy	Thu Mar 03 23:33:41 2016 +0100
@@ -60,7 +60,7 @@
      (*otherwise report exceptions as warnings*)
      handle exn =>
        if Exn.is_interrupt exn then
-         reraise exn
+         Exn.reraise exn
        else
          (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
           " raised exception: " ^ Runtime.exn_message exn);
diff -r ff99681b3fd8 -r 922e702ae8ca src/HOL/Tools/Old_Datatype/old_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -778,7 +778,7 @@
       Old_Datatype_Aux.check_nonempty descr
         handle (exn as Old_Datatype_Aux.Datatype_Empty s) =>
           if #strict config then error ("Nonemptiness check failed for datatype " ^ quote s)
-          else reraise exn;
+          else Exn.reraise exn;
 
     val _ =
       Old_Datatype_Aux.message config
diff -r ff99681b3fd8 -r 922e702ae8ca src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -192,7 +192,7 @@
              handle
                ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
              | exn =>
-               if Exn.is_interrupt exn then reraise exn
+               if Exn.is_interrupt exn then Exn.reraise exn
                else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
 
         val _ =
diff -r ff99681b3fd8 -r 922e702ae8ca src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -573,7 +573,7 @@
     (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def)
   | exn =>
     if Exn.is_interrupt exn then
-      reraise exn
+      Exn.reraise exn
     else
       (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn);
        def)
diff -r ff99681b3fd8 -r 922e702ae8ca src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -123,7 +123,7 @@
           SMT_Solver.smt_filter ctxt goal facts i slice_timeout
           handle exn =>
             if Exn.is_interrupt exn orelse debug then
-              reraise exn
+              Exn.reraise exn
             else
               {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)),
                fact_ids = NONE, atp_proof = K []}
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Concurrent/bash.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -54,7 +54,7 @@
                   Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
           in Synchronized.change result (K res) end
           handle exn =>
-            (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
+            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
 
     fun read_pid 0 = NONE
       | read_pid count =
@@ -95,7 +95,7 @@
       val pid = read_pid 1;
       val _ = cleanup ();
     in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
-    handle exn => (terminate (read_pid 10); cleanup (); reraise exn)
+    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
   end);
 
 end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Concurrent/bash_windows.ML
--- a/src/Pure/Concurrent/bash_windows.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Concurrent/bash_windows.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -48,7 +48,7 @@
             val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
           in Synchronized.change result (K res) end
           handle exn =>
-            (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
+            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
 
     fun read_pid 0 = NONE
       | read_pid count =
@@ -93,7 +93,7 @@
       val pid = read_pid 1;
       val _ = cleanup ();
     in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
-    handle exn => (terminate (read_pid 10); cleanup (); reraise exn)
+    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
   end);
 
 end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Concurrent/future.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -348,7 +348,7 @@
      (Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt");
       List.app cancel_later (cancel_all ());
       signal work_available; true)
-    else reraise exn;
+    else Exn.reraise exn;
 
 fun scheduler_loop () =
  (while
@@ -409,8 +409,8 @@
     val _ = Single_Assignment.assign result res
       handle exn as Fail _ =>
         (case Single_Assignment.peek result of
-          SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
-        | _ => reraise exn);
+          SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt e then e else exn)
+        | _ => Exn.reraise exn);
     val ok =
       (case the (Single_Assignment.peek result) of
         Exn.Exn exn =>
@@ -600,7 +600,7 @@
         | exn =>
             if Exn.is_interrupt exn
             then raise Fail "Concurrent attempt to fulfill promise"
-            else reraise exn;
+            else Exn.reraise exn;
     fun job () =
       Multithreading.with_attributes Multithreading.no_interrupts
         (fn _ => Exn.release (Exn.capture assign () before abort ()));
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Concurrent/multithreading.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/multithreading.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,196 @@
+(*  Title:      Pure/Concurrent/multithreading.ML
+    Author:     Makarius
+
+Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
+*)
+
+signature BASIC_MULTITHREADING =
+sig
+  val interruptible: ('a -> 'b) -> 'a -> 'b
+  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
+end;
+
+signature MULTITHREADING =
+sig
+  include BASIC_MULTITHREADING
+  val no_interrupts: Thread.threadAttribute list
+  val public_interrupts: Thread.threadAttribute list
+  val private_interrupts: Thread.threadAttribute list
+  val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
+  val interrupted: unit -> unit  (*exception Interrupt*)
+  val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
+  val max_threads_value: unit -> int
+  val max_threads_update: int -> unit
+  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
+  val enabled: unit -> bool
+  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
+    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
+  val trace: int ref
+  val tracing: int -> (unit -> string) -> unit
+  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
+  val real_time: ('a -> unit) -> 'a -> Time.time
+  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
+  val serial: unit -> int
+end;
+
+structure Multithreading: MULTITHREADING =
+struct
+
+(* thread attributes *)
+
+val no_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
+
+val test_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
+
+val public_interrupts =
+  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
+
+val private_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
+
+val sync_interrupts = map
+  (fn x as Thread.InterruptState Thread.InterruptDefer => x
+    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
+    | x => x);
+
+val safe_interrupts = map
+  (fn Thread.InterruptState Thread.InterruptAsynch =>
+      Thread.InterruptState Thread.InterruptAsynchOnce
+    | x => x);
+
+fun interrupted () =
+  let
+    val orig_atts = safe_interrupts (Thread.getAttributes ());
+    val _ = Thread.setAttributes test_interrupts;
+    val test = Exn.capture Thread.testInterrupt ();
+    val _ = Thread.setAttributes orig_atts;
+  in Exn.release test end;
+
+fun with_attributes new_atts e =
+  let
+    val orig_atts = safe_interrupts (Thread.getAttributes ());
+    val result = Exn.capture (fn () =>
+      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
+    val _ = Thread.setAttributes orig_atts;
+  in Exn.release result end;
+
+
+(* portable wrappers *)
+
+fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
+
+fun uninterruptible f x =
+  with_attributes no_interrupts (fn atts =>
+    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
+
+
+(* options *)
+
+fun num_processors () =
+  (case Thread.numPhysicalProcessors () of
+    SOME n => n
+  | NONE => Thread.numProcessors ());
+
+fun max_threads_result m =
+  if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8);
+
+val max_threads = ref 1;
+
+fun max_threads_value () = ! max_threads;
+
+fun max_threads_update m = max_threads := max_threads_result m;
+
+fun max_threads_setmp m f x =
+  uninterruptible (fn restore_attributes => fn () =>
+    let
+      val max_threads_orig = ! max_threads;
+      val _ = max_threads_update m;
+      val result = Exn.capture (restore_attributes f) x;
+      val _ = max_threads := max_threads_orig;
+    in Exn.release result end) ();
+
+fun enabled () = max_threads_value () > 1;
+
+
+(* synchronous wait *)
+
+fun sync_wait opt_atts time cond lock =
+  with_attributes
+    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
+    (fn _ =>
+      (case time of
+        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
+      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
+      handle exn => Exn.Exn exn);
+
+
+(* tracing *)
+
+val trace = ref 0;
+
+fun tracing level msg =
+  if level > ! trace then ()
+  else uninterruptible (fn _ => fn () =>
+    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
+      handle _ (*sic*) => ()) ();
+
+fun tracing_time detailed time =
+  tracing
+   (if not detailed then 5
+    else if Time.>= (time, seconds 1.0) then 1
+    else if Time.>= (time, seconds 0.1) then 2
+    else if Time.>= (time, seconds 0.01) then 3
+    else if Time.>= (time, seconds 0.001) then 4 else 5);
+
+fun real_time f x =
+  let
+    val timer = Timer.startRealTimer ();
+    val () = f x;
+    val time = Timer.checkRealTimer timer;
+  in time end;
+
+
+(* synchronized evaluation *)
+
+fun synchronized name lock e =
+  Exn.release (uninterruptible (fn restore_attributes => fn () =>
+    let
+      val immediate =
+        if Mutex.trylock lock then true
+        else
+          let
+            val _ = tracing 5 (fn () => name ^ ": locking ...");
+            val time = real_time Mutex.lock lock;
+            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
+          in false end;
+      val result = Exn.capture (restore_attributes e) ();
+      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
+      val _ = Mutex.unlock lock;
+    in result end) ());
+
+
+(* serial numbers *)
+
+local
+
+val serial_lock = Mutex.mutex ();
+val serial_count = ref 0;
+
+in
+
+val serial = uninterruptible (fn _ => fn () =>
+  let
+    val _ = Mutex.lock serial_lock;
+    val _ = serial_count := ! serial_count + 1;
+    val res = ! serial_count;
+    val _ = Mutex.unlock serial_lock;
+  in res end);
+
+end;
+
+end;
+
+structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
+open Basic_Multithreading;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Concurrent/par_exn.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -73,7 +73,7 @@
 fun release_first results =
   (case get_first plain_exn results of
     NONE => release_all results
-  | SOME exn => reraise exn);
+  | SOME exn => Exn.reraise exn);
 
 end;
 
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -46,7 +46,7 @@
         val results =
           restore_attributes Future.join_results futures
             handle exn =>
-              (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
+              (if Exn.is_interrupt exn then Future.cancel_group group else (); Exn.reraise exn);
       in results end) ();
 
 fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Concurrent/single_assignment.ML
--- a/src/Pure/Concurrent/single_assignment.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Concurrent/single_assignment.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -39,7 +39,7 @@
           NONE =>
             (case Multithreading.sync_wait NONE NONE cond lock of
               Exn.Res _ => wait ()
-            | Exn.Exn exn => reraise exn)
+            | Exn.Exn exn => Exn.reraise exn)
         | SOME x => x);
     in wait () end);
 
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Concurrent/standard_thread.ML
--- a/src/Pure/Concurrent/standard_thread.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Concurrent/standard_thread.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -49,14 +49,14 @@
 type params = {name: string, stack_limit: int option, interrupts: bool};
 
 fun attributes ({stack_limit, interrupts, ...}: params) =
-  ML_Stack.limit stack_limit @
+  Thread.MaximumMLStack stack_limit ::
   (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
 
 fun fork (params: params) body =
   Thread.fork (fn () =>
-    print_exception_trace General.exnMessage tracing (fn () =>
+    Exn.trace General.exnMessage tracing (fn () =>
       (set_name (#name params); body ())
-        handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
+        handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn),
     attributes params);
 
 
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Concurrent/synchronized.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -49,7 +49,7 @@
               (case Multithreading.sync_wait NONE (time_limit x) cond lock of
                 Exn.Res true => try_change ()
               | Exn.Res false => NONE
-              | Exn.Exn exn => reraise exn)
+              | Exn.Exn exn => Exn.reraise exn)
           | SOME (y, x') =>
               uninterruptible (fn _ => fn () =>
                 (var := x'; ConditionVar.broadcast cond; SOME y)) ())
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Concurrent/unsynchronized.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/unsynchronized.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,30 @@
+(*  Title:      Pure/Concurrent/unsynchronized.ML
+    Author:     Makarius
+
+Raw ML references as unsynchronized state variables.
+*)
+
+structure Unsynchronized =
+struct
+
+datatype ref = datatype ref;
+
+val op := = op :=;
+val ! = !;
+
+fun change r f = r := f (! r);
+fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
+
+fun inc i = (i := ! i + (1: int); ! i);
+fun dec i = (i := ! i - (1: int); ! i);
+
+fun setmp flag value f x =
+  uninterruptible (fn restore_attributes => fn () =>
+    let
+      val orig_value = ! flag;
+      val _ = flag := value;
+      val result = Exn.capture (restore_attributes f) x;
+      val _ = flag := orig_value;
+    in Exn.release result end) ();
+
+end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/General/basics.ML
--- a/src/Pure/General/basics.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/General/basics.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -102,7 +102,7 @@
 (* partiality *)
 
 fun try f x = SOME (f x)
-  handle exn => if Exn.is_interrupt exn then reraise exn else NONE;
+  handle exn => if Exn.is_interrupt exn then Exn.reraise exn else NONE;
 
 fun can f x = is_some (try f x);
 
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/General/exn.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/exn.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,134 @@
+(*  Title:      Pure/General/exn.ML
+    Author:     Makarius
+
+Support for exceptions.
+*)
+
+signature BASIC_EXN =
+sig
+  exception ERROR of string
+  val error: string -> 'a
+  val cat_error: string -> string -> 'a
+end;
+
+signature EXN =
+sig
+  include BASIC_EXN
+  val reraise: exn -> 'a
+  datatype 'a result = Res of 'a | Exn of exn
+  val get_res: 'a result -> 'a option
+  val get_exn: 'a result -> exn option
+  val capture: ('a -> 'b) -> 'a -> 'b result
+  val release: 'a result -> 'a
+  val map_res: ('a -> 'b) -> 'a result -> 'b result
+  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
+  val map_exn: (exn -> exn) -> 'a result -> 'a result
+  exception Interrupt
+  val interrupt: unit -> 'a
+  val is_interrupt: exn -> bool
+  val interrupt_exn: 'a result
+  val is_interrupt_exn: 'a result -> bool
+  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
+  val return_code: exn -> int -> int
+  val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
+  exception EXCEPTIONS of exn list
+  val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
+end;
+
+structure Exn: EXN =
+struct
+
+(* reraise *)
+
+fun reraise exn =
+  (case PolyML.exceptionLocation exn of
+    NONE => raise exn
+  | SOME location => PolyML.raiseWithLocation (exn, location));
+
+
+(* user errors *)
+
+exception ERROR of string;
+
+fun error msg = raise ERROR msg;
+
+fun cat_error "" msg = error msg
+  | cat_error msg "" = error msg
+  | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
+
+
+(* exceptions as values *)
+
+datatype 'a result =
+  Res of 'a |
+  Exn of exn;
+
+fun get_res (Res x) = SOME x
+  | get_res _ = NONE;
+
+fun get_exn (Exn exn) = SOME exn
+  | get_exn _ = NONE;
+
+fun capture f x = Res (f x) handle e => Exn e;
+
+fun release (Res y) = y
+  | release (Exn e) = reraise e;
+
+fun map_res f (Res x) = Res (f x)
+  | map_res f (Exn e) = Exn e;
+
+fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
+
+fun map_exn f (Res x) = Res x
+  | map_exn f (Exn e) = Exn (f e);
+
+
+(* interrupts *)
+
+exception Interrupt = SML90.Interrupt;
+
+fun interrupt () = raise Interrupt;
+
+fun is_interrupt Interrupt = true
+  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
+  | is_interrupt _ = false;
+
+val interrupt_exn = Exn Interrupt;
+
+fun is_interrupt_exn (Exn exn) = is_interrupt exn
+  | is_interrupt_exn _ = false;
+
+fun interruptible_capture f x =
+  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
+
+
+(* POSIX return code *)
+
+fun return_code exn rc =
+  if is_interrupt exn then (130: int) else rc;
+
+fun capture_exit rc f x =
+  f x handle exn => exit (return_code exn rc);
+
+
+(* concatenated exceptions *)
+
+exception EXCEPTIONS of exn list;
+
+
+(* low-level trace *)
+
+fun trace exn_message output e =
+  PolyML.Exception.traceException
+    (e, fn (trace, exn) =>
+      let
+        val title = "Exception trace - " ^ exn_message exn;
+        val () = output (String.concatWith "\n" (title :: trace));
+      in reraise exn end);
+
+end;
+
+datatype illegal = Interrupt;
+
+structure Basic_Exn: BASIC_EXN = Exn;
+open Basic_Exn;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/General/exn.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/exn.scala	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,137 @@
+/*  Title:      Pure/General/exn.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Support for exceptions (arbitrary throwables).
+*/
+
+package isabelle
+
+
+object Exn
+{
+  /* user errors */
+
+  class User_Error(message: String) extends RuntimeException(message)
+  {
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: User_Error => message == other.getMessage
+        case _ => false
+      }
+    override def hashCode: Int = message.hashCode
+
+    override def toString: String = "ERROR(" + message + ")"
+  }
+
+  object ERROR
+  {
+    def apply(message: String): User_Error = new User_Error(message)
+    def unapply(exn: Throwable): Option[String] = user_message(exn)
+  }
+
+  def error(message: String): Nothing = throw ERROR(message)
+
+  def cat_message(msg1: String, msg2: String): String =
+    if (msg1 == "") msg2
+    else if (msg2 == "") msg1
+    else msg1 + "\n" + msg2
+
+  def cat_error(msg1: String, msg2: String): Nothing =
+    error(cat_message(msg1, msg2))
+
+
+  /* exceptions as values */
+
+  sealed abstract class Result[A]
+  {
+    def user_error: Result[A] =
+      this match {
+        case Exn(ERROR(msg)) => Exn(ERROR(msg))
+        case _ => this
+      }
+  }
+  case class Res[A](res: A) extends Result[A]
+  case class Exn[A](exn: Throwable) extends Result[A]
+
+  def capture[A](e: => A): Result[A] =
+    try { Res(e) }
+    catch { case exn: Throwable => Exn[A](exn) }
+
+  def release[A](result: Result[A]): A =
+    result match {
+      case Res(x) => x
+      case Exn(exn) => throw exn
+    }
+
+  def release_first[A](results: List[Result[A]]): List[A] =
+    results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
+      case Some(Exn(exn)) => throw exn
+      case _ => results.map(release(_))
+    }
+
+
+  /* interrupts */
+
+  def is_interrupt(exn: Throwable): Boolean =
+  {
+    var found_interrupt = false
+    var e = exn
+    while (!found_interrupt && e != null) {
+      found_interrupt |= e.isInstanceOf[InterruptedException]
+      e = e.getCause
+    }
+    found_interrupt
+  }
+
+  object Interrupt
+  {
+    def apply(): Throwable = new InterruptedException
+    def unapply(exn: Throwable): Boolean = is_interrupt(exn)
+
+    def expose() { if (Thread.interrupted) throw apply() }
+    def impose() { Thread.currentThread.interrupt }
+
+    def postpone[A](body: => A): Option[A] =
+    {
+      val interrupted = Thread.interrupted
+      val result = capture { body }
+      if (interrupted) impose()
+      result match {
+        case Res(x) => Some(x)
+        case Exn(e) =>
+          if (is_interrupt(e)) { impose(); None }
+          else throw e
+      }
+    }
+
+    val return_code = 130
+  }
+
+
+  /* POSIX return code */
+
+  def return_code(exn: Throwable, rc: Int): Int =
+    if (is_interrupt(exn)) Interrupt.return_code else rc
+
+
+  /* message */
+
+  def user_message(exn: Throwable): Option[String] =
+    if (exn.getClass == classOf[RuntimeException] ||
+        exn.getClass == classOf[User_Error])
+    {
+      val msg = exn.getMessage
+      Some(if (msg == null || msg == "") "Error" else msg)
+    }
+    else if (exn.isInstanceOf[java.io.IOException])
+    {
+      val msg = exn.getMessage
+      Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
+    }
+    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
+    else None
+
+  def message(exn: Throwable): String =
+    user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
+}
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/General/linear_set.ML
--- a/src/Pure/General/linear_set.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/General/linear_set.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -137,9 +137,11 @@
 
 val _ =
   PolyML.addPrettyPrinter (fn depth => fn pretty => fn set =>
-    ml_pretty
+    ML_Pretty.to_polyml
       (ML_Pretty.enum "," "{" "}"
-        (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty))
+        (ML_Pretty.pair
+          (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
+          (ML_Pretty.from_polyml o pretty))
         (dest set, depth)));
 
 end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/General/secure.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/secure.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,27 @@
+(*  Title:      Pure/General/secure.ML
+    Author:     Makarius
+
+Secure critical operations.
+*)
+
+signature SECURE =
+sig
+  val set_secure: unit -> unit
+  val is_secure: unit -> bool
+  val deny: string -> unit
+  val deny_ml: unit -> unit
+end;
+
+structure Secure: SECURE =
+struct
+
+val secure = Unsynchronized.ref false;
+
+fun set_secure () = secure := true;
+fun is_secure () = ! secure;
+
+fun deny msg = if is_secure () then error msg else ();
+
+fun deny_ml () = deny "Cannot evaluate ML source in secure mode";
+
+end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/General/table.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -412,9 +412,11 @@
 
 val _ =
   PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
-    ml_pretty
+    ML_Pretty.to_polyml
       (ML_Pretty.enum "," "{" "}"
-        (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty))
+        (ML_Pretty.pair
+          (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
+          (ML_Pretty.from_polyml o pretty))
         (dest tab, depth)));
 
 
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Isar/runtime.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -141,8 +141,8 @@
 
 val exn_error_message = Output.error_message o exn_message;
 val exn_system_message = Output.system_message o exn_message;
-fun exn_trace e = print_exception_trace exn_message tracing e;
-fun exn_trace_system e = print_exception_trace exn_message Output.system_message e;
+fun exn_trace e = Exn.trace exn_message tracing e;
+fun exn_trace_system e = Exn.trace exn_message Output.system_message e;
 
 
 (* exception debugger *)
@@ -189,7 +189,7 @@
 
 fun toplevel_error output_exn f x = f x
   handle exn =>
-    if Exn.is_interrupt exn then reraise exn
+    if Exn.is_interrupt exn then Exn.reraise exn
     else
       let
         val opt_ctxt =
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -594,7 +594,7 @@
   (case transition int tr st of
     (st', NONE) => st'
   | (_, SOME (exn, info)) =>
-      if Exn.is_interrupt exn then reraise exn
+      if Exn.is_interrupt exn then Exn.reraise exn
       else raise Runtime.EXCURSION_FAIL (exn, info));
 
 val command = command_exception false;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ML/exn_output.ML
--- a/src/Pure/ML/exn_output.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/ML/exn_output.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -20,7 +20,7 @@
 
 fun pretty (exn: exn) =
   Pretty.from_ML
-    (pretty_ml
+    (ML_Pretty.from_polyml
       (PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
 
 end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ML/fixed_int_dummy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/fixed_int_dummy.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,6 @@
+(*  Title:      Pure/ML/fixed_int_dummy.ML
+
+FixedInt dummy that is not fixed (up to Poly/ML 5.6).
+*)
+
+structure FixedInt = IntInf;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ML/install_pp_polyml.ML
--- a/src/Pure/ML/install_pp_polyml.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/ML/install_pp_polyml.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -5,64 +5,64 @@
 *)
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T =>
-  ml_pretty (Pretty.to_ML (Pretty.str "<pretty>")));
+  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<pretty>")));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
-  ml_pretty (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
-  ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
+  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
-  ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
+  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
-  ml_pretty (Pretty.to_ML (Pretty.position pos)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.position pos)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
-  ml_pretty (Pretty.to_ML (Binding.pp binding)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Binding.pp binding)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn th =>
-  ml_pretty (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn ct =>
-  ml_pretty (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn cT =>
-  ml_pretty (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn T =>
-  ml_pretty (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
-  ml_pretty (Pretty.to_ML (Context.pretty_thy thy)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Context.pretty_thy thy)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
-  ml_pretty (Pretty.to_ML (Proof_Display.pp_context ctxt)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_context ctxt)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
-  ml_pretty (Pretty.to_ML (Ast.pretty_ast ast)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Ast.pretty_ast ast)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
-  ml_pretty (Pretty.to_ML (Path.pretty path)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Path.pretty path)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
-  ml_pretty (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
+  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
-  ml_pretty (Pretty.to_ML (Pretty.str "<Proof.state>")));
+  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<Proof.state>")));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
-  ml_pretty (Pretty.to_ML (Toplevel.pretty_abstract st)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Toplevel.pretty_abstract st)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
-  ml_pretty (Pretty.to_ML (Morphism.pretty morphism)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Morphism.pretty morphism)));
 
 PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
-  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
+  ML_Pretty.to_polyml (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
 
 PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
-  ml_pretty (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
+  ML_Pretty.to_polyml (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
 
 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
   pretty (Synchronized.value var, depth));
@@ -83,7 +83,7 @@
 local
 
 open PolyML;
-val from_ML = Pretty.from_ML o pretty_ml;
+val from_ML = Pretty.from_ML o ML_Pretty.from_polyml;
 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
 fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
 
@@ -110,7 +110,7 @@
 
 val _ =
   PolyML.addPrettyPrinter (fn depth => fn _ => fn t =>
-    ml_pretty (Pretty.to_ML (prt_term false depth t)));
+    ML_Pretty.to_polyml (Pretty.to_ML (prt_term false depth t)));
 
 local
 
@@ -157,7 +157,7 @@
 
 val _ =
   PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
-    ml_pretty (Pretty.to_ML (prt_proof false depth prf)));
+    ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf)));
 
 end;
 
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -65,7 +65,7 @@
           let
             val xml =
               ML_Name_Space.displayTypeExpression (types, depth, space)
-              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+              |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of
               |> Output.output |> YXML.parse_body;
           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
       end;
@@ -98,10 +98,8 @@
       | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
       | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
       | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
-      | reported loc pt =
-          (case ML_Parse_Tree.completions pt of
-            SOME names => reported_completions loc names
-          | NONE => I)
+      | reported loc (PolyML.PTcompletions names) = reported_completions loc names
+      | reported _ _ = I
     and reported_tree (loc, props) = fold (reported loc) props;
 
     val persistent_reports = reported_tree parse_tree [];
@@ -123,16 +121,14 @@
 
     fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ())
       | breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ())
-      | breakpoints loc pt =
-          (case ML_Parse_Tree.breakpoint pt of
-            SOME b =>
-              let val pos = breakpoint_position loc in
-                if is_reported pos then
-                  let val id = serial ();
-                  in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
-                else I
-              end
-          | NONE => I)
+      | breakpoints loc (PolyML.PTbreakPoint b) =
+          let val pos = breakpoint_position loc in
+            if is_reported pos then
+              let val id = serial ();
+              in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
+            else I
+          end
+      | breakpoints _ _ = I
     and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
 
     val all_breakpoints = rev (breakpoints_tree parse_tree []);
@@ -197,7 +193,7 @@
         val pos = Exn_Properties.position_of loc;
         val txt =
           (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
-          Pretty.string_of (Pretty.from_ML (pretty_ml msg));
+          Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml msg));
       in if hard then err txt else warn txt end;
 
 
@@ -209,7 +205,8 @@
       let
         fun display disp x =
           if depth > 0 then
-            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
+            (write (disp x |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of);
+              write "\n")
           else ();
 
         fun apply_fix (a, b) =
@@ -264,14 +261,14 @@
       PolyML.Compiler.CPFileName location_props,
       PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
-      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
-     ML_Compiler_Parameters.debug debug;
+      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
+      PolyML.Compiler.CPDebug debug];
 
     val _ =
       (while not (List.null (! input_buffer)) do
         PolyML.compiler (get, parameters) ())
       handle exn =>
-        if Exn.is_interrupt exn then reraise exn
+        if Exn.is_interrupt exn then Exn.reraise exn
         else
           let
             val exn_msg =
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ML/ml_compiler0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_compiler0.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,110 @@
+(*  Title:      Pure/ML/ml_compiler0.ML
+
+Runtime compilation and evaluation (bootstrap version of
+Pure/ML/ml_compiler.ML).
+*)
+
+signature ML_COMPILER0 =
+sig
+  type context =
+   {name_space: ML_Name_Space.T,
+    here: int -> string -> string,
+    print: string -> unit,
+    error: string -> unit}
+  val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
+  val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
+  val debug_option: bool option -> bool
+  val use_operations: (bool option -> string -> unit) ->
+    {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit}
+end;
+
+structure ML_Compiler0: ML_COMPILER0 =
+struct
+
+type context =
+ {name_space: ML_Name_Space.T,
+  here: int -> string -> string,
+  print: string -> unit,
+  error: string -> unit};
+
+fun drop_newline s =
+  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
+  else s;
+
+fun ml_positions start_line name txt =
+  let
+    fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
+          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
+          in positions line cs (s :: res) end
+      | positions line (c :: cs) res =
+          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
+      | positions _ [] res = rev res;
+  in String.concat (positions start_line (String.explode txt) []) end;
+
+fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
+  let
+    val _ = Secure.deny_ml ();
+
+    val current_line = Unsynchronized.ref line;
+    val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
+    val out_buffer = Unsynchronized.ref ([]: string list);
+    fun output () = drop_newline (implode (rev (! out_buffer)));
+
+    fun get () =
+      (case ! in_buffer of
+        [] => NONE
+      | c :: cs =>
+          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
+    fun put s = out_buffer := s :: ! out_buffer;
+    fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
+     (put (if hard then "Error: " else "Warning: ");
+      PolyML.prettyPrint (put, 76) msg1;
+      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
+      put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
+
+    val parameters =
+     [PolyML.Compiler.CPOutStream put,
+      PolyML.Compiler.CPNameSpace name_space,
+      PolyML.Compiler.CPErrorMessageProc put_message,
+      PolyML.Compiler.CPLineNo (fn () => ! current_line),
+      PolyML.Compiler.CPFileName file,
+      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
+      PolyML.Compiler.CPDebug debug];
+    val _ =
+      (while not (List.null (! in_buffer)) do
+        PolyML.compiler (get, parameters) ())
+      handle exn =>
+        if Exn.is_interrupt exn then Exn.reraise exn
+        else
+         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+          error (output ()); Exn.reraise exn);
+  in if verbose then print (output ()) else () end;
+
+fun use_file context {verbose, debug} file =
+  let
+    val instream = TextIO.openIn file;
+    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
+  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
+
+
+fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
+  | debug_option (SOME debug) = debug;
+
+fun use_operations (use_ : bool option -> string -> unit) =
+  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
+
+end;
+
+val {use, use_debug, use_no_debug} =
+  let
+    val context: ML_Compiler0.context =
+     {name_space = ML_Name_Space.global,
+      here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
+      print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
+      error = fn s => error s};
+  in
+    ML_Compiler0.use_operations (fn opt_debug => fn file =>
+      ML_Compiler0.use_file context
+        {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
+      handle ERROR msg => (#print context msg; raise error "ML error"))
+  end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ML/ml_debugger.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_debugger.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,72 @@
+(*  Title:      Pure/ML/ml_debugger.ML
+    Author:     Makarius
+
+ML debugger interface -- for Poly/ML 5.6, or later.
+*)
+
+signature ML_DEBUGGER =
+sig
+  type exn_id
+  val exn_id: exn -> exn_id
+  val print_exn_id: exn_id -> string
+  val eq_exn_id: exn_id * exn_id -> bool
+  type location
+  val on_entry: (string * location -> unit) option -> unit
+  val on_exit: (string * location -> unit) option -> unit
+  val on_exit_exception: (string * location -> exn -> unit) option -> unit
+  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
+  type state
+  val state: Thread.thread -> state list
+  val debug_function: state -> string
+  val debug_function_arg: state -> ML_Name_Space.valueVal
+  val debug_function_result: state -> ML_Name_Space.valueVal
+  val debug_location: state -> location
+  val debug_name_space: state -> ML_Name_Space.T
+  val debug_local_name_space: state -> ML_Name_Space.T
+end;
+
+structure ML_Debugger: ML_DEBUGGER =
+struct
+
+(* exceptions *)
+
+abstype exn_id = Exn_Id of string * int Unsynchronized.ref
+with
+
+fun exn_id exn =
+  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
+
+fun print_exn_id (Exn_Id (name, _)) = name;
+fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
+
+end;
+
+val _ =
+  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
+    let val s = print_exn_id exn_id
+    in ML_Pretty.to_polyml (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
+
+
+(* hooks *)
+
+type location = PolyML.location;
+
+val on_entry = PolyML.DebuggerInterface.setOnEntry;
+val on_exit = PolyML.DebuggerInterface.setOnExit;
+val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
+val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
+
+
+(* debugger operations *)
+
+type state = PolyML.DebuggerInterface.debugState;
+
+val state = PolyML.DebuggerInterface.debugState;
+val debug_function = PolyML.DebuggerInterface.debugFunction;
+val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
+val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
+val debug_location = PolyML.DebuggerInterface.debugLocation;
+val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
+val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
+
+end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ML/ml_heap.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_heap.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,17 @@
+(*  Title:      Pure/ML/ml_heap.ML
+    Author:     Makarius
+
+ML heap operations.
+*)
+
+signature ML_HEAP =
+sig
+  val share_common_data: unit -> unit
+  val save_state: string -> unit
+end;
+
+structure ML_Heap: ML_HEAP =
+struct
+  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
+end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ML/ml_name_space.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_name_space.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,39 @@
+(*  Title:      Pure/ML/ml_name_space.ML
+    Author:     Makarius
+
+Name space for Poly/ML.
+*)
+
+structure ML_Name_Space =
+struct
+  open PolyML.NameSpace;
+
+  type T = PolyML.NameSpace.nameSpace;
+  val global = PolyML.globalNameSpace;
+  val forget_global_structure = PolyML.Compiler.forgetStructure;
+
+  type valueVal = Values.value;
+  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
+  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
+  val initial_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
+
+  type typeVal = TypeConstrs.typeConstr;
+  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
+  val initial_type = #allType global ();
+
+  type fixityVal = Infixes.fixity;
+  fun displayFix (_: string, x) = Infixes.print x;
+  val initial_fixity = #allFix global ();
+
+  type structureVal = Structures.structureVal;
+  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
+  val initial_structure = #allStruct global ();
+
+  type signatureVal = Signatures.signatureVal;
+  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
+  val initial_signature = #allSig global ();
+
+  type functorVal = Functors.functorVal;
+  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
+  val initial_functor = #allFunct global ();
+end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ML/ml_pretty.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_pretty.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,84 @@
+(*  Title:      Pure/ML/ml_pretty.ML
+    Author:     Makarius
+
+Minimal support for raw ML pretty printing, notably for toplevel pp.
+*)
+
+signature ML_PRETTY =
+sig
+  datatype pretty =
+    Block of (string * string) * bool * FixedInt.int * pretty list |
+    String of string * FixedInt.int |
+    Break of bool * FixedInt.int * FixedInt.int
+  val block: pretty list -> pretty
+  val str: string -> pretty
+  val brk: FixedInt.int -> pretty
+  val pair: ('a * int -> pretty) -> ('b * int -> pretty) -> ('a * 'b) * int -> pretty
+  val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
+  val to_polyml: pretty -> PolyML.pretty
+  val from_polyml: PolyML.pretty -> pretty
+end;
+
+structure ML_Pretty: ML_PRETTY =
+struct
+
+datatype pretty =
+  Block of (string * string) * bool * FixedInt.int * pretty list |
+  String of string * FixedInt.int |
+  Break of bool * FixedInt.int * FixedInt.int;
+
+fun block prts = Block (("", ""), false, 2, prts);
+fun str s = String (s, FixedInt.fromInt (size s));
+fun brk width = Break (false, width, 0);
+
+fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
+  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
+
+fun enum sep lpar rpar pretty (args, depth: FixedInt.int) =
+  let
+    fun elems _ [] = []
+      | elems 0 _ = [str "..."]
+      | elems d [x] = [pretty (x, d)]
+      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
+  in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
+
+
+(* convert *)
+
+fun to_polyml (Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
+  | to_polyml (Break (true, _, _)) =
+      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
+        [PolyML.PrettyString " "])
+  | to_polyml (Block ((bg, en), consistent, ind, prts)) =
+      let val context =
+        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
+        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
+      in PolyML.PrettyBlock (ind, consistent, context, map to_polyml prts) end
+  | to_polyml (String (s, len)) =
+      if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
+      else
+        PolyML.PrettyBlock
+          (0, false,
+            [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
+
+val from_polyml =
+  let
+    fun convert _ (PolyML.PrettyBreak (width, offset)) = Break (false, width, offset)
+      | convert _ (PolyML.PrettyBlock (_, _,
+            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
+          Break (true, 1, 0)
+      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
+          let
+            fun property name default =
+              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
+                SOME (PolyML.ContextProperty (_, b)) => b
+              | _ => default);
+            val bg = property "begin" "";
+            val en = property "end" "";
+            val len' = property "length" len;
+          in Block ((bg, en), consistent, ind, map (convert len') prts) end
+      | convert len (PolyML.PrettyString s) =
+          String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
+  in convert "" end;
+
+end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ML/ml_profiling.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_profiling.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,19 @@
+(*  Title:      Pure/ML/ml_profiling.ML
+    Author:     Makarius
+
+Profiling for Poly/ML 5.6.
+*)
+
+structure ML_Profiling =
+struct
+
+fun profile_time pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
+
+fun profile_time_thread pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
+
+fun profile_allocations pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
+
+end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ML/ml_system.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_system.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -0,0 +1,58 @@
+(*  Title:      Pure/ML/ml_system.ML
+    Author:     Makarius
+
+ML system and platform operations.
+*)
+
+signature ML_SYSTEM =
+sig
+  val name: string
+  val platform: string
+  val platform_is_windows: bool
+  val platform_path: string -> string
+  val standard_path: string -> string
+end;
+
+structure ML_System: ML_SYSTEM =
+struct
+
+val SOME name = OS.Process.getEnv "ML_SYSTEM";
+val SOME platform = OS.Process.getEnv "ML_PLATFORM";
+val platform_is_windows = String.isSuffix "windows" platform;
+
+val platform_path =
+  if platform_is_windows then
+    fn path =>
+      if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then
+        (case String.tokens (fn c => c = #"/") path of
+          "cygdrive" :: drive :: arcs =>
+            let
+              val vol =
+                (case Char.fromString drive of
+                  NONE => drive ^ ":"
+                | SOME d => String.str (Char.toUpper d) ^ ":");
+            in String.concatWith "\\" (vol :: arcs) end
+        | arcs =>
+            (case OS.Process.getEnv "CYGWIN_ROOT" of
+              SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
+            | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
+      else String.translate (fn #"/" => "\\" | c => String.str c) path
+  else fn path => path;
+
+val standard_path =
+  if platform_is_windows then
+    fn path =>
+      let
+        val {vol, arcs, isAbs} = OS.Path.fromString path;
+        val path' = String.translate (fn #"\\" => "/" | c => String.str c) path;
+      in
+        if isAbs then
+          (case String.explode vol of
+            [d, #":"] =>
+              String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs)
+          | _ => path')
+        else path'
+      end
+  else fn path => path;
+
+end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/PIDE/command.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -195,7 +195,7 @@
       Outer_Syntax.side_comments span |> maps (fn cmt =>
         (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
           handle exn =>
-            if Exn.is_interrupt exn then reraise exn
+            if Exn.is_interrupt exn then Exn.reraise exn
             else Runtime.exn_messages_ids exn)) ();
 
 fun report tr m =
@@ -277,7 +277,7 @@
 fun print_error tr opt_context e =
   (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
     handle exn =>
-      if Exn.is_interrupt exn then reraise exn
+      if Exn.is_interrupt exn then Exn.reraise exn
       else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
 
 fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process;
@@ -312,7 +312,7 @@
 
     fun bad_print name args exn =
       make_print name args {delay = NONE, pri = 0, persistent = false,
-        strict = false, print_fn = fn _ => fn _ => reraise exn};
+        strict = false, print_fn = fn _ => fn _ => Exn.reraise exn};
 
     fun new_print name args get_pr =
       let
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -486,7 +486,7 @@
                           else NONE
                       | NONE => NONE)) node ()
                    else ())
-                   handle exn => (Output.system_message (Runtime.exn_message exn); reraise exn);
+                   handle exn => (Output.system_message (Runtime.exn_message exn); Exn.reraise exn);
                 val future =
                   (singleton o Future.forks)
                    {name = "theory:" ^ name,
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/PIDE/protocol.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -120,7 +120,7 @@
   Isabelle_Process.protocol_command "Document.dialog_result"
     (fn [serial, result] =>
       Active.dialog_result (Markup.parse_int serial) result
-        handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
+        handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
 
 val _ =
   Isabelle_Process.protocol_command "ML_Heap.share_common_data"
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ROOT_polyml-5.6.ML
--- a/src/Pure/RAW/ROOT_polyml-5.6.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(*  Title:      Pure/RAW/ROOT_polyml-5.6.ML
-    Author:     Makarius
-
-Compatibility wrapper for Poly/ML 5.6.
-*)
-
-structure Thread =
-struct
-  open Thread;
-
-  structure Thread =
-  struct
-    open Thread;
-
-    fun numProcessors () =
-      (case Thread.numPhysicalProcessors () of
-        SOME n => n
-      | NONE => Thread.numProcessors ());
-  end;
-end;
-
-use "RAW/ROOT_polyml.ML";
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,191 +0,0 @@
-(*  Title:      Pure/RAW/ROOT_polyml.ML
-    Author:     Makarius
-
-Compatibility wrapper for Poly/ML.
-*)
-
-(* initial ML name space *)
-
-use "RAW/ml_system.ML";
-
-if ML_System.name = "polyml-5.6"
-then use "RAW/ml_name_space_polyml-5.6.ML"
-else use "RAW/ml_name_space_polyml.ML";
-
-if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
-else use "RAW/fixed_int_dummy.ML";
-
-structure ML_Name_Space =
-struct
-  open ML_Name_Space;
-  val initial_val =
-    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
-      (#allVal global ());
-  val initial_type = #allType global ();
-  val initial_fixity = #allFix global ();
-  val initial_structure = #allStruct global ();
-  val initial_signature = #allSig global ();
-  val initial_functor = #allFunct global ();
-end;
-
-
-(* ML heap operations *)
-
-if ML_System.name = "polyml-5.3.0"
-then use "RAW/ml_heap_polyml-5.3.0.ML"
-else use "RAW/ml_heap.ML";
-
-
-(* exceptions *)
-
-fun reraise exn =
-  (case PolyML.exceptionLocation exn of
-    NONE => raise exn
-  | SOME location => PolyML.raiseWithLocation (exn, location));
-
-exception Interrupt = SML90.Interrupt;
-
-use "RAW/exn.ML";
-
-if ML_System.name = "polyml-5.6"
-then use "RAW/exn_trace.ML"
-else use "RAW/exn_trace_raw.ML";
-
-
-(* multithreading *)
-
-val seconds = Time.fromReal;
-
-if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
-then ()
-else use "RAW/single_assignment_polyml.ML";
-
-open Thread;
-use "RAW/multithreading.ML";
-
-if ML_System.name = "polyml-5.6"
-then use "RAW/ml_stack_polyml-5.6.ML"
-else use "RAW/ml_stack_dummy.ML";
-
-use "RAW/unsynchronized.ML";
-val _ = PolyML.Compiler.forgetValue "ref";
-val _ = PolyML.Compiler.forgetType "ref";
-
-
-(* pervasive environment *)
-
-val _ = PolyML.Compiler.forgetValue "isSome";
-val _ = PolyML.Compiler.forgetValue "getOpt";
-val _ = PolyML.Compiler.forgetValue "valOf";
-val _ = PolyML.Compiler.forgetValue "foldl";
-val _ = PolyML.Compiler.forgetValue "foldr";
-val _ = PolyML.Compiler.forgetValue "print";
-val _ = PolyML.Compiler.forgetValue "explode";
-val _ = PolyML.Compiler.forgetValue "concat";
-
-val ord = SML90.ord;
-val chr = SML90.chr;
-val raw_explode = SML90.explode;
-val implode = SML90.implode;
-
-fun quit () = exit 0;
-
-
-(* ML runtime system *)
-
-if ML_System.name = "polyml-5.6"
-then use "RAW/ml_profiling_polyml-5.6.ML"
-else use "RAW/ml_profiling_polyml.ML";
-
-val pointer_eq = PolyML.pointerEq;
-
-
-(* ML toplevel pretty printing *)
-
-use "RAW/ml_pretty.ML";
-
-local
-  val depth = Unsynchronized.ref 10;
-in
-  fun get_default_print_depth () = ! depth;
-  fun default_print_depth n = (depth := n; PolyML.print_depth n);
-  val _ = default_print_depth 10;
-end;
-
-val error_depth = PolyML.error_depth;
-
-val pretty_ml =
-  let
-    fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset)
-      | convert _ (PolyML.PrettyBlock (_, _,
-            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
-          ML_Pretty.Break (true, 1, 0)
-      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
-          let
-            fun property name default =
-              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
-                SOME (PolyML.ContextProperty (_, b)) => b
-              | _ => default);
-            val bg = property "begin" "";
-            val en = property "end" "";
-            val len' = property "length" len;
-          in ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end
-      | convert len (PolyML.PrettyString s) =
-          ML_Pretty.String
-            (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
-  in convert "" end;
-
-fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
-  | ml_pretty (ML_Pretty.Break (true, _, _)) =
-      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
-        [PolyML.PrettyString " "])
-  | ml_pretty (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
-      let val context =
-        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
-        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
-      in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end
-  | ml_pretty (ML_Pretty.String (s, len)) =
-      if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
-      else
-        PolyML.PrettyBlock
-          (0, false,
-            [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
-
-
-(* ML compiler *)
-
-use "RAW/secure.ML";
-
-structure ML_Name_Space =
-struct
-  open ML_Name_Space;
-  val display_val = pretty_ml o displayVal;
-end;
-
-use "RAW/ml_compiler_parameters.ML";
-if ML_System.name = "polyml-5.6"
-then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
-
-use "RAW/ml_positions.ML";
-use "RAW/ml_compiler0.ML";
-
-PolyML.Compiler.reportUnreferencedIds := true;
-PolyML.Compiler.printInAlphabeticalOrder := false;
-PolyML.Compiler.maxInlineSize := 80;
-PolyML.Compiler.prompt1 := "ML> ";
-PolyML.Compiler.prompt2 := "ML# ";
-
-use "RAW/ml_parse_tree.ML";
-if ML_System.name = "polyml-5.6"
-then use "RAW/ml_parse_tree_polyml-5.6.ML" else ();
-
-fun ml_make_string struct_name =
-  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
-    struct_name ^ ".ML_print_depth ()))))))";
-
-
-(* ML debugger *)
-
-if ML_System.name = "polyml-5.6"
-then use_no_debug "RAW/ml_debugger_polyml-5.6.ML"
-else use_no_debug "RAW/ml_debugger.ML";
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/exn.ML
--- a/src/Pure/RAW/exn.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,113 +0,0 @@
-(*  Title:      Pure/RAW/exn.ML
-    Author:     Makarius
-
-Support for exceptions.
-*)
-
-signature BASIC_EXN =
-sig
-  exception ERROR of string
-  val error: string -> 'a
-  val cat_error: string -> string -> 'a
-end;
-
-signature EXN =
-sig
-  include BASIC_EXN
-  datatype 'a result = Res of 'a | Exn of exn
-  val get_res: 'a result -> 'a option
-  val get_exn: 'a result -> exn option
-  val capture: ('a -> 'b) -> 'a -> 'b result
-  val release: 'a result -> 'a
-  val map_res: ('a -> 'b) -> 'a result -> 'b result
-  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
-  val map_exn: (exn -> exn) -> 'a result -> 'a result
-  exception Interrupt
-  val interrupt: unit -> 'a
-  val is_interrupt: exn -> bool
-  val interrupt_exn: 'a result
-  val is_interrupt_exn: 'a result -> bool
-  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
-  val return_code: exn -> int -> int
-  val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
-  exception EXCEPTIONS of exn list
-end;
-
-structure Exn: EXN =
-struct
-
-(* user errors *)
-
-exception ERROR of string;
-
-fun error msg = raise ERROR msg;
-
-fun cat_error "" msg = error msg
-  | cat_error msg "" = error msg
-  | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
-
-
-(* exceptions as values *)
-
-datatype 'a result =
-  Res of 'a |
-  Exn of exn;
-
-fun get_res (Res x) = SOME x
-  | get_res _ = NONE;
-
-fun get_exn (Exn exn) = SOME exn
-  | get_exn _ = NONE;
-
-fun capture f x = Res (f x) handle e => Exn e;
-
-fun release (Res y) = y
-  | release (Exn e) = reraise e;
-
-fun map_res f (Res x) = Res (f x)
-  | map_res f (Exn e) = Exn e;
-
-fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
-
-fun map_exn f (Res x) = Res x
-  | map_exn f (Exn e) = Exn (f e);
-
-
-(* interrupts *)
-
-exception Interrupt = Interrupt;
-
-fun interrupt () = raise Interrupt;
-
-fun is_interrupt Interrupt = true
-  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
-  | is_interrupt _ = false;
-
-val interrupt_exn = Exn Interrupt;
-
-fun is_interrupt_exn (Exn exn) = is_interrupt exn
-  | is_interrupt_exn _ = false;
-
-fun interruptible_capture f x =
-  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
-
-
-(* POSIX return code *)
-
-fun return_code exn rc =
-  if is_interrupt exn then (130: int) else rc;
-
-fun capture_exit rc f x =
-  f x handle exn => exit (return_code exn rc);
-
-
-(* concatenated exceptions *)
-
-exception EXCEPTIONS of exn list;
-
-end;
-
-datatype illegal = Interrupt;
-
-structure Basic_Exn: BASIC_EXN = Exn;
-open Basic_Exn;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/exn.scala
--- a/src/Pure/RAW/exn.scala	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,137 +0,0 @@
-/*  Title:      Pure/RAW/exn.scala
-    Module:     PIDE
-    Author:     Makarius
-
-Support for exceptions (arbitrary throwables).
-*/
-
-package isabelle
-
-
-object Exn
-{
-  /* user errors */
-
-  class User_Error(message: String) extends RuntimeException(message)
-  {
-    override def equals(that: Any): Boolean =
-      that match {
-        case other: User_Error => message == other.getMessage
-        case _ => false
-      }
-    override def hashCode: Int = message.hashCode
-
-    override def toString: String = "ERROR(" + message + ")"
-  }
-
-  object ERROR
-  {
-    def apply(message: String): User_Error = new User_Error(message)
-    def unapply(exn: Throwable): Option[String] = user_message(exn)
-  }
-
-  def error(message: String): Nothing = throw ERROR(message)
-
-  def cat_message(msg1: String, msg2: String): String =
-    if (msg1 == "") msg2
-    else if (msg2 == "") msg1
-    else msg1 + "\n" + msg2
-
-  def cat_error(msg1: String, msg2: String): Nothing =
-    error(cat_message(msg1, msg2))
-
-
-  /* exceptions as values */
-
-  sealed abstract class Result[A]
-  {
-    def user_error: Result[A] =
-      this match {
-        case Exn(ERROR(msg)) => Exn(ERROR(msg))
-        case _ => this
-      }
-  }
-  case class Res[A](res: A) extends Result[A]
-  case class Exn[A](exn: Throwable) extends Result[A]
-
-  def capture[A](e: => A): Result[A] =
-    try { Res(e) }
-    catch { case exn: Throwable => Exn[A](exn) }
-
-  def release[A](result: Result[A]): A =
-    result match {
-      case Res(x) => x
-      case Exn(exn) => throw exn
-    }
-
-  def release_first[A](results: List[Result[A]]): List[A] =
-    results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
-      case Some(Exn(exn)) => throw exn
-      case _ => results.map(release(_))
-    }
-
-
-  /* interrupts */
-
-  def is_interrupt(exn: Throwable): Boolean =
-  {
-    var found_interrupt = false
-    var e = exn
-    while (!found_interrupt && e != null) {
-      found_interrupt |= e.isInstanceOf[InterruptedException]
-      e = e.getCause
-    }
-    found_interrupt
-  }
-
-  object Interrupt
-  {
-    def apply(): Throwable = new InterruptedException
-    def unapply(exn: Throwable): Boolean = is_interrupt(exn)
-
-    def expose() { if (Thread.interrupted) throw apply() }
-    def impose() { Thread.currentThread.interrupt }
-
-    def postpone[A](body: => A): Option[A] =
-    {
-      val interrupted = Thread.interrupted
-      val result = capture { body }
-      if (interrupted) impose()
-      result match {
-        case Res(x) => Some(x)
-        case Exn(e) =>
-          if (is_interrupt(e)) { impose(); None }
-          else throw e
-      }
-    }
-
-    val return_code = 130
-  }
-
-
-  /* POSIX return code */
-
-  def return_code(exn: Throwable, rc: Int): Int =
-    if (is_interrupt(exn)) Interrupt.return_code else rc
-
-
-  /* message */
-
-  def user_message(exn: Throwable): Option[String] =
-    if (exn.getClass == classOf[RuntimeException] ||
-        exn.getClass == classOf[User_Error])
-    {
-      val msg = exn.getMessage
-      Some(if (msg == null || msg == "") "Error" else msg)
-    }
-    else if (exn.isInstanceOf[java.io.IOException])
-    {
-      val msg = exn.getMessage
-      Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
-    }
-    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
-    else None
-
-  def message(exn: Throwable): String =
-    user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
-}
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/exn_trace.ML
--- a/src/Pure/RAW/exn_trace.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      Pure/RAW/exn_trace.ML
-    Author:     Makarius
-
-Exception trace via ML output, for Poly/ML 5.5.1 or later.
-*)
-
-fun print_exception_trace exn_message output e =
-  PolyML.Exception.traceException
-    (e, fn (trace, exn) =>
-      let
-        val title = "Exception trace - " ^ exn_message exn;
-        val _ = output (String.concatWith "\n" (title :: trace));
-      in reraise exn end);
-
-PolyML.Compiler.reportExhaustiveHandlers := true;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/exn_trace_raw.ML
--- a/src/Pure/RAW/exn_trace_raw.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(*  Title:      Pure/RAW/exn_trace_raw.ML
-    Author:     Makarius
-
-Raw exception trace for Poly/ML 5.3.0.
-*)
-
-fun print_exception_trace (_: exn -> string) (_: string -> unit) =
-  PolyML.exception_trace;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/fixed_int_dummy.ML
--- a/src/Pure/RAW/fixed_int_dummy.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(*  Title:      Pure/RAW/fixed_int_dummy.ML
-
-FixedInt dummy that is not fixed (up to Poly/ML 5.6).
-*)
-
-structure FixedInt = IntInf;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_compiler0.ML
--- a/src/Pure/RAW/ml_compiler0.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,100 +0,0 @@
-(*  Title:      Pure/RAW/ml_compiler0.ML
-
-Runtime compilation and evaluation (bootstrap version of
-Pure/ML/ml_compiler.ML).
-*)
-
-signature ML_COMPILER0 =
-sig
-  type context =
-   {name_space: ML_Name_Space.T,
-    here: int -> string -> string,
-    print: string -> unit,
-    error: string -> unit}
-  val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
-  val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
-  val debug_option: bool option -> bool
-  val use_operations: (bool option -> string -> unit) ->
-    {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit}
-end;
-
-structure ML_Compiler0: ML_COMPILER0 =
-struct
-
-type context =
- {name_space: ML_Name_Space.T,
-  here: int -> string -> string,
-  print: string -> unit,
-  error: string -> unit};
-
-fun drop_newline s =
-  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
-  else s;
-
-fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
-  let
-    val _ = Secure.deny_ml ();
-
-    val current_line = Unsynchronized.ref line;
-    val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
-    val out_buffer = Unsynchronized.ref ([]: string list);
-    fun output () = drop_newline (implode (rev (! out_buffer)));
-
-    fun get () =
-      (case ! in_buffer of
-        [] => NONE
-      | c :: cs =>
-          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
-    fun put s = out_buffer := s :: ! out_buffer;
-    fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
-     (put (if hard then "Error: " else "Warning: ");
-      PolyML.prettyPrint (put, 76) msg1;
-      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
-      put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
-
-    val parameters =
-     [PolyML.Compiler.CPOutStream put,
-      PolyML.Compiler.CPNameSpace name_space,
-      PolyML.Compiler.CPErrorMessageProc put_message,
-      PolyML.Compiler.CPLineNo (fn () => ! current_line),
-      PolyML.Compiler.CPFileName file,
-      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
-      ML_Compiler_Parameters.debug debug;
-    val _ =
-      (while not (List.null (! in_buffer)) do
-        PolyML.compiler (get, parameters) ())
-      handle exn =>
-        if Exn.is_interrupt exn then reraise exn
-        else
-         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-          error (output ()); reraise exn);
-  in if verbose then print (output ()) else () end;
-
-fun use_file context {verbose, debug} file =
-  let
-    val instream = TextIO.openIn file;
-    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
-
-
-fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
-  | debug_option (SOME debug) = debug;
-
-fun use_operations (use_ : bool option -> string -> unit) =
-  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
-
-end;
-
-val {use, use_debug, use_no_debug} =
-  let
-    val context: ML_Compiler0.context =
-     {name_space = ML_Name_Space.global,
-      here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
-      print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
-      error = fn s => error s};
-  in
-    ML_Compiler0.use_operations (fn opt_debug => fn file =>
-      ML_Compiler0.use_file context
-        {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
-      handle ERROR msg => (#print context msg; raise error "ML error"))
-  end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_compiler_parameters.ML
--- a/src/Pure/RAW/ml_compiler_parameters.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      Pure/RAW/ml_compiler_parameters.ML
-    Author:     Makarius
-
-Additional ML compiler parameters for Poly/ML.
-*)
-
-signature ML_COMPILER_PARAMETERS =
-sig
-  val debug: bool -> PolyML.Compiler.compilerParameters list
-end;
-
-structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
-struct
-
-fun debug _ = [];
-
-end;
\ No newline at end of file
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
--- a/src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(*  Title:      Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
-    Author:     Makarius
-
-Additional ML compiler parameters for Poly/ML 5.6, or later.
-*)
-
-structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
-struct
-
-fun debug b = [PolyML.Compiler.CPDebug b];
-
-end;
\ No newline at end of file
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_debugger.ML
--- a/src/Pure/RAW/ml_debugger.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(*  Title:      Pure/RAW/ml_debugger.ML
-    Author:     Makarius
-
-ML debugger interface -- dummy version.
-*)
-
-signature ML_DEBUGGER =
-sig
-  type exn_id
-  val exn_id: exn -> exn_id
-  val print_exn_id: exn_id -> string
-  val eq_exn_id: exn_id * exn_id -> bool
-  val on_entry: (string * 'location -> unit) option -> unit
-  val on_exit: (string * 'location -> unit) option -> unit
-  val on_exit_exception: (string * 'location -> exn -> unit) option -> unit
-  val on_breakpoint: ('location * bool Unsynchronized.ref -> unit) option -> unit
-  type state
-  val state: Thread.thread -> state list
-  val debug_function: state -> string
-  val debug_function_arg: state -> ML_Name_Space.valueVal
-  val debug_function_result: state -> ML_Name_Space.valueVal
-  val debug_location: state -> 'location
-  val debug_name_space: state -> ML_Name_Space.T
-  val debug_local_name_space: state -> ML_Name_Space.T
-end;
-
-structure ML_Debugger: ML_DEBUGGER =
-struct
-
-(* exceptions *)
-
-abstype exn_id = Exn_Id of string
-with
-
-fun exn_id exn = Exn_Id (General.exnName exn);
-fun print_exn_id (Exn_Id name) = name;
-fun eq_exn_id (Exn_Id name1, Exn_Id name2) = name1 = name2;  (*over-approximation*)
-
-end;
-
-
-(* hooks *)
-
-fun on_entry _ = ();
-fun on_exit _ = ();
-fun on_exit_exception _ = ();
-fun on_breakpoint _ = ();
-
-
-(* debugger *)
-
-fun fail () = raise Fail "No debugger support on this ML platform";
-
-type state = unit;
-
-fun state _ = [];
-fun debug_function () = fail ();
-fun debug_function_arg () = fail ();
-fun debug_function_result () = fail ();
-fun debug_location () = fail ();
-fun debug_name_space () = fail ();
-fun debug_local_name_space () = fail ();
-
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_debugger_polyml-5.6.ML
--- a/src/Pure/RAW/ml_debugger_polyml-5.6.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(*  Title:      Pure/RAW/ml_debugger_polyml-5.6.ML
-    Author:     Makarius
-
-ML debugger interface -- for Poly/ML 5.6, or later.
-*)
-
-signature ML_DEBUGGER =
-sig
-  type exn_id
-  val exn_id: exn -> exn_id
-  val print_exn_id: exn_id -> string
-  val eq_exn_id: exn_id * exn_id -> bool
-  type location
-  val on_entry: (string * location -> unit) option -> unit
-  val on_exit: (string * location -> unit) option -> unit
-  val on_exit_exception: (string * location -> exn -> unit) option -> unit
-  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
-  type state
-  val state: Thread.thread -> state list
-  val debug_function: state -> string
-  val debug_function_arg: state -> ML_Name_Space.valueVal
-  val debug_function_result: state -> ML_Name_Space.valueVal
-  val debug_location: state -> location
-  val debug_name_space: state -> ML_Name_Space.T
-  val debug_local_name_space: state -> ML_Name_Space.T
-end;
-
-structure ML_Debugger: ML_DEBUGGER =
-struct
-
-(* exceptions *)
-
-abstype exn_id = Exn_Id of string * int Unsynchronized.ref
-with
-
-fun exn_id exn =
-  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
-
-fun print_exn_id (Exn_Id (name, _)) = name;
-fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
-
-end;
-
-val _ =
-  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
-    let val s = print_exn_id exn_id
-    in ml_pretty (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
-
-
-(* hooks *)
-
-type location = PolyML.location;
-
-val on_entry = PolyML.DebuggerInterface.setOnEntry;
-val on_exit = PolyML.DebuggerInterface.setOnExit;
-val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
-val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
-
-
-(* debugger operations *)
-
-type state = PolyML.DebuggerInterface.debugState;
-
-val state = PolyML.DebuggerInterface.debugState;
-val debug_function = PolyML.DebuggerInterface.debugFunction;
-val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
-val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
-val debug_location = PolyML.DebuggerInterface.debugLocation;
-val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
-val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
-
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_heap.ML
--- a/src/Pure/RAW/ml_heap.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      Pure/RAW/ml_heap.ML
-    Author:     Makarius
-
-ML heap operations.
-*)
-
-signature ML_HEAP =
-sig
-  val share_common_data: unit -> unit
-  val save_state: string -> unit
-end;
-
-structure ML_Heap: ML_HEAP =
-struct
-  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_heap_polyml-5.3.0.ML
--- a/src/Pure/RAW/ml_heap_polyml-5.3.0.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      Pure/RAW/ml_heap_polyml-5.3.0.ML
-    Author:     Makarius
-
-ML heap operations.
-*)
-
-signature ML_HEAP =
-sig
-  val share_common_data: unit -> unit
-  val save_state: string -> unit
-end;
-
-structure ML_Heap: ML_HEAP =
-struct
-  fun share_common_data () = ();
-  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_name_space_polyml-5.6.ML
--- a/src/Pure/RAW/ml_name_space_polyml-5.6.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  Title:      Pure/RAW/ml_name_space_polyml-5.6.ML
-    Author:     Makarius
-
-Name space for Poly/ML.
-*)
-
-structure ML_Name_Space =
-struct
-  open PolyML.NameSpace;
-
-  type T = PolyML.NameSpace.nameSpace;
-  val global = PolyML.globalNameSpace;
-  val forget_global_structure = PolyML.Compiler.forgetStructure;
-
-  type valueVal = Values.value;
-  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
-  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
-
-  type typeVal = TypeConstrs.typeConstr;
-  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
-
-  type fixityVal = Infixes.fixity;
-  fun displayFix (_: string, x) = Infixes.print x;
-
-  type structureVal = Structures.structureVal;
-  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
-
-  type signatureVal = Signatures.signatureVal;
-  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
-
-  type functorVal = Functors.functorVal;
-  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_name_space_polyml.ML
--- a/src/Pure/RAW/ml_name_space_polyml.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(*  Title:      Pure/RAW/ml_name_space_polyml.ML
-    Author:     Makarius
-
-Name space for Poly/ML.
-*)
-
-structure ML_Name_Space =
-struct
-  open PolyML.NameSpace;
-  type T = nameSpace;
-  val global = PolyML.globalNameSpace;
-  val forget_global_structure = PolyML.Compiler.forgetStructure;
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_parse_tree.ML
--- a/src/Pure/RAW/ml_parse_tree.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      Pure/RAW/ml_parse_tree.ML
-    Author:     Makarius
-
-Additional ML parse tree components for Poly/ML.
-*)
-
-signature ML_PARSE_TREE =
-sig
-  val completions: PolyML.ptProperties -> string list option
-  val breakpoint: PolyML.ptProperties -> bool Unsynchronized.ref option
-end;
-
-structure ML_Parse_Tree: ML_PARSE_TREE =
-struct
-
-fun completions _ = NONE;
-fun breakpoint _ = NONE;
-
-end;
\ No newline at end of file
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_parse_tree_polyml-5.6.ML
--- a/src/Pure/RAW/ml_parse_tree_polyml-5.6.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/RAW/ml_parse_tree_polyml-5.6.ML
-    Author:     Makarius
-
-Additional ML parse tree components for Poly/ML 5.6, or later.
-*)
-
-structure ML_Parse_Tree: ML_PARSE_TREE =
-struct
-
-fun completions (PolyML.PTcompletions x) = SOME x
-  | completions _ = NONE;
-
-fun breakpoint (PolyML.PTbreakPoint x) = SOME x
-  | breakpoint _ = NONE;
-
-end;
\ No newline at end of file
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_positions.ML
--- a/src/Pure/RAW/ml_positions.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/RAW/ml_positions.ML
-    Author:     Makarius
-
-Approximate ML antiquotation @{here} for Isabelle/Pure bootstrap.
-*)
-
-fun ml_positions start_line name txt =
-  let
-    fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
-          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
-          in positions line cs (s :: res) end
-      | positions line (c :: cs) res =
-          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
-      | positions _ [] res = rev res;
-  in String.concat (positions start_line (String.explode txt) []) end;
-
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_pretty.ML
--- a/src/Pure/RAW/ml_pretty.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(*  Title:      Pure/RAW/ml_pretty.ML
-    Author:     Makarius
-
-Minimal support for raw ML pretty printing -- for boot-strapping only.
-*)
-
-structure ML_Pretty =
-struct
-
-datatype pretty =
-  Block of (string * string) * bool * FixedInt.int * pretty list |
-  String of string * FixedInt.int |
-  Break of bool * FixedInt.int * FixedInt.int;
-
-fun block prts = Block (("", ""), false, 2, prts);
-fun str s = String (s, FixedInt.fromInt (size s));
-fun brk width = Break (false, width, 0);
-
-fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
-  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
-
-fun enum sep lpar rpar pretty (args, depth: FixedInt.int) =
-  let
-    fun elems _ [] = []
-      | elems 0 _ = [str "..."]
-      | elems d [x] = [pretty (x, d)]
-      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
-  in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
-
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_profiling_polyml-5.6.ML
--- a/src/Pure/RAW/ml_profiling_polyml-5.6.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      Pure/RAW/ml_profiling_polyml-5.6.ML
-    Author:     Makarius
-
-Profiling for Poly/ML 5.6.
-*)
-
-structure ML_Profiling =
-struct
-
-fun profile_time pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
-
-fun profile_time_thread pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
-
-fun profile_allocations pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
-
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_profiling_polyml.ML
--- a/src/Pure/RAW/ml_profiling_polyml.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title:      Pure/RAW/ml_profiling_polyml.ML
-    Author:     Makarius
-
-Profiling for Poly/ML.
-*)
-
-structure ML_Profiling =
-struct
-
-local
-
-fun profile n f x =
-  let
-    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
-    val res = Exn.capture f x;
-    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
-  in Exn.release res end;
-
-in
-
-fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x;
-fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x;
-fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x;
-
-end;
-
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_stack_dummy.ML
--- a/src/Pure/RAW/ml_stack_dummy.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/RAW/ml_stack_dummy.ML
-
-Maximum stack size (in words) for ML threads -- dummy version.
-*)
-
-signature ML_STACK =
-sig
-  val limit: int option -> Thread.threadAttribute list
-end;
-
-structure ML_Stack: ML_STACK =
-struct
-
-fun limit (_: int option) : Thread.threadAttribute list = [];
-
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_stack_polyml-5.6.ML
--- a/src/Pure/RAW/ml_stack_polyml-5.6.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/RAW/ml_stack_polyml-5.6.ML
-
-Maximum stack size (in words) for ML threads -- Poly/ML 5.6, or later.
-*)
-
-signature ML_STACK =
-sig
-  val limit: int option -> Thread.threadAttribute list
-end;
-
-structure ML_Stack: ML_STACK =
-struct
-
-fun limit m = [Thread.MaximumMLStack m];
-
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/ml_system.ML
--- a/src/Pure/RAW/ml_system.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(*  Title:      Pure/RAW/ml_system.ML
-    Author:     Makarius
-
-ML system and platform operations.
-*)
-
-signature ML_SYSTEM =
-sig
-  val name: string
-  val platform: string
-  val platform_is_windows: bool
-  val platform_path: string -> string
-  val standard_path: string -> string
-end;
-
-structure ML_System: ML_SYSTEM =
-struct
-
-val SOME name = OS.Process.getEnv "ML_SYSTEM";
-val SOME platform = OS.Process.getEnv "ML_PLATFORM";
-val platform_is_windows = String.isSuffix "windows" platform;
-
-val platform_path =
-  if platform_is_windows then
-    fn path =>
-      if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then
-        (case String.tokens (fn c => c = #"/") path of
-          "cygdrive" :: drive :: arcs =>
-            let
-              val vol =
-                (case Char.fromString drive of
-                  NONE => drive ^ ":"
-                | SOME d => String.str (Char.toUpper d) ^ ":");
-            in String.concatWith "\\" (vol :: arcs) end
-        | arcs =>
-            (case OS.Process.getEnv "CYGWIN_ROOT" of
-              SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
-            | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
-      else String.translate (fn #"/" => "\\" | c => String.str c) path
-  else fn path => path;
-
-val standard_path =
-  if platform_is_windows then
-    fn path =>
-      let
-        val {vol, arcs, isAbs} = OS.Path.fromString path;
-        val path' = String.translate (fn #"\\" => "/" | c => String.str c) path;
-      in
-        if isAbs then
-          (case String.explode vol of
-            [d, #":"] =>
-              String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs)
-          | _ => path')
-        else path'
-      end
-  else fn path => path;
-
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/multithreading.ML
--- a/src/Pure/RAW/multithreading.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,191 +0,0 @@
-(*  Title:      Pure/RAW/multithreading.ML
-    Author:     Makarius
-
-Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
-*)
-
-signature BASIC_MULTITHREADING =
-sig
-  val interruptible: ('a -> 'b) -> 'a -> 'b
-  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-end;
-
-signature MULTITHREADING =
-sig
-  include BASIC_MULTITHREADING
-  val no_interrupts: Thread.threadAttribute list
-  val public_interrupts: Thread.threadAttribute list
-  val private_interrupts: Thread.threadAttribute list
-  val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
-  val interrupted: unit -> unit  (*exception Interrupt*)
-  val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
-  val max_threads_value: unit -> int
-  val max_threads_update: int -> unit
-  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
-  val enabled: unit -> bool
-  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
-    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
-  val trace: int ref
-  val tracing: int -> (unit -> string) -> unit
-  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
-  val real_time: ('a -> unit) -> 'a -> Time.time
-  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
-  val serial: unit -> int
-end;
-
-structure Multithreading: MULTITHREADING =
-struct
-
-(* thread attributes *)
-
-val no_interrupts =
-  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
-
-val test_interrupts =
-  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
-
-val public_interrupts =
-  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
-
-val private_interrupts =
-  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
-
-val sync_interrupts = map
-  (fn x as Thread.InterruptState Thread.InterruptDefer => x
-    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
-    | x => x);
-
-val safe_interrupts = map
-  (fn Thread.InterruptState Thread.InterruptAsynch =>
-      Thread.InterruptState Thread.InterruptAsynchOnce
-    | x => x);
-
-fun interrupted () =
-  let
-    val orig_atts = safe_interrupts (Thread.getAttributes ());
-    val _ = Thread.setAttributes test_interrupts;
-    val test = Exn.capture Thread.testInterrupt ();
-    val _ = Thread.setAttributes orig_atts;
-  in Exn.release test end;
-
-fun with_attributes new_atts e =
-  let
-    val orig_atts = safe_interrupts (Thread.getAttributes ());
-    val result = Exn.capture (fn () =>
-      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
-    val _ = Thread.setAttributes orig_atts;
-  in Exn.release result end;
-
-
-(* portable wrappers *)
-
-fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
-
-fun uninterruptible f x =
-  with_attributes no_interrupts (fn atts =>
-    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
-
-
-(* options *)
-
-fun max_threads_result m =
-  if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 1), 8);
-
-val max_threads = ref 1;
-
-fun max_threads_value () = ! max_threads;
-
-fun max_threads_update m = max_threads := max_threads_result m;
-
-fun max_threads_setmp m f x =
-  uninterruptible (fn restore_attributes => fn () =>
-    let
-      val max_threads_orig = ! max_threads;
-      val _ = max_threads_update m;
-      val result = Exn.capture (restore_attributes f) x;
-      val _ = max_threads := max_threads_orig;
-    in Exn.release result end) ();
-
-fun enabled () = max_threads_value () > 1;
-
-
-(* synchronous wait *)
-
-fun sync_wait opt_atts time cond lock =
-  with_attributes
-    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
-    (fn _ =>
-      (case time of
-        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
-      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
-      handle exn => Exn.Exn exn);
-
-
-(* tracing *)
-
-val trace = ref 0;
-
-fun tracing level msg =
-  if level > ! trace then ()
-  else uninterruptible (fn _ => fn () =>
-    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
-      handle _ (*sic*) => ()) ();
-
-fun tracing_time detailed time =
-  tracing
-   (if not detailed then 5
-    else if Time.>= (time, seconds 1.0) then 1
-    else if Time.>= (time, seconds 0.1) then 2
-    else if Time.>= (time, seconds 0.01) then 3
-    else if Time.>= (time, seconds 0.001) then 4 else 5);
-
-fun real_time f x =
-  let
-    val timer = Timer.startRealTimer ();
-    val () = f x;
-    val time = Timer.checkRealTimer timer;
-  in time end;
-
-
-(* synchronized evaluation *)
-
-fun synchronized name lock e =
-  Exn.release (uninterruptible (fn restore_attributes => fn () =>
-    let
-      val immediate =
-        if Mutex.trylock lock then true
-        else
-          let
-            val _ = tracing 5 (fn () => name ^ ": locking ...");
-            val time = real_time Mutex.lock lock;
-            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
-          in false end;
-      val result = Exn.capture (restore_attributes e) ();
-      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
-      val _ = Mutex.unlock lock;
-    in result end) ());
-
-
-(* serial numbers *)
-
-local
-
-val serial_lock = Mutex.mutex ();
-val serial_count = ref 0;
-
-in
-
-val serial = uninterruptible (fn _ => fn () =>
-  let
-    val _ = Mutex.lock serial_lock;
-    val _ = serial_count := ! serial_count + 1;
-    val res = ! serial_count;
-    val _ = Mutex.unlock serial_lock;
-  in res end);
-
-end;
-
-end;
-
-structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
-open Basic_Multithreading;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/secure.ML
--- a/src/Pure/RAW/secure.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title:      Pure/RAW/secure.ML
-    Author:     Makarius
-
-Secure critical operations.
-*)
-
-signature SECURE =
-sig
-  val set_secure: unit -> unit
-  val is_secure: unit -> bool
-  val deny: string -> unit
-  val deny_ml: unit -> unit
-end;
-
-structure Secure: SECURE =
-struct
-
-val secure = Unsynchronized.ref false;
-
-fun set_secure () = secure := true;
-fun is_secure () = ! secure;
-
-fun deny msg = if is_secure () then error msg else ();
-
-fun deny_ml () = deny "Cannot evaluate ML source in secure mode";
-
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/single_assignment_polyml.ML
--- a/src/Pure/RAW/single_assignment_polyml.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  Title:      Pure/RAW/single_assignment_polyml.ML
-    Author:     Makarius
-
-References with single assignment.  Unsynchronized!  Emulates
-structure SingleAssignment from Poly/ML 5.4.
-*)
-
-signature SINGLE_ASSIGNMENT =
-sig
-  type 'a saref
-  exception Locked
-  val saref: unit -> 'a saref
-  val savalue: 'a saref -> 'a option
-  val saset: 'a saref * 'a -> unit
-end;
-
-structure SingleAssignment: SINGLE_ASSIGNMENT =
-struct
-
-exception Locked;
-
-abstype 'a saref = SARef of 'a option ref
-with
-
-fun saref () = SARef (ref NONE);
-
-fun savalue (SARef r) = ! r;
-
-fun saset (SARef (r as ref NONE), x) =
-      (r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r)
-  | saset _ = raise Locked;
-
-end;
-
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/RAW/unsynchronized.ML
--- a/src/Pure/RAW/unsynchronized.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(*  Title:      Pure/RAW/unsynchronized.ML
-    Author:     Makarius
-
-Raw ML references as unsynchronized state variables.
-*)
-
-structure Unsynchronized =
-struct
-
-datatype ref = datatype ref;
-
-val op := = op :=;
-val ! = !;
-
-fun change r f = r := f (! r);
-fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
-
-fun inc i = (i := ! i + (1: int); ! i);
-fun dec i = (i := ! i - (1: int); ! i);
-
-fun setmp flag value f x =
-  uninterruptible (fn restore_attributes => fn () =>
-    let
-      val orig_value = ! flag;
-      val _ = flag := value;
-      val result = Exn.capture (restore_attributes f) x;
-      val _ = flag := orig_value;
-    in Exn.release result end) ();
-
-end;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/ROOT	Thu Mar 03 23:33:41 2016 +0100
@@ -1,69 +1,8 @@
 chapter Pure
 
-session RAW =
-  theories
-  files
-    "RAW/ROOT_polyml-5.6.ML"
-    "RAW/ROOT_polyml.ML"
-    "RAW/exn.ML"
-    "RAW/exn_trace.ML"
-    "RAW/exn_trace_raw.ML"
-    "RAW/fixed_int_dummy.ML"
-    "RAW/ml_compiler0.ML"
-    "RAW/ml_compiler_parameters.ML"
-    "RAW/ml_compiler_parameters_polyml-5.6.ML"
-    "RAW/ml_debugger.ML"
-    "RAW/ml_debugger_polyml-5.6.ML"
-    "RAW/ml_heap.ML"
-    "RAW/ml_heap_polyml-5.3.0.ML"
-    "RAW/ml_name_space_polyml-5.6.ML"
-    "RAW/ml_name_space_polyml.ML"
-    "RAW/ml_parse_tree.ML"
-    "RAW/ml_parse_tree_polyml-5.6.ML"
-    "RAW/ml_positions.ML"
-    "RAW/ml_pretty.ML"
-    "RAW/ml_profiling_polyml-5.6.ML"
-    "RAW/ml_profiling_polyml.ML"
-    "RAW/ml_stack_dummy.ML"
-    "RAW/ml_stack_polyml-5.6.ML"
-    "RAW/ml_system.ML"
-    "RAW/multithreading.ML"
-    "RAW/secure.ML"
-    "RAW/single_assignment_polyml.ML"
-    "RAW/unsynchronized.ML"
-
 session Pure =
   global_theories Pure
   files
-    "RAW/ROOT_polyml-5.6.ML"
-    "RAW/ROOT_polyml.ML"
-    "RAW/exn.ML"
-    "RAW/exn_trace.ML"
-    "RAW/exn_trace_raw.ML"
-    "RAW/fixed_int_dummy.ML"
-    "RAW/ml_compiler0.ML"
-    "RAW/ml_compiler_parameters.ML"
-    "RAW/ml_compiler_parameters_polyml-5.6.ML"
-    "RAW/ml_debugger.ML"
-    "RAW/ml_debugger_polyml-5.6.ML"
-    "RAW/ml_heap.ML"
-    "RAW/ml_heap_polyml-5.3.0.ML"
-    "RAW/ml_name_space_polyml-5.6.ML"
-    "RAW/ml_name_space_polyml.ML"
-    "RAW/ml_parse_tree.ML"
-    "RAW/ml_parse_tree_polyml-5.6.ML"
-    "RAW/ml_positions.ML"
-    "RAW/ml_pretty.ML"
-    "RAW/ml_profiling_polyml-5.6.ML"
-    "RAW/ml_profiling_polyml.ML"
-    "RAW/ml_stack_dummy.ML"
-    "RAW/ml_stack_polyml-5.6.ML"
-    "RAW/ml_system.ML"
-    "RAW/multithreading.ML"
-    "RAW/secure.ML"
-    "RAW/single_assignment_polyml.ML"
-    "RAW/unsynchronized.ML"
-
     "Concurrent/bash.ML"
     "Concurrent/bash_windows.ML"
     "Concurrent/cache.ML"
@@ -72,6 +11,7 @@
     "Concurrent/future.ML"
     "Concurrent/lazy.ML"
     "Concurrent/mailbox.ML"
+    "Concurrent/multithreading.ML"
     "Concurrent/par_exn.ML"
     "Concurrent/par_list.ML"
     "Concurrent/random.ML"
@@ -80,6 +20,7 @@
     "Concurrent/synchronized.ML"
     "Concurrent/task_queue.ML"
     "Concurrent/time_limit.ML"
+    "Concurrent/unsynchronized.ML"
     "General/alist.ML"
     "General/antiquote.ML"
     "General/balanced_tree.ML"
@@ -88,6 +29,7 @@
     "General/buffer.ML"
     "General/change_table.ML"
     "General/completion.ML"
+    "General/exn.ML"
     "General/file.ML"
     "General/graph.ML"
     "General/graph_display.ML"
@@ -107,6 +49,7 @@
     "General/queue.ML"
     "General/same.ML"
     "General/scan.ML"
+    "General/secure.ML"
     "General/seq.ML"
     "General/sha1.ML"
     "General/sha1_polyml.ML"
@@ -160,17 +103,25 @@
     "ML/exn_debugger.ML"
     "ML/exn_output.ML"
     "ML/exn_properties.ML"
+    "ML/fixed_int_dummy.ML"
     "ML/install_pp_polyml.ML"
     "ML/ml_antiquotation.ML"
     "ML/ml_compiler.ML"
+    "ML/ml_compiler0.ML"
     "ML/ml_context.ML"
+    "ML/ml_debugger.ML"
     "ML/ml_env.ML"
     "ML/ml_file.ML"
+    "ML/ml_heap.ML"
     "ML/ml_lex.ML"
+    "ML/ml_name_space.ML"
     "ML/ml_options.ML"
+    "ML/ml_pretty.ML"
+    "ML/ml_profiling.ML"
     "ML/ml_statistics.ML"
     "ML/ml_statistics_dummy.ML"
     "ML/ml_syntax.ML"
+    "ML/ml_system.ML"
     "PIDE/active.ML"
     "PIDE/command.ML"
     "PIDE/command_span.ML"
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -1,6 +1,14 @@
-(*** Isabelle/Pure bootstrap from "RAW" environment ***)
+(*** Isabelle/Pure bootstrap from RAW_ML_SYSTEM ***)
+
+(** bootstrap phase 0: Poly/ML setup **)
+
+(* initial ML name space *)
 
-(** bootstrap phase 0: towards ML within position context *)
+use "ML/ml_system.ML";
+use "ML/ml_name_space.ML";
+
+if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
+else use "ML/fixed_int_dummy.ML";
 
 structure Distribution =     (*filled-in by makedist*)
 struct
@@ -10,6 +18,87 @@
 end;
 
 
+(* multithreading *)
+
+use "General/exn.ML";
+
+val seconds = Time.fromReal;
+
+open Thread;
+use "Concurrent/multithreading.ML";
+
+use "Concurrent/unsynchronized.ML";
+val _ = PolyML.Compiler.forgetValue "ref";
+val _ = PolyML.Compiler.forgetType "ref";
+
+
+(* pervasive environment *)
+
+val _ = PolyML.Compiler.forgetValue "isSome";
+val _ = PolyML.Compiler.forgetValue "getOpt";
+val _ = PolyML.Compiler.forgetValue "valOf";
+val _ = PolyML.Compiler.forgetValue "foldl";
+val _ = PolyML.Compiler.forgetValue "foldr";
+val _ = PolyML.Compiler.forgetValue "print";
+val _ = PolyML.Compiler.forgetValue "explode";
+val _ = PolyML.Compiler.forgetValue "concat";
+
+val ord = SML90.ord;
+val chr = SML90.chr;
+val raw_explode = SML90.explode;
+val implode = SML90.implode;
+
+fun quit () = exit 0;
+
+
+(* ML runtime system *)
+
+use "ML/ml_heap.ML";
+use "ML/ml_profiling.ML";
+
+val pointer_eq = PolyML.pointerEq;
+
+
+(* ML toplevel pretty printing *)
+
+use "ML/ml_pretty.ML";
+
+local
+  val depth = Unsynchronized.ref 10;
+in
+  fun get_default_print_depth () = ! depth;
+  fun default_print_depth n = (depth := n; PolyML.print_depth n);
+  val _ = default_print_depth 10;
+end;
+
+val error_depth = PolyML.error_depth;
+
+
+(* ML compiler *)
+
+use "General/secure.ML";
+use "ML/ml_compiler0.ML";
+
+PolyML.Compiler.reportUnreferencedIds := true;
+PolyML.Compiler.reportExhaustiveHandlers := true;
+PolyML.Compiler.printInAlphabeticalOrder := false;
+PolyML.Compiler.maxInlineSize := 80;
+PolyML.Compiler.prompt1 := "ML> ";
+PolyML.Compiler.prompt2 := "ML# ";
+
+fun ml_make_string struct_name =
+  "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
+    struct_name ^ ".ML_print_depth ()))))))";
+
+
+(* ML debugger *)
+
+use_no_debug "ML/ml_debugger.ML";
+
+
+
+(** bootstrap phase 1: towards ML within position context *)
+
 (* library of general tools *)
 
 use "General/basics.ML";
@@ -52,7 +141,7 @@
 
 
 
-(** bootstrap phase 1: towards ML within Isar context *)
+(** bootstrap phase 2: towards ML within Isar context *)
 
 (* library of general tools *)
 
@@ -101,9 +190,7 @@
 
 use "ML/exn_properties.ML";
 
-if ML_System.name = "polyml-5.6"
-then use "ML/ml_statistics.ML"
-else use "ML/ml_statistics_dummy.ML";
+use "ML/ml_statistics.ML";
 
 use "Concurrent/standard_thread.ML";
 use "Concurrent/single_assignment.ML";
@@ -238,7 +325,7 @@
 
 
 
-(** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)
+(** bootstrap phase 3: towards Pure.thy and final ML toplevel setup *)
 
 (*basic proof engine*)
 use "par_tactical.ML";
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -310,7 +310,7 @@
 
 fun report_result ctxt pos ambig_msgs results =
   (case (proper_results results, failed_results results) of
-    ([], (reports, exn) :: _) => (Context_Position.reports_text ctxt reports; reraise exn)
+    ([], (reports, exn) :: _) => (Context_Position.reports_text ctxt reports; Exn.reraise exn)
   | ([(reports, x)], _) => (Context_Position.reports_text ctxt reports; x)
   | _ =>
       if null ambig_msgs then
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/System/invoke_scala.ML
--- a/src/Pure/System/invoke_scala.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/System/invoke_scala.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -63,7 +63,7 @@
   Isabelle_Process.protocol_command "Invoke_Scala.fulfill"
     (fn [id, tag, res] =>
       fulfill id tag res
-        handle exn => if Exn.is_interrupt exn then () else reraise exn);
+        handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
 
 end;
 
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/System/isabelle_process.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -188,7 +188,7 @@
 val init = uninterruptible (fn _ => fn socket =>
   let
     val _ = SHA1_Samples.test ()
-      handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); reraise exn);
+      handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
     val _ = Output.physical_stderr Symbol.STX;
 
     val _ = Printer.show_markup_default := true;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/System/system_channel.ML
--- a/src/Pure/System/system_channel.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/System/system_channel.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -32,8 +32,7 @@
   in read [] end;
 
 fun inputN (System_Channel (in_stream, _)) n =
-  if n = 0 then ""  (*workaround for polyml-5.5.1 or earlier*)
-  else Byte.bytesToString (BinIO.inputN (in_stream, n));
+  Byte.bytesToString (BinIO.inputN (in_stream, n));
 
 fun output (System_Channel (_, out_stream)) s =
   File.output out_stream s;
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 03 23:33:41 2016 +0100
@@ -54,7 +54,7 @@
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
   }
 
-  def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
+  def is_pure(name: String): Boolean = name == "Pure"
 
   def session_info(options: Options, select: Boolean, dir: Path,
       chapter: String, entry: Session_Entry): (String, Session_Info) =
@@ -581,33 +581,13 @@
       """
       . "$ISABELLE_HOME/lib/scripts/timestart.bash"
       """ +
-      (if (is_pure(name)) {
-        val ml_system = Isabelle_System.getenv("ML_SYSTEM")
-        val ml_system_base = Library.space_explode('-', ml_system).headOption getOrElse ml_system
-        val ml_root =
-          List(ml_system, ml_system_base).map(a => "RAW/ROOT_" + a + ".ML").
-            find(b => Path.explode("~~/src/Pure/" + b).file.isFile) getOrElse
-            error("Missing compatibility file for ML system " + quote(ml_system))
-
-        if (name == "RAW") {
-          """
-            rm -f "$OUTPUT"
-            "$ISABELLE_PROCESS" \
-              -e 'use """ + quote(ml_root) + """ handle _ => OS.Process.exit OS.Process.failure;' \
-              -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
-              -q RAW_ML_SYSTEM
-          """
-        }
-        else {
-          """
-            rm -f "$OUTPUT"
-            "$ISABELLE_PROCESS" \
-              -e '(use """ + quote(ml_root) + """; use "ROOT.ML") handle _ => OS.Process.exit OS.Process.failure;' \
-              -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
-              -q RAW_ML_SYSTEM
-          """
-        }
-      }
+      (if (is_pure(name))
+        """
+          rm -f "$OUTPUT"
+          "$ISABELLE_PROCESS" -f "ROOT.ML" \
+            -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
+            -q RAW_ML_SYSTEM
+        """
       else
         """
         rm -f "$OUTPUT"
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Tools/debugger.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -33,7 +33,7 @@
 
 fun error_wrapper e = e ()
   handle exn =>
-    if Exn.is_interrupt exn then reraise exn
+    if Exn.is_interrupt exn then Exn.reraise exn
     else error_message (Runtime.exn_message exn);
 
 
@@ -190,7 +190,8 @@
 
     fun print x =
       Pretty.from_ML
-        (ML_Name_Space.display_val (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
+        (ML_Pretty.from_polyml
+          (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space)));
     fun print_all () =
       #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
       |> sort_by #1 |> map (Pretty.item o single o print o #2)
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -405,7 +405,7 @@
         (case result of
           SOME promise => Future.fulfill promise reply
         | NONE => ()) (* FIXME handle protocol failure, just like in active.ML (!?) *)
-      end handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn)
+      end handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn)
 
 
 
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/build-jars	Thu Mar 03 23:33:41 2016 +0100
@@ -28,6 +28,7 @@
   General/antiquote.scala
   General/bytes.scala
   General/completion.scala
+  General/exn.scala
   General/file.scala
   General/graph.scala
   General/graph_display.scala
@@ -71,7 +72,6 @@
   PIDE/text.scala
   PIDE/xml.scala
   PIDE/yxml.scala
-  RAW/exn.scala
   ROOT.scala
   System/command_line.scala
   System/cygwin.scala
diff -r ff99681b3fd8 -r 922e702ae8ca src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Pure/morphism.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -52,7 +52,8 @@
 exception MORPHISM of string * exn;
 
 fun app (name, f) x = f x
-  handle exn => if Exn.is_interrupt exn then reraise exn else raise MORPHISM (name, exn);
+  handle exn =>
+    if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn);
 
 fun apply fs = fold_rev app fs;
 
diff -r ff99681b3fd8 -r 922e702ae8ca src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Tools/Code/code_ml.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -869,7 +869,7 @@
       check = { env_var = "ISABELLE_PROCESS",
         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
         make_command = fn _ =>
-          "\"$ISABELLE_PROCESS\" -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
+          "\"$ISABELLE_PROCESS\" -q -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
   #> Code_Target.add_language
     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
       check = { env_var = "ISABELLE_OCAML",
diff -r ff99681b3fd8 -r 922e702ae8ca src/Tools/try.ML
--- a/src/Tools/try.ML	Thu Mar 03 17:03:09 2016 +0100
+++ b/src/Tools/try.ML	Thu Mar 03 23:33:41 2016 +0100
@@ -114,7 +114,7 @@
                   (true, (_, outcome)) => List.app Output.information outcome
                 | _ => ())
               else ()
-            end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
+            end handle exn => if Exn.is_interrupt exn then Exn.reraise exn else ()}
       else NONE)