--- a/Admin/Release/CHECKLIST Wed Feb 17 21:08:18 2016 +0100
+++ b/Admin/Release/CHECKLIST Wed Feb 17 23:06:24 2016 +0100
@@ -1,11 +1,11 @@
Checklist for official releases
===============================
-- check latest updates of polyml, smlnj, jdk, scala, jedit;
+- check latest updates of polyml, jdk, scala, jedit;
- check Admin/components;
-- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj;
+- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0;
- test 'display_drafts' command;
--- a/Admin/isatest/isatest-makeall Wed Feb 17 21:08:18 2016 +0100
+++ b/Admin/isatest/isatest-makeall Wed Feb 17 23:06:24 2016 +0100
@@ -24,7 +24,7 @@
echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
echo
echo "Examples:"
- echo " $PRG ~/settings/at-poly ~/settings/at-sml"
+ echo " $PRG ~/settings/at-poly"
echo " $PRG -l \"HOL-Library HOL-Bali\" ~/settings/at-poly"
exit 1
}
@@ -92,14 +92,7 @@
[ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
- case "$SETTINGS" in
- *sml*)
- BUILD_ARGS="-o timeout=72000 $BUILD_ARGS"
- ;;
- *)
- BUILD_ARGS="-o timeout=10800 $BUILD_ARGS"
- ;;
- esac
+ BUILD_ARGS="-o timeout=10800 $BUILD_ARGS"
# logfile setup
--- a/Admin/isatest/isatest-makedist Wed Feb 17 21:08:18 2016 +0100
+++ b/Admin/isatest/isatest-makedist Wed Feb 17 23:06:24 2016 +0100
@@ -102,8 +102,6 @@
$SSH lxbroy10 "$MAKEALL -x HOL-Proofs $HOME/settings/at64-poly"
sleep 15
-$SSH lxbroy3 "$MAKEALL -l HOL-Unix $HOME/settings/at-sml-dev-e"
-sleep 15
$SSH lxbroy4 "
$MAKEALL -l HOL-Library $HOME/settings/at-poly;
$MAKEALL -l HOL-Library $HOME/settings/at-poly-e;
--- a/Admin/isatest/isatest-stats Wed Feb 17 21:08:18 2016 +0100
+++ b/Admin/isatest/isatest-stats Wed Feb 17 23:06:24 2016 +0100
@@ -6,7 +6,7 @@
THIS="$(cd "$(dirname "$0")"; pwd)"
-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"
+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"
ISABELLE_SESSIONS="
HOL
--- a/Admin/isatest/settings/at-sml-dev-e Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-
-ML_SYSTEM=smlnj
-ML_HOME="/home/smlnj/110.79/bin"
-ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
-ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-
-ISABELLE_GHC=/usr/bin/ghc
-
-ISABELLE_HOME_USER="$HOME/isabelle-at-sml-dev-e"
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf"
-
--- a/NEWS Wed Feb 17 21:08:18 2016 +0100
+++ b/NEWS Wed Feb 17 23:06:24 2016 +0100
@@ -33,6 +33,12 @@
INCOMPATIBILITY.
+*** System ***
+
+* SML/NJ is no longer supported.
+
+
+
New in Isabelle2016 (February 2016)
-----------------------------------
--- a/etc/settings Wed Feb 17 21:08:18 2016 +0100
+++ b/etc/settings Wed Feb 17 23:06:24 2016 +0100
@@ -129,17 +129,9 @@
###
-### Misc old-style settings
+### Misc settings
###
-# Standard ML of New Jersey (slow!)
-#ML_SYSTEM=smlnj-110
-#ML_HOME="/usr/local/smlnj/bin"
-#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
-#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-#SMLNJ_CYGWIN_RUNTIME=1
-
-# Misc programming languages
#ISABELLE_GHC="/usr/bin/ghc"
#ISABELLE_OCAML="/usr/bin/ocaml"
#ISABELLE_SWIPL="/usr/bin/swipl"
--- a/lib/scripts/getsettings Wed Feb 17 21:08:18 2016 +0100
+++ b/lib/scripts/getsettings Wed Feb 17 23:06:24 2016 +0100
@@ -290,16 +290,6 @@
#enforce JAVA_HOME
export JAVA_HOME="$ISABELLE_JDK_HOME/jre"
-#build condition etc.
-case "$ML_SYSTEM" in
- polyml*)
- ML_SYSTEM_POLYML="true"
- ;;
- *)
- ML_SYSTEM_POLYML=""
- ;;
-esac
-
set +o allexport
fi
--- a/lib/scripts/run-smlnj Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,97 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# SML/NJ startup script (for 110 or later).
-
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-function fail_out()
-{
- fail "Unable to create output heap file: \"$OUTFILE\""
-}
-
-function check_mlhome_file()
-{
- [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-function check_heap_file()
-{
- if [ ! -f "$1" ]; then
- echo "Expected to find ML heap file $1" >&2
- return 1
- else
- return 0
- fi
-}
-
-
-
-## compiler binaries
-
-[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
-
-SML="$ML_HOME/sml"
-ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
-
-check_mlhome_file "$SML"
-check_mlhome_file "$ARCH_N_OPSYS"
-
-eval $("$ARCH_N_OPSYS")
-
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
- EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
- DB=""
-else
- EXIT=""
- DB="@SMLload=$INFILE"
-fi
-
-if [ -z "$OUTFILE" ]; then
- MLEXIT=""
-else
- if [ -z "$INFILE" ]; then
- MLEXIT="if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};"
- else
- MLEXIT="Session.save \"$OUTFILE\";"
- fi
- [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-fi
-
-
-## run it!
-
-MLTEXT="$EXIT $MLTEXT"
-
-if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
-else
- FEEDER_OPTS="-q"
-fi
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-RC="$?"
-
-
-## fix heap file name and permissions
-
-if [ -n "$OUTFILE" ]; then
- check_heap_file "$OUTFILE" && [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-fi
-
-exit "$RC"
--- a/src/Doc/Implementation/ML.thy Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Doc/Implementation/ML.thy Wed Feb 17 23:06:24 2016 +0100
@@ -505,7 +505,7 @@
ML and Isar are intertwined via an open-ended bootstrap process that
provides more and more programming facilities and logical content in an
alternating manner. Bootstrapping starts from the raw environment of
- existing implementations of Standard ML (mainly Poly/ML, but also SML/NJ).
+ existing implementations of Standard ML (mainly Poly/ML).
Isabelle/Pure marks the point where the raw ML toplevel is superseded by
Isabelle/ML within the Isar theory and proof language, with a uniform
@@ -1379,8 +1379,7 @@
\<^descr> Type @{ML_type int} represents regular mathematical integers, which are
\<^emph>\<open>unbounded\<close>. Overflow is treated properly, but should never happen in
practice.\<^footnote>\<open>The size limit for integer bit patterns in memory is 64\,MB for
- 32-bit Poly/ML, and much higher for 64-bit systems.\<close> This works uniformly
- for all supported ML platforms (Poly/ML and SML/NJ).
+ 32-bit Poly/ML, and much higher for 64-bit systems.\<close>
Literal integers in ML text are forced to be of this one true integer type
--- adhoc overloading of SML97 is disabled.
--- a/src/Doc/ROOT Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Doc/ROOT Wed Feb 17 23:06:24 2016 +0100
@@ -126,7 +126,7 @@
"root.tex"
session Implementation (doc) in "Implementation" = "HOL-Proofs" +
- options [condition = ML_SYSTEM_POLYML, document_variants = "implementation", quick_and_dirty]
+ options [document_variants = "implementation", quick_and_dirty]
theories
Eq
Integration
--- a/src/Doc/System/Basics.thy Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Doc/System/Basics.thy Wed Feb 17 23:06:24 2016 +0100
@@ -187,12 +187,6 @@
of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
values.
- \<^descr>[@{setting_def ML_SYSTEM_POLYML}\<open>\<^sup>*\<close>] is \<^verbatim>\<open>true\<close> for @{setting ML_SYSTEM}
- values derived from Poly/ML, as opposed to SML/NJ where it is empty. This is
- particularly useful with the build option @{system_option condition}
- (\secref{sec:system-options}) to restrict big sessions to something that
- SML/NJ can still handle.
-
\<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
essential for Isabelle/Scala and other JVM-based tools to work properly.
--- a/src/HOL/ROOT Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/ROOT Wed Feb 17 23:06:24 2016 +0100
@@ -18,7 +18,7 @@
description {*
HOL-Main with explicit proof terms.
*}
- options [condition = ML_SYSTEM_POLYML, document = false, quick_and_dirty = false]
+ options [document = false, quick_and_dirty = false]
theories Proofs (*sequential change of global flag!*)
theories "~~/src/HOL/Library/Old_Datatype"
files
@@ -245,24 +245,24 @@
document_files "root.bib" "root.tex"
session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
- options [condition = ML_SYSTEM_POLYML, document = false, browser_info = false]
+ options [document = false, browser_info = false]
theories
Generate
Generate_Binary_Nat
Generate_Target_Nat
Generate_Efficient_Datastructures
Generate_Pretty_Char
- theories [condition = "ML_SYSTEM_POLYML,ISABELLE_GHC"]
+ theories [condition = "ISABELLE_GHC"]
Code_Test_GHC
- theories [condition = "ML_SYSTEM_POLYML,ISABELLE_MLTON"]
+ theories [condition = "ISABELLE_MLTON"]
Code_Test_MLton
- theories [condition = "ML_SYSTEM_POLYML,ISABELLE_OCAMLC"]
+ theories [condition = "ISABELLE_OCAMLC"]
Code_Test_OCaml
- theories [condition = "ML_SYSTEM_POLYML,ISABELLE_POLYML"]
+ theories [condition = "ISABELLE_POLYML"]
Code_Test_PolyML
- theories [condition = "ML_SYSTEM_POLYML,ISABELLE_SCALA"]
+ theories [condition = "ISABELLE_SCALA"]
Code_Test_Scala
- theories [condition = "ML_SYSTEM_POLYML,ISABELLE_SMLNJ"]
+ theories [condition = "ISABELLE_SMLNJ"]
Code_Test_SMLNJ
session "HOL-Metis_Examples" in Metis_Examples = HOL +
@@ -394,11 +394,11 @@
description {*
Various decision procedures, typically involving reflection.
*}
- options [condition = ML_SYSTEM_POLYML, document = false]
+ options [document = false]
theories Decision_Procs
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
- options [condition = ML_SYSTEM_POLYML, document = false, parallel_proofs = 0]
+ options [document = false, parallel_proofs = 0]
theories
Hilbert_Classical
XML_Data
@@ -407,7 +407,7 @@
description {*
Examples for program extraction in Higher-Order Logic.
*}
- options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0, quick_and_dirty = false]
+ options [parallel_proofs = 0, quick_and_dirty = false]
theories [document = false]
"~~/src/HOL/Library/Code_Target_Numeral"
"~~/src/HOL/Library/Monad_Syntax"
@@ -432,7 +432,7 @@
The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
*}
- options [condition = ML_SYSTEM_POLYML, print_mode = "no_brackets",
+ options [print_mode = "no_brackets",
parallel_proofs = 0, quick_and_dirty = false]
theories [document = false]
"~~/src/HOL/Library/Code_Target_Int"
@@ -531,7 +531,6 @@
description {*
Miscellaneous examples for Higher-Order Logic.
*}
- options [condition = ML_SYSTEM_POLYML]
theories [document = false]
"~~/src/HOL/Library/State_Monad"
Code_Binary_Nat_examples
@@ -702,7 +701,7 @@
TPTP-related extensions.
*}
- options [condition = ML_SYSTEM_POLYML, document = false]
+ options [document = false]
theories
ATP_Theory_Export
MaSh_Eval
@@ -748,7 +747,7 @@
theories Nominal
session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
- options [condition = ML_SYSTEM_POLYML, document = false]
+ options [document = false]
theories
Class3
CK_Machine
@@ -837,11 +836,11 @@
theories Mirabelle_Test
session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
- options [condition = ML_SYSTEM_POLYML, document = false, timeout = 60]
+ options [document = false, timeout = 60]
theories Ex
session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
- options [condition = ML_SYSTEM_POLYML, document = false, quick_and_dirty]
+ options [document = false, quick_and_dirty]
theories
Boogie
SMT_Examples
@@ -980,7 +979,7 @@
session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
options [document = false]
- theories [condition = ML_SYSTEM_POLYML]
+ theories
Examples
Predicate_Compile_Tests
Predicate_Compile_Quickcheck_Examples
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Feb 17 23:06:24 2016 +0100
@@ -169,7 +169,6 @@
fun alphanumerated_name prefix name =
prefix ^ (raw_explode #> map alphanumerate #> implode) name
-(*SMLNJ complains if type annotation not used below*)
fun mk_binding (config : config) ident =
let
val pre_binding = Binding.name (alphanumerated_name "bnd_" ident)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Feb 17 23:06:24 2016 +0100
@@ -1609,10 +1609,8 @@
(* values_timeout configuration *)
-val default_values_timeout = if ML_System.is_smlnj then 1200.0 else 40.0
-
val values_timeout =
- Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
+ Attrib.setup_config_real @{binding values_timeout} (K 40.0)
val _ =
Theory.setup
--- a/src/Pure/General/socket_io.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/General/socket_io.ML Wed Feb 17 23:06:24 2016 +0100
@@ -25,7 +25,7 @@
val rd =
BinPrimIO.RD {
name = name,
- chunkSize = io_buffer_size,
+ chunkSize = 4096,
readVec = SOME (fn n => Socket.recvVec (socket, n)),
readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
readVecNB = NONE,
@@ -44,7 +44,7 @@
val wr =
BinPrimIO.WR {
name = name,
- chunkSize = io_buffer_size,
+ chunkSize = 4096,
writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
writeVecNB = NONE,
--- a/src/Pure/ML/exn_output.ML Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: Pure/ML/exn_output.ML
- Author: Makarius
-
-Auxiliary operations for exception output -- generic version.
-*)
-
-signature EXN_OUTPUT =
-sig
- val position: exn -> Position.T
- val pretty: exn -> Pretty.T
-end
-
-structure Exn_Output: EXN_OUTPUT =
-struct
-
-fun position (_: exn) = Position.none
-val pretty = Pretty.str o General.exnMessage;
-
-end;
-
--- a/src/Pure/ML/exn_output_polyml.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ML/exn_output_polyml.ML Wed Feb 17 23:06:24 2016 +0100
@@ -4,6 +4,12 @@
Auxiliary operations for exception output -- Poly/ML version.
*)
+signature EXN_OUTPUT =
+sig
+ val position: exn -> Position.T
+ val pretty: exn -> Pretty.T
+end;
+
structure Exn_Output: EXN_OUTPUT =
struct
@@ -16,4 +22,3 @@
Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
end;
-
--- a/src/Pure/ML/exn_properties_dummy.ML Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(* Title: Pure/ML/exn_properties_dummy.ML
- Author: Makarius
-
-Exception properties -- dummy version.
-*)
-
-signature EXN_PROPERTIES =
-sig
- val position_of: 'location -> Position.T
- val get: exn -> Properties.T
- val update: Properties.entry list -> exn -> exn
-end;
-
-structure Exn_Properties: EXN_PROPERTIES =
-struct
-
-fun position_of _ = Position.none;
-
-fun get _ = [];
-fun update _ exn = exn;
-
-end;
-
--- a/src/Pure/ML/ml_compiler.ML Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(* Title: Pure/ML/ml_compiler.ML
- Author: Makarius
-
-Runtime compilation and evaluation -- generic version.
-*)
-
-signature ML_COMPILER =
-sig
- type flags =
- {SML: bool, exchange: bool, redirect: bool, verbose: bool,
- debug: bool option, writeln: string -> unit, warning: string -> unit}
- val flags: flags
- val verbose: bool -> flags -> flags
- val eval: flags -> Position.T -> ML_Lex.token list -> unit
-end
-
-structure ML_Compiler: ML_COMPILER =
-struct
-
-type flags =
- {SML: bool, exchange: bool, redirect: bool, verbose: bool,
- debug: bool option, writeln: string -> unit, warning: string -> unit};
-
-val flags: flags =
- {SML = false, exchange = false, redirect = false, verbose = false,
- debug = NONE, writeln = writeln, warning = warning};
-
-fun verbose b (flags: flags) =
- {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
- verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
-
-fun eval (flags: flags) pos toks =
- let
- val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
- val line = the_default 1 (Position.line_of pos);
- val file = the_default "ML" (Position.file_of pos);
- val debug = the_default false (#debug flags);
- val text = ML_Lex.flatten toks;
- in
- Secure.use_text ML_Env.local_context
- {line = line, file = file, verbose = #verbose flags, debug = debug} text
- end;
-
-end;
--- a/src/Pure/ML/ml_compiler_polyml.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML Wed Feb 17 23:06:24 2016 +0100
@@ -4,10 +4,33 @@
Runtime compilation and evaluation -- Poly/ML version.
*)
+signature ML_COMPILER =
+sig
+ type flags =
+ {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+ debug: bool option, writeln: string -> unit, warning: string -> unit}
+ val flags: flags
+ val verbose: bool -> flags -> flags
+ val eval: flags -> Position.T -> ML_Lex.token list -> unit
+end
+
+
structure ML_Compiler: ML_COMPILER =
struct
-open ML_Compiler;
+(* flags *)
+
+type flags =
+ {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+ debug: bool option, writeln: string -> unit, warning: string -> unit};
+
+val flags: flags =
+ {SML = false, exchange = false, redirect = false, verbose = false,
+ debug = NONE, writeln = writeln, warning = warning};
+
+fun verbose b (flags: flags) =
+ {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
+ verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
(* parse trees *)
--- a/src/Pure/ML/ml_env.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ML/ml_env.ML Wed Feb 17 23:06:24 2016 +0100
@@ -163,8 +163,7 @@
end;
val local_context: use_context =
- {tune_source = ML_Parse.fix_ints,
- name_space = name_space {SML = false, exchange = false},
+ {name_space = name_space {SML = false, exchange = false},
str_of_pos = Position.here oo Position.line_file,
print = writeln,
error = error};
--- a/src/Pure/ML/ml_parse.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ML/ml_parse.ML Wed Feb 17 23:06:24 2016 +0100
@@ -6,7 +6,6 @@
signature ML_PARSE =
sig
- val fix_ints: string -> string
val global_context: use_context
end;
@@ -43,30 +42,10 @@
val blanks = Scan.repeat improper >> implode;
-(* fix_ints *)
-
-(*approximation only -- corrupts numeric record field patterns *)
-val fix_int =
- $$$ "#" ^^ blanks ^^ int ||
- ($$$ "infix" || $$$ "infixr") ^^ blanks ^^ int ||
- int >> (fn x => "(" ^ x ^ ":int)") ||
- regular ||
- bad_input;
-
-val fix_ints =
- ML_System.is_smlnj ?
- (Source.of_string #>
- ML_Lex.source #>
- Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) #>
- Source.exhaust #>
- implode);
-
-
(* global use_context *)
val global_context: use_context =
- {tune_source = fix_ints,
- name_space = ML_Name_Space.global,
+ {name_space = ML_Name_Space.global,
str_of_pos = Position.here oo Position.line_file,
print = writeln,
error = error};
--- a/src/Pure/RAW/ROOT_polyml.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML Wed Feb 17 23:06:24 2016 +0100
@@ -102,8 +102,6 @@
val raw_explode = SML90.explode;
val implode = SML90.implode;
-val io_buffer_size = 4096;
-
fun quit () = exit 0;
--- a/src/Pure/RAW/ROOT_smlnj.ML Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,194 +0,0 @@
-(* Title: Pure/RAW/ROOT_smlnj.ML
-
-Compatibility file for Standard ML of New Jersey.
-*)
-
-val io_buffer_size = 4096;
-use "RAW/proper_int.ML";
-
-exception Interrupt;
-fun reraise exn = raise exn;
-
-fun exit rc = Posix.Process.exit (Word8.fromInt rc);
-fun quit () = exit 0;
-
-use "RAW/overloading_smlnj.ML";
-use "RAW/exn.ML";
-use "RAW/single_assignment.ML";
-use "RAW/universal.ML";
-use "RAW/thread_dummy.ML";
-use "RAW/multithreading.ML";
-use "RAW/ml_stack_dummy.ML";
-use "RAW/ml_pretty.ML";
-use "RAW/ml_name_space.ML";
-structure PolyML = struct end;
-use "RAW/pp_dummy.ML";
-use "RAW/use_context.ML";
-use "RAW/ml_positions.ML";
-
-
-val seconds = Time.fromReal;
-
-(*low-level pointer equality*)
-CM.autoload "$smlnj/init/init.cmi";
-val pointer_eq = InlineT.ptreql;
-
-
-(* restore old-style character / string functions *)
-
-val ord = mk_int o SML90.ord;
-val chr = SML90.chr o dest_int;
-val raw_explode = SML90.explode;
-val implode = SML90.implode;
-
-
-(* New Jersey ML parameters *)
-
-val _ =
- (Control.Print.printLength := 1000;
- Control.Print.printDepth := 350;
- Control.Print.stringDepth := 250;
- Control.Print.signatures := 2;
- Control.MC.matchRedundantError := false);
-
-
-(* Poly/ML emulation *)
-
-(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
-local
- val depth = ref (10: int);
-in
- fun get_default_print_depth () = ! depth;
- fun default_print_depth n =
- (depth := n;
- Control.Print.printDepth := dest_int n div 2;
- Control.Print.printLength := dest_int n);
- val _ = default_print_depth 10;
-end;
-
-fun ml_make_string (_: string) = "(fn _ => \"?\")";
-
-
-(*prompts*)
-fun ml_prompts p1 p2 =
- (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
-
-(*dummy implementation*)
-structure ML_Profiling =
-struct
- fun profile_time (_: (int * string) list -> unit) f x = f x;
- fun profile_time_thread (_: (int * string) list -> unit) f x = f x;
- fun profile_allocations (_: (int * string) list -> unit) f x = f x;
-end;
-
-(*dummy implementation*)
-fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();
-
-
-(* ML command execution *)
-
-fun use_text ({tune_source, print, error, ...}: use_context)
- {line, file, verbose, debug = _: bool} text =
- let
- val ref out_orig = Control.Print.out;
-
- val out_buffer = ref ([]: string list);
- val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
- fun output () =
- let val str = implode (rev (! out_buffer))
- in String.substring (str, 0, Int.max (0, size str - 1)) end;
- in
- Control.Print.out := out;
- Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file text)))
- handle exn =>
- (Control.Print.out := out_orig;
- error ((if file = "" then "" else "Error in " ^ file ^ "\n") ^ output ()); raise exn);
- Control.Print.out := out_orig;
- if verbose then print (output ()) else ()
- end;
-
-fun use_file context {verbose, debug} file =
- let
- val instream = TextIO.openIn file;
- val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
-
-
-(* toplevel pretty printing *)
-
-fun ml_pprint pps =
- let
- fun str "" = ()
- | str s = PrettyPrint.string pps s;
- fun pprint (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
- (str bg;
- (if consistent then PrettyPrint.openHVBox else PrettyPrint.openHOVBox) pps
- (PrettyPrint.Rel (dest_int ind));
- List.app pprint prts; PrettyPrint.closeBox pps;
- str en)
- | pprint (ML_Pretty.String (s, _)) = str s
- | pprint (ML_Pretty.Break (false, width, offset)) =
- PrettyPrint.break pps {nsp = dest_int width, offset = dest_int offset}
- | pprint (ML_Pretty.Break (true, _, _)) = PrettyPrint.newline pps;
- in pprint end;
-
-fun toplevel_pp context path pp =
- use_text context {line = 1, file = "pp", verbose = false, debug = false}
- ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"") path) ^
- "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
-
-
-
-(** interrupts **)
-
-local
-
-fun change_signal new_handler f x =
- let
- val old_handler = Signals.setHandler (Signals.sigINT, new_handler);
- val result = Exn.capture (f old_handler) x;
- val _ = Signals.setHandler (Signals.sigINT, old_handler);
- in Exn.release result end;
-
-in
-
-fun interruptible (f: 'a -> 'b) x =
- let
- val result = ref (Exn.interrupt_exn: 'b Exn.result);
- val old_handler = Signals.inqHandler Signals.sigINT;
- in
- SMLofNJ.Cont.callcc (fn cont =>
- (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont));
- result := Exn.capture f x));
- Signals.setHandler (Signals.sigINT, old_handler);
- Exn.release (! result)
- end;
-
-fun uninterruptible f =
- change_signal Signals.IGNORE
- (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
-
-end;
-
-
-use "RAW/unsynchronized.ML";
-use "RAW/ml_debugger.ML";
-
-
-(* ML system operations *)
-
-fun ml_platform_path (s: string) = s;
-fun ml_standard_path (s: string) = s;
-
-use "RAW/ml_system.ML";
-
-structure ML_System =
-struct
-
-open ML_System;
-
-fun save_state name =
- if SMLofNJ.exportML name then ()
- else OS.FileSys.rename {old = name ^ "." ^ platform, new = name};
-
-end;
--- a/src/Pure/RAW/compiler_polyml.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/RAW/compiler_polyml.ML Wed Feb 17 23:06:24 2016 +0100
@@ -11,12 +11,11 @@
in
-fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+fun use_text ({name_space, str_of_pos, print, error, ...}: use_context)
{line, file, verbose, debug} text =
let
val current_line = Unsynchronized.ref line;
- val in_buffer =
- Unsynchronized.ref (String.explode (tune_source (ml_positions line file text)));
+ val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
val out_buffer = Unsynchronized.ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
--- a/src/Pure/RAW/ml_name_space.ML Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(* Title: Pure/RAW/ml_name_space.ML
- Author: Makarius
-
-ML name space -- dummy version of Poly/ML 5.2 facility.
-*)
-
-structure ML_Name_Space =
-struct
-
-type valueVal = unit;
-type typeVal = unit;
-type fixityVal = unit;
-type structureVal = unit;
-type signatureVal = unit;
-type functorVal = unit;
-
-type T =
- {lookupVal: string -> valueVal option,
- lookupType: string -> typeVal option,
- lookupFix: string -> fixityVal option,
- lookupStruct: string -> structureVal option,
- lookupSig: string -> signatureVal option,
- lookupFunct: string -> functorVal option,
- enterVal: string * valueVal -> unit,
- enterType: string * typeVal -> unit,
- enterFix: string * fixityVal -> unit,
- enterStruct: string * structureVal -> unit,
- enterSig: string * signatureVal -> unit,
- enterFunct: string * functorVal -> unit,
- allVal: unit -> (string * valueVal) list,
- allType: unit -> (string * typeVal) list,
- allFix: unit -> (string * fixityVal) list,
- allStruct: unit -> (string * structureVal) list,
- allSig: unit -> (string * signatureVal) list,
- allFunct: unit -> (string * functorVal) list};
-
-val global: T =
- {lookupVal = fn _ => NONE,
- lookupType = fn _ => NONE,
- lookupFix = fn _ => NONE,
- lookupStruct = fn _ => NONE,
- lookupSig = fn _ => NONE,
- lookupFunct = fn _ => NONE,
- enterVal = fn _ => (),
- enterType = fn _ => (),
- enterFix = fn _ => (),
- enterStruct = fn _ => (),
- enterSig = fn _ => (),
- enterFunct = fn _ => (),
- allVal = fn _ => [],
- allType = fn _ => [],
- allFix = fn _ => [],
- allStruct = fn _ => [],
- allSig = fn _ => [],
- allFunct = fn _ => []};
-
-val initial_val : (string * valueVal) list = [];
-val initial_type : (string * typeVal) list = [];
-val initial_fixity : (string * fixityVal) list = [];
-val initial_structure : (string * structureVal) list = [];
-val initial_signature : (string * signatureVal) list = [];
-val initial_functor : (string * functorVal) list = [];
-
-fun forget_global_structure (_: string) = ();
-
-fun display_val (_, _: int, _: T) = ML_Pretty.String ("?", 1);
-
-end;
--- a/src/Pure/RAW/ml_system.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/RAW/ml_system.ML Wed Feb 17 23:06:24 2016 +0100
@@ -7,8 +7,6 @@
signature ML_SYSTEM =
sig
val name: string
- val is_polyml: bool
- val is_smlnj: bool
val platform: string
val platform_is_windows: bool
val share_common_data: unit -> unit
@@ -19,8 +17,6 @@
struct
val SOME name = OS.Process.getEnv "ML_SYSTEM";
-val is_polyml = String.isPrefix "polyml" name;
-val is_smlnj = String.isPrefix "smlnj" name;
val SOME platform = OS.Process.getEnv "ML_PLATFORM";
val platform_is_windows = String.isSuffix "windows" platform;
--- a/src/Pure/RAW/overloading_smlnj.ML Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(* Title: Pure/RAW/overloading_smlnj.ML
- Author: Makarius
-
-Overloading in SML/NJ (cf. smlnj/base/system/smlnj/init/pervasive.sml).
-*)
-
-Control.overloadKW := true;
-
-overload ~ : ('a -> 'a) as
- IntInf.~ and Int31.~ and Int32.~ and Int64.~ and
- Word.~ and Word8.~ and Word32.~ and Word64.~ and Real.~;
-overload + : ('a * 'a -> 'a) as
- IntInf.+ and Int31.+ and Int32.+ and Int64.+ and
- Word.+ and Word8.+ and Word32.+ and Word64.+ and Real.+;
-overload - : ('a * 'a -> 'a) as
- IntInf.- and Int31.- and Int32.- and Int64.- and
- Word.- and Word8.- and Word32.- and Word64.- and Real.-;
-overload * : ('a * 'a -> 'a) as
- IntInf.* and Int31.* and Int32.* and Int64.* and
- Word.* and Word8.* and Word32.* and Word64.* and Real.*;
-overload div: ('a * 'a -> 'a) as
- IntInf.div and Int31.div and Int32.div and Int64.div and
- Word.div and Word8.div and Word32.div and Word64.div;
-overload mod: ('a * 'a -> 'a) as
- IntInf.mod and Int31.mod and Int32.mod and Int64.mod and
- Word.mod and Word8.mod and Word32.mod and Word64.mod;
-overload < : ('a * 'a -> bool) as
- IntInf.< and Int31.< and Int32.< and Int64.< and Real.< and
- Word.< and Word8.< and Word32.< and Word64.< and Char.< and String.<;
-overload <= : ('a * 'a -> bool) as
- IntInf.<= and Int31.<= and Int32.<= and Int64.<= and Real.<= and
- Word.<= and Word8.<= and Word32.<= and Word64.<= and Char.<= and String.<=;
-overload > : ('a * 'a -> bool) as
- IntInf.> and Int31.> and Int32.> and Int64.> and Real.> and
- Word.> and Word8.> and Word32.> and Word64.> and Char.> and String.>;
-overload >= : ('a * 'a -> bool) as
- IntInf.>= and Int31.>= and Int32.>= and Int64.>= and Real.>= and
- Word.>= and Word8.>= and Word32.>= and Word64.>= and Char.>= and String.>=;
-overload abs: ('a -> 'a) as IntInf.abs and Int31.abs and Int32.abs and Int64.abs and Real.abs;
-
-Control.overloadKW := false;
--- a/src/Pure/RAW/pp_dummy.ML Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Pure/RAW/pp_dummy.ML
-
-Dummy setup for toplevel pretty printing.
-*)
-
-fun ml_pretty _ = raise Fail "ml_pretty dummy";
-fun pretty_ml _ = raise Fail "pretty_ml dummy";
-
-structure PolyML =
-struct
- fun addPrettyPrinter _ = ();
- fun prettyRepresentation _ =
- raise Fail "PolyML.prettyRepresentation dummy";
- open PolyML;
-end;
-
--- a/src/Pure/RAW/proper_int.ML Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,289 +0,0 @@
-(* Title: Pure/RAW/proper_int.ML
- Author: Makarius
-
-SML basis with type int representing proper integers, not machine
-words.
-*)
-
-val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
-val dest_int = IntInf.toInt: IntInf.int -> Int.int;
-
-
-(* Int *)
-
-type int = IntInf.int;
-
-structure IntInf =
-struct
- open IntInf;
- fun fromInt (a: int) = a;
- fun toInt (a: int) = a;
- val log2 = mk_int o IntInf.log2;
- val sign = mk_int o IntInf.sign;
-end;
-
-structure Int = IntInf;
-
-
-(* List *)
-
-structure List =
-struct
- open List;
- fun length a = mk_int (List.length a);
- fun nth (a, b) = List.nth (a, dest_int b);
- fun take (a, b) = List.take (a, dest_int b);
- fun drop (a, b) = List.drop (a, dest_int b);
- fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
-end;
-
-val length = List.length;
-
-
-(* Array *)
-
-structure Array =
-struct
- open Array;
- val maxLen = mk_int Array.maxLen;
- fun array (a, b) = Array.array (dest_int a, b);
- fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
- fun length a = mk_int (Array.length a);
- fun sub (a, b) = Array.sub (a, dest_int b);
- fun update (a, b, c) = Array.update (a, dest_int b, c);
- fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
- fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
- fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
- fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
- fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
- fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
- fun findi a b =
- (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
- NONE => NONE
- | SOME (c, d) => SOME (mk_int c, d));
-end;
-
-
-(* Vector *)
-
-structure Vector =
-struct
- open Vector;
- val maxLen = mk_int Vector.maxLen;
- fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
- fun length a = mk_int (Vector.length a);
- fun sub (a, b) = Vector.sub (a, dest_int b);
- fun update (a, b, c) = Vector.update (a, dest_int b, c);
- fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
- fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
- fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
- fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
- fun findi a b =
- (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
- NONE => NONE
- | SOME (c, d) => SOME (mk_int c, d));
-end;
-
-
-(* CharVector *)
-
-structure CharVector =
-struct
- open CharVector;
- fun tabulate (a, b) = CharVector.tabulate (dest_int a, b o mk_int);
-end;
-
-
-(* Word8VectorSlice *)
-
-structure Word8VectorSlice =
-struct
- open Word8VectorSlice;
- val length = mk_int o Word8VectorSlice.length;
- fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c);
-end;
-
-
-(* Char *)
-
-structure Char =
-struct
- open Char;
- val maxOrd = mk_int Char.maxOrd;
- val chr = Char.chr o dest_int;
- val ord = mk_int o Char.ord;
-end;
-
-val chr = Char.chr;
-val ord = Char.ord;
-
-
-(* String *)
-
-structure String =
-struct
- open String;
- val maxSize = mk_int String.maxSize;
- val size = mk_int o String.size;
- fun sub (a, b) = String.sub (a, dest_int b);
- fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
- fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
-end;
-
-val size = String.size;
-val substring = String.substring;
-
-
-(* Substring *)
-
-structure Substring =
-struct
- open Substring;
- fun sub (a, b) = Substring.sub (a, dest_int b);
- val size = mk_int o Substring.size;
- fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
- fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
- fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
- fun triml a b = Substring.triml (dest_int a) b;
- fun trimr a b = Substring.trimr (dest_int a) b;
- fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
- fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
-end;
-
-
-(* StringCvt *)
-
-structure StringCvt =
-struct
- open StringCvt;
- datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option;
- fun realfmt fmt = Real.fmt
- (case fmt of
- EXACT => StringCvt.EXACT
- | FIX NONE => StringCvt.FIX NONE
- | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
- | GEN NONE => StringCvt.GEN NONE
- | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
- | SCI NONE => StringCvt.SCI NONE
- | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
- fun padRight a b c = StringCvt.padRight a (dest_int b) c;
- fun padLeft a b c = StringCvt.padLeft a (dest_int b) c;
-end;
-
-
-(* Word *)
-
-structure Word =
-struct
- open Word;
- val wordSize = mk_int Word.wordSize;
- val toInt = Word.toLargeInt;
- val toIntX = Word.toLargeIntX;
- val fromInt = Word.fromLargeInt;
-end;
-
-structure Word8 =
-struct
- open Word8;
- val wordSize = mk_int Word8.wordSize;
- val toInt = Word8.toLargeInt;
- val toIntX = Word8.toLargeIntX;
- val fromInt = Word8.fromLargeInt;
-end;
-
-structure Word32 =
-struct
- open Word32;
- val wordSize = mk_int Word32.wordSize;
- val toInt = Word32.toLargeInt;
- val toIntX = Word32.toLargeIntX;
- val fromInt = Word32.fromLargeInt;
-end;
-
-structure LargeWord =
-struct
- open LargeWord;
- val wordSize = mk_int LargeWord.wordSize;
- val toInt = LargeWord.toLargeInt;
- val toIntX = LargeWord.toLargeIntX;
- val fromInt = LargeWord.fromLargeInt;
-end;
-
-
-(* Real *)
-
-structure Real =
-struct
- open Real;
- val radix = mk_int Real.radix;
- val precision = mk_int Real.precision;
- fun sign a = mk_int (Real.sign a);
- fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
- fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
- val ceil = mk_int o Real.ceil;
- val floor = mk_int o Real.floor;
- val real = Real.fromInt o dest_int;
- val round = mk_int o Real.round;
- val trunc = mk_int o Real.trunc;
- fun toInt a b = mk_int (Real.toInt a b);
- fun fromInt a = Real.fromInt (dest_int a);
- val fmt = StringCvt.realfmt;
-end;
-
-val ceil = Real.ceil;
-val floor = Real.floor;
-val real = Real.real;
-val round = Real.round;
-val trunc = Real.trunc;
-
-
-(* TextIO *)
-
-structure TextIO =
-struct
- open TextIO;
- fun inputN (a, b) = TextIO.inputN (a, dest_int b);
- fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
-end;
-
-
-(* BinIO *)
-
-structure BinIO =
-struct
- open BinIO;
- fun inputN (a, b) = BinIO.inputN (a, dest_int b);
- fun canInput (a, b) = Option.map mk_int (BinIO.canInput (a, dest_int b));
-end;
-
-
-(* Time *)
-
-structure Time =
-struct
- open Time;
- fun fmt a b = Time.fmt (dest_int a) b;
-end;
-
-
-(* Sockets *)
-
-structure INetSock =
-struct
- open INetSock;
- fun toAddr (a, b) = INetSock.toAddr (a, dest_int b);
- fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;
-end;
-
-
-(* OS.FileSys *)
-
-structure OS =
-struct
- open OS;
- structure FileSys =
- struct
- open FileSys;
- fun fileSize a = mk_int (FileSys.fileSize a);
- end;
-end;
--- a/src/Pure/RAW/single_assignment.ML Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: Pure/RAW/single_assignment.ML
- Author: Makarius
-
-References with single assignment. Unsynchronized!
-*)
-
-signature SINGLE_ASSIGNMENT =
-sig
- type 'a saref
- exception Locked
- val saref: unit -> 'a saref
- val savalue: 'a saref -> 'a option
- val saset: 'a saref * 'a -> unit
-end;
-
-structure SingleAssignment: SINGLE_ASSIGNMENT =
-struct
-
-exception Locked;
-
-abstype 'a saref = SARef of 'a option ref
-with
-
-fun saref () = SARef (ref NONE);
-
-fun savalue (SARef r) = ! r;
-
-fun saset (SARef (r as ref NONE), x) = r := SOME x
- | saset _ = raise Locked;
-
-end;
-
-end;
--- a/src/Pure/RAW/thread_dummy.ML Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-(* Title: Pure/RAW/thread_dummy.ML
- Author: Makarius
-
-Default (mostly dummy) implementation of thread structures
-(cf. polyml/basis/Thread.sml).
-*)
-
-exception Thread of string;
-
-local fun fail _ = raise Thread "No multithreading support on this ML platform" in
-
-structure Mutex =
-struct
- type mutex = unit;
- fun mutex _ = ();
- fun lock _ = fail ();
- fun unlock _ = fail ();
- fun trylock _ = fail ();
-end;
-
-structure ConditionVar =
-struct
- type conditionVar = unit;
- fun conditionVar _ = ();
- fun wait _ = fail ();
- fun waitUntil _ = fail ();
- fun signal _ = fail ();
- fun broadcast _ = fail ();
-end;
-
-structure Thread =
-struct
- type thread = unit;
-
- datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
- and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
-
- fun unavailable () = fail ();
-
- fun fork _ = fail ();
- fun exit _ = fail ();
- fun isActive _ = fail ();
-
- fun equal _ = fail ();
- fun self _ = fail ();
-
- fun interrupt _ = fail ();
- fun broadcastInterrupt _ = fail ();
- fun testInterrupt _ = fail ();
-
- fun kill _ = fail ();
-
- fun setAttributes _ = fail ();
- fun getAttributes _ = fail ();
-
- fun numProcessors _ = fail ();
-
-
-(* thread data *)
-
-local
-
-val data = ref ([]: Universal.universal ref list);
-
-fun find_data tag =
- let
- fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
- | find [] = NONE;
- in find (! data) end;
-
-in
-
-fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag);
-
-fun setLocal (tag, x) =
- (case find_data tag of
- SOME r => r := Universal.tagInject tag x
- | NONE => data := ref (Universal.tagInject tag x) :: ! data);
-
-end;
-end;
-end;
--- a/src/Pure/RAW/universal.ML Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(* Title: Pure/RAW/universal.ML
- Author: Makarius
-
-Universal values via tagged union. Emulates structure Universal
-from Poly/ML 5.1.
-*)
-
-signature UNIVERSAL =
-sig
- type universal
- type 'a tag
- val tag: unit -> 'a tag
- val tagIs: 'a tag -> universal -> bool
- val tagInject: 'a tag -> 'a -> universal
- val tagProject: 'a tag -> universal -> 'a
-end;
-
-structure Universal: UNIVERSAL =
-struct
-
-type universal = exn;
-
-datatype 'a tag = Tag of
- {is: universal -> bool,
- inject: 'a -> universal,
- project: universal -> 'a};
-
-fun tag () =
- let exception Universal of 'a in
- Tag {
- is = fn Universal _ => true | _ => false,
- inject = Universal,
- project = fn Universal x => x}
- end;
-
-fun tagIs (Tag {is, ...}) = is;
-fun tagInject (Tag {inject, ...}) = inject;
-fun tagProject (Tag {project, ...}) = project;
-
-end;
-
--- a/src/Pure/RAW/use_context.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/RAW/use_context.ML Wed Feb 17 23:06:24 2016 +0100
@@ -5,8 +5,7 @@
*)
type use_context =
- {tune_source: string -> string,
- name_space: ML_Name_Space.T,
+ {name_space: ML_Name_Space.T,
str_of_pos: int -> string -> string,
print: string -> unit,
error: string -> unit};
--- a/src/Pure/ROOT Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ROOT Wed Feb 17 23:06:24 2016 +0100
@@ -6,7 +6,6 @@
"RAW/ROOT_polyml-5.5.2.ML"
"RAW/ROOT_polyml-5.6.ML"
"RAW/ROOT_polyml.ML"
- "RAW/ROOT_smlnj.ML"
"RAW/compiler_polyml.ML"
"RAW/exn.ML"
"RAW/exn_trace_polyml-5.5.1.ML"
@@ -14,7 +13,6 @@
"RAW/ml_compiler_parameters_polyml-5.6.ML"
"RAW/ml_debugger.ML"
"RAW/ml_debugger_polyml-5.6.ML"
- "RAW/ml_name_space.ML"
"RAW/ml_name_space_polyml-5.6.ML"
"RAW/ml_name_space_polyml.ML"
"RAW/ml_parse_tree.ML"
@@ -28,14 +26,8 @@
"RAW/ml_system.ML"
"RAW/multithreading.ML"
"RAW/multithreading_polyml.ML"
- "RAW/overloading_smlnj.ML"
- "RAW/pp_dummy.ML"
- "RAW/proper_int.ML"
"RAW/share_common_data_polyml-5.3.0.ML"
- "RAW/single_assignment.ML"
"RAW/single_assignment_polyml.ML"
- "RAW/thread_dummy.ML"
- "RAW/universal.ML"
"RAW/unsynchronized.ML"
"RAW/use_context.ML"
"RAW/windows_path.ML"
@@ -46,7 +38,6 @@
"RAW/ROOT_polyml-5.5.2.ML"
"RAW/ROOT_polyml-5.6.ML"
"RAW/ROOT_polyml.ML"
- "RAW/ROOT_smlnj.ML"
"RAW/compiler_polyml.ML"
"RAW/exn.ML"
"RAW/exn_trace_polyml-5.5.1.ML"
@@ -54,7 +45,6 @@
"RAW/ml_compiler_parameters_polyml-5.6.ML"
"RAW/ml_debugger.ML"
"RAW/ml_debugger_polyml-5.6.ML"
- "RAW/ml_name_space.ML"
"RAW/ml_name_space_polyml-5.6.ML"
"RAW/ml_name_space_polyml.ML"
"RAW/ml_parse_tree.ML"
@@ -68,14 +58,8 @@
"RAW/ml_system.ML"
"RAW/multithreading.ML"
"RAW/multithreading_polyml.ML"
- "RAW/overloading_smlnj.ML"
- "RAW/pp_dummy.ML"
- "RAW/proper_int.ML"
"RAW/share_common_data_polyml-5.3.0.ML"
- "RAW/single_assignment.ML"
"RAW/single_assignment_polyml.ML"
- "RAW/thread_dummy.ML"
- "RAW/universal.ML"
"RAW/unsynchronized.ML"
"RAW/use_context.ML"
"RAW/windows_path.ML"
@@ -179,13 +163,10 @@
"Isar/token.ML"
"Isar/toplevel.ML"
"Isar/typedecl.ML"
- "ML/exn_output.ML"
"ML/exn_output_polyml.ML"
- "ML/exn_properties_dummy.ML"
"ML/exn_properties_polyml.ML"
"ML/install_pp_polyml.ML"
"ML/ml_antiquotation.ML"
- "ML/ml_compiler.ML"
"ML/ml_compiler_polyml.ML"
"ML/ml_context.ML"
"ML/ml_env.ML"
--- a/src/Pure/ROOT.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ROOT.ML Wed Feb 17 23:06:24 2016 +0100
@@ -76,7 +76,7 @@
use "General/timing.ML";
use "General/sha1.ML";
-if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
+use "General/sha1_polyml.ML";
use "General/sha1_samples.ML";
use "PIDE/yxml.ML";
@@ -98,9 +98,7 @@
(* concurrency within the ML runtime *)
-if ML_System.is_polyml
-then use "ML/exn_properties_polyml.ML"
-else use "ML/exn_properties_dummy.ML";
+use "ML/exn_properties_polyml.ML";
if ML_System.name = "polyml-5.5.0"
orelse ML_System.name = "polyml-5.5.1"
@@ -123,8 +121,7 @@
use "Concurrent/task_queue.ML";
use "Concurrent/future.ML";
use "Concurrent/event_timer.ML";
-
-if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
+use "Concurrent/time_limit.ML";
use "Concurrent/lazy.ML";
if Multithreading.available then ()
@@ -203,13 +200,11 @@
use "ML/ml_syntax.ML";
use "ML/ml_env.ML";
use "ML/ml_options.ML";
-use "ML/exn_output.ML";
-if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
+use "ML/exn_output_polyml.ML";
use "ML/ml_options.ML";
use "Isar/runtime.ML";
use "PIDE/execution.ML";
-use "ML/ml_compiler.ML";
-if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
+use "ML/ml_compiler_polyml.ML";
use "skip_proof.ML";
use "goal.ML";
@@ -359,7 +354,7 @@
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
toplevel_pp ["Morphism", "morphism"] "Morphism.pretty";
-if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
+use "ML/install_pp_polyml.ML";
(* the Pure theory *)
--- a/src/Tools/Code/code_runtime.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Tools/Code/code_runtime.ML Wed Feb 17 23:06:24 2016 +0100
@@ -510,8 +510,7 @@
fun abort _ = error "Only value bindings allowed.";
val notifying_context : use_context =
- {tune_source = #tune_source ML_Env.local_context,
- name_space =
+ {name_space =
{lookupVal = #lookupVal ML_Env.local_name_space,
lookupType = #lookupType ML_Env.local_name_space,
lookupFix = #lookupFix ML_Env.local_name_space,
--- a/src/Tools/ROOT Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Tools/ROOT Wed Feb 17 23:06:24 2016 +0100
@@ -1,11 +1,8 @@
session Spec_Check in Spec_Check = Pure +
theories
Spec_Check
- theories [condition = ML_SYSTEM_POLYML]
Examples
session SML in SML = Pure +
- options [condition = ML_SYSTEM_POLYML]
theories
Examples
-
--- a/src/Tools/Spec_Check/spec_check.ML Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Tools/Spec_Check/spec_check.ML Wed Feb 17 23:06:24 2016 +0100
@@ -128,8 +128,7 @@
let
val return = Unsynchronized.ref "return"
val use_context : use_context =
- {tune_source = #tune_source ML_Env.local_context,
- name_space = #name_space ML_Env.local_context,
+ {name_space = #name_space ML_Env.local_context,
str_of_pos = #str_of_pos ML_Env.local_context,
print = fn r => return := r,
error = #error ML_Env.local_context}