--- a/Admin/CHECKLIST Thu May 24 14:46:14 2012 +0200
+++ b/Admin/CHECKLIST Thu May 24 15:01:17 2012 +0200
@@ -1,7 +1,7 @@
Checklist for official releases
===============================
-- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
+- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj;
- test Proof General 4.1, 3.7.1.1;
--- a/Admin/isatest/settings/at-poly Thu May 24 14:46:14 2012 +0200
+++ b/Admin/isatest/settings/at-poly Thu May 24 15:01:17 2012 +0200
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.2.1"
- ML_SYSTEM="polyml-5.2.1"
+ POLYML_HOME="/home/polyml/polyml-5.3.0"
+ ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86-linux"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 500"
--- a/NEWS Thu May 24 14:46:14 2012 +0200
+++ b/NEWS Thu May 24 15:01:17 2012 +0200
@@ -10,6 +10,13 @@
is called fastforce / fast_force_tac already since Isabelle2011-1.
+*** System ***
+
+* Discontinued support for Poly/ML 5.2.1, which was the last version
+without exception positions and advanced ML compiler/toplevel
+configuration.
+
+
New in Isabelle2012 (May 2012)
------------------------------
--- a/src/Pure/IsaMakefile Thu May 24 14:46:14 2012 +0200
+++ b/src/Pure/IsaMakefile Thu May 24 15:01:17 2012 +0200
@@ -23,7 +23,6 @@
BOOTSTRAP_FILES = \
General/exn.ML \
- ML-Systems/compiler_polyml-5.2.ML \
ML-Systems/compiler_polyml-5.3.ML \
ML-Systems/ml_name_space.ML \
ML-Systems/ml_pretty.ML \
@@ -31,11 +30,9 @@
ML-Systems/multithreading.ML \
ML-Systems/multithreading_polyml.ML \
ML-Systems/overloading_smlnj.ML \
- ML-Systems/polyml-5.2.1.ML \
ML-Systems/polyml.ML \
ML-Systems/polyml_common.ML \
ML-Systems/pp_dummy.ML \
- ML-Systems/pp_polyml.ML \
ML-Systems/proper_int.ML \
ML-Systems/single_assignment.ML \
ML-Systems/single_assignment_polyml.ML \
@@ -145,7 +142,6 @@
Isar/toplevel.ML \
Isar/typedecl.ML \
ML/install_pp_polyml-5.3.ML \
- ML/install_pp_polyml.ML \
ML/ml_antiquote.ML \
ML/ml_compiler.ML \
ML/ml_compiler_polyml-5.3.ML \
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML Thu May 24 14:46:14 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(* Title: Pure/ML-Systems/compiler_polyml-5.2.ML
-
-Runtime compilation for Poly/ML 5.2.x.
-*)
-
-local
-
-fun drop_newline s =
- if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
- else s;
-
-in
-
-fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
- (start_line, name) verbose txt =
- let
- val current_line = Unsynchronized.ref start_line;
- val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
- val out_buffer = Unsynchronized.ref ([]: string list);
- fun output () = drop_newline (implode (rev (! out_buffer)));
-
- fun get () =
- (case ! in_buffer of
- [] => NONE
- | c :: cs =>
- (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
- fun put s = out_buffer := s :: ! out_buffer;
- fun message (msg, is_err, line) =
- (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n";
-
- val parameters =
- [PolyML.Compiler.CPOutStream put,
- PolyML.Compiler.CPLineNo (fn () => ! current_line),
- PolyML.Compiler.CPErrorMessageProc (put o message),
- PolyML.Compiler.CPNameSpace name_space];
- val _ =
- (while not (List.null (! in_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- if Exn.is_interrupt exn then reraise exn
- else
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); reraise exn);
- in if verbose then print (output ()) else () end;
-
-fun use_file context verbose name =
- let
- val instream = TextIO.openIn name;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;
-
-end;
-
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Thu May 24 14:46:14 2012 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Thu May 24 15:01:17 2012 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/ML-Systems/multithreading_polyml.ML
Author: Makarius
-Multithreading in Poly/ML 5.2.1 or later (cf. polyml/basis/Thread.sml).
+Multithreading in Poly/ML 5.3.0 or later (cf. polyml/basis/Thread.sml).
*)
signature MULTITHREADING_POLYML =
--- a/src/Pure/ML-Systems/polyml-5.2.1.ML Thu May 24 14:46:14 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-5.2.1.ML
-
-Compatibility wrapper for Poly/ML 5.2.1.
-*)
-
-open Thread;
-
-structure ML_Name_Space =
-struct
- open PolyML.NameSpace;
- type T = PolyML.NameSpace.nameSpace;
- val global = PolyML.globalNameSpace;
-end;
-
-fun reraise exn = raise exn;
-fun set_exn_serial (_: int) (exn: exn) = exn;
-fun get_exn_serial (exn: exn) : int option = NONE;
-
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/multithreading_polyml.ML";
-use "ML-Systems/unsynchronized.ML";
-
-val _ = PolyML.Compiler.forgetValue "ref";
-val _ = PolyML.Compiler.forgetType "ref";
-
-val pointer_eq = PolyML.pointerEq;
-
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
-use "ML-Systems/compiler_polyml-5.2.ML";
-use "ML-Systems/pp_polyml.ML";
-use "ML-Systems/pp_dummy.ML";
-
-use "ML-Systems/ml_system.ML";
-
--- a/src/Pure/ML-Systems/pp_polyml.ML Thu May 24 14:46:14 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: Pure/ML-Systems/pp_polyml.ML
-
-Toplevel pretty printing for Poly/ML before 5.3.
-*)
-
-fun ml_pprint (print, begin_blk, brk, end_blk) =
- let
- fun str "" = ()
- | str s = print s;
- fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
- (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
- | pprint (ML_Pretty.String (s, _)) = str s
- | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
- | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
- in pprint end;
-
-fun toplevel_pp context (_: string list) pp =
- use_text context (1, "pp") false
- ("PolyML.install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
-
--- a/src/Pure/ML/install_pp_polyml.ML Thu May 24 14:46:14 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: Pure/ML/install_pp_polyml.ML
- Author: Makarius
-
-Extra toplevel pretty-printing for Poly/ML.
-*)
-
-PolyML.install_pp
- (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
- (case Future.peek x of
- NONE => str "<future>"
- | SOME (Exn.Exn _) => str "<failed>"
- | SOME (Exn.Res y) => print (y, depth)));
-
-PolyML.install_pp
- (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
- (case Lazy.peek x of
- NONE => str "<lazy>"
- | SOME (Exn.Exn _) => str "<failed>"
- | SOME (Exn.Res y) => print (y, depth)));
-
--- a/src/Pure/ROOT.ML Thu May 24 14:46:14 2012 +0200
+++ b/src/Pure/ROOT.ML Thu May 24 15:01:17 2012 +0200
@@ -191,7 +191,7 @@
use "ML/ml_env.ML";
use "Isar/runtime.ML";
use "ML/ml_compiler.ML";
-if ML_System.name = "polyml-5.2.1" orelse ML_System.is_smlnj then ()
+if ML_System.is_smlnj then ()
else use "ML/ml_compiler_polyml-5.3.ML";
use "ML/ml_context.ML";
--- a/src/Pure/pure_setup.ML Thu May 24 14:46:14 2012 +0200
+++ b/src/Pure/pure_setup.ML Thu May 24 15:01:17 2012 +0200
@@ -36,9 +36,7 @@
toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
-if ML_System.name = "polyml-5.2.1"
-then use "ML/install_pp_polyml.ML"
-else if ML_System.is_polyml
+if ML_System.is_polyml
then use "ML/install_pp_polyml-5.3.ML"
else ();