--- 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";
--- 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"
-
--- 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:
--- 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"
--- 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
--- 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 $_;
}
-
--- 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:
--- 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:
--- 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
--- 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.
--- 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}).
--- 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 =
--- 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
--- 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;
--- 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"
--- 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
--- 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);
--- 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);
--- 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
--- 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 _ =
--- 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)
--- 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 []}
--- 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;
--- 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;
--- 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 ()));
--- /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;
--- 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;
--- 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);
--- 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);
--- 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);
--- 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)) ())
--- /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;
--- 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);
--- /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;
--- /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)
+}
--- 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;
--- /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;
--- 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)));
--- 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 =
--- 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;
--- 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;
--- /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;
--- 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;
--- 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 =
--- /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;
--- /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;
--- /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;
--- /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;
--- /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;
--- /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;
--- /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;
--- 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
--- 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,
--- 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"
--- 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";
--- 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";
--- 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;
--- 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)
-}
--- 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;
--- 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;
--- 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;
--- 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;
--- 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
--- 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
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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
--- 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
--- 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;
-
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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"
--- 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";
--- 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
--- 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;
--- 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;
--- 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;
--- 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"
--- 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)
--- 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)
--- 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
--- 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;
--- 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",
--- 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)