--- a/Admin/Release/CHECKLIST Sun Feb 28 19:56:57 2016 +0100
+++ b/Admin/Release/CHECKLIST Sun Feb 28 21:20:51 2016 +0100
@@ -5,7 +5,7 @@
- check Admin/components;
-- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0;
+- test polyml-5.3.0;
- test 'display_drafts' command;
--- a/lib/scripts/run-polyml Sun Feb 28 19:56:57 2016 +0100
+++ b/lib/scripts/run-polyml Sun Feb 28 21:20:51 2016 +0100
@@ -1,8 +1,9 @@
#!/usr/bin/env bash
+# :mode=shellscript:
#
# Author: Makarius
#
-# Startup script for Poly/ML 5.1 ... 5.5.
+# Startup script for Poly/ML 5.6.
export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
@@ -39,12 +40,30 @@
## prepare databases
+case "$ML_PLATFORM" in
+ *-windows)
+ PLATFORM_INFILE="$(platform_path -m "$INFILE")"
+ PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
+ ;;
+ *)
+ PLATFORM_INFILE="$INFILE"
+ PLATFORM_OUTFILE="$OUTFILE"
+ ;;
+esac
+
if [ -z "$INFILE" ]; then
INIT=""
- EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+ case "$ML_PLATFORM" in
+ *-windows)
+ EXIT="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));"
+ ;;
+ *)
+ EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+ ;;
+ esac
else
check_file "$INFILE"
- INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
+ INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
EXIT=""
fi
@@ -52,7 +71,7 @@
MLEXIT=""
else
if [ -z "$INFILE" ]; then
- MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+ MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);"
else
MLEXIT="Session.save \"$OUTFILE\";"
fi
@@ -64,16 +83,22 @@
MLTEXT="$INIT $EXIT $MLTEXT"
-if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
+if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
+ "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
+ --error-exit </dev/null
+ RC="$?"
else
- FEEDER_OPTS="-q"
+ if [ -z "$TERMINATE" ]; then
+ FEEDER_OPTS=""
+ else
+ FEEDER_OPTS="-q"
+ ML_OPTIONS="$ML_OPTIONS --error-exit"
+ fi
+ "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+ { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+ RC="$?"
fi
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-RC="$?"
-
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
exit "$RC"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/run-polyml-5.3.0 Sun Feb 28 21:20:51 2016 +0100
@@ -0,0 +1,81 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# Startup script for Poly/ML 5.3.0.
+
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
+
+
+## diagnostics
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+function fail_out()
+{
+ fail "Unable to create output heap file: \"$OUTFILE\""
+}
+
+function check_file()
+{
+ [ ! -f "$1" ] && fail "Unable to locate \"$1\""
+}
+
+
+## compiler executables and libraries
+
+[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
+
+POLY="$ML_HOME/poly"
+check_file "$POLY"
+
+librarypath "$ML_HOME"
+
+
+
+## prepare databases
+
+if [ -z "$INFILE" ]; then
+ INIT=""
+ EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+else
+ check_file "$INFILE"
+ INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
+ EXIT=""
+fi
+
+if [ -z "$OUTFILE" ]; then
+ MLEXIT=""
+else
+ if [ -z "$INFILE" ]; then
+ MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+ else
+ MLEXIT="Session.save \"$OUTFILE\";"
+ fi
+ [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+fi
+
+
+## run it!
+
+MLTEXT="$INIT $EXIT $MLTEXT"
+
+if [ -z "$TERMINATE" ]; then
+ FEEDER_OPTS=""
+else
+ FEEDER_OPTS="-q"
+fi
+
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+ { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+RC="$?"
+
+[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+
+exit "$RC"
+
+#:wrap=soft:maxLineLen=100:
--- a/lib/scripts/run-polyml-5.5.1 Sun Feb 28 19:56:57 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-#!/usr/bin/env bash
-# :mode=shellscript:
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.5.1.
-
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-function fail_out()
-{
- fail "Unable to create output heap file: \"$OUTFILE\""
-}
-
-function check_file()
-{
- [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## compiler executables and libraries
-
-[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-librarypath "$ML_HOME"
-
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
- INIT=""
- EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-else
- check_file "$INFILE"
- INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
- EXIT=""
-fi
-
-if [ -z "$OUTFILE" ]; then
- MLEXIT=""
-else
- if [ -z "$INFILE" ]; then
- MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
- else
- MLEXIT="Session.save \"$OUTFILE\";"
- fi
- [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-fi
-
-
-## run it!
-
-MLTEXT="$INIT $EXIT $MLTEXT"
-
-if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
- "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
- --error-exit </dev/null
- RC="$?"
-else
- if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
- else
- FEEDER_OPTS="-q"
- ML_OPTIONS="$ML_OPTIONS --error-exit"
- fi
- "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
- RC="$?"
-fi
-
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100:
--- a/lib/scripts/run-polyml-5.5.2 Sun Feb 28 19:56:57 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-#!/usr/bin/env bash
-# :mode=shellscript:
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.5.2.
-
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-function fail_out()
-{
- fail "Unable to create output heap file: \"$OUTFILE\""
-}
-
-function check_file()
-{
- [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## compiler executables and libraries
-
-[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-librarypath "$ML_HOME"
-
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
- INIT=""
- EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-else
- check_file "$INFILE"
- INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
- EXIT=""
-fi
-
-if [ -z "$OUTFILE" ]; then
- MLEXIT=""
-else
- if [ -z "$INFILE" ]; then
- MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
- else
- MLEXIT="Session.save \"$OUTFILE\";"
- fi
- [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-fi
-
-
-## run it!
-
-MLTEXT="$INIT $EXIT $MLTEXT"
-
-if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
- "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
- --error-exit </dev/null
- RC="$?"
-else
- if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
- else
- FEEDER_OPTS="-q"
- ML_OPTIONS="$ML_OPTIONS --error-exit"
- fi
- "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
- RC="$?"
-fi
-
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100:
--- a/lib/scripts/run-polyml-5.6 Sun Feb 28 19:56:57 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-#!/usr/bin/env bash
-# :mode=shellscript:
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.6.
-
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-function fail_out()
-{
- fail "Unable to create output heap file: \"$OUTFILE\""
-}
-
-function check_file()
-{
- [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## compiler executables and libraries
-
-[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-librarypath "$ML_HOME"
-
-
-
-## prepare databases
-
-case "$ML_PLATFORM" in
- *-windows)
- PLATFORM_INFILE="$(platform_path -m "$INFILE")"
- PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
- ;;
- *)
- PLATFORM_INFILE="$INFILE"
- PLATFORM_OUTFILE="$OUTFILE"
- ;;
-esac
-
-if [ -z "$INFILE" ]; then
- INIT=""
- case "$ML_PLATFORM" in
- *-windows)
- EXIT="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));"
- ;;
- *)
- EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
- ;;
- esac
-else
- check_file "$INFILE"
- INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
- EXIT=""
-fi
-
-if [ -z "$OUTFILE" ]; then
- MLEXIT=""
-else
- if [ -z "$INFILE" ]; then
- MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);"
- else
- MLEXIT="Session.save \"$OUTFILE\";"
- fi
- [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-fi
-
-
-## run it!
-
-MLTEXT="$INIT $EXIT $MLTEXT"
-
-if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
- "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
- --error-exit </dev/null
- RC="$?"
-else
- if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
- else
- FEEDER_OPTS="-q"
- ML_OPTIONS="$ML_OPTIONS --error-exit"
- fi
- "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
- RC="$?"
-fi
-
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_statistics.ML Sun Feb 28 21:20:51 2016 +0100
@@ -0,0 +1,59 @@
+(* Title: Pure/ML/ml_statistics.ML
+ Author: Makarius
+
+ML runtime statistics for Poly/ML 5.5.0 or later.
+*)
+
+signature ML_STATISTICS =
+sig
+ val get: unit -> Properties.T
+end;
+
+structure ML_Statistics: ML_STATISTICS =
+struct
+
+fun get () =
+ let
+ val
+ {gcFullGCs,
+ gcPartialGCs,
+ sizeAllocation,
+ sizeAllocationFree,
+ sizeHeap,
+ sizeHeapFreeLastFullGC,
+ sizeHeapFreeLastGC,
+ threadsInML,
+ threadsTotal,
+ threadsWaitCondVar,
+ threadsWaitIO,
+ threadsWaitMutex,
+ threadsWaitSignal,
+ timeGCSystem,
+ timeGCUser,
+ timeNonGCSystem,
+ timeNonGCUser,
+ userCounters} = PolyML.Statistics.getLocalStats ();
+ val user_counters =
+ Vector.foldri
+ (fn (i, j, res) => ("user_counter" ^ Markup.print_int i, Markup.print_int j) :: res)
+ [] userCounters;
+ in
+ [("full_GCs", Markup.print_int gcFullGCs),
+ ("partial_GCs", Markup.print_int gcPartialGCs),
+ ("size_allocation", Markup.print_int sizeAllocation),
+ ("size_allocation_free", Markup.print_int sizeAllocationFree),
+ ("size_heap", Markup.print_int sizeHeap),
+ ("size_heap_free_last_full_GC", Markup.print_int sizeHeapFreeLastFullGC),
+ ("size_heap_free_last_GC", Markup.print_int sizeHeapFreeLastGC),
+ ("threads_in_ML", Markup.print_int threadsInML),
+ ("threads_total", Markup.print_int threadsTotal),
+ ("threads_wait_condvar", Markup.print_int threadsWaitCondVar),
+ ("threads_wait_IO", Markup.print_int threadsWaitIO),
+ ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
+ ("threads_wait_signal", Markup.print_int threadsWaitSignal),
+ ("time_CPU", Markup.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
+ ("time_GC", Markup.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
+ user_counters
+ end;
+
+end;
--- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML Sun Feb 28 19:56:57 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Title: Pure/ML/ml_statistics_polyml-5.5.0.ML
- Author: Makarius
-
-ML runtime statistics for Poly/ML 5.5.0.
-*)
-
-signature ML_STATISTICS =
-sig
- val get: unit -> Properties.T
-end;
-
-structure ML_Statistics: ML_STATISTICS =
-struct
-
-fun get () =
- let
- val
- {gcFullGCs,
- gcPartialGCs,
- sizeAllocation,
- sizeAllocationFree,
- sizeHeap,
- sizeHeapFreeLastFullGC,
- sizeHeapFreeLastGC,
- threadsInML,
- threadsTotal,
- threadsWaitCondVar,
- threadsWaitIO,
- threadsWaitMutex,
- threadsWaitSignal,
- timeGCSystem,
- timeGCUser,
- timeNonGCSystem,
- timeNonGCUser,
- userCounters} = PolyML.Statistics.getLocalStats ();
- val user_counters =
- Vector.foldri
- (fn (i, j, res) => ("user_counter" ^ Markup.print_int i, Markup.print_int j) :: res)
- [] userCounters;
- in
- [("full_GCs", Markup.print_int gcFullGCs),
- ("partial_GCs", Markup.print_int gcPartialGCs),
- ("size_allocation", Markup.print_int sizeAllocation),
- ("size_allocation_free", Markup.print_int sizeAllocationFree),
- ("size_heap", Markup.print_int sizeHeap),
- ("size_heap_free_last_full_GC", Markup.print_int sizeHeapFreeLastFullGC),
- ("size_heap_free_last_GC", Markup.print_int sizeHeapFreeLastGC),
- ("threads_in_ML", Markup.print_int threadsInML),
- ("threads_total", Markup.print_int threadsTotal),
- ("threads_wait_condvar", Markup.print_int threadsWaitCondVar),
- ("threads_wait_IO", Markup.print_int threadsWaitIO),
- ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
- ("threads_wait_signal", Markup.print_int threadsWaitSignal),
- ("time_CPU", Markup.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
- ("time_GC", Markup.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
- user_counters
- end;
-
-end;
-
--- a/src/Pure/RAW/ROOT_polyml-5.5.2.ML Sun Feb 28 19:56:57 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(* Title: Pure/RAW/ROOT_polyml-5.5.2.ML
- Author: Makarius
-
-Compatibility wrapper for Poly/ML 5.5.2.
-*)
-
-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 Sun Feb 28 19:56:57 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML Sun Feb 28 21:20:51 2016 +0100
@@ -59,13 +59,9 @@
use "RAW/exn.ML";
-fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
-
-if ML_System.name = "polyml-5.5.1"
- orelse ML_System.name = "polyml-5.5.2"
- orelse ML_System.name = "polyml-5.6"
-then use "RAW/exn_trace_polyml-5.5.1.ML"
-else ();
+if ML_System.name = "polyml-5.6"
+then use "RAW/exn_trace.ML"
+else use "RAW/exn_trace_dummy.ML";
(* multithreading *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/exn_trace.ML Sun Feb 28 21:20:51 2016 +0100
@@ -0,0 +1,15 @@
+(* 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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/exn_trace_dummy.ML Sun Feb 28 21:20:51 2016 +0100
@@ -0,0 +1,7 @@
+(* Title: Pure/RAW/exn_trace.ML
+ Author: Makarius
+
+Exception trace dummy.
+*)
+
+fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
--- a/src/Pure/RAW/exn_trace_polyml-5.5.1.ML Sun Feb 28 19:56:57 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Pure/RAW/exn_trace_polyml-5.5.1.ML
- Author: Makarius
-
-Exception trace for Poly/ML 5.5.1 via ML output.
-*)
-
-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/ROOT Sun Feb 28 19:56:57 2016 +0100
+++ b/src/Pure/ROOT Sun Feb 28 21:20:51 2016 +0100
@@ -3,12 +3,12 @@
session RAW =
theories
files
- "RAW/ROOT_polyml-5.5.2.ML"
"RAW/ROOT_polyml-5.6.ML"
"RAW/ROOT_polyml.ML"
"RAW/compiler_polyml.ML"
"RAW/exn.ML"
- "RAW/exn_trace_polyml-5.5.1.ML"
+ "RAW/exn_trace.ML"
+ "RAW/exn_trace_dummy.ML"
"RAW/fixed_int_dummy.ML"
"RAW/ml_compiler_parameters.ML"
"RAW/ml_compiler_parameters_polyml-5.6.ML"
@@ -35,12 +35,12 @@
session Pure =
global_theories Pure
files
- "RAW/ROOT_polyml-5.5.2.ML"
"RAW/ROOT_polyml-5.6.ML"
"RAW/ROOT_polyml.ML"
"RAW/compiler_polyml.ML"
"RAW/exn.ML"
- "RAW/exn_trace_polyml-5.5.1.ML"
+ "RAW/exn_trace.ML"
+ "RAW/exn_trace_dummy.ML"
"RAW/fixed_int_dummy.ML"
"RAW/ml_compiler_parameters.ML"
"RAW/ml_compiler_parameters_polyml-5.6.ML"
@@ -169,8 +169,8 @@
"ML/ml_lex.ML"
"ML/ml_options.ML"
"ML/ml_parse.ML"
+ "ML/ml_statistics.ML"
"ML/ml_statistics_dummy.ML"
- "ML/ml_statistics_polyml-5.5.0.ML"
"ML/ml_syntax.ML"
"PIDE/active.ML"
"PIDE/command.ML"
--- a/src/Pure/ROOT.ML Sun Feb 28 19:56:57 2016 +0100
+++ b/src/Pure/ROOT.ML Sun Feb 28 21:20:51 2016 +0100
@@ -96,11 +96,8 @@
use "ML/exn_properties.ML";
-if ML_System.name = "polyml-5.5.0"
- orelse ML_System.name = "polyml-5.5.1"
- orelse ML_System.name = "polyml-5.5.2"
- orelse ML_System.name = "polyml-5.6"
-then use "ML/ml_statistics_polyml-5.5.0.ML"
+if ML_System.name = "polyml-5.6"
+then use "ML/ml_statistics.ML"
else use "ML/ml_statistics_dummy.ML";
use "Concurrent/standard_thread.ML";