discontinued support for Poly/ML 5.2.1;
authorwenzelm
Thu May 24 15:01:17 2012 +0200 (2012-05-24 ago)
changeset 4797959ec72d3d0b9
parent 47978 f8f503a1782a
child 47980 c81801f881b3
discontinued support for Poly/ML 5.2.1;
Admin/CHECKLIST
Admin/isatest/settings/at-poly
NEWS
src/Pure/IsaMakefile
src/Pure/ML-Systems/compiler_polyml-5.2.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ML-Systems/polyml-5.2.1.ML
src/Pure/ML-Systems/pp_polyml.ML
src/Pure/ML/install_pp_polyml.ML
src/Pure/ROOT.ML
src/Pure/pure_setup.ML
     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