# HG changeset patch
# User wenzelm
# Date 1337864477 -7200
# Node ID 59ec72d3d0b9b87c70d824581ad88395852a9768
# Parent  f8f503a1782a383244c6f61297d81297507d5549
discontinued support for Poly/ML 5.2.1;

diff -r f8f503a1782a -r 59ec72d3d0b9 Admin/CHECKLIST
--- 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;
 
diff -r f8f503a1782a -r 59ec72d3d0b9 Admin/isatest/settings/at-poly
--- 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"
diff -r f8f503a1782a -r 59ec72d3d0b9 NEWS
--- 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)
 ------------------------------
diff -r f8f503a1782a -r 59ec72d3d0b9 src/Pure/IsaMakefile
--- 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				\
diff -r f8f503a1782a -r 59ec72d3d0b9 src/Pure/ML-Systems/compiler_polyml-5.2.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;
-
diff -r f8f503a1782a -r 59ec72d3d0b9 src/Pure/ML-Systems/multithreading_polyml.ML
--- 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 =
diff -r f8f503a1782a -r 59ec72d3d0b9 src/Pure/ML-Systems/polyml-5.2.1.ML
--- 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";
-
diff -r f8f503a1782a -r 59ec72d3d0b9 src/Pure/ML-Systems/pp_polyml.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 ^ "))");
-
diff -r f8f503a1782a -r 59ec72d3d0b9 src/Pure/ML/install_pp_polyml.ML
--- 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)));
-
diff -r f8f503a1782a -r 59ec72d3d0b9 src/Pure/ROOT.ML
--- 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";
 
diff -r f8f503a1782a -r 59ec72d3d0b9 src/Pure/pure_setup.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 ();