support only polyml-5.3.0 and polyml-5.6;
authorwenzelm
Sun Feb 28 21:20:51 2016 +0100 (2016-02-28)
changeset 624597a5d88dd8cc9
parent 62456 11e06f5283bc
child 62460 4b2018eb92e8
support only polyml-5.3.0 and polyml-5.6;
Admin/Release/CHECKLIST
lib/scripts/run-polyml
lib/scripts/run-polyml-5.3.0
lib/scripts/run-polyml-5.5.1
lib/scripts/run-polyml-5.5.2
lib/scripts/run-polyml-5.6
src/Pure/ML/ml_statistics.ML
src/Pure/ML/ml_statistics_polyml-5.5.0.ML
src/Pure/RAW/ROOT_polyml-5.5.2.ML
src/Pure/RAW/ROOT_polyml.ML
src/Pure/RAW/exn_trace.ML
src/Pure/RAW/exn_trace_dummy.ML
src/Pure/RAW/exn_trace_polyml-5.5.1.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/Admin/Release/CHECKLIST	Sun Feb 28 19:56:57 2016 +0100
     1.2 +++ b/Admin/Release/CHECKLIST	Sun Feb 28 21:20:51 2016 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  - check Admin/components;
     1.6  
     1.7 -- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0;
     1.8 +- test polyml-5.3.0;
     1.9  
    1.10  - test 'display_drafts' command;
    1.11  
     2.1 --- a/lib/scripts/run-polyml	Sun Feb 28 19:56:57 2016 +0100
     2.2 +++ b/lib/scripts/run-polyml	Sun Feb 28 21:20:51 2016 +0100
     2.3 @@ -1,8 +1,9 @@
     2.4  #!/usr/bin/env bash
     2.5 +# :mode=shellscript:
     2.6  #
     2.7  # Author: Makarius
     2.8  #
     2.9 -# Startup script for Poly/ML 5.1 ... 5.5.
    2.10 +# Startup script for Poly/ML 5.6.
    2.11  
    2.12  export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
    2.13  
    2.14 @@ -39,12 +40,30 @@
    2.15  
    2.16  ## prepare databases
    2.17  
    2.18 +case "$ML_PLATFORM" in
    2.19 +  *-windows)
    2.20 +    PLATFORM_INFILE="$(platform_path -m "$INFILE")"
    2.21 +    PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
    2.22 +    ;;
    2.23 +  *)
    2.24 +    PLATFORM_INFILE="$INFILE"
    2.25 +    PLATFORM_OUTFILE="$OUTFILE"
    2.26 +    ;;
    2.27 +esac
    2.28 +
    2.29  if [ -z "$INFILE" ]; then
    2.30    INIT=""
    2.31 -  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    2.32 +  case "$ML_PLATFORM" in
    2.33 +    *-windows)
    2.34 +      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));"
    2.35 +      ;;
    2.36 +    *)
    2.37 +      EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    2.38 +      ;;
    2.39 +  esac
    2.40  else
    2.41    check_file "$INFILE"
    2.42 -  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));"
    2.43 +  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));"
    2.44    EXIT=""
    2.45  fi
    2.46  
    2.47 @@ -52,7 +71,7 @@
    2.48    MLEXIT=""
    2.49  else
    2.50    if [ -z "$INFILE" ]; then
    2.51 -    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);"
    2.52 +    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);"
    2.53    else
    2.54      MLEXIT="Session.save \"$OUTFILE\";"
    2.55    fi
    2.56 @@ -64,16 +83,22 @@
    2.57  
    2.58  MLTEXT="$INIT $EXIT $MLTEXT"
    2.59  
    2.60 -if [ -z "$TERMINATE" ]; then
    2.61 -  FEEDER_OPTS=""
    2.62 +if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
    2.63 +  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
    2.64 +    --error-exit </dev/null
    2.65 +  RC="$?"
    2.66  else
    2.67 -  FEEDER_OPTS="-q"
    2.68 +  if [ -z "$TERMINATE" ]; then
    2.69 +    FEEDER_OPTS=""
    2.70 +  else
    2.71 +    FEEDER_OPTS="-q"
    2.72 +    ML_OPTIONS="$ML_OPTIONS --error-exit"
    2.73 +  fi
    2.74 +  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    2.75 +    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    2.76 +  RC="$?"
    2.77  fi
    2.78  
    2.79 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    2.80 -  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    2.81 -RC="$?"
    2.82 -
    2.83  [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    2.84  
    2.85  exit "$RC"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/lib/scripts/run-polyml-5.3.0	Sun Feb 28 21:20:51 2016 +0100
     3.3 @@ -0,0 +1,81 @@
     3.4 +#!/usr/bin/env bash
     3.5 +#
     3.6 +# Author: Makarius
     3.7 +#
     3.8 +# Startup script for Poly/ML 5.3.0.
     3.9 +
    3.10 +export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
    3.11 +
    3.12 +
    3.13 +## diagnostics
    3.14 +
    3.15 +function fail()
    3.16 +{
    3.17 +  echo "$1" >&2
    3.18 +  exit 2
    3.19 +}
    3.20 +
    3.21 +function fail_out()
    3.22 +{
    3.23 +  fail "Unable to create output heap file: \"$OUTFILE\""
    3.24 +}
    3.25 +
    3.26 +function check_file()
    3.27 +{
    3.28 +  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    3.29 +}
    3.30 +
    3.31 +
    3.32 +## compiler executables and libraries
    3.33 +
    3.34 +[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
    3.35 +
    3.36 +POLY="$ML_HOME/poly"
    3.37 +check_file "$POLY"
    3.38 +
    3.39 +librarypath "$ML_HOME"
    3.40 +
    3.41 +
    3.42 +
    3.43 +## prepare databases
    3.44 +
    3.45 +if [ -z "$INFILE" ]; then
    3.46 +  INIT=""
    3.47 +  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    3.48 +else
    3.49 +  check_file "$INFILE"
    3.50 +  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));"
    3.51 +  EXIT=""
    3.52 +fi
    3.53 +
    3.54 +if [ -z "$OUTFILE" ]; then
    3.55 +  MLEXIT=""
    3.56 +else
    3.57 +  if [ -z "$INFILE" ]; then
    3.58 +    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);"
    3.59 +  else
    3.60 +    MLEXIT="Session.save \"$OUTFILE\";"
    3.61 +  fi
    3.62 +  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    3.63 +fi
    3.64 +
    3.65 +
    3.66 +## run it!
    3.67 +
    3.68 +MLTEXT="$INIT $EXIT $MLTEXT"
    3.69 +
    3.70 +if [ -z "$TERMINATE" ]; then
    3.71 +  FEEDER_OPTS=""
    3.72 +else
    3.73 +  FEEDER_OPTS="-q"
    3.74 +fi
    3.75 +
    3.76 +"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    3.77 +  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    3.78 +RC="$?"
    3.79 +
    3.80 +[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    3.81 +
    3.82 +exit "$RC"
    3.83 +
    3.84 +#:wrap=soft:maxLineLen=100:
     4.1 --- a/lib/scripts/run-polyml-5.5.1	Sun Feb 28 19:56:57 2016 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,88 +0,0 @@
     4.4 -#!/usr/bin/env bash
     4.5 -# :mode=shellscript:
     4.6 -#
     4.7 -# Author: Makarius
     4.8 -#
     4.9 -# Startup script for Poly/ML 5.5.1.
    4.10 -
    4.11 -export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
    4.12 -
    4.13 -
    4.14 -## diagnostics
    4.15 -
    4.16 -function fail()
    4.17 -{
    4.18 -  echo "$1" >&2
    4.19 -  exit 2
    4.20 -}
    4.21 -
    4.22 -function fail_out()
    4.23 -{
    4.24 -  fail "Unable to create output heap file: \"$OUTFILE\""
    4.25 -}
    4.26 -
    4.27 -function check_file()
    4.28 -{
    4.29 -  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    4.30 -}
    4.31 -
    4.32 -
    4.33 -## compiler executables and libraries
    4.34 -
    4.35 -[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
    4.36 -
    4.37 -POLY="$ML_HOME/poly"
    4.38 -check_file "$POLY"
    4.39 -
    4.40 -librarypath "$ML_HOME"
    4.41 -
    4.42 -
    4.43 -
    4.44 -## prepare databases
    4.45 -
    4.46 -if [ -z "$INFILE" ]; then
    4.47 -  INIT=""
    4.48 -  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    4.49 -else
    4.50 -  check_file "$INFILE"
    4.51 -  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));"
    4.52 -  EXIT=""
    4.53 -fi
    4.54 -
    4.55 -if [ -z "$OUTFILE" ]; then
    4.56 -  MLEXIT=""
    4.57 -else
    4.58 -  if [ -z "$INFILE" ]; then
    4.59 -    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);"
    4.60 -  else
    4.61 -    MLEXIT="Session.save \"$OUTFILE\";"
    4.62 -  fi
    4.63 -  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    4.64 -fi
    4.65 -
    4.66 -
    4.67 -## run it!
    4.68 -
    4.69 -MLTEXT="$INIT $EXIT $MLTEXT"
    4.70 -
    4.71 -if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
    4.72 -  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
    4.73 -    --error-exit </dev/null
    4.74 -  RC="$?"
    4.75 -else
    4.76 -  if [ -z "$TERMINATE" ]; then
    4.77 -    FEEDER_OPTS=""
    4.78 -  else
    4.79 -    FEEDER_OPTS="-q"
    4.80 -    ML_OPTIONS="$ML_OPTIONS --error-exit"
    4.81 -  fi
    4.82 -  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    4.83 -    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    4.84 -  RC="$?"
    4.85 -fi
    4.86 -
    4.87 -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    4.88 -
    4.89 -exit "$RC"
    4.90 -
    4.91 -#:wrap=soft:maxLineLen=100:
     5.1 --- a/lib/scripts/run-polyml-5.5.2	Sun Feb 28 19:56:57 2016 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,88 +0,0 @@
     5.4 -#!/usr/bin/env bash
     5.5 -# :mode=shellscript:
     5.6 -#
     5.7 -# Author: Makarius
     5.8 -#
     5.9 -# Startup script for Poly/ML 5.5.2.
    5.10 -
    5.11 -export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
    5.12 -
    5.13 -
    5.14 -## diagnostics
    5.15 -
    5.16 -function fail()
    5.17 -{
    5.18 -  echo "$1" >&2
    5.19 -  exit 2
    5.20 -}
    5.21 -
    5.22 -function fail_out()
    5.23 -{
    5.24 -  fail "Unable to create output heap file: \"$OUTFILE\""
    5.25 -}
    5.26 -
    5.27 -function check_file()
    5.28 -{
    5.29 -  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    5.30 -}
    5.31 -
    5.32 -
    5.33 -## compiler executables and libraries
    5.34 -
    5.35 -[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
    5.36 -
    5.37 -POLY="$ML_HOME/poly"
    5.38 -check_file "$POLY"
    5.39 -
    5.40 -librarypath "$ML_HOME"
    5.41 -
    5.42 -
    5.43 -
    5.44 -## prepare databases
    5.45 -
    5.46 -if [ -z "$INFILE" ]; then
    5.47 -  INIT=""
    5.48 -  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    5.49 -else
    5.50 -  check_file "$INFILE"
    5.51 -  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));"
    5.52 -  EXIT=""
    5.53 -fi
    5.54 -
    5.55 -if [ -z "$OUTFILE" ]; then
    5.56 -  MLEXIT=""
    5.57 -else
    5.58 -  if [ -z "$INFILE" ]; then
    5.59 -    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);"
    5.60 -  else
    5.61 -    MLEXIT="Session.save \"$OUTFILE\";"
    5.62 -  fi
    5.63 -  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    5.64 -fi
    5.65 -
    5.66 -
    5.67 -## run it!
    5.68 -
    5.69 -MLTEXT="$INIT $EXIT $MLTEXT"
    5.70 -
    5.71 -if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
    5.72 -  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
    5.73 -    --error-exit </dev/null
    5.74 -  RC="$?"
    5.75 -else
    5.76 -  if [ -z "$TERMINATE" ]; then
    5.77 -    FEEDER_OPTS=""
    5.78 -  else
    5.79 -    FEEDER_OPTS="-q"
    5.80 -    ML_OPTIONS="$ML_OPTIONS --error-exit"
    5.81 -  fi
    5.82 -  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    5.83 -    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    5.84 -  RC="$?"
    5.85 -fi
    5.86 -
    5.87 -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    5.88 -
    5.89 -exit "$RC"
    5.90 -
    5.91 -#:wrap=soft:maxLineLen=100:
     6.1 --- a/lib/scripts/run-polyml-5.6	Sun Feb 28 19:56:57 2016 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,106 +0,0 @@
     6.4 -#!/usr/bin/env bash
     6.5 -# :mode=shellscript:
     6.6 -#
     6.7 -# Author: Makarius
     6.8 -#
     6.9 -# Startup script for Poly/ML 5.6.
    6.10 -
    6.11 -export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
    6.12 -
    6.13 -
    6.14 -## diagnostics
    6.15 -
    6.16 -function fail()
    6.17 -{
    6.18 -  echo "$1" >&2
    6.19 -  exit 2
    6.20 -}
    6.21 -
    6.22 -function fail_out()
    6.23 -{
    6.24 -  fail "Unable to create output heap file: \"$OUTFILE\""
    6.25 -}
    6.26 -
    6.27 -function check_file()
    6.28 -{
    6.29 -  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    6.30 -}
    6.31 -
    6.32 -
    6.33 -## compiler executables and libraries
    6.34 -
    6.35 -[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
    6.36 -
    6.37 -POLY="$ML_HOME/poly"
    6.38 -check_file "$POLY"
    6.39 -
    6.40 -librarypath "$ML_HOME"
    6.41 -
    6.42 -
    6.43 -
    6.44 -## prepare databases
    6.45 -
    6.46 -case "$ML_PLATFORM" in
    6.47 -  *-windows)
    6.48 -    PLATFORM_INFILE="$(platform_path -m "$INFILE")"
    6.49 -    PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
    6.50 -    ;;
    6.51 -  *)
    6.52 -    PLATFORM_INFILE="$INFILE"
    6.53 -    PLATFORM_OUTFILE="$OUTFILE"
    6.54 -    ;;
    6.55 -esac
    6.56 -
    6.57 -if [ -z "$INFILE" ]; then
    6.58 -  INIT=""
    6.59 -  case "$ML_PLATFORM" in
    6.60 -    *-windows)
    6.61 -      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));"
    6.62 -      ;;
    6.63 -    *)
    6.64 -      EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    6.65 -      ;;
    6.66 -  esac
    6.67 -else
    6.68 -  check_file "$INFILE"
    6.69 -  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));"
    6.70 -  EXIT=""
    6.71 -fi
    6.72 -
    6.73 -if [ -z "$OUTFILE" ]; then
    6.74 -  MLEXIT=""
    6.75 -else
    6.76 -  if [ -z "$INFILE" ]; then
    6.77 -    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);"
    6.78 -  else
    6.79 -    MLEXIT="Session.save \"$OUTFILE\";"
    6.80 -  fi
    6.81 -  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    6.82 -fi
    6.83 -
    6.84 -
    6.85 -## run it!
    6.86 -
    6.87 -MLTEXT="$INIT $EXIT $MLTEXT"
    6.88 -
    6.89 -if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
    6.90 -  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
    6.91 -    --error-exit </dev/null
    6.92 -  RC="$?"
    6.93 -else
    6.94 -  if [ -z "$TERMINATE" ]; then
    6.95 -    FEEDER_OPTS=""
    6.96 -  else
    6.97 -    FEEDER_OPTS="-q"
    6.98 -    ML_OPTIONS="$ML_OPTIONS --error-exit"
    6.99 -  fi
   6.100 -  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
   6.101 -    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
   6.102 -  RC="$?"
   6.103 -fi
   6.104 -
   6.105 -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
   6.106 -
   6.107 -exit "$RC"
   6.108 -
   6.109 -#:wrap=soft:maxLineLen=100:
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/ML/ml_statistics.ML	Sun Feb 28 21:20:51 2016 +0100
     7.3 @@ -0,0 +1,59 @@
     7.4 +(*  Title:      Pure/ML/ml_statistics.ML
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +ML runtime statistics for Poly/ML 5.5.0 or later.
     7.8 +*)
     7.9 +
    7.10 +signature ML_STATISTICS =
    7.11 +sig
    7.12 +  val get: unit -> Properties.T
    7.13 +end;
    7.14 +
    7.15 +structure ML_Statistics: ML_STATISTICS =
    7.16 +struct
    7.17 +
    7.18 +fun get () =
    7.19 +  let
    7.20 +    val
    7.21 +     {gcFullGCs,
    7.22 +      gcPartialGCs,
    7.23 +      sizeAllocation,
    7.24 +      sizeAllocationFree,
    7.25 +      sizeHeap,
    7.26 +      sizeHeapFreeLastFullGC,
    7.27 +      sizeHeapFreeLastGC,
    7.28 +      threadsInML,
    7.29 +      threadsTotal,
    7.30 +      threadsWaitCondVar,
    7.31 +      threadsWaitIO,
    7.32 +      threadsWaitMutex,
    7.33 +      threadsWaitSignal,
    7.34 +      timeGCSystem,
    7.35 +      timeGCUser,
    7.36 +      timeNonGCSystem,
    7.37 +      timeNonGCUser,
    7.38 +      userCounters} = PolyML.Statistics.getLocalStats ();
    7.39 +    val user_counters =
    7.40 +      Vector.foldri
    7.41 +        (fn (i, j, res) => ("user_counter" ^ Markup.print_int i, Markup.print_int j) :: res)
    7.42 +        [] userCounters;
    7.43 +  in
    7.44 +    [("full_GCs", Markup.print_int gcFullGCs),
    7.45 +     ("partial_GCs", Markup.print_int gcPartialGCs),
    7.46 +     ("size_allocation", Markup.print_int sizeAllocation),
    7.47 +     ("size_allocation_free", Markup.print_int sizeAllocationFree),
    7.48 +     ("size_heap", Markup.print_int sizeHeap),
    7.49 +     ("size_heap_free_last_full_GC", Markup.print_int sizeHeapFreeLastFullGC),
    7.50 +     ("size_heap_free_last_GC", Markup.print_int sizeHeapFreeLastGC),
    7.51 +     ("threads_in_ML", Markup.print_int threadsInML),
    7.52 +     ("threads_total", Markup.print_int threadsTotal),
    7.53 +     ("threads_wait_condvar", Markup.print_int threadsWaitCondVar),
    7.54 +     ("threads_wait_IO", Markup.print_int threadsWaitIO),
    7.55 +     ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
    7.56 +     ("threads_wait_signal", Markup.print_int threadsWaitSignal),
    7.57 +     ("time_CPU", Markup.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
    7.58 +     ("time_GC", Markup.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
    7.59 +    user_counters
    7.60 +  end;
    7.61 +
    7.62 +end;
     8.1 --- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Sun Feb 28 19:56:57 2016 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,60 +0,0 @@
     8.4 -(*  Title:      Pure/ML/ml_statistics_polyml-5.5.0.ML
     8.5 -    Author:     Makarius
     8.6 -
     8.7 -ML runtime statistics for Poly/ML 5.5.0.
     8.8 -*)
     8.9 -
    8.10 -signature ML_STATISTICS =
    8.11 -sig
    8.12 -  val get: unit -> Properties.T
    8.13 -end;
    8.14 -
    8.15 -structure ML_Statistics: ML_STATISTICS =
    8.16 -struct
    8.17 -
    8.18 -fun get () =
    8.19 -  let
    8.20 -    val
    8.21 -     {gcFullGCs,
    8.22 -      gcPartialGCs,
    8.23 -      sizeAllocation,
    8.24 -      sizeAllocationFree,
    8.25 -      sizeHeap,
    8.26 -      sizeHeapFreeLastFullGC,
    8.27 -      sizeHeapFreeLastGC,
    8.28 -      threadsInML,
    8.29 -      threadsTotal,
    8.30 -      threadsWaitCondVar,
    8.31 -      threadsWaitIO,
    8.32 -      threadsWaitMutex,
    8.33 -      threadsWaitSignal,
    8.34 -      timeGCSystem,
    8.35 -      timeGCUser,
    8.36 -      timeNonGCSystem,
    8.37 -      timeNonGCUser,
    8.38 -      userCounters} = PolyML.Statistics.getLocalStats ();
    8.39 -    val user_counters =
    8.40 -      Vector.foldri
    8.41 -        (fn (i, j, res) => ("user_counter" ^ Markup.print_int i, Markup.print_int j) :: res)
    8.42 -        [] userCounters;
    8.43 -  in
    8.44 -    [("full_GCs", Markup.print_int gcFullGCs),
    8.45 -     ("partial_GCs", Markup.print_int gcPartialGCs),
    8.46 -     ("size_allocation", Markup.print_int sizeAllocation),
    8.47 -     ("size_allocation_free", Markup.print_int sizeAllocationFree),
    8.48 -     ("size_heap", Markup.print_int sizeHeap),
    8.49 -     ("size_heap_free_last_full_GC", Markup.print_int sizeHeapFreeLastFullGC),
    8.50 -     ("size_heap_free_last_GC", Markup.print_int sizeHeapFreeLastGC),
    8.51 -     ("threads_in_ML", Markup.print_int threadsInML),
    8.52 -     ("threads_total", Markup.print_int threadsTotal),
    8.53 -     ("threads_wait_condvar", Markup.print_int threadsWaitCondVar),
    8.54 -     ("threads_wait_IO", Markup.print_int threadsWaitIO),
    8.55 -     ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
    8.56 -     ("threads_wait_signal", Markup.print_int threadsWaitSignal),
    8.57 -     ("time_CPU", Markup.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
    8.58 -     ("time_GC", Markup.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
    8.59 -    user_counters
    8.60 -  end;
    8.61 -
    8.62 -end;
    8.63 -
     9.1 --- a/src/Pure/RAW/ROOT_polyml-5.5.2.ML	Sun Feb 28 19:56:57 2016 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,23 +0,0 @@
     9.4 -(*  Title:      Pure/RAW/ROOT_polyml-5.5.2.ML
     9.5 -    Author:     Makarius
     9.6 -
     9.7 -Compatibility wrapper for Poly/ML 5.5.2.
     9.8 -*)
     9.9 -
    9.10 -structure Thread =
    9.11 -struct
    9.12 -  open Thread;
    9.13 -
    9.14 -  structure Thread =
    9.15 -  struct
    9.16 -    open Thread;
    9.17 -
    9.18 -    fun numProcessors () =
    9.19 -      (case Thread.numPhysicalProcessors () of
    9.20 -        SOME n => n
    9.21 -      | NONE => Thread.numProcessors ());
    9.22 -  end;
    9.23 -end;
    9.24 -
    9.25 -use "RAW/ROOT_polyml.ML";
    9.26 -
    10.1 --- a/src/Pure/RAW/ROOT_polyml.ML	Sun Feb 28 19:56:57 2016 +0100
    10.2 +++ b/src/Pure/RAW/ROOT_polyml.ML	Sun Feb 28 21:20:51 2016 +0100
    10.3 @@ -59,13 +59,9 @@
    10.4  
    10.5  use "RAW/exn.ML";
    10.6  
    10.7 -fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
    10.8 -
    10.9 -if ML_System.name = "polyml-5.5.1"
   10.10 -  orelse ML_System.name = "polyml-5.5.2"
   10.11 -  orelse ML_System.name = "polyml-5.6"
   10.12 -then use "RAW/exn_trace_polyml-5.5.1.ML"
   10.13 -else ();
   10.14 +if ML_System.name = "polyml-5.6"
   10.15 +then use "RAW/exn_trace.ML"
   10.16 +else use "RAW/exn_trace_dummy.ML";
   10.17  
   10.18  
   10.19  (* multithreading *)
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Pure/RAW/exn_trace.ML	Sun Feb 28 21:20:51 2016 +0100
    11.3 @@ -0,0 +1,15 @@
    11.4 +(*  Title:      Pure/RAW/exn_trace.ML
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +Exception trace via ML output, for Poly/ML 5.5.1 or later.
    11.8 +*)
    11.9 +
   11.10 +fun print_exception_trace exn_message output e =
   11.11 +  PolyML.Exception.traceException
   11.12 +    (e, fn (trace, exn) =>
   11.13 +      let
   11.14 +        val title = "Exception trace - " ^ exn_message exn;
   11.15 +        val _ = output (String.concatWith "\n" (title :: trace));
   11.16 +      in reraise exn end);
   11.17 +
   11.18 +PolyML.Compiler.reportExhaustiveHandlers := true;
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Pure/RAW/exn_trace_dummy.ML	Sun Feb 28 21:20:51 2016 +0100
    12.3 @@ -0,0 +1,7 @@
    12.4 +(*  Title:      Pure/RAW/exn_trace.ML
    12.5 +    Author:     Makarius
    12.6 +
    12.7 +Exception trace dummy.
    12.8 +*)
    12.9 +
   12.10 +fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
    13.1 --- a/src/Pure/RAW/exn_trace_polyml-5.5.1.ML	Sun Feb 28 19:56:57 2016 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,16 +0,0 @@
    13.4 -(*  Title:      Pure/RAW/exn_trace_polyml-5.5.1.ML
    13.5 -    Author:     Makarius
    13.6 -
    13.7 -Exception trace for Poly/ML 5.5.1 via ML output.
    13.8 -*)
    13.9 -
   13.10 -fun print_exception_trace exn_message output e =
   13.11 -  PolyML.Exception.traceException
   13.12 -    (e, fn (trace, exn) =>
   13.13 -      let
   13.14 -        val title = "Exception trace - " ^ exn_message exn;
   13.15 -        val _ = output (String.concatWith "\n" (title :: trace));
   13.16 -      in reraise exn end);
   13.17 -
   13.18 -PolyML.Compiler.reportExhaustiveHandlers := true;
   13.19 -
    14.1 --- a/src/Pure/ROOT	Sun Feb 28 19:56:57 2016 +0100
    14.2 +++ b/src/Pure/ROOT	Sun Feb 28 21:20:51 2016 +0100
    14.3 @@ -3,12 +3,12 @@
    14.4  session RAW =
    14.5    theories
    14.6    files
    14.7 -    "RAW/ROOT_polyml-5.5.2.ML"
    14.8      "RAW/ROOT_polyml-5.6.ML"
    14.9      "RAW/ROOT_polyml.ML"
   14.10      "RAW/compiler_polyml.ML"
   14.11      "RAW/exn.ML"
   14.12 -    "RAW/exn_trace_polyml-5.5.1.ML"
   14.13 +    "RAW/exn_trace.ML"
   14.14 +    "RAW/exn_trace_dummy.ML"
   14.15      "RAW/fixed_int_dummy.ML"
   14.16      "RAW/ml_compiler_parameters.ML"
   14.17      "RAW/ml_compiler_parameters_polyml-5.6.ML"
   14.18 @@ -35,12 +35,12 @@
   14.19  session Pure =
   14.20    global_theories Pure
   14.21    files
   14.22 -    "RAW/ROOT_polyml-5.5.2.ML"
   14.23      "RAW/ROOT_polyml-5.6.ML"
   14.24      "RAW/ROOT_polyml.ML"
   14.25      "RAW/compiler_polyml.ML"
   14.26      "RAW/exn.ML"
   14.27 -    "RAW/exn_trace_polyml-5.5.1.ML"
   14.28 +    "RAW/exn_trace.ML"
   14.29 +    "RAW/exn_trace_dummy.ML"
   14.30      "RAW/fixed_int_dummy.ML"
   14.31      "RAW/ml_compiler_parameters.ML"
   14.32      "RAW/ml_compiler_parameters_polyml-5.6.ML"
   14.33 @@ -169,8 +169,8 @@
   14.34      "ML/ml_lex.ML"
   14.35      "ML/ml_options.ML"
   14.36      "ML/ml_parse.ML"
   14.37 +    "ML/ml_statistics.ML"
   14.38      "ML/ml_statistics_dummy.ML"
   14.39 -    "ML/ml_statistics_polyml-5.5.0.ML"
   14.40      "ML/ml_syntax.ML"
   14.41      "PIDE/active.ML"
   14.42      "PIDE/command.ML"
    15.1 --- a/src/Pure/ROOT.ML	Sun Feb 28 19:56:57 2016 +0100
    15.2 +++ b/src/Pure/ROOT.ML	Sun Feb 28 21:20:51 2016 +0100
    15.3 @@ -96,11 +96,8 @@
    15.4  
    15.5  use "ML/exn_properties.ML";
    15.6  
    15.7 -if ML_System.name = "polyml-5.5.0"
    15.8 -  orelse ML_System.name = "polyml-5.5.1"
    15.9 -  orelse ML_System.name = "polyml-5.5.2"
   15.10 -  orelse ML_System.name = "polyml-5.6"
   15.11 -then use "ML/ml_statistics_polyml-5.5.0.ML"
   15.12 +if ML_System.name = "polyml-5.6"
   15.13 +then use "ML/ml_statistics.ML"
   15.14  else use "ML/ml_statistics_dummy.ML";
   15.15  
   15.16  use "Concurrent/standard_thread.ML";