--- a/Admin/Release/CHECKLIST Wed Feb 17 21:51:58 2016 +0100
+++ b/Admin/Release/CHECKLIST Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/Admin/isatest/isatest-makeall Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/Admin/isatest/isatest-makedist Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/Admin/isatest/isatest-stats Wed Feb 17 23:29:35 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:51:58 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:51:58 2016 +0100
+++ b/NEWS Wed Feb 17 23:29:35 2016 +0100
@@ -136,6 +136,12 @@
INCOMPATIBILITY.
+*** System ***
+
+* SML/NJ is no longer supported.
+
+
+
New in Isabelle2016 (February 2016)
-----------------------------------
--- a/etc/settings Wed Feb 17 21:51:58 2016 +0100
+++ b/etc/settings Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/lib/scripts/getsettings Wed Feb 17 23:29:35 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:51:58 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:51:58 2016 +0100
+++ b/src/Doc/Implementation/ML.thy Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/src/Doc/ROOT Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/src/Doc/System/Basics.thy Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/src/HOL/ROOT Wed Feb 17 23:29:35 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
@@ -246,24 +246,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 +
@@ -395,11 +395,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
@@ -408,7 +408,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"
@@ -433,7 +433,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"
@@ -532,7 +532,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
@@ -703,7 +702,7 @@
TPTP-related extensions.
*}
- options [condition = ML_SYSTEM_POLYML, document = false]
+ options [document = false]
theories
ATP_Theory_Export
MaSh_Eval
@@ -749,7 +748,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
@@ -838,11 +837,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
@@ -981,7 +980,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:51:58 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Feb 17 23:29:35 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/secure.ML Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/General/secure.ML Wed Feb 17 23:29:35 2016 +0100
@@ -13,7 +13,6 @@
val use_text: use_context ->
{line: int, file: string, verbose: bool, debug: bool} -> string -> unit
val use_file: use_context -> {verbose: bool, debug: bool} -> string -> unit
- val toplevel_pp: string list -> string -> unit
end;
structure Secure: SECURE =
@@ -36,11 +35,8 @@
val raw_use_text = use_text;
val raw_use_file = use_file;
-val raw_toplevel_pp = toplevel_pp;
fun use_text context flags (text: string) = (secure_mltext (); raw_use_text context flags text);
fun use_file context flags (file: string) = (secure_mltext (); raw_use_file context flags file);
-fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
-
end;
--- a/src/Pure/General/socket_io.ML Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/General/socket_io.ML Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/src/Pure/ML/exn_output.ML Wed Feb 17 23:29:35 2016 +0100
@@ -1,20 +1,24 @@
(* Title: Pure/ML/exn_output.ML
Author: Makarius
-Auxiliary operations for exception output -- generic version.
+Auxiliary operations for exception output.
*)
signature EXN_OUTPUT =
sig
val position: exn -> Position.T
val pretty: exn -> Pretty.T
-end
+end;
structure Exn_Output: EXN_OUTPUT =
struct
-fun position (_: exn) = Position.none
-val pretty = Pretty.str o General.exnMessage;
+fun position exn =
+ (case PolyML.exceptionLocation exn of
+ NONE => Position.none
+ | SOME loc => Exn_Properties.position_of loc);
+
+fun pretty (exn: exn) =
+ Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
end;
-
--- a/src/Pure/ML/exn_output_polyml.ML Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: Pure/ML/exn_output_polyml.ML
- Author: Makarius
-
-Auxiliary operations for exception output -- Poly/ML version.
-*)
-
-structure Exn_Output: EXN_OUTPUT =
-struct
-
-fun position exn =
- (case PolyML.exceptionLocation exn of
- NONE => Position.none
- | SOME loc => Exn_Properties.position_of loc);
-
-fun pretty (exn: exn) =
- Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
-
-end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_properties.ML Wed Feb 17 23:29:35 2016 +0100
@@ -0,0 +1,63 @@
+(* Title: Pure/ML/exn_properties.ML
+ Author: Makarius
+
+Exception properties.
+*)
+
+signature EXN_PROPERTIES =
+sig
+ val position_of: PolyML.location -> Position.T
+ val get: exn -> Properties.T
+ val update: Properties.entry list -> exn -> exn
+end;
+
+structure Exn_Properties: EXN_PROPERTIES =
+struct
+
+(* source locations *)
+
+fun props_of (loc: PolyML.location) =
+ (case YXML.parse_body (#file loc) of
+ [] => []
+ | [XML.Text file] =>
+ if file = "Standard Basis" then []
+ else [(Markup.fileN, ml_standard_path file)]
+ | body => XML.Decode.properties body);
+
+fun position_of loc =
+ Position.make
+ {line = #startLine loc,
+ offset = #startPosition loc,
+ end_offset = #endPosition loc,
+ props = props_of loc};
+
+
+(* exception properties *)
+
+fun get exn =
+ (case PolyML.exceptionLocation exn of
+ NONE => []
+ | SOME loc => props_of loc);
+
+fun update entries exn =
+ let
+ val loc =
+ the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
+ (PolyML.exceptionLocation exn);
+ val props = props_of loc;
+ val props' = fold Properties.put entries props;
+ in
+ if props = props' then exn
+ else
+ let
+ val loc' =
+ {file = YXML.string_of_body (XML.Encode.properties props'),
+ startLine = #startLine loc, endLine = #endLine loc,
+ startPosition = #startPosition loc, endPosition = #endPosition loc};
+ in
+ uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
+ handle exn' => exn'
+ end
+ end;
+
+end;
--- a/src/Pure/ML/exn_properties_dummy.ML Wed Feb 17 21:51:58 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/exn_properties_polyml.ML Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(* Title: Pure/ML/exn_properties_polyml.ML
- Author: Makarius
-
-Exception properties for Poly/ML.
-*)
-
-signature EXN_PROPERTIES =
-sig
- val position_of: PolyML.location -> Position.T
- val get: exn -> Properties.T
- val update: Properties.entry list -> exn -> exn
-end;
-
-structure Exn_Properties: EXN_PROPERTIES =
-struct
-
-(* source locations *)
-
-fun props_of (loc: PolyML.location) =
- (case YXML.parse_body (#file loc) of
- [] => []
- | [XML.Text file] =>
- if file = "Standard Basis" then []
- else [(Markup.fileN, ml_standard_path file)]
- | body => XML.Decode.properties body);
-
-fun position_of loc =
- Position.make
- {line = #startLine loc,
- offset = #startPosition loc,
- end_offset = #endPosition loc,
- props = props_of loc};
-
-
-(* exception properties *)
-
-fun get exn =
- (case PolyML.exceptionLocation exn of
- NONE => []
- | SOME loc => props_of loc);
-
-fun update entries exn =
- let
- val loc =
- the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
- (PolyML.exceptionLocation exn);
- val props = props_of loc;
- val props' = fold Properties.put entries props;
- in
- if props = props' then exn
- else
- let
- val loc' =
- {file = YXML.string_of_body (XML.Encode.properties props'),
- startLine = #startLine loc, endLine = #endLine loc,
- startPosition = #startPosition loc, endPosition = #endPosition loc};
- in
- uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
- handle exn' => exn'
- end
- end;
-
-end;
-
--- a/src/Pure/ML/install_pp_polyml.ML Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/ML/install_pp_polyml.ML Wed Feb 17 23:29:35 2016 +0100
@@ -1,9 +1,63 @@
(* Title: Pure/ML/install_pp_polyml.ML
Author: Makarius
-Extra toplevel pretty-printing for Poly/ML.
+ML toplevel pretty-printing for Poly/ML.
*)
+PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T =>
+ ml_pretty (Pretty.to_ML (Pretty.str "<pretty>")));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
+ ml_pretty (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
+ ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
+ ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
+ ml_pretty (Pretty.to_ML (Pretty.position pos)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
+ ml_pretty (Pretty.to_ML (Binding.pp binding)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn th =>
+ ml_pretty (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn ct =>
+ ml_pretty (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn cT =>
+ ml_pretty (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn T =>
+ ml_pretty (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
+ ml_pretty (Pretty.to_ML (Context.pretty_thy thy)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
+ ml_pretty (Pretty.to_ML (Proof_Display.pp_context ctxt)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
+ ml_pretty (Pretty.to_ML (Ast.pretty_ast ast)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
+ ml_pretty (Pretty.to_ML (Path.pretty path)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
+ ml_pretty (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
+ ml_pretty (Pretty.to_ML (Pretty.str "<Proof.state>")));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
+ ml_pretty (Pretty.to_ML (Toplevel.pretty_abstract st)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
+ ml_pretty (Pretty.to_ML (Morphism.pretty morphism)));
+
PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
@@ -107,4 +161,3 @@
end;
end;
-
--- a/src/Pure/ML/ml_compiler.ML Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML Wed Feb 17 23:29:35 2016 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/ML/ml_compiler.ML
Author: Makarius
-Runtime compilation and evaluation -- generic version.
+Runtime compilation and evaluation.
*)
signature ML_COMPILER =
@@ -14,9 +14,12 @@
val eval: flags -> Position.T -> ML_Lex.token list -> unit
end
+
structure ML_Compiler: ML_COMPILER =
struct
+(* flags *)
+
type flags =
{SML: bool, exchange: bool, redirect: bool, verbose: bool,
debug: bool option, writeln: string -> unit, warning: string -> unit};
@@ -29,16 +32,257 @@
{SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
+
+(* parse trees *)
+
+fun breakpoint_position loc =
+ let val pos = Position.reset_range (Exn_Properties.position_of loc) in
+ (case Position.offset_of pos of
+ NONE => pos
+ | SOME 1 => pos
+ | SOME j =>
+ Position.properties_of pos
+ |> Properties.put (Markup.offsetN, Markup.print_int (j - 1))
+ |> Position.of_properties)
+ end;
+
+fun report_parse_tree redirect depth space parse_tree =
+ let
+ val is_visible =
+ (case Context.thread_data () of
+ SOME context => Context_Position.is_visible_generic context
+ | NONE => true);
+ fun is_reported pos = is_visible andalso Position.is_reported pos;
+
+
+ (* syntax reports *)
+
+ fun reported_types loc types =
+ let val pos = Exn_Properties.position_of loc in
+ is_reported pos ?
+ let
+ val xml =
+ ML_Name_Space.displayTypeExpression (types, depth, space)
+ |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+ |> Output.output |> YXML.parse_body;
+ in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
+ end;
+
+ fun reported_entity kind loc decl =
+ let
+ val pos = Exn_Properties.position_of loc;
+ val def_pos = Exn_Properties.position_of decl;
+ in
+ (is_reported pos andalso pos <> def_pos) ?
+ let
+ fun markup () =
+ (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
+ in cons (pos, markup, fn () => "") end
+ end;
+
+ fun reported_completions loc names =
+ let val pos = Exn_Properties.position_of loc in
+ if is_reported pos andalso not (null names) then
+ let
+ val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
+ val xml = Completion.encode completion;
+ in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
+ else I
+ end;
+
+ fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
+ | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
+ | reported loc (PolyML.PTtype types) = reported_types loc types
+ | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
+ | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
+ | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
+ | reported loc pt =
+ (case ML_Parse_Tree.completions pt of
+ SOME names => reported_completions loc names
+ | NONE => I)
+ and reported_tree (loc, props) = fold (reported loc) props;
+
+ val persistent_reports = reported_tree parse_tree [];
+
+ fun output () =
+ persistent_reports
+ |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
+ |> Output.report;
+ val _ =
+ if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
+ then
+ Execution.print
+ {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
+ output
+ else output ();
+
+
+ (* breakpoints *)
+
+ fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ())
+ | breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ())
+ | breakpoints loc pt =
+ (case ML_Parse_Tree.breakpoint pt of
+ SOME b =>
+ let val pos = breakpoint_position loc in
+ if is_reported pos then
+ let val id = serial ();
+ in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
+ else I
+ end
+ | NONE => I)
+ and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
+
+ val all_breakpoints = rev (breakpoints_tree parse_tree []);
+ val _ = Position.reports (map #1 all_breakpoints);
+ val _ =
+ if is_some (Context.thread_data ()) then
+ Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints)
+ else ();
+ in () end;
+
+
+(* eval ML source tokens *)
+
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;
+ val _ = Secure.secure_mltext ();
+ val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags};
+ val opt_context = Context.thread_data ();
+
+
+ (* input *)
+
+ val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
+
+ val input_explode =
+ if #SML flags then String.explode
+ else maps (String.explode o Symbol.esc) o Symbol.explode;
+
+ val input_buffer =
+ Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of)));
+
+ fun get () =
+ (case ! input_buffer of
+ (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
+ | ([], _) :: rest => (input_buffer := rest; SOME #" ")
+ | [] => NONE);
+
+ fun get_pos () =
+ (case ! input_buffer of
+ (_ :: _, tok) :: _ => ML_Lex.pos_of tok
+ | ([], tok) :: _ => ML_Lex.end_pos_of tok
+ | [] => Position.none);
+
+
+ (* output *)
+
+ val writeln_buffer = Unsynchronized.ref Buffer.empty;
+ fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
+ fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer)));
+
+ val warnings = Unsynchronized.ref ([]: string list);
+ fun warn msg = Unsynchronized.change warnings (cons msg);
+ fun output_warnings () = List.app (#warning flags) (rev (! warnings));
+
+ val error_buffer = Unsynchronized.ref Buffer.empty;
+ fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
+ fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
+ fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
+
+ fun message {message = msg, hard, location = loc, context = _} =
+ let
+ val pos = Exn_Properties.position_of loc;
+ val txt =
+ (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
+ Pretty.string_of (Pretty.from_ML (pretty_ml msg));
+ in if hard then err txt else warn txt end;
+
+
+ (* results *)
+
+ val depth = ML_Options.get_print_depth ();
+
+ fun apply_result {fixes, types, signatures, structures, functors, values} =
+ let
+ fun display disp x =
+ if depth > 0 then
+ (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
+ else ();
+
+ fun apply_fix (a, b) =
+ (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
+ fun apply_type (a, b) =
+ (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space));
+ fun apply_sig (a, b) =
+ (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space));
+ fun apply_struct (a, b) =
+ (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space));
+ fun apply_funct (a, b) =
+ (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space));
+ fun apply_val (a, b) =
+ (#enterVal space (a, b); display ML_Name_Space.displayVal (b, depth, space));
+ in
+ List.app apply_fix fixes;
+ List.app apply_type types;
+ List.app apply_sig signatures;
+ List.app apply_struct structures;
+ List.app apply_funct functors;
+ List.app apply_val values
+ end;
+
+ exception STATIC_ERRORS of unit;
+
+ fun result_fun (phase1, phase2) () =
+ ((case phase1 of
+ NONE => ()
+ | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
+ (case phase2 of
+ NONE => raise STATIC_ERRORS ()
+ | SOME code =>
+ apply_result
+ ((code
+ |> Runtime.debugging opt_context
+ |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
+
+
+ (* compiler invocation *)
+
+ val debug =
+ (case #debug flags of
+ SOME debug => debug
+ | NONE => ML_Options.debugger_enabled opt_context);
+
+ val parameters =
+ [PolyML.Compiler.CPOutStream write,
+ PolyML.Compiler.CPNameSpace space,
+ PolyML.Compiler.CPErrorMessageProc message,
+ PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
+ PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
+ PolyML.Compiler.CPFileName location_props,
+ PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
+ PolyML.Compiler.CPCompilerResultFun result_fun,
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
+ ML_Compiler_Parameters.debug debug;
+
+ val _ =
+ (while not (List.null (! input_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else
+ let
+ val exn_msg =
+ (case exn of
+ STATIC_ERRORS () => ""
+ | Runtime.TOPLEVEL_ERROR => ""
+ | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
+ val _ = output_warnings ();
+ val _ = output_writeln ();
+ in raise_error exn_msg end;
in
- Secure.use_text ML_Env.local_context
- {line = line, file = file, verbose = #verbose flags, debug = debug} text
+ if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
+ else ()
end;
end;
--- a/src/Pure/ML/ml_compiler_polyml.ML Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,265 +0,0 @@
-(* Title: Pure/ML/ml_compiler_polyml.ML
- Author: Makarius
-
-Runtime compilation and evaluation -- Poly/ML version.
-*)
-
-structure ML_Compiler: ML_COMPILER =
-struct
-
-open ML_Compiler;
-
-
-(* parse trees *)
-
-fun breakpoint_position loc =
- let val pos = Position.reset_range (Exn_Properties.position_of loc) in
- (case Position.offset_of pos of
- NONE => pos
- | SOME 1 => pos
- | SOME j =>
- Position.properties_of pos
- |> Properties.put (Markup.offsetN, Markup.print_int (j - 1))
- |> Position.of_properties)
- end;
-
-fun report_parse_tree redirect depth space parse_tree =
- let
- val is_visible =
- (case Context.thread_data () of
- SOME context => Context_Position.is_visible_generic context
- | NONE => true);
- fun is_reported pos = is_visible andalso Position.is_reported pos;
-
-
- (* syntax reports *)
-
- fun reported_types loc types =
- let val pos = Exn_Properties.position_of loc in
- is_reported pos ?
- let
- val xml =
- ML_Name_Space.displayTypeExpression (types, depth, space)
- |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
- |> Output.output |> YXML.parse_body;
- in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
- end;
-
- fun reported_entity kind loc decl =
- let
- val pos = Exn_Properties.position_of loc;
- val def_pos = Exn_Properties.position_of decl;
- in
- (is_reported pos andalso pos <> def_pos) ?
- let
- fun markup () =
- (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
- in cons (pos, markup, fn () => "") end
- end;
-
- fun reported_completions loc names =
- let val pos = Exn_Properties.position_of loc in
- if is_reported pos andalso not (null names) then
- let
- val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
- val xml = Completion.encode completion;
- in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
- else I
- end;
-
- fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
- | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
- | reported loc (PolyML.PTtype types) = reported_types loc types
- | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
- | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
- | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
- | reported loc pt =
- (case ML_Parse_Tree.completions pt of
- SOME names => reported_completions loc names
- | NONE => I)
- and reported_tree (loc, props) = fold (reported loc) props;
-
- val persistent_reports = reported_tree parse_tree [];
-
- fun output () =
- persistent_reports
- |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
- |> Output.report;
- val _ =
- if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
- then
- Execution.print
- {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
- output
- else output ();
-
-
- (* breakpoints *)
-
- fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ())
- | breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ())
- | breakpoints loc pt =
- (case ML_Parse_Tree.breakpoint pt of
- SOME b =>
- let val pos = breakpoint_position loc in
- if is_reported pos then
- let val id = serial ();
- in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
- else I
- end
- | NONE => I)
- and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
-
- val all_breakpoints = rev (breakpoints_tree parse_tree []);
- val _ = Position.reports (map #1 all_breakpoints);
- val _ =
- if is_some (Context.thread_data ()) then
- Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints)
- else ();
- in () end;
-
-
-(* eval ML source tokens *)
-
-fun eval (flags: flags) pos toks =
- let
- val _ = Secure.secure_mltext ();
- val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags};
- val opt_context = Context.thread_data ();
-
-
- (* input *)
-
- val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
-
- val input_explode =
- if #SML flags then String.explode
- else maps (String.explode o Symbol.esc) o Symbol.explode;
-
- val input_buffer =
- Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of)));
-
- fun get () =
- (case ! input_buffer of
- (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
- | ([], _) :: rest => (input_buffer := rest; SOME #" ")
- | [] => NONE);
-
- fun get_pos () =
- (case ! input_buffer of
- (_ :: _, tok) :: _ => ML_Lex.pos_of tok
- | ([], tok) :: _ => ML_Lex.end_pos_of tok
- | [] => Position.none);
-
-
- (* output *)
-
- val writeln_buffer = Unsynchronized.ref Buffer.empty;
- fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
- fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer)));
-
- val warnings = Unsynchronized.ref ([]: string list);
- fun warn msg = Unsynchronized.change warnings (cons msg);
- fun output_warnings () = List.app (#warning flags) (rev (! warnings));
-
- val error_buffer = Unsynchronized.ref Buffer.empty;
- fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
- fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
- fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
-
- fun message {message = msg, hard, location = loc, context = _} =
- let
- val pos = Exn_Properties.position_of loc;
- val txt =
- (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
- Pretty.string_of (Pretty.from_ML (pretty_ml msg));
- in if hard then err txt else warn txt end;
-
-
- (* results *)
-
- val depth = ML_Options.get_print_depth ();
-
- fun apply_result {fixes, types, signatures, structures, functors, values} =
- let
- fun display disp x =
- if depth > 0 then
- (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
- else ();
-
- fun apply_fix (a, b) =
- (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
- fun apply_type (a, b) =
- (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space));
- fun apply_sig (a, b) =
- (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space));
- fun apply_struct (a, b) =
- (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space));
- fun apply_funct (a, b) =
- (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space));
- fun apply_val (a, b) =
- (#enterVal space (a, b); display ML_Name_Space.displayVal (b, depth, space));
- in
- List.app apply_fix fixes;
- List.app apply_type types;
- List.app apply_sig signatures;
- List.app apply_struct structures;
- List.app apply_funct functors;
- List.app apply_val values
- end;
-
- exception STATIC_ERRORS of unit;
-
- fun result_fun (phase1, phase2) () =
- ((case phase1 of
- NONE => ()
- | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
- (case phase2 of
- NONE => raise STATIC_ERRORS ()
- | SOME code =>
- apply_result
- ((code
- |> Runtime.debugging opt_context
- |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
-
-
- (* compiler invocation *)
-
- val debug =
- (case #debug flags of
- SOME debug => debug
- | NONE => ML_Options.debugger_enabled opt_context);
-
- val parameters =
- [PolyML.Compiler.CPOutStream write,
- PolyML.Compiler.CPNameSpace space,
- PolyML.Compiler.CPErrorMessageProc message,
- PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
- PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
- PolyML.Compiler.CPFileName location_props,
- PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
- PolyML.Compiler.CPCompilerResultFun result_fun,
- PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
- ML_Compiler_Parameters.debug debug;
-
- val _ =
- (while not (List.null (! input_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- if Exn.is_interrupt exn then reraise exn
- else
- let
- val exn_msg =
- (case exn of
- STATIC_ERRORS () => ""
- | Runtime.TOPLEVEL_ERROR => ""
- | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
- val _ = output_warnings ();
- val _ = output_writeln ();
- in raise_error exn_msg end;
- in
- if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
- else ()
- end;
-
-end;
--- a/src/Pure/ML/ml_env.ML Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/ML/ml_env.ML Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/src/Pure/ML/ml_parse.ML Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML Wed Feb 17 23:29:35 2016 +0100
@@ -102,8 +102,6 @@
val raw_explode = SML90.explode;
val implode = SML90.implode;
-val io_buffer_size = 4096;
-
fun quit () = exit 0;
@@ -191,10 +189,6 @@
if ML_System.name = "polyml-5.6"
then use "RAW/ml_parse_tree_polyml-5.6.ML" else ();
-fun toplevel_pp context (_: string list) pp =
- use_text context {line = 1, file = "pp", verbose = false, debug = false}
- ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
-
fun ml_make_string struct_name =
"(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
struct_name ^ ".ML_print_depth ())))))";
--- a/src/Pure/RAW/ROOT_smlnj.ML Wed Feb 17 21:51:58 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:51:58 2016 +0100
+++ b/src/Pure/RAW/compiler_polyml.ML Wed Feb 17 23:29:35 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:51:58 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:51:58 2016 +0100
+++ b/src/Pure/RAW/ml_system.ML Wed Feb 17 23:29:35 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:51:58 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:51:58 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:51:58 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:51:58 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:51:58 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:51:58 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:51:58 2016 +0100
+++ b/src/Pure/RAW/use_context.ML Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/src/Pure/ROOT Wed Feb 17 23:29:35 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"
@@ -180,13 +164,10 @@
"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/exn_properties.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"
"ML/ml_file.ML"
--- a/src/Pure/ROOT.ML Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/ROOT.ML Wed Feb 17 23:29:35 2016 +0100
@@ -47,8 +47,6 @@
Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
handle ERROR msg => (writeln msg; error "ML error")) ();
-val toplevel_pp = Secure.toplevel_pp;
-
(** bootstrap phase 1: towards ML within Isar context *)
@@ -76,7 +74,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 +96,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.ML";
if ML_System.name = "polyml-5.5.0"
orelse ML_System.name = "polyml-5.5.1"
@@ -123,8 +119,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 ()
@@ -204,12 +199,10 @@
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/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 "skip_proof.ML";
use "goal.ML";
@@ -338,28 +331,7 @@
structure Output: OUTPUT = Output; (*seal system channels!*)
-(* ML toplevel pretty printing *)
-
-toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
-toplevel_pp ["Scan", "lexicon"] "Lexicon.pp_lexicon";
-toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
-toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
-toplevel_pp ["Position", "T"] "Pretty.position";
-toplevel_pp ["Binding", "binding"] "Binding.pp";
-toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm Thy_Info.pure_theory";
-toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm Thy_Info.pure_theory";
-toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp Thy_Info.pure_theory";
-toplevel_pp ["typ"] "Proof_Display.pp_typ Thy_Info.pure_theory";
-toplevel_pp ["Context", "theory"] "Context.pretty_thy";
-toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
-toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
-toplevel_pp ["Path", "T"] "Path.pretty";
-toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
-toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
-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:51:58 2016 +0100
+++ b/src/Tools/Code/code_runtime.ML Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/src/Tools/ROOT Wed Feb 17 23:29:35 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:51:58 2016 +0100
+++ b/src/Tools/Spec_Check/spec_check.ML Wed Feb 17 23:29:35 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}