1.1 --- a/Admin/CHECKLIST Thu May 24 14:46:14 2012 +0200
1.2 +++ b/Admin/CHECKLIST Thu May 24 15:01:17 2012 +0200
1.3 @@ -1,7 +1,7 @@
1.4 Checklist for official releases
1.5 ===============================
1.6
1.7 -- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
1.8 +- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj;
1.9
1.10 - test Proof General 4.1, 3.7.1.1;
1.11
2.1 --- a/Admin/isatest/settings/at-poly Thu May 24 14:46:14 2012 +0200
2.2 +++ b/Admin/isatest/settings/at-poly Thu May 24 15:01:17 2012 +0200
2.3 @@ -1,7 +1,7 @@
2.4 # -*- shell-script -*- :mode=shellscript:
2.5
2.6 - POLYML_HOME="/home/polyml/polyml-5.2.1"
2.7 - ML_SYSTEM="polyml-5.2.1"
2.8 + POLYML_HOME="/home/polyml/polyml-5.3.0"
2.9 + ML_SYSTEM="polyml-5.3.0"
2.10 ML_PLATFORM="x86-linux"
2.11 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
2.12 ML_OPTIONS="-H 500"
3.1 --- a/NEWS Thu May 24 14:46:14 2012 +0200
3.2 +++ b/NEWS Thu May 24 15:01:17 2012 +0200
3.3 @@ -10,6 +10,13 @@
3.4 is called fastforce / fast_force_tac already since Isabelle2011-1.
3.5
3.6
3.7 +*** System ***
3.8 +
3.9 +* Discontinued support for Poly/ML 5.2.1, which was the last version
3.10 +without exception positions and advanced ML compiler/toplevel
3.11 +configuration.
3.12 +
3.13 +
3.14
3.15 New in Isabelle2012 (May 2012)
3.16 ------------------------------
4.1 --- a/src/Pure/IsaMakefile Thu May 24 14:46:14 2012 +0200
4.2 +++ b/src/Pure/IsaMakefile Thu May 24 15:01:17 2012 +0200
4.3 @@ -23,7 +23,6 @@
4.4
4.5 BOOTSTRAP_FILES = \
4.6 General/exn.ML \
4.7 - ML-Systems/compiler_polyml-5.2.ML \
4.8 ML-Systems/compiler_polyml-5.3.ML \
4.9 ML-Systems/ml_name_space.ML \
4.10 ML-Systems/ml_pretty.ML \
4.11 @@ -31,11 +30,9 @@
4.12 ML-Systems/multithreading.ML \
4.13 ML-Systems/multithreading_polyml.ML \
4.14 ML-Systems/overloading_smlnj.ML \
4.15 - ML-Systems/polyml-5.2.1.ML \
4.16 ML-Systems/polyml.ML \
4.17 ML-Systems/polyml_common.ML \
4.18 ML-Systems/pp_dummy.ML \
4.19 - ML-Systems/pp_polyml.ML \
4.20 ML-Systems/proper_int.ML \
4.21 ML-Systems/single_assignment.ML \
4.22 ML-Systems/single_assignment_polyml.ML \
4.23 @@ -145,7 +142,6 @@
4.24 Isar/toplevel.ML \
4.25 Isar/typedecl.ML \
4.26 ML/install_pp_polyml-5.3.ML \
4.27 - ML/install_pp_polyml.ML \
4.28 ML/ml_antiquote.ML \
4.29 ML/ml_compiler.ML \
4.30 ML/ml_compiler_polyml-5.3.ML \
5.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML Thu May 24 14:46:14 2012 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,53 +0,0 @@
5.4 -(* Title: Pure/ML-Systems/compiler_polyml-5.2.ML
5.5 -
5.6 -Runtime compilation for Poly/ML 5.2.x.
5.7 -*)
5.8 -
5.9 -local
5.10 -
5.11 -fun drop_newline s =
5.12 - if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
5.13 - else s;
5.14 -
5.15 -in
5.16 -
5.17 -fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
5.18 - (start_line, name) verbose txt =
5.19 - let
5.20 - val current_line = Unsynchronized.ref start_line;
5.21 - val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
5.22 - val out_buffer = Unsynchronized.ref ([]: string list);
5.23 - fun output () = drop_newline (implode (rev (! out_buffer)));
5.24 -
5.25 - fun get () =
5.26 - (case ! in_buffer of
5.27 - [] => NONE
5.28 - | c :: cs =>
5.29 - (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
5.30 - fun put s = out_buffer := s :: ! out_buffer;
5.31 - fun message (msg, is_err, line) =
5.32 - (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n";
5.33 -
5.34 - val parameters =
5.35 - [PolyML.Compiler.CPOutStream put,
5.36 - PolyML.Compiler.CPLineNo (fn () => ! current_line),
5.37 - PolyML.Compiler.CPErrorMessageProc (put o message),
5.38 - PolyML.Compiler.CPNameSpace name_space];
5.39 - val _ =
5.40 - (while not (List.null (! in_buffer)) do
5.41 - PolyML.compiler (get, parameters) ())
5.42 - handle exn =>
5.43 - if Exn.is_interrupt exn then reraise exn
5.44 - else
5.45 - (put ("Exception- " ^ General.exnMessage exn ^ " raised");
5.46 - error (output ()); reraise exn);
5.47 - in if verbose then print (output ()) else () end;
5.48 -
5.49 -fun use_file context verbose name =
5.50 - let
5.51 - val instream = TextIO.openIn name;
5.52 - val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
5.53 - in use_text context (1, name) verbose txt end;
5.54 -
5.55 -end;
5.56 -
6.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML Thu May 24 14:46:14 2012 +0200
6.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Thu May 24 15:01:17 2012 +0200
6.3 @@ -1,7 +1,7 @@
6.4 (* Title: Pure/ML-Systems/multithreading_polyml.ML
6.5 Author: Makarius
6.6
6.7 -Multithreading in Poly/ML 5.2.1 or later (cf. polyml/basis/Thread.sml).
6.8 +Multithreading in Poly/ML 5.3.0 or later (cf. polyml/basis/Thread.sml).
6.9 *)
6.10
6.11 signature MULTITHREADING_POLYML =
7.1 --- a/src/Pure/ML-Systems/polyml-5.2.1.ML Thu May 24 14:46:14 2012 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,35 +0,0 @@
7.4 -(* Title: Pure/ML-Systems/polyml-5.2.1.ML
7.5 -
7.6 -Compatibility wrapper for Poly/ML 5.2.1.
7.7 -*)
7.8 -
7.9 -open Thread;
7.10 -
7.11 -structure ML_Name_Space =
7.12 -struct
7.13 - open PolyML.NameSpace;
7.14 - type T = PolyML.NameSpace.nameSpace;
7.15 - val global = PolyML.globalNameSpace;
7.16 -end;
7.17 -
7.18 -fun reraise exn = raise exn;
7.19 -fun set_exn_serial (_: int) (exn: exn) = exn;
7.20 -fun get_exn_serial (exn: exn) : int option = NONE;
7.21 -
7.22 -use "ML-Systems/polyml_common.ML";
7.23 -use "ML-Systems/multithreading_polyml.ML";
7.24 -use "ML-Systems/unsynchronized.ML";
7.25 -
7.26 -val _ = PolyML.Compiler.forgetValue "ref";
7.27 -val _ = PolyML.Compiler.forgetType "ref";
7.28 -
7.29 -val pointer_eq = PolyML.pointerEq;
7.30 -
7.31 -fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
7.32 -
7.33 -use "ML-Systems/compiler_polyml-5.2.ML";
7.34 -use "ML-Systems/pp_polyml.ML";
7.35 -use "ML-Systems/pp_dummy.ML";
7.36 -
7.37 -use "ML-Systems/ml_system.ML";
7.38 -
8.1 --- a/src/Pure/ML-Systems/pp_polyml.ML Thu May 24 14:46:14 2012 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,20 +0,0 @@
8.4 -(* Title: Pure/ML-Systems/pp_polyml.ML
8.5 -
8.6 -Toplevel pretty printing for Poly/ML before 5.3.
8.7 -*)
8.8 -
8.9 -fun ml_pprint (print, begin_blk, brk, end_blk) =
8.10 - let
8.11 - fun str "" = ()
8.12 - | str s = print s;
8.13 - fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
8.14 - (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
8.15 - | pprint (ML_Pretty.String (s, _)) = str s
8.16 - | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
8.17 - | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
8.18 - in pprint end;
8.19 -
8.20 -fun toplevel_pp context (_: string list) pp =
8.21 - use_text context (1, "pp") false
8.22 - ("PolyML.install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
8.23 -
9.1 --- a/src/Pure/ML/install_pp_polyml.ML Thu May 24 14:46:14 2012 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,20 +0,0 @@
9.4 -(* Title: Pure/ML/install_pp_polyml.ML
9.5 - Author: Makarius
9.6 -
9.7 -Extra toplevel pretty-printing for Poly/ML.
9.8 -*)
9.9 -
9.10 -PolyML.install_pp
9.11 - (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
9.12 - (case Future.peek x of
9.13 - NONE => str "<future>"
9.14 - | SOME (Exn.Exn _) => str "<failed>"
9.15 - | SOME (Exn.Res y) => print (y, depth)));
9.16 -
9.17 -PolyML.install_pp
9.18 - (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
9.19 - (case Lazy.peek x of
9.20 - NONE => str "<lazy>"
9.21 - | SOME (Exn.Exn _) => str "<failed>"
9.22 - | SOME (Exn.Res y) => print (y, depth)));
9.23 -
10.1 --- a/src/Pure/ROOT.ML Thu May 24 14:46:14 2012 +0200
10.2 +++ b/src/Pure/ROOT.ML Thu May 24 15:01:17 2012 +0200
10.3 @@ -191,7 +191,7 @@
10.4 use "ML/ml_env.ML";
10.5 use "Isar/runtime.ML";
10.6 use "ML/ml_compiler.ML";
10.7 -if ML_System.name = "polyml-5.2.1" orelse ML_System.is_smlnj then ()
10.8 +if ML_System.is_smlnj then ()
10.9 else use "ML/ml_compiler_polyml-5.3.ML";
10.10 use "ML/ml_context.ML";
10.11
11.1 --- a/src/Pure/pure_setup.ML Thu May 24 14:46:14 2012 +0200
11.2 +++ b/src/Pure/pure_setup.ML Thu May 24 15:01:17 2012 +0200
11.3 @@ -36,9 +36,7 @@
11.4 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
11.5 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
11.6
11.7 -if ML_System.name = "polyml-5.2.1"
11.8 -then use "ML/install_pp_polyml.ML"
11.9 -else if ML_System.is_polyml
11.10 +if ML_System.is_polyml
11.11 then use "ML/install_pp_polyml-5.3.ML"
11.12 else ();
11.13