SML/NJ is no longer supported;
authorwenzelm
Wed Feb 17 23:06:24 2016 +0100 (19 months ago)
changeset 62354fdd6989cc8a0
parent 62341 a594429637fd
child 62355 00f7618a9f2b
SML/NJ is no longer supported;
Admin/Release/CHECKLIST
Admin/isatest/isatest-makeall
Admin/isatest/isatest-makedist
Admin/isatest/isatest-stats
Admin/isatest/settings/at-sml-dev-e
NEWS
etc/settings
lib/scripts/getsettings
lib/scripts/run-smlnj
src/Doc/Implementation/ML.thy
src/Doc/ROOT
src/Doc/System/Basics.thy
src/HOL/ROOT
src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/Pure/General/socket_io.ML
src/Pure/ML/exn_output.ML
src/Pure/ML/exn_output_polyml.ML
src/Pure/ML/exn_properties_dummy.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_parse.ML
src/Pure/RAW/ROOT_polyml.ML
src/Pure/RAW/ROOT_smlnj.ML
src/Pure/RAW/compiler_polyml.ML
src/Pure/RAW/ml_name_space.ML
src/Pure/RAW/ml_system.ML
src/Pure/RAW/overloading_smlnj.ML
src/Pure/RAW/pp_dummy.ML
src/Pure/RAW/proper_int.ML
src/Pure/RAW/single_assignment.ML
src/Pure/RAW/thread_dummy.ML
src/Pure/RAW/universal.ML
src/Pure/RAW/use_context.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Tools/Code/code_runtime.ML
src/Tools/ROOT
src/Tools/Spec_Check/spec_check.ML
     1.1 --- a/Admin/Release/CHECKLIST	Wed Feb 17 21:08:18 2016 +0100
     1.2 +++ b/Admin/Release/CHECKLIST	Wed Feb 17 23:06:24 2016 +0100
     1.3 @@ -1,11 +1,11 @@
     1.4  Checklist for official releases
     1.5  ===============================
     1.6  
     1.7 -- check latest updates of polyml, smlnj, jdk, scala, jedit;
     1.8 +- check latest updates of polyml, jdk, scala, jedit;
     1.9  
    1.10  - check Admin/components;
    1.11  
    1.12 -- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj;
    1.13 +- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0;
    1.14  
    1.15  - test 'display_drafts' command;
    1.16  
     2.1 --- a/Admin/isatest/isatest-makeall	Wed Feb 17 21:08:18 2016 +0100
     2.2 +++ b/Admin/isatest/isatest-makeall	Wed Feb 17 23:06:24 2016 +0100
     2.3 @@ -24,7 +24,7 @@
     2.4    echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
     2.5    echo
     2.6    echo "Examples:"
     2.7 -  echo "  $PRG ~/settings/at-poly ~/settings/at-sml"
     2.8 +  echo "  $PRG ~/settings/at-poly"
     2.9    echo "  $PRG -l \"HOL-Library HOL-Bali\" ~/settings/at-poly"
    2.10    exit 1
    2.11  }
    2.12 @@ -92,14 +92,7 @@
    2.13  
    2.14      [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
    2.15  
    2.16 -    case "$SETTINGS" in
    2.17 -      *sml*)
    2.18 -        BUILD_ARGS="-o timeout=72000 $BUILD_ARGS"
    2.19 -        ;;
    2.20 -      *)
    2.21 -        BUILD_ARGS="-o timeout=10800 $BUILD_ARGS"
    2.22 -        ;;
    2.23 -    esac
    2.24 +    BUILD_ARGS="-o timeout=10800 $BUILD_ARGS"
    2.25  
    2.26      # logfile setup
    2.27  
     3.1 --- a/Admin/isatest/isatest-makedist	Wed Feb 17 21:08:18 2016 +0100
     3.2 +++ b/Admin/isatest/isatest-makedist	Wed Feb 17 23:06:24 2016 +0100
     3.3 @@ -102,8 +102,6 @@
     3.4  
     3.5  $SSH lxbroy10 "$MAKEALL -x HOL-Proofs $HOME/settings/at64-poly"
     3.6  sleep 15
     3.7 -$SSH lxbroy3 "$MAKEALL -l HOL-Unix $HOME/settings/at-sml-dev-e"
     3.8 -sleep 15
     3.9  $SSH lxbroy4 "
    3.10    $MAKEALL -l HOL-Library $HOME/settings/at-poly;
    3.11    $MAKEALL -l HOL-Library $HOME/settings/at-poly-e;
     4.1 --- a/Admin/isatest/isatest-stats	Wed Feb 17 21:08:18 2016 +0100
     4.2 +++ b/Admin/isatest/isatest-stats	Wed Feb 17 23:06:24 2016 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  
     4.5  THIS="$(cd "$(dirname "$0")"; pwd)"
     4.6  
     4.7 -PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly-M8-skip_proofs mac-poly64-M8 at-sml-dev"
     4.8 +PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly-M8-skip_proofs mac-poly64-M8"
     4.9  
    4.10  ISABELLE_SESSIONS="
    4.11    HOL
     5.1 --- a/Admin/isatest/settings/at-sml-dev-e	Wed Feb 17 21:08:18 2016 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,29 +0,0 @@
     5.4 -# -*- shell-script -*- :mode=shellscript:
     5.5 -
     5.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
     5.7 -
     5.8 -ML_SYSTEM=smlnj
     5.9 -ML_HOME="/home/smlnj/110.79/bin"
    5.10 -ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
    5.11 -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
    5.12 -
    5.13 -ISABELLE_GHC=/usr/bin/ghc
    5.14 -
    5.15 -ISABELLE_HOME_USER="$HOME/isabelle-at-sml-dev-e"
    5.16 -
    5.17 -# Where to look for isabelle tools (multiple dirs separated by ':').
    5.18 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
    5.19 -
    5.20 -# Location for temporary files (should be on a local file system).
    5.21 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
    5.22 -
    5.23 -
    5.24 -# Heap input locations. ML system identifier is included in lookup.
    5.25 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
    5.26 -
    5.27 -# Heap output location. ML system identifier is appended automatically later on.
    5.28 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
    5.29 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
    5.30 -
    5.31 -ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf"
    5.32 -
     6.1 --- a/NEWS	Wed Feb 17 21:08:18 2016 +0100
     6.2 +++ b/NEWS	Wed Feb 17 23:06:24 2016 +0100
     6.3 @@ -33,6 +33,12 @@
     6.4      INCOMPATIBILITY.
     6.5  
     6.6  
     6.7 +*** System ***
     6.8 +
     6.9 +* SML/NJ is no longer supported.
    6.10 +
    6.11 +
    6.12 +
    6.13  New in Isabelle2016 (February 2016)
    6.14  -----------------------------------
    6.15  
     7.1 --- a/etc/settings	Wed Feb 17 21:08:18 2016 +0100
     7.2 +++ b/etc/settings	Wed Feb 17 23:06:24 2016 +0100
     7.3 @@ -129,17 +129,9 @@
     7.4  
     7.5  
     7.6  ###
     7.7 -### Misc old-style settings
     7.8 +### Misc settings
     7.9  ###
    7.10  
    7.11 -# Standard ML of New Jersey (slow!)
    7.12 -#ML_SYSTEM=smlnj-110
    7.13 -#ML_HOME="/usr/local/smlnj/bin"
    7.14 -#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
    7.15 -#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
    7.16 -#SMLNJ_CYGWIN_RUNTIME=1
    7.17 -
    7.18 -# Misc programming languages
    7.19  #ISABELLE_GHC="/usr/bin/ghc"
    7.20  #ISABELLE_OCAML="/usr/bin/ocaml"
    7.21  #ISABELLE_SWIPL="/usr/bin/swipl"
     8.1 --- a/lib/scripts/getsettings	Wed Feb 17 21:08:18 2016 +0100
     8.2 +++ b/lib/scripts/getsettings	Wed Feb 17 23:06:24 2016 +0100
     8.3 @@ -290,16 +290,6 @@
     8.4  #enforce JAVA_HOME
     8.5  export JAVA_HOME="$ISABELLE_JDK_HOME/jre"
     8.6  
     8.7 -#build condition etc.
     8.8 -case "$ML_SYSTEM" in
     8.9 -  polyml*)
    8.10 -    ML_SYSTEM_POLYML="true"
    8.11 -    ;;
    8.12 -  *)
    8.13 -    ML_SYSTEM_POLYML=""
    8.14 -    ;;
    8.15 -esac
    8.16 -
    8.17  set +o allexport
    8.18  
    8.19  fi
     9.1 --- a/lib/scripts/run-smlnj	Wed Feb 17 21:08:18 2016 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,97 +0,0 @@
     9.4 -#!/usr/bin/env bash
     9.5 -#
     9.6 -# Author: Markus Wenzel, TU Muenchen
     9.7 -#
     9.8 -# SML/NJ startup script (for 110 or later).
     9.9 -
    9.10 -export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
    9.11 -
    9.12 -
    9.13 -## diagnostics
    9.14 -
    9.15 -function fail()
    9.16 -{
    9.17 -  echo "$1" >&2
    9.18 -  exit 2
    9.19 -}
    9.20 -
    9.21 -function fail_out()
    9.22 -{
    9.23 -  fail "Unable to create output heap file: \"$OUTFILE\""
    9.24 -}
    9.25 -
    9.26 -function check_mlhome_file()
    9.27 -{
    9.28 -  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    9.29 -}
    9.30 -
    9.31 -function check_heap_file()
    9.32 -{
    9.33 -  if [ ! -f "$1" ]; then
    9.34 -    echo "Expected to find ML heap file $1" >&2
    9.35 -    return 1
    9.36 -  else
    9.37 -    return 0
    9.38 -  fi
    9.39 -}
    9.40 -
    9.41 -
    9.42 -
    9.43 -## compiler binaries
    9.44 -
    9.45 -[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
    9.46 -
    9.47 -SML="$ML_HOME/sml"
    9.48 -ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
    9.49 -
    9.50 -check_mlhome_file "$SML"
    9.51 -check_mlhome_file "$ARCH_N_OPSYS"
    9.52 -
    9.53 -eval $("$ARCH_N_OPSYS")
    9.54 -
    9.55 -
    9.56 -
    9.57 -## prepare databases
    9.58 -
    9.59 -if [ -z "$INFILE" ]; then
    9.60 -  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    9.61 -  DB=""
    9.62 -else
    9.63 -  EXIT=""
    9.64 -  DB="@SMLload=$INFILE"
    9.65 -fi
    9.66 -
    9.67 -if [ -z "$OUTFILE" ]; then
    9.68 -  MLEXIT=""
    9.69 -else
    9.70 -  if [ -z "$INFILE" ]; then
    9.71 -    MLEXIT="if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};"
    9.72 -  else
    9.73 -    MLEXIT="Session.save \"$OUTFILE\";"
    9.74 -  fi
    9.75 -  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    9.76 -fi
    9.77 -
    9.78 -
    9.79 -## run it!
    9.80 -
    9.81 -MLTEXT="$EXIT $MLTEXT"
    9.82 -
    9.83 -if [ -z "$TERMINATE" ]; then
    9.84 -  FEEDER_OPTS=""
    9.85 -else
    9.86 -  FEEDER_OPTS="-q"
    9.87 -fi
    9.88 -
    9.89 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    9.90 -  { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    9.91 -RC="$?"
    9.92 -
    9.93 -
    9.94 -## fix heap file name and permissions
    9.95 -
    9.96 -if [ -n "$OUTFILE" ]; then
    9.97 -  check_heap_file "$OUTFILE" && [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    9.98 -fi
    9.99 -
   9.100 -exit "$RC"
    10.1 --- a/src/Doc/Implementation/ML.thy	Wed Feb 17 21:08:18 2016 +0100
    10.2 +++ b/src/Doc/Implementation/ML.thy	Wed Feb 17 23:06:24 2016 +0100
    10.3 @@ -505,7 +505,7 @@
    10.4    ML and Isar are intertwined via an open-ended bootstrap process that
    10.5    provides more and more programming facilities and logical content in an
    10.6    alternating manner. Bootstrapping starts from the raw environment of
    10.7 -  existing implementations of Standard ML (mainly Poly/ML, but also SML/NJ).
    10.8 +  existing implementations of Standard ML (mainly Poly/ML).
    10.9  
   10.10    Isabelle/Pure marks the point where the raw ML toplevel is superseded by
   10.11    Isabelle/ML within the Isar theory and proof language, with a uniform
   10.12 @@ -1379,8 +1379,7 @@
   10.13    \<^descr> Type @{ML_type int} represents regular mathematical integers, which are
   10.14    \<^emph>\<open>unbounded\<close>. Overflow is treated properly, but should never happen in
   10.15    practice.\<^footnote>\<open>The size limit for integer bit patterns in memory is 64\,MB for
   10.16 -  32-bit Poly/ML, and much higher for 64-bit systems.\<close> This works uniformly
   10.17 -  for all supported ML platforms (Poly/ML and SML/NJ).
   10.18 +  32-bit Poly/ML, and much higher for 64-bit systems.\<close>
   10.19  
   10.20    Literal integers in ML text are forced to be of this one true integer type
   10.21    --- adhoc overloading of SML97 is disabled.
    11.1 --- a/src/Doc/ROOT	Wed Feb 17 21:08:18 2016 +0100
    11.2 +++ b/src/Doc/ROOT	Wed Feb 17 23:06:24 2016 +0100
    11.3 @@ -126,7 +126,7 @@
    11.4      "root.tex"
    11.5  
    11.6  session Implementation (doc) in "Implementation" = "HOL-Proofs" +
    11.7 -  options [condition = ML_SYSTEM_POLYML, document_variants = "implementation", quick_and_dirty]
    11.8 +  options [document_variants = "implementation", quick_and_dirty]
    11.9    theories
   11.10      Eq
   11.11      Integration
    12.1 --- a/src/Doc/System/Basics.thy	Wed Feb 17 21:08:18 2016 +0100
    12.2 +++ b/src/Doc/System/Basics.thy	Wed Feb 17 23:06:24 2016 +0100
    12.3 @@ -187,12 +187,6 @@
    12.4    of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
    12.5    values.
    12.6  
    12.7 -  \<^descr>[@{setting_def ML_SYSTEM_POLYML}\<open>\<^sup>*\<close>] is \<^verbatim>\<open>true\<close> for @{setting ML_SYSTEM}
    12.8 -  values derived from Poly/ML, as opposed to SML/NJ where it is empty. This is
    12.9 -  particularly useful with the build option @{system_option condition}
   12.10 -  (\secref{sec:system-options}) to restrict big sessions to something that
   12.11 -  SML/NJ can still handle.
   12.12 -
   12.13    \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
   12.14    Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
   12.15    essential for Isabelle/Scala and other JVM-based tools to work properly.
    13.1 --- a/src/HOL/ROOT	Wed Feb 17 21:08:18 2016 +0100
    13.2 +++ b/src/HOL/ROOT	Wed Feb 17 23:06:24 2016 +0100
    13.3 @@ -18,7 +18,7 @@
    13.4    description {*
    13.5      HOL-Main with explicit proof terms.
    13.6    *}
    13.7 -  options [condition = ML_SYSTEM_POLYML, document = false, quick_and_dirty = false]
    13.8 +  options [document = false, quick_and_dirty = false]
    13.9    theories Proofs (*sequential change of global flag!*)
   13.10    theories "~~/src/HOL/Library/Old_Datatype"
   13.11    files
   13.12 @@ -245,24 +245,24 @@
   13.13    document_files "root.bib" "root.tex"
   13.14  
   13.15  session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   13.16 -  options [condition = ML_SYSTEM_POLYML, document = false, browser_info = false]
   13.17 +  options [document = false, browser_info = false]
   13.18    theories
   13.19      Generate
   13.20      Generate_Binary_Nat
   13.21      Generate_Target_Nat
   13.22      Generate_Efficient_Datastructures
   13.23      Generate_Pretty_Char
   13.24 -  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_GHC"]
   13.25 +  theories [condition = "ISABELLE_GHC"]
   13.26      Code_Test_GHC
   13.27 -  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_MLTON"]
   13.28 +  theories [condition = "ISABELLE_MLTON"]
   13.29      Code_Test_MLton
   13.30 -  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_OCAMLC"]
   13.31 +  theories [condition = "ISABELLE_OCAMLC"]
   13.32      Code_Test_OCaml
   13.33 -  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_POLYML"]
   13.34 +  theories [condition = "ISABELLE_POLYML"]
   13.35      Code_Test_PolyML
   13.36 -  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_SCALA"]
   13.37 +  theories [condition = "ISABELLE_SCALA"]
   13.38      Code_Test_Scala
   13.39 -  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_SMLNJ"]
   13.40 +  theories [condition = "ISABELLE_SMLNJ"]
   13.41      Code_Test_SMLNJ
   13.42  
   13.43  session "HOL-Metis_Examples" in Metis_Examples = HOL +
   13.44 @@ -394,11 +394,11 @@
   13.45    description {*
   13.46      Various decision procedures, typically involving reflection.
   13.47    *}
   13.48 -  options [condition = ML_SYSTEM_POLYML, document = false]
   13.49 +  options [document = false]
   13.50    theories Decision_Procs
   13.51  
   13.52  session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   13.53 -  options [condition = ML_SYSTEM_POLYML, document = false, parallel_proofs = 0]
   13.54 +  options [document = false, parallel_proofs = 0]
   13.55    theories
   13.56      Hilbert_Classical
   13.57      XML_Data
   13.58 @@ -407,7 +407,7 @@
   13.59    description {*
   13.60      Examples for program extraction in Higher-Order Logic.
   13.61    *}
   13.62 -  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0, quick_and_dirty = false]
   13.63 +  options [parallel_proofs = 0, quick_and_dirty = false]
   13.64    theories [document = false]
   13.65      "~~/src/HOL/Library/Code_Target_Numeral"
   13.66      "~~/src/HOL/Library/Monad_Syntax"
   13.67 @@ -432,7 +432,7 @@
   13.68      The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
   13.69      theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   13.70    *}
   13.71 -  options [condition = ML_SYSTEM_POLYML, print_mode = "no_brackets",
   13.72 +  options [print_mode = "no_brackets",
   13.73      parallel_proofs = 0, quick_and_dirty = false]
   13.74    theories [document = false]
   13.75      "~~/src/HOL/Library/Code_Target_Int"
   13.76 @@ -531,7 +531,6 @@
   13.77    description {*
   13.78      Miscellaneous examples for Higher-Order Logic.
   13.79    *}
   13.80 -  options [condition = ML_SYSTEM_POLYML]
   13.81    theories [document = false]
   13.82      "~~/src/HOL/Library/State_Monad"
   13.83      Code_Binary_Nat_examples
   13.84 @@ -702,7 +701,7 @@
   13.85  
   13.86      TPTP-related extensions.
   13.87    *}
   13.88 -  options [condition = ML_SYSTEM_POLYML, document = false]
   13.89 +  options [document = false]
   13.90    theories
   13.91      ATP_Theory_Export
   13.92      MaSh_Eval
   13.93 @@ -748,7 +747,7 @@
   13.94    theories Nominal
   13.95  
   13.96  session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   13.97 -  options [condition = ML_SYSTEM_POLYML, document = false]
   13.98 +  options [document = false]
   13.99    theories
  13.100      Class3
  13.101      CK_Machine
  13.102 @@ -837,11 +836,11 @@
  13.103    theories Mirabelle_Test
  13.104  
  13.105  session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
  13.106 -  options [condition = ML_SYSTEM_POLYML, document = false, timeout = 60]
  13.107 +  options [document = false, timeout = 60]
  13.108    theories Ex
  13.109  
  13.110  session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
  13.111 -  options [condition = ML_SYSTEM_POLYML, document = false, quick_and_dirty]
  13.112 +  options [document = false, quick_and_dirty]
  13.113    theories
  13.114      Boogie
  13.115      SMT_Examples
  13.116 @@ -980,7 +979,7 @@
  13.117  
  13.118  session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
  13.119    options [document = false]
  13.120 -  theories [condition = ML_SYSTEM_POLYML]
  13.121 +  theories
  13.122      Examples
  13.123      Predicate_Compile_Tests
  13.124      Predicate_Compile_Quickcheck_Examples
    14.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Feb 17 21:08:18 2016 +0100
    14.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Feb 17 23:06:24 2016 +0100
    14.3 @@ -169,7 +169,6 @@
    14.4  fun alphanumerated_name prefix name =
    14.5    prefix ^ (raw_explode #> map alphanumerate #> implode) name
    14.6  
    14.7 -(*SMLNJ complains if type annotation not used below*)
    14.8  fun mk_binding (config : config) ident =
    14.9    let
   14.10      val pre_binding = Binding.name (alphanumerated_name "bnd_" ident)
    15.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 17 21:08:18 2016 +0100
    15.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 17 23:06:24 2016 +0100
    15.3 @@ -1609,10 +1609,8 @@
    15.4  
    15.5  (* values_timeout configuration *)
    15.6  
    15.7 -val default_values_timeout = if ML_System.is_smlnj then 1200.0 else 40.0
    15.8 -
    15.9  val values_timeout =
   15.10 -  Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
   15.11 +  Attrib.setup_config_real @{binding values_timeout} (K 40.0)
   15.12  
   15.13  val _ =
   15.14    Theory.setup
    16.1 --- a/src/Pure/General/socket_io.ML	Wed Feb 17 21:08:18 2016 +0100
    16.2 +++ b/src/Pure/General/socket_io.ML	Wed Feb 17 23:06:24 2016 +0100
    16.3 @@ -25,7 +25,7 @@
    16.4      val rd =
    16.5        BinPrimIO.RD {
    16.6          name = name,
    16.7 -        chunkSize = io_buffer_size,
    16.8 +        chunkSize = 4096,
    16.9          readVec = SOME (fn n => Socket.recvVec (socket, n)),
   16.10          readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
   16.11          readVecNB = NONE,
   16.12 @@ -44,7 +44,7 @@
   16.13      val wr =
   16.14        BinPrimIO.WR {
   16.15          name = name,
   16.16 -        chunkSize = io_buffer_size,
   16.17 +        chunkSize = 4096,
   16.18          writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
   16.19          writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
   16.20          writeVecNB = NONE,
    17.1 --- a/src/Pure/ML/exn_output.ML	Wed Feb 17 21:08:18 2016 +0100
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,20 +0,0 @@
    17.4 -(*  Title:      Pure/ML/exn_output.ML
    17.5 -    Author:     Makarius
    17.6 -
    17.7 -Auxiliary operations for exception output -- generic version.
    17.8 -*)
    17.9 -
   17.10 -signature EXN_OUTPUT =
   17.11 -sig
   17.12 -  val position: exn -> Position.T
   17.13 -  val pretty: exn -> Pretty.T
   17.14 -end
   17.15 -
   17.16 -structure Exn_Output: EXN_OUTPUT =
   17.17 -struct
   17.18 -
   17.19 -fun position (_: exn) = Position.none
   17.20 -val pretty = Pretty.str o General.exnMessage;
   17.21 -
   17.22 -end;
   17.23 -
    18.1 --- a/src/Pure/ML/exn_output_polyml.ML	Wed Feb 17 21:08:18 2016 +0100
    18.2 +++ b/src/Pure/ML/exn_output_polyml.ML	Wed Feb 17 23:06:24 2016 +0100
    18.3 @@ -4,6 +4,12 @@
    18.4  Auxiliary operations for exception output -- Poly/ML version.
    18.5  *)
    18.6  
    18.7 +signature EXN_OUTPUT =
    18.8 +sig
    18.9 +  val position: exn -> Position.T
   18.10 +  val pretty: exn -> Pretty.T
   18.11 +end;
   18.12 +
   18.13  structure Exn_Output: EXN_OUTPUT =
   18.14  struct
   18.15  
   18.16 @@ -16,4 +22,3 @@
   18.17    Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
   18.18  
   18.19  end;
   18.20 -
    19.1 --- a/src/Pure/ML/exn_properties_dummy.ML	Wed Feb 17 21:08:18 2016 +0100
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,23 +0,0 @@
    19.4 -(*  Title:      Pure/ML/exn_properties_dummy.ML
    19.5 -    Author:     Makarius
    19.6 -
    19.7 -Exception properties -- dummy version.
    19.8 -*)
    19.9 -
   19.10 -signature EXN_PROPERTIES =
   19.11 -sig
   19.12 -  val position_of: 'location -> Position.T
   19.13 -  val get: exn -> Properties.T
   19.14 -  val update: Properties.entry list -> exn -> exn
   19.15 -end;
   19.16 -
   19.17 -structure Exn_Properties: EXN_PROPERTIES =
   19.18 -struct
   19.19 -
   19.20 -fun position_of _ = Position.none;
   19.21 -
   19.22 -fun get _ = [];
   19.23 -fun update _ exn = exn;
   19.24 -
   19.25 -end;
   19.26 -
    20.1 --- a/src/Pure/ML/ml_compiler.ML	Wed Feb 17 21:08:18 2016 +0100
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,44 +0,0 @@
    20.4 -(*  Title:      Pure/ML/ml_compiler.ML
    20.5 -    Author:     Makarius
    20.6 -
    20.7 -Runtime compilation and evaluation -- generic version.
    20.8 -*)
    20.9 -
   20.10 -signature ML_COMPILER =
   20.11 -sig
   20.12 -  type flags =
   20.13 -    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
   20.14 -      debug: bool option, writeln: string -> unit, warning: string -> unit}
   20.15 -  val flags: flags
   20.16 -  val verbose: bool -> flags -> flags
   20.17 -  val eval: flags -> Position.T -> ML_Lex.token list -> unit
   20.18 -end
   20.19 -
   20.20 -structure ML_Compiler: ML_COMPILER =
   20.21 -struct
   20.22 -
   20.23 -type flags =
   20.24 -  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
   20.25 -    debug: bool option, writeln: string -> unit, warning: string -> unit};
   20.26 -
   20.27 -val flags: flags =
   20.28 -  {SML = false, exchange = false, redirect = false, verbose = false,
   20.29 -    debug = NONE, writeln = writeln, warning = warning};
   20.30 -
   20.31 -fun verbose b (flags: flags) =
   20.32 -  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
   20.33 -    verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
   20.34 -
   20.35 -fun eval (flags: flags) pos toks =
   20.36 -  let
   20.37 -    val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
   20.38 -    val line = the_default 1 (Position.line_of pos);
   20.39 -    val file = the_default "ML" (Position.file_of pos);
   20.40 -    val debug = the_default false (#debug flags);
   20.41 -    val text = ML_Lex.flatten toks;
   20.42 -  in
   20.43 -    Secure.use_text ML_Env.local_context
   20.44 -      {line = line, file = file, verbose = #verbose flags, debug = debug} text
   20.45 -  end;
   20.46 -
   20.47 -end;
    21.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Feb 17 21:08:18 2016 +0100
    21.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Feb 17 23:06:24 2016 +0100
    21.3 @@ -4,10 +4,33 @@
    21.4  Runtime compilation and evaluation -- Poly/ML version.
    21.5  *)
    21.6  
    21.7 +signature ML_COMPILER =
    21.8 +sig
    21.9 +  type flags =
   21.10 +    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
   21.11 +      debug: bool option, writeln: string -> unit, warning: string -> unit}
   21.12 +  val flags: flags
   21.13 +  val verbose: bool -> flags -> flags
   21.14 +  val eval: flags -> Position.T -> ML_Lex.token list -> unit
   21.15 +end
   21.16 +
   21.17 +
   21.18  structure ML_Compiler: ML_COMPILER =
   21.19  struct
   21.20  
   21.21 -open ML_Compiler;
   21.22 +(* flags *)
   21.23 +
   21.24 +type flags =
   21.25 +  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
   21.26 +    debug: bool option, writeln: string -> unit, warning: string -> unit};
   21.27 +
   21.28 +val flags: flags =
   21.29 +  {SML = false, exchange = false, redirect = false, verbose = false,
   21.30 +    debug = NONE, writeln = writeln, warning = warning};
   21.31 +
   21.32 +fun verbose b (flags: flags) =
   21.33 +  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
   21.34 +    verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
   21.35  
   21.36  
   21.37  (* parse trees *)
    22.1 --- a/src/Pure/ML/ml_env.ML	Wed Feb 17 21:08:18 2016 +0100
    22.2 +++ b/src/Pure/ML/ml_env.ML	Wed Feb 17 23:06:24 2016 +0100
    22.3 @@ -163,8 +163,7 @@
    22.4    end;
    22.5  
    22.6  val local_context: use_context =
    22.7 - {tune_source = ML_Parse.fix_ints,
    22.8 -  name_space = name_space {SML = false, exchange = false},
    22.9 + {name_space = name_space {SML = false, exchange = false},
   22.10    str_of_pos = Position.here oo Position.line_file,
   22.11    print = writeln,
   22.12    error = error};
    23.1 --- a/src/Pure/ML/ml_parse.ML	Wed Feb 17 21:08:18 2016 +0100
    23.2 +++ b/src/Pure/ML/ml_parse.ML	Wed Feb 17 23:06:24 2016 +0100
    23.3 @@ -6,7 +6,6 @@
    23.4  
    23.5  signature ML_PARSE =
    23.6  sig
    23.7 -  val fix_ints: string -> string
    23.8    val global_context: use_context
    23.9  end;
   23.10  
   23.11 @@ -43,30 +42,10 @@
   23.12  val blanks = Scan.repeat improper >> implode;
   23.13  
   23.14  
   23.15 -(* fix_ints *)
   23.16 -
   23.17 -(*approximation only -- corrupts numeric record field patterns *)
   23.18 -val fix_int =
   23.19 -  $$$ "#" ^^ blanks ^^ int ||
   23.20 -  ($$$ "infix" || $$$ "infixr") ^^ blanks ^^ int ||
   23.21 -  int >> (fn x => "(" ^ x ^ ":int)") ||
   23.22 -  regular ||
   23.23 -  bad_input;
   23.24 -
   23.25 -val fix_ints =
   23.26 -  ML_System.is_smlnj ?
   23.27 -   (Source.of_string #>
   23.28 -    ML_Lex.source #>
   23.29 -    Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) #>
   23.30 -    Source.exhaust #>
   23.31 -    implode);
   23.32 -
   23.33 -
   23.34  (* global use_context *)
   23.35  
   23.36  val global_context: use_context =
   23.37 - {tune_source = fix_ints,
   23.38 -  name_space = ML_Name_Space.global,
   23.39 + {name_space = ML_Name_Space.global,
   23.40    str_of_pos = Position.here oo Position.line_file,
   23.41    print = writeln,
   23.42    error = error};
    24.1 --- a/src/Pure/RAW/ROOT_polyml.ML	Wed Feb 17 21:08:18 2016 +0100
    24.2 +++ b/src/Pure/RAW/ROOT_polyml.ML	Wed Feb 17 23:06:24 2016 +0100
    24.3 @@ -102,8 +102,6 @@
    24.4  val raw_explode = SML90.explode;
    24.5  val implode = SML90.implode;
    24.6  
    24.7 -val io_buffer_size = 4096;
    24.8 -
    24.9  fun quit () = exit 0;
   24.10  
   24.11  
    25.1 --- a/src/Pure/RAW/ROOT_smlnj.ML	Wed Feb 17 21:08:18 2016 +0100
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,194 +0,0 @@
    25.4 -(*  Title:      Pure/RAW/ROOT_smlnj.ML
    25.5 -
    25.6 -Compatibility file for Standard ML of New Jersey.
    25.7 -*)
    25.8 -
    25.9 -val io_buffer_size = 4096;
   25.10 -use "RAW/proper_int.ML";
   25.11 -
   25.12 -exception Interrupt;
   25.13 -fun reraise exn = raise exn;
   25.14 -
   25.15 -fun exit rc = Posix.Process.exit (Word8.fromInt rc);
   25.16 -fun quit () = exit 0;
   25.17 -
   25.18 -use "RAW/overloading_smlnj.ML";
   25.19 -use "RAW/exn.ML";
   25.20 -use "RAW/single_assignment.ML";
   25.21 -use "RAW/universal.ML";
   25.22 -use "RAW/thread_dummy.ML";
   25.23 -use "RAW/multithreading.ML";
   25.24 -use "RAW/ml_stack_dummy.ML";
   25.25 -use "RAW/ml_pretty.ML";
   25.26 -use "RAW/ml_name_space.ML";
   25.27 -structure PolyML = struct end;
   25.28 -use "RAW/pp_dummy.ML";
   25.29 -use "RAW/use_context.ML";
   25.30 -use "RAW/ml_positions.ML";
   25.31 -
   25.32 -
   25.33 -val seconds = Time.fromReal;
   25.34 -
   25.35 -(*low-level pointer equality*)
   25.36 -CM.autoload "$smlnj/init/init.cmi";
   25.37 -val pointer_eq = InlineT.ptreql;
   25.38 -
   25.39 -
   25.40 -(* restore old-style character / string functions *)
   25.41 -
   25.42 -val ord = mk_int o SML90.ord;
   25.43 -val chr = SML90.chr o dest_int;
   25.44 -val raw_explode = SML90.explode;
   25.45 -val implode = SML90.implode;
   25.46 -
   25.47 -
   25.48 -(* New Jersey ML parameters *)
   25.49 -
   25.50 -val _ =
   25.51 - (Control.Print.printLength := 1000;
   25.52 -  Control.Print.printDepth := 350;
   25.53 -  Control.Print.stringDepth := 250;
   25.54 -  Control.Print.signatures := 2;
   25.55 -  Control.MC.matchRedundantError := false);
   25.56 -
   25.57 -
   25.58 -(* Poly/ML emulation *)
   25.59 -
   25.60 -(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
   25.61 -local
   25.62 -  val depth = ref (10: int);
   25.63 -in
   25.64 -  fun get_default_print_depth () = ! depth;
   25.65 -  fun default_print_depth n =
   25.66 -   (depth := n;
   25.67 -    Control.Print.printDepth := dest_int n div 2;
   25.68 -    Control.Print.printLength := dest_int n);
   25.69 -  val _ = default_print_depth 10;
   25.70 -end;
   25.71 -
   25.72 -fun ml_make_string (_: string) = "(fn _ => \"?\")";
   25.73 -
   25.74 -
   25.75 -(*prompts*)
   25.76 -fun ml_prompts p1 p2 =
   25.77 -  (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
   25.78 -
   25.79 -(*dummy implementation*)
   25.80 -structure ML_Profiling =
   25.81 -struct
   25.82 -  fun profile_time (_: (int * string) list -> unit) f x = f x;
   25.83 -  fun profile_time_thread (_: (int * string) list -> unit) f x = f x;
   25.84 -  fun profile_allocations (_: (int * string) list -> unit) f x = f x;
   25.85 -end;
   25.86 -
   25.87 -(*dummy implementation*)
   25.88 -fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();
   25.89 -
   25.90 -
   25.91 -(* ML command execution *)
   25.92 -
   25.93 -fun use_text ({tune_source, print, error, ...}: use_context)
   25.94 -    {line, file, verbose, debug = _: bool} text =
   25.95 -  let
   25.96 -    val ref out_orig = Control.Print.out;
   25.97 -
   25.98 -    val out_buffer = ref ([]: string list);
   25.99 -    val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
  25.100 -    fun output () =
  25.101 -      let val str = implode (rev (! out_buffer))
  25.102 -      in String.substring (str, 0, Int.max (0, size str - 1)) end;
  25.103 -  in
  25.104 -    Control.Print.out := out;
  25.105 -    Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file text)))
  25.106 -      handle exn =>
  25.107 -        (Control.Print.out := out_orig;
  25.108 -          error ((if file = "" then "" else "Error in " ^ file ^ "\n") ^ output ()); raise exn);
  25.109 -    Control.Print.out := out_orig;
  25.110 -    if verbose then print (output ()) else ()
  25.111 -  end;
  25.112 -
  25.113 -fun use_file context {verbose, debug} file =
  25.114 -  let
  25.115 -    val instream = TextIO.openIn file;
  25.116 -    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
  25.117 -  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
  25.118 -
  25.119 -
  25.120 -(* toplevel pretty printing *)
  25.121 -
  25.122 -fun ml_pprint pps =
  25.123 -  let
  25.124 -    fun str "" = ()
  25.125 -      | str s = PrettyPrint.string pps s;
  25.126 -    fun pprint (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
  25.127 -         (str bg;
  25.128 -          (if consistent then PrettyPrint.openHVBox else PrettyPrint.openHOVBox) pps
  25.129 -            (PrettyPrint.Rel (dest_int ind));
  25.130 -          List.app pprint prts; PrettyPrint.closeBox pps;
  25.131 -          str en)
  25.132 -      | pprint (ML_Pretty.String (s, _)) = str s
  25.133 -      | pprint (ML_Pretty.Break (false, width, offset)) =
  25.134 -          PrettyPrint.break pps {nsp = dest_int width, offset = dest_int offset}
  25.135 -      | pprint (ML_Pretty.Break (true, _, _)) = PrettyPrint.newline pps;
  25.136 -  in pprint end;
  25.137 -
  25.138 -fun toplevel_pp context path pp =
  25.139 -  use_text context {line = 1, file = "pp", verbose = false, debug = false}
  25.140 -    ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"")  path) ^
  25.141 -      "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
  25.142 -
  25.143 -
  25.144 -
  25.145 -(** interrupts **)
  25.146 -
  25.147 -local
  25.148 -
  25.149 -fun change_signal new_handler f x =
  25.150 -  let
  25.151 -    val old_handler = Signals.setHandler (Signals.sigINT, new_handler);
  25.152 -    val result = Exn.capture (f old_handler) x;
  25.153 -    val _ = Signals.setHandler (Signals.sigINT, old_handler);
  25.154 -  in Exn.release result end;
  25.155 -
  25.156 -in
  25.157 -
  25.158 -fun interruptible (f: 'a -> 'b) x =
  25.159 -  let
  25.160 -    val result = ref (Exn.interrupt_exn: 'b Exn.result);
  25.161 -    val old_handler = Signals.inqHandler Signals.sigINT;
  25.162 -  in
  25.163 -    SMLofNJ.Cont.callcc (fn cont =>
  25.164 -      (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont));
  25.165 -        result := Exn.capture f x));
  25.166 -    Signals.setHandler (Signals.sigINT, old_handler);
  25.167 -    Exn.release (! result)
  25.168 -  end;
  25.169 -
  25.170 -fun uninterruptible f =
  25.171 -  change_signal Signals.IGNORE
  25.172 -    (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
  25.173 -
  25.174 -end;
  25.175 -
  25.176 -
  25.177 -use "RAW/unsynchronized.ML";
  25.178 -use "RAW/ml_debugger.ML";
  25.179 -
  25.180 -
  25.181 -(* ML system operations *)
  25.182 -
  25.183 -fun ml_platform_path (s: string) = s;
  25.184 -fun ml_standard_path (s: string) = s;
  25.185 -
  25.186 -use "RAW/ml_system.ML";
  25.187 -
  25.188 -structure ML_System =
  25.189 -struct
  25.190 -
  25.191 -open ML_System;
  25.192 -
  25.193 -fun save_state name =
  25.194 -  if SMLofNJ.exportML name then ()
  25.195 -  else OS.FileSys.rename {old = name ^ "." ^ platform, new = name};
  25.196 -
  25.197 -end;
    26.1 --- a/src/Pure/RAW/compiler_polyml.ML	Wed Feb 17 21:08:18 2016 +0100
    26.2 +++ b/src/Pure/RAW/compiler_polyml.ML	Wed Feb 17 23:06:24 2016 +0100
    26.3 @@ -11,12 +11,11 @@
    26.4  
    26.5  in
    26.6  
    26.7 -fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
    26.8 +fun use_text ({name_space, str_of_pos, print, error, ...}: use_context)
    26.9      {line, file, verbose, debug} text =
   26.10    let
   26.11      val current_line = Unsynchronized.ref line;
   26.12 -    val in_buffer =
   26.13 -      Unsynchronized.ref (String.explode (tune_source (ml_positions line file text)));
   26.14 +    val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
   26.15      val out_buffer = Unsynchronized.ref ([]: string list);
   26.16      fun output () = drop_newline (implode (rev (! out_buffer)));
   26.17  
    27.1 --- a/src/Pure/RAW/ml_name_space.ML	Wed Feb 17 21:08:18 2016 +0100
    27.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.3 @@ -1,68 +0,0 @@
    27.4 -(*  Title:      Pure/RAW/ml_name_space.ML
    27.5 -    Author:     Makarius
    27.6 -
    27.7 -ML name space -- dummy version of Poly/ML 5.2 facility.
    27.8 -*)
    27.9 -
   27.10 -structure ML_Name_Space =
   27.11 -struct
   27.12 -
   27.13 -type valueVal = unit;
   27.14 -type typeVal = unit;
   27.15 -type fixityVal = unit;
   27.16 -type structureVal = unit;
   27.17 -type signatureVal = unit;
   27.18 -type functorVal = unit;
   27.19 -
   27.20 -type T =
   27.21 - {lookupVal:    string -> valueVal option,
   27.22 -  lookupType:   string -> typeVal option,
   27.23 -  lookupFix:    string -> fixityVal option,
   27.24 -  lookupStruct: string -> structureVal option,
   27.25 -  lookupSig:    string -> signatureVal option,
   27.26 -  lookupFunct:  string -> functorVal option,
   27.27 -  enterVal:     string * valueVal -> unit,
   27.28 -  enterType:    string * typeVal -> unit,
   27.29 -  enterFix:     string * fixityVal -> unit,
   27.30 -  enterStruct:  string * structureVal -> unit,
   27.31 -  enterSig:     string * signatureVal -> unit,
   27.32 -  enterFunct:   string * functorVal -> unit,
   27.33 -  allVal:       unit -> (string * valueVal) list,
   27.34 -  allType:      unit -> (string * typeVal) list,
   27.35 -  allFix:       unit -> (string * fixityVal) list,
   27.36 -  allStruct:    unit -> (string * structureVal) list,
   27.37 -  allSig:       unit -> (string * signatureVal) list,
   27.38 -  allFunct:     unit -> (string * functorVal) list};
   27.39 -
   27.40 -val global: T =
   27.41 - {lookupVal = fn _ => NONE,
   27.42 -  lookupType = fn _ => NONE,
   27.43 -  lookupFix = fn _ => NONE,
   27.44 -  lookupStruct = fn _ => NONE,
   27.45 -  lookupSig = fn _ => NONE,
   27.46 -  lookupFunct = fn _ => NONE,
   27.47 -  enterVal = fn _ => (),
   27.48 -  enterType = fn _ => (),
   27.49 -  enterFix = fn _ => (),
   27.50 -  enterStruct = fn _ => (),
   27.51 -  enterSig = fn _ => (),
   27.52 -  enterFunct = fn _ => (),
   27.53 -  allVal = fn _ => [],
   27.54 -  allType = fn _ => [],
   27.55 -  allFix = fn _ => [],
   27.56 -  allStruct = fn _ => [],
   27.57 -  allSig = fn _ => [],
   27.58 -  allFunct = fn _ => []};
   27.59 -
   27.60 -val initial_val : (string * valueVal) list = [];
   27.61 -val initial_type : (string * typeVal) list = [];
   27.62 -val initial_fixity : (string * fixityVal) list = [];
   27.63 -val initial_structure : (string * structureVal) list = [];
   27.64 -val initial_signature : (string * signatureVal) list = [];
   27.65 -val initial_functor : (string * functorVal) list = [];
   27.66 -
   27.67 -fun forget_global_structure (_: string) = ();
   27.68 -
   27.69 -fun display_val (_, _: int, _: T) = ML_Pretty.String ("?", 1);
   27.70 -
   27.71 -end;
    28.1 --- a/src/Pure/RAW/ml_system.ML	Wed Feb 17 21:08:18 2016 +0100
    28.2 +++ b/src/Pure/RAW/ml_system.ML	Wed Feb 17 23:06:24 2016 +0100
    28.3 @@ -7,8 +7,6 @@
    28.4  signature ML_SYSTEM =
    28.5  sig
    28.6    val name: string
    28.7 -  val is_polyml: bool
    28.8 -  val is_smlnj: bool
    28.9    val platform: string
   28.10    val platform_is_windows: bool
   28.11    val share_common_data: unit -> unit
   28.12 @@ -19,8 +17,6 @@
   28.13  struct
   28.14  
   28.15  val SOME name = OS.Process.getEnv "ML_SYSTEM";
   28.16 -val is_polyml = String.isPrefix "polyml" name;
   28.17 -val is_smlnj = String.isPrefix "smlnj" name;
   28.18  
   28.19  val SOME platform = OS.Process.getEnv "ML_PLATFORM";
   28.20  val platform_is_windows = String.isSuffix "windows" platform;
    29.1 --- a/src/Pure/RAW/overloading_smlnj.ML	Wed Feb 17 21:08:18 2016 +0100
    29.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.3 @@ -1,41 +0,0 @@
    29.4 -(*  Title:      Pure/RAW/overloading_smlnj.ML
    29.5 -    Author:     Makarius
    29.6 -
    29.7 -Overloading in SML/NJ (cf. smlnj/base/system/smlnj/init/pervasive.sml).
    29.8 -*)
    29.9 -
   29.10 -Control.overloadKW := true;
   29.11 -
   29.12 -overload ~ : ('a -> 'a) as
   29.13 -  IntInf.~ and Int31.~ and Int32.~ and Int64.~ and
   29.14 -  Word.~ and Word8.~ and Word32.~ and Word64.~ and Real.~;
   29.15 -overload + : ('a * 'a -> 'a) as
   29.16 -  IntInf.+ and Int31.+ and Int32.+ and Int64.+ and
   29.17 -  Word.+ and Word8.+ and Word32.+ and Word64.+ and Real.+;
   29.18 -overload - : ('a * 'a -> 'a) as
   29.19 -  IntInf.- and Int31.- and Int32.- and Int64.- and
   29.20 -  Word.- and Word8.- and Word32.- and Word64.- and Real.-;
   29.21 -overload * : ('a * 'a -> 'a) as
   29.22 -  IntInf.* and Int31.* and Int32.* and Int64.* and
   29.23 -  Word.* and Word8.* and Word32.* and Word64.* and Real.*;
   29.24 -overload div: ('a * 'a -> 'a) as
   29.25 -  IntInf.div and Int31.div and Int32.div and Int64.div and
   29.26 -  Word.div and Word8.div and Word32.div and Word64.div;
   29.27 -overload mod: ('a * 'a -> 'a) as
   29.28 -  IntInf.mod and Int31.mod and Int32.mod and Int64.mod and
   29.29 -  Word.mod and Word8.mod and Word32.mod and Word64.mod;
   29.30 -overload < : ('a * 'a -> bool) as
   29.31 -  IntInf.< and Int31.< and Int32.< and Int64.< and Real.< and
   29.32 -  Word.< and Word8.< and Word32.< and Word64.< and Char.< and String.<;
   29.33 -overload <= : ('a * 'a -> bool) as
   29.34 -  IntInf.<= and Int31.<= and Int32.<= and Int64.<= and Real.<= and
   29.35 -  Word.<= and Word8.<= and Word32.<= and Word64.<= and Char.<= and String.<=;
   29.36 -overload > : ('a * 'a -> bool) as
   29.37 -  IntInf.> and Int31.> and Int32.> and Int64.> and Real.> and
   29.38 -  Word.> and Word8.> and Word32.> and Word64.> and Char.> and String.>;
   29.39 -overload >= : ('a * 'a -> bool) as
   29.40 -  IntInf.>= and Int31.>= and Int32.>= and Int64.>= and Real.>= and
   29.41 -  Word.>= and Word8.>= and Word32.>= and Word64.>= and Char.>= and String.>=;
   29.42 -overload abs: ('a -> 'a) as IntInf.abs and Int31.abs and Int32.abs and Int64.abs and Real.abs;
   29.43 -
   29.44 -Control.overloadKW := false;
    30.1 --- a/src/Pure/RAW/pp_dummy.ML	Wed Feb 17 21:08:18 2016 +0100
    30.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.3 @@ -1,16 +0,0 @@
    30.4 -(*  Title:      Pure/RAW/pp_dummy.ML
    30.5 -
    30.6 -Dummy setup for toplevel pretty printing.
    30.7 -*)
    30.8 -
    30.9 -fun ml_pretty _ = raise Fail "ml_pretty dummy";
   30.10 -fun pretty_ml _ = raise Fail "pretty_ml dummy";
   30.11 -
   30.12 -structure PolyML =
   30.13 -struct
   30.14 -  fun addPrettyPrinter _ = ();
   30.15 -  fun prettyRepresentation _ =
   30.16 -    raise Fail "PolyML.prettyRepresentation dummy";
   30.17 -  open PolyML;
   30.18 -end;
   30.19 -
    31.1 --- a/src/Pure/RAW/proper_int.ML	Wed Feb 17 21:08:18 2016 +0100
    31.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.3 @@ -1,289 +0,0 @@
    31.4 -(*  Title:      Pure/RAW/proper_int.ML
    31.5 -    Author:     Makarius
    31.6 -
    31.7 -SML basis with type int representing proper integers, not machine
    31.8 -words.
    31.9 -*)
   31.10 -
   31.11 -val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
   31.12 -val dest_int = IntInf.toInt: IntInf.int -> Int.int;
   31.13 -
   31.14 -
   31.15 -(* Int *)
   31.16 -
   31.17 -type int = IntInf.int;
   31.18 -
   31.19 -structure IntInf =
   31.20 -struct
   31.21 -  open IntInf;
   31.22 -  fun fromInt (a: int) = a;
   31.23 -  fun toInt (a: int) = a;
   31.24 -  val log2 = mk_int o IntInf.log2;
   31.25 -  val sign = mk_int o IntInf.sign;
   31.26 -end;
   31.27 -
   31.28 -structure Int = IntInf;
   31.29 -
   31.30 -
   31.31 -(* List *)
   31.32 -
   31.33 -structure List =
   31.34 -struct
   31.35 -  open List;
   31.36 -  fun length a = mk_int (List.length a);
   31.37 -  fun nth (a, b) = List.nth (a, dest_int b);
   31.38 -  fun take (a, b) = List.take (a, dest_int b);
   31.39 -  fun drop (a, b) = List.drop (a, dest_int b);
   31.40 -  fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
   31.41 -end;
   31.42 -
   31.43 -val length = List.length;
   31.44 -
   31.45 -
   31.46 -(* Array *)
   31.47 -
   31.48 -structure Array =
   31.49 -struct
   31.50 -  open Array;
   31.51 -  val maxLen = mk_int Array.maxLen;
   31.52 -  fun array (a, b) = Array.array (dest_int a, b);
   31.53 -  fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
   31.54 -  fun length a = mk_int (Array.length a);
   31.55 -  fun sub (a, b) = Array.sub (a, dest_int b);
   31.56 -  fun update (a, b, c) = Array.update (a, dest_int b, c);
   31.57 -  fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
   31.58 -  fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
   31.59 -  fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
   31.60 -  fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
   31.61 -  fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
   31.62 -  fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
   31.63 -  fun findi a b =
   31.64 -    (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
   31.65 -      NONE => NONE
   31.66 -    | SOME (c, d) => SOME (mk_int c, d));
   31.67 -end;
   31.68 -
   31.69 -
   31.70 -(* Vector *)
   31.71 -
   31.72 -structure Vector =
   31.73 -struct
   31.74 -  open Vector;
   31.75 -  val maxLen = mk_int Vector.maxLen;
   31.76 -  fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
   31.77 -  fun length a = mk_int (Vector.length a);
   31.78 -  fun sub (a, b) = Vector.sub (a, dest_int b);
   31.79 -  fun update (a, b, c) = Vector.update (a, dest_int b, c);
   31.80 -  fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
   31.81 -  fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
   31.82 -  fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
   31.83 -  fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
   31.84 -  fun findi a b =
   31.85 -    (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
   31.86 -      NONE => NONE
   31.87 -    | SOME (c, d) => SOME (mk_int c, d));
   31.88 -end;
   31.89 -
   31.90 -
   31.91 -(* CharVector *)
   31.92 -
   31.93 -structure CharVector =
   31.94 -struct
   31.95 -  open CharVector;
   31.96 -  fun tabulate (a, b) = CharVector.tabulate (dest_int a, b o mk_int);
   31.97 -end;
   31.98 -
   31.99 -
  31.100 -(* Word8VectorSlice *)
  31.101 -
  31.102 -structure Word8VectorSlice =
  31.103 -struct
  31.104 -  open Word8VectorSlice;
  31.105 -  val length = mk_int o Word8VectorSlice.length;
  31.106 -  fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c);
  31.107 -end;
  31.108 -
  31.109 -
  31.110 -(* Char *)
  31.111 -
  31.112 -structure Char =
  31.113 -struct
  31.114 -  open Char;
  31.115 -  val maxOrd = mk_int Char.maxOrd;
  31.116 -  val chr = Char.chr o dest_int;
  31.117 -  val ord = mk_int o Char.ord;
  31.118 -end;
  31.119 -
  31.120 -val chr = Char.chr;
  31.121 -val ord = Char.ord;
  31.122 -
  31.123 -
  31.124 -(* String *)
  31.125 -
  31.126 -structure String =
  31.127 -struct
  31.128 -  open String;
  31.129 -  val maxSize = mk_int String.maxSize;
  31.130 -  val size = mk_int o String.size;
  31.131 -  fun sub (a, b) = String.sub (a, dest_int b);
  31.132 -  fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
  31.133 -  fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
  31.134 -end;
  31.135 -
  31.136 -val size = String.size;
  31.137 -val substring = String.substring;
  31.138 -
  31.139 -
  31.140 -(* Substring *)
  31.141 -
  31.142 -structure Substring =
  31.143 -struct
  31.144 -  open Substring;
  31.145 -  fun sub (a, b) = Substring.sub (a, dest_int b);
  31.146 -  val size = mk_int o Substring.size;
  31.147 -  fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
  31.148 -  fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
  31.149 -  fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
  31.150 -  fun triml a b = Substring.triml (dest_int a) b;
  31.151 -  fun trimr a b = Substring.trimr (dest_int a) b;
  31.152 -  fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
  31.153 -  fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
  31.154 -end;
  31.155 -
  31.156 -
  31.157 -(* StringCvt *)
  31.158 -
  31.159 -structure StringCvt =
  31.160 -struct
  31.161 -  open StringCvt;
  31.162 -  datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option;
  31.163 -  fun realfmt fmt = Real.fmt
  31.164 -    (case fmt of
  31.165 -      EXACT => StringCvt.EXACT
  31.166 -    | FIX NONE => StringCvt.FIX NONE
  31.167 -    | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
  31.168 -    | GEN NONE => StringCvt.GEN NONE
  31.169 -    | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
  31.170 -    | SCI NONE => StringCvt.SCI NONE
  31.171 -    | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
  31.172 -  fun padRight a b c = StringCvt.padRight a (dest_int b) c;
  31.173 -  fun padLeft a b c = StringCvt.padLeft a (dest_int b) c;
  31.174 -end;
  31.175 -
  31.176 -
  31.177 -(* Word *)
  31.178 -
  31.179 -structure Word =
  31.180 -struct
  31.181 -  open Word;
  31.182 -  val wordSize = mk_int Word.wordSize;
  31.183 -  val toInt = Word.toLargeInt;
  31.184 -  val toIntX = Word.toLargeIntX;
  31.185 -  val fromInt = Word.fromLargeInt;
  31.186 -end;
  31.187 -
  31.188 -structure Word8 =
  31.189 -struct
  31.190 -  open Word8;
  31.191 -  val wordSize = mk_int Word8.wordSize;
  31.192 -  val toInt = Word8.toLargeInt;
  31.193 -  val toIntX = Word8.toLargeIntX;
  31.194 -  val fromInt = Word8.fromLargeInt;
  31.195 -end;
  31.196 -
  31.197 -structure Word32 =
  31.198 -struct
  31.199 -  open Word32;
  31.200 -  val wordSize = mk_int Word32.wordSize;
  31.201 -  val toInt = Word32.toLargeInt;
  31.202 -  val toIntX = Word32.toLargeIntX;
  31.203 -  val fromInt = Word32.fromLargeInt;
  31.204 -end;
  31.205 -
  31.206 -structure LargeWord =
  31.207 -struct
  31.208 -  open LargeWord;
  31.209 -  val wordSize = mk_int LargeWord.wordSize;
  31.210 -  val toInt = LargeWord.toLargeInt;
  31.211 -  val toIntX = LargeWord.toLargeIntX;
  31.212 -  val fromInt = LargeWord.fromLargeInt;
  31.213 -end;
  31.214 -
  31.215 -
  31.216 -(* Real *)
  31.217 -
  31.218 -structure Real =
  31.219 -struct
  31.220 -  open Real;
  31.221 -  val radix = mk_int Real.radix;
  31.222 -  val precision = mk_int Real.precision;
  31.223 -  fun sign a = mk_int (Real.sign a);
  31.224 -  fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
  31.225 -  fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
  31.226 -  val ceil = mk_int o Real.ceil;
  31.227 -  val floor = mk_int o Real.floor;
  31.228 -  val real = Real.fromInt o dest_int;
  31.229 -  val round = mk_int o Real.round;
  31.230 -  val trunc = mk_int o Real.trunc;
  31.231 -  fun toInt a b = mk_int (Real.toInt a b);
  31.232 -  fun fromInt a = Real.fromInt (dest_int a);
  31.233 -  val fmt = StringCvt.realfmt;
  31.234 -end;
  31.235 -
  31.236 -val ceil = Real.ceil;
  31.237 -val floor = Real.floor;
  31.238 -val real = Real.real;
  31.239 -val round = Real.round;
  31.240 -val trunc = Real.trunc;
  31.241 -
  31.242 -
  31.243 -(* TextIO *)
  31.244 -
  31.245 -structure TextIO =
  31.246 -struct
  31.247 -  open TextIO;
  31.248 -  fun inputN (a, b) = TextIO.inputN (a, dest_int b);
  31.249 -  fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
  31.250 -end;
  31.251 -
  31.252 -
  31.253 -(* BinIO *)
  31.254 -
  31.255 -structure BinIO =
  31.256 -struct
  31.257 -  open BinIO;
  31.258 -  fun inputN (a, b) = BinIO.inputN (a, dest_int b);
  31.259 -  fun canInput (a, b) = Option.map mk_int (BinIO.canInput (a, dest_int b));
  31.260 -end;
  31.261 -
  31.262 -
  31.263 -(* Time *)
  31.264 -
  31.265 -structure Time =
  31.266 -struct
  31.267 -  open Time;
  31.268 -  fun fmt a b = Time.fmt (dest_int a) b;
  31.269 -end;
  31.270 -
  31.271 -
  31.272 -(* Sockets *)
  31.273 -
  31.274 -structure INetSock =
  31.275 -struct
  31.276 -  open INetSock;
  31.277 -  fun toAddr (a, b) = INetSock.toAddr (a, dest_int b);
  31.278 -  fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;
  31.279 -end;
  31.280 -
  31.281 -
  31.282 -(* OS.FileSys *)
  31.283 -
  31.284 -structure OS =
  31.285 -struct
  31.286 -  open OS;
  31.287 -  structure FileSys =
  31.288 -  struct
  31.289 -    open FileSys;
  31.290 -    fun fileSize a = mk_int (FileSys.fileSize a);
  31.291 -  end;
  31.292 -end;
    32.1 --- a/src/Pure/RAW/single_assignment.ML	Wed Feb 17 21:08:18 2016 +0100
    32.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.3 @@ -1,33 +0,0 @@
    32.4 -(*  Title:      Pure/RAW/single_assignment.ML
    32.5 -    Author:     Makarius
    32.6 -
    32.7 -References with single assignment.  Unsynchronized!
    32.8 -*)
    32.9 -
   32.10 -signature SINGLE_ASSIGNMENT =
   32.11 -sig
   32.12 -  type 'a saref
   32.13 -  exception Locked
   32.14 -  val saref: unit -> 'a saref
   32.15 -  val savalue: 'a saref -> 'a option
   32.16 -  val saset: 'a saref * 'a -> unit
   32.17 -end;
   32.18 -
   32.19 -structure SingleAssignment: SINGLE_ASSIGNMENT =
   32.20 -struct
   32.21 -
   32.22 -exception Locked;
   32.23 -
   32.24 -abstype 'a saref = SARef of 'a option ref
   32.25 -with
   32.26 -
   32.27 -fun saref () = SARef (ref NONE);
   32.28 -
   32.29 -fun savalue (SARef r) = ! r;
   32.30 -
   32.31 -fun saset (SARef (r as ref NONE), x) = r := SOME x
   32.32 -  | saset _ = raise Locked;
   32.33 -
   32.34 -end;
   32.35 -
   32.36 -end;
    33.1 --- a/src/Pure/RAW/thread_dummy.ML	Wed Feb 17 21:08:18 2016 +0100
    33.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.3 @@ -1,82 +0,0 @@
    33.4 -(*  Title:      Pure/RAW/thread_dummy.ML
    33.5 -    Author:     Makarius
    33.6 -
    33.7 -Default (mostly dummy) implementation of thread structures
    33.8 -(cf. polyml/basis/Thread.sml).
    33.9 -*)
   33.10 -
   33.11 -exception Thread of string;
   33.12 -
   33.13 -local fun fail _ = raise Thread "No multithreading support on this ML platform" in
   33.14 -
   33.15 -structure Mutex =
   33.16 -struct
   33.17 -  type mutex = unit;
   33.18 -  fun mutex _ = ();
   33.19 -  fun lock _ = fail ();
   33.20 -  fun unlock _ = fail ();
   33.21 -  fun trylock _ = fail ();
   33.22 -end;
   33.23 -
   33.24 -structure ConditionVar =
   33.25 -struct
   33.26 -  type conditionVar = unit;
   33.27 -  fun conditionVar _ = ();
   33.28 -  fun wait _ = fail ();
   33.29 -  fun waitUntil _ = fail ();
   33.30 -  fun signal _ = fail ();
   33.31 -  fun broadcast _ = fail ();
   33.32 -end;
   33.33 -
   33.34 -structure Thread =
   33.35 -struct
   33.36 -  type thread = unit;
   33.37 -
   33.38 -  datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
   33.39 -    and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
   33.40 -
   33.41 -  fun unavailable () = fail ();
   33.42 -
   33.43 -  fun fork _ = fail ();
   33.44 -  fun exit _ = fail ();
   33.45 -  fun isActive _ = fail ();
   33.46 -
   33.47 -  fun equal _ = fail ();
   33.48 -  fun self _ = fail ();
   33.49 -
   33.50 -  fun interrupt _ = fail ();
   33.51 -  fun broadcastInterrupt _ = fail ();
   33.52 -  fun testInterrupt _ = fail ();
   33.53 -
   33.54 -  fun kill _ = fail ();
   33.55 -
   33.56 -  fun setAttributes _ = fail ();
   33.57 -  fun getAttributes _ = fail ();
   33.58 -
   33.59 -  fun numProcessors _ = fail ();
   33.60 -
   33.61 -
   33.62 -(* thread data *)
   33.63 -
   33.64 -local
   33.65 -
   33.66 -val data = ref ([]: Universal.universal  ref list);
   33.67 -
   33.68 -fun find_data tag =
   33.69 -  let
   33.70 -    fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
   33.71 -      | find [] = NONE;
   33.72 -  in find (! data) end;
   33.73 -
   33.74 -in
   33.75 -
   33.76 -fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag);
   33.77 -
   33.78 -fun setLocal (tag, x) =
   33.79 -  (case find_data tag of
   33.80 -    SOME r => r := Universal.tagInject tag x
   33.81 -  | NONE => data :=  ref (Universal.tagInject tag x) :: ! data);
   33.82 -
   33.83 -end;
   33.84 -end;
   33.85 -end;
    34.1 --- a/src/Pure/RAW/universal.ML	Wed Feb 17 21:08:18 2016 +0100
    34.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    34.3 @@ -1,41 +0,0 @@
    34.4 -(*  Title:      Pure/RAW/universal.ML
    34.5 -    Author:     Makarius
    34.6 -
    34.7 -Universal values via tagged union.  Emulates structure Universal
    34.8 -from Poly/ML 5.1.
    34.9 -*)
   34.10 -
   34.11 -signature UNIVERSAL =
   34.12 -sig
   34.13 -  type universal
   34.14 -  type 'a tag
   34.15 -  val tag: unit -> 'a tag
   34.16 -  val tagIs: 'a tag -> universal -> bool
   34.17 -  val tagInject: 'a tag -> 'a -> universal
   34.18 -  val tagProject: 'a tag -> universal -> 'a
   34.19 -end;
   34.20 -
   34.21 -structure Universal: UNIVERSAL =
   34.22 -struct
   34.23 -
   34.24 -type universal = exn;
   34.25 -
   34.26 -datatype 'a tag = Tag of
   34.27 - {is: universal -> bool,
   34.28 -  inject: 'a -> universal,
   34.29 -  project: universal -> 'a};
   34.30 -
   34.31 -fun tag () =
   34.32 -  let exception Universal of 'a in
   34.33 -   Tag {
   34.34 -    is = fn Universal _ => true | _ => false,
   34.35 -    inject = Universal,
   34.36 -    project = fn Universal x => x}
   34.37 -  end;
   34.38 -
   34.39 -fun tagIs (Tag {is, ...}) = is;
   34.40 -fun tagInject (Tag {inject, ...}) = inject;
   34.41 -fun tagProject (Tag {project, ...}) = project;
   34.42 -
   34.43 -end;
   34.44 -
    35.1 --- a/src/Pure/RAW/use_context.ML	Wed Feb 17 21:08:18 2016 +0100
    35.2 +++ b/src/Pure/RAW/use_context.ML	Wed Feb 17 23:06:24 2016 +0100
    35.3 @@ -5,8 +5,7 @@
    35.4  *)
    35.5  
    35.6  type use_context =
    35.7 - {tune_source: string -> string,
    35.8 -  name_space: ML_Name_Space.T,
    35.9 + {name_space: ML_Name_Space.T,
   35.10    str_of_pos: int -> string -> string,
   35.11    print: string -> unit,
   35.12    error: string -> unit};
    36.1 --- a/src/Pure/ROOT	Wed Feb 17 21:08:18 2016 +0100
    36.2 +++ b/src/Pure/ROOT	Wed Feb 17 23:06:24 2016 +0100
    36.3 @@ -6,7 +6,6 @@
    36.4      "RAW/ROOT_polyml-5.5.2.ML"
    36.5      "RAW/ROOT_polyml-5.6.ML"
    36.6      "RAW/ROOT_polyml.ML"
    36.7 -    "RAW/ROOT_smlnj.ML"
    36.8      "RAW/compiler_polyml.ML"
    36.9      "RAW/exn.ML"
   36.10      "RAW/exn_trace_polyml-5.5.1.ML"
   36.11 @@ -14,7 +13,6 @@
   36.12      "RAW/ml_compiler_parameters_polyml-5.6.ML"
   36.13      "RAW/ml_debugger.ML"
   36.14      "RAW/ml_debugger_polyml-5.6.ML"
   36.15 -    "RAW/ml_name_space.ML"
   36.16      "RAW/ml_name_space_polyml-5.6.ML"
   36.17      "RAW/ml_name_space_polyml.ML"
   36.18      "RAW/ml_parse_tree.ML"
   36.19 @@ -28,14 +26,8 @@
   36.20      "RAW/ml_system.ML"
   36.21      "RAW/multithreading.ML"
   36.22      "RAW/multithreading_polyml.ML"
   36.23 -    "RAW/overloading_smlnj.ML"
   36.24 -    "RAW/pp_dummy.ML"
   36.25 -    "RAW/proper_int.ML"
   36.26      "RAW/share_common_data_polyml-5.3.0.ML"
   36.27 -    "RAW/single_assignment.ML"
   36.28      "RAW/single_assignment_polyml.ML"
   36.29 -    "RAW/thread_dummy.ML"
   36.30 -    "RAW/universal.ML"
   36.31      "RAW/unsynchronized.ML"
   36.32      "RAW/use_context.ML"
   36.33      "RAW/windows_path.ML"
   36.34 @@ -46,7 +38,6 @@
   36.35      "RAW/ROOT_polyml-5.5.2.ML"
   36.36      "RAW/ROOT_polyml-5.6.ML"
   36.37      "RAW/ROOT_polyml.ML"
   36.38 -    "RAW/ROOT_smlnj.ML"
   36.39      "RAW/compiler_polyml.ML"
   36.40      "RAW/exn.ML"
   36.41      "RAW/exn_trace_polyml-5.5.1.ML"
   36.42 @@ -54,7 +45,6 @@
   36.43      "RAW/ml_compiler_parameters_polyml-5.6.ML"
   36.44      "RAW/ml_debugger.ML"
   36.45      "RAW/ml_debugger_polyml-5.6.ML"
   36.46 -    "RAW/ml_name_space.ML"
   36.47      "RAW/ml_name_space_polyml-5.6.ML"
   36.48      "RAW/ml_name_space_polyml.ML"
   36.49      "RAW/ml_parse_tree.ML"
   36.50 @@ -68,14 +58,8 @@
   36.51      "RAW/ml_system.ML"
   36.52      "RAW/multithreading.ML"
   36.53      "RAW/multithreading_polyml.ML"
   36.54 -    "RAW/overloading_smlnj.ML"
   36.55 -    "RAW/pp_dummy.ML"
   36.56 -    "RAW/proper_int.ML"
   36.57      "RAW/share_common_data_polyml-5.3.0.ML"
   36.58 -    "RAW/single_assignment.ML"
   36.59      "RAW/single_assignment_polyml.ML"
   36.60 -    "RAW/thread_dummy.ML"
   36.61 -    "RAW/universal.ML"
   36.62      "RAW/unsynchronized.ML"
   36.63      "RAW/use_context.ML"
   36.64      "RAW/windows_path.ML"
   36.65 @@ -179,13 +163,10 @@
   36.66      "Isar/token.ML"
   36.67      "Isar/toplevel.ML"
   36.68      "Isar/typedecl.ML"
   36.69 -    "ML/exn_output.ML"
   36.70      "ML/exn_output_polyml.ML"
   36.71 -    "ML/exn_properties_dummy.ML"
   36.72      "ML/exn_properties_polyml.ML"
   36.73      "ML/install_pp_polyml.ML"
   36.74      "ML/ml_antiquotation.ML"
   36.75 -    "ML/ml_compiler.ML"
   36.76      "ML/ml_compiler_polyml.ML"
   36.77      "ML/ml_context.ML"
   36.78      "ML/ml_env.ML"
    37.1 --- a/src/Pure/ROOT.ML	Wed Feb 17 21:08:18 2016 +0100
    37.2 +++ b/src/Pure/ROOT.ML	Wed Feb 17 23:06:24 2016 +0100
    37.3 @@ -76,7 +76,7 @@
    37.4  use "General/timing.ML";
    37.5  
    37.6  use "General/sha1.ML";
    37.7 -if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
    37.8 +use "General/sha1_polyml.ML";
    37.9  use "General/sha1_samples.ML";
   37.10  
   37.11  use "PIDE/yxml.ML";
   37.12 @@ -98,9 +98,7 @@
   37.13  
   37.14  (* concurrency within the ML runtime *)
   37.15  
   37.16 -if ML_System.is_polyml
   37.17 -then use "ML/exn_properties_polyml.ML"
   37.18 -else use "ML/exn_properties_dummy.ML";
   37.19 +use "ML/exn_properties_polyml.ML";
   37.20  
   37.21  if ML_System.name = "polyml-5.5.0"
   37.22    orelse ML_System.name = "polyml-5.5.1"
   37.23 @@ -123,8 +121,7 @@
   37.24  use "Concurrent/task_queue.ML";
   37.25  use "Concurrent/future.ML";
   37.26  use "Concurrent/event_timer.ML";
   37.27 -
   37.28 -if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
   37.29 +use "Concurrent/time_limit.ML";
   37.30  
   37.31  use "Concurrent/lazy.ML";
   37.32  if Multithreading.available then ()
   37.33 @@ -203,13 +200,11 @@
   37.34  use "ML/ml_syntax.ML";
   37.35  use "ML/ml_env.ML";
   37.36  use "ML/ml_options.ML";
   37.37 -use "ML/exn_output.ML";
   37.38 -if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
   37.39 +use "ML/exn_output_polyml.ML";
   37.40  use "ML/ml_options.ML";
   37.41  use "Isar/runtime.ML";
   37.42  use "PIDE/execution.ML";
   37.43 -use "ML/ml_compiler.ML";
   37.44 -if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
   37.45 +use "ML/ml_compiler_polyml.ML";
   37.46  
   37.47  use "skip_proof.ML";
   37.48  use "goal.ML";
   37.49 @@ -359,7 +354,7 @@
   37.50  toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
   37.51  toplevel_pp ["Morphism", "morphism"] "Morphism.pretty";
   37.52  
   37.53 -if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
   37.54 +use "ML/install_pp_polyml.ML";
   37.55  
   37.56  
   37.57  (* the Pure theory *)
    38.1 --- a/src/Tools/Code/code_runtime.ML	Wed Feb 17 21:08:18 2016 +0100
    38.2 +++ b/src/Tools/Code/code_runtime.ML	Wed Feb 17 23:06:24 2016 +0100
    38.3 @@ -510,8 +510,7 @@
    38.4  fun abort _ = error "Only value bindings allowed.";
    38.5  
    38.6  val notifying_context : use_context =
    38.7 - {tune_source = #tune_source ML_Env.local_context,
    38.8 -  name_space =
    38.9 + {name_space =
   38.10     {lookupVal    = #lookupVal ML_Env.local_name_space,
   38.11      lookupType   = #lookupType ML_Env.local_name_space,
   38.12      lookupFix    = #lookupFix ML_Env.local_name_space,
    39.1 --- a/src/Tools/ROOT	Wed Feb 17 21:08:18 2016 +0100
    39.2 +++ b/src/Tools/ROOT	Wed Feb 17 23:06:24 2016 +0100
    39.3 @@ -1,11 +1,8 @@
    39.4  session Spec_Check in Spec_Check = Pure +
    39.5    theories
    39.6      Spec_Check
    39.7 -  theories [condition = ML_SYSTEM_POLYML]
    39.8      Examples
    39.9  
   39.10  session SML in SML = Pure +
   39.11 -  options [condition = ML_SYSTEM_POLYML]
   39.12    theories
   39.13      Examples
   39.14 -
    40.1 --- a/src/Tools/Spec_Check/spec_check.ML	Wed Feb 17 21:08:18 2016 +0100
    40.2 +++ b/src/Tools/Spec_Check/spec_check.ML	Wed Feb 17 23:06:24 2016 +0100
    40.3 @@ -128,8 +128,7 @@
    40.4    let
    40.5      val return = Unsynchronized.ref "return"
    40.6      val use_context : use_context =
    40.7 -     {tune_source = #tune_source ML_Env.local_context,
    40.8 -      name_space = #name_space ML_Env.local_context,
    40.9 +     {name_space = #name_space ML_Env.local_context,
   40.10        str_of_pos = #str_of_pos ML_Env.local_context,
   40.11        print = fn r => return := r,
   40.12        error = #error ML_Env.local_context}