1.1 --- a/etc/settings Mon Nov 09 20:47:39 2009 +0100
1.2 +++ b/etc/settings Mon Nov 09 21:30:54 2009 +0100
1.3 @@ -29,23 +29,18 @@
1.4 ML_OPTIONS="-H 200"
1.5 ML_SOURCES="$ML_HOME/../src"
1.6
1.7 -# Poly/ML 5.2.1
1.8 +# Poly/ML 5.3.0
1.9 #ML_PLATFORM=x86-linux
1.10 #ML_HOME=/usr/local/polyml/x86-linux
1.11 -#ML_SYSTEM=polyml-5.2.1
1.12 +#ML_SYSTEM=polyml-5.3.0
1.13 #ML_OPTIONS="-H 500"
1.14 +#ML_SOURCES="$ML_HOME/../src"
1.15
1.16 -# Poly/ML 5.2.1 (64 bit)
1.17 +# Poly/ML 5.3.0 (64 bit)
1.18 #ML_PLATFORM=x86_64-linux
1.19 #ML_HOME=/usr/local/polyml/x86_64-linux
1.20 -#ML_SYSTEM=polyml-5.2.1
1.21 +#ML_SYSTEM=polyml-5.3.0
1.22 #ML_OPTIONS="-H 1000"
1.23 -
1.24 -# Poly/ML 5.3 (experimental)
1.25 -#ML_PLATFORM=x86-linux
1.26 -#ML_HOME=/usr/local/polyml/x86-linux
1.27 -#ML_SYSTEM=polyml-experimental
1.28 -#ML_OPTIONS="-H 500"
1.29 #ML_SOURCES="$ML_HOME/../src"
1.30
1.31 # Standard ML of New Jersey (slow!)
2.1 --- a/src/Pure/IsaMakefile Mon Nov 09 20:47:39 2009 +0100
2.2 +++ b/src/Pure/IsaMakefile Mon Nov 09 21:30:54 2009 +0100
2.3 @@ -27,9 +27,10 @@
2.4 ML-Systems/ml_pretty.ML ML-Systems/mosml.ML \
2.5 ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \
2.6 ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \
2.7 - ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML \
2.8 - ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
2.9 - ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
2.10 + ML-Systems/polyml-5.1.ML ML-Systems/polyml-5.2.ML \
2.11 + ML-Systems/polyml-5.2.1.ML ML-Systems/polyml.ML \
2.12 + ML-Systems/polyml_common.ML ML-Systems/pp_polyml.ML \
2.13 + ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
2.14 ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
2.15 ML-Systems/timing.ML ML-Systems/time_limit.ML \
2.16 ML-Systems/universal.ML ML-Systems/unsynchronized.ML
3.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Mon Nov 09 20:47:39 2009 +0100
3.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Mon Nov 09 21:30:54 2009 +0100
3.3 @@ -1,6 +1,6 @@
3.4 (* Title: Pure/ML-Systems/compiler_polyml-5.3.ML
3.5
3.6 -Runtime compilation for Poly/ML 5.3.
3.7 +Runtime compilation for Poly/ML 5.3.0.
3.8 *)
3.9
3.10 local
4.1 --- a/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Mon Nov 09 20:47:39 2009 +0100
4.2 +++ b/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Mon Nov 09 21:30:54 2009 +0100
4.3 @@ -1,6 +1,6 @@
4.4 (* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML
4.5
4.6 -Extra toplevel pretty-printing for Poly/ML 5.3.
4.7 +Extra toplevel pretty-printing for Poly/ML 5.3.0.
4.8 *)
4.9
4.10 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML Mon Nov 09 21:30:54 2009 +0100
5.3 @@ -0,0 +1,28 @@
5.4 +(* Title: Pure/ML-Systems/polyml-5.2.1.ML
5.5 +
5.6 +Compatibility wrapper for Poly/ML 5.2.1.
5.7 +*)
5.8 +
5.9 +use "ML-Systems/unsynchronized.ML";
5.10 +
5.11 +open Thread;
5.12 +
5.13 +structure ML_Name_Space =
5.14 +struct
5.15 + open PolyML.NameSpace;
5.16 + type T = PolyML.NameSpace.nameSpace;
5.17 + val global = PolyML.globalNameSpace;
5.18 +end;
5.19 +
5.20 +fun reraise exn = raise exn;
5.21 +
5.22 +use "ML-Systems/polyml_common.ML";
5.23 +use "ML-Systems/multithreading_polyml.ML";
5.24 +
5.25 +val pointer_eq = PolyML.pointerEq;
5.26 +
5.27 +fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
5.28 +
5.29 +use "ML-Systems/compiler_polyml-5.2.ML";
5.30 +use "ML-Systems/pp_polyml.ML";
5.31 +
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Pure/ML-Systems/polyml-5.2.ML Mon Nov 09 21:30:54 2009 +0100
6.3 @@ -0,0 +1,30 @@
6.4 +(* Title: Pure/ML-Systems/polyml-5.2.ML
6.5 +
6.6 +Compatibility wrapper for Poly/ML 5.2.
6.7 +*)
6.8 +
6.9 +use "ML-Systems/unsynchronized.ML";
6.10 +
6.11 +open Thread;
6.12 +
6.13 +structure ML_Name_Space =
6.14 +struct
6.15 + open PolyML.NameSpace;
6.16 + type T = PolyML.NameSpace.nameSpace;
6.17 + val global = PolyML.globalNameSpace;
6.18 +end;
6.19 +
6.20 +fun reraise exn = raise exn;
6.21 +
6.22 +use "ML-Systems/polyml_common.ML";
6.23 +
6.24 +use "ML-Systems/thread_dummy.ML";
6.25 +use "ML-Systems/multithreading.ML";
6.26 +
6.27 +val pointer_eq = PolyML.pointerEq;
6.28 +
6.29 +fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
6.30 +
6.31 +use "ML-Systems/compiler_polyml-5.2.ML";
6.32 +use "ML-Systems/pp_polyml.ML";
6.33 +
7.1 --- a/src/Pure/ML-Systems/polyml-experimental.ML Mon Nov 09 20:47:39 2009 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,68 +0,0 @@
7.4 -(* Title: Pure/ML-Systems/polyml-experimental.ML
7.5 -
7.6 -Compatibility wrapper for Poly/ML 5.3.
7.7 -*)
7.8 -
7.9 -use "ML-Systems/unsynchronized.ML";
7.10 -
7.11 -open Thread;
7.12 -
7.13 -structure ML_Name_Space =
7.14 -struct
7.15 - open PolyML.NameSpace;
7.16 - type T = PolyML.NameSpace.nameSpace;
7.17 - val global = PolyML.globalNameSpace;
7.18 -end;
7.19 -
7.20 -fun reraise exn =
7.21 - (case PolyML.exceptionLocation exn of
7.22 - NONE => raise exn
7.23 - | SOME location => PolyML.raiseWithLocation (exn, location));
7.24 -
7.25 -use "ML-Systems/polyml_common.ML";
7.26 -use "ML-Systems/multithreading_polyml.ML";
7.27 -
7.28 -val pointer_eq = PolyML.pointerEq;
7.29 -
7.30 -fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
7.31 -
7.32 -use "ML-Systems/compiler_polyml-5.3.ML";
7.33 -PolyML.Compiler.reportUnreferencedIds := true;
7.34 -
7.35 -
7.36 -(* toplevel pretty printing *)
7.37 -
7.38 -val pretty_ml =
7.39 - let
7.40 - fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
7.41 - let
7.42 - fun property name default =
7.43 - (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
7.44 - SOME (PolyML.ContextProperty (_, b)) => b
7.45 - | NONE => default);
7.46 - val bg = property "begin" "";
7.47 - val en = property "end" "";
7.48 - val len' = property "length" len;
7.49 - in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
7.50 - | convert len (PolyML.PrettyString s) =
7.51 - ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
7.52 - | convert _ (PolyML.PrettyBreak (wd, _)) =
7.53 - ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
7.54 - in convert "" end;
7.55 -
7.56 -fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
7.57 - let val context =
7.58 - (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
7.59 - (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
7.60 - in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
7.61 - | ml_pretty (ML_Pretty.String (s, len)) =
7.62 - if len = size s then PolyML.PrettyString s
7.63 - else PolyML.PrettyBlock
7.64 - (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s])
7.65 - | ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
7.66 - | ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0);
7.67 -
7.68 -fun toplevel_pp context (_: string list) pp =
7.69 - use_text context (1, "pp") false
7.70 - ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
7.71 -
8.1 --- a/src/Pure/ML-Systems/polyml.ML Mon Nov 09 20:47:39 2009 +0100
8.2 +++ b/src/Pure/ML-Systems/polyml.ML Mon Nov 09 21:30:54 2009 +0100
8.3 @@ -1,6 +1,6 @@
8.4 (* Title: Pure/ML-Systems/polyml.ML
8.5
8.6 -Compatibility wrapper for Poly/ML 5.2 and 5.2.1.
8.7 +Compatibility wrapper for Poly/ML 5.3.0.
8.8 *)
8.9
8.10 use "ML-Systems/unsynchronized.ML";
8.11 @@ -14,18 +14,55 @@
8.12 val global = PolyML.globalNameSpace;
8.13 end;
8.14
8.15 -fun reraise exn = raise exn;
8.16 +fun reraise exn =
8.17 + (case PolyML.exceptionLocation exn of
8.18 + NONE => raise exn
8.19 + | SOME location => PolyML.raiseWithLocation (exn, location));
8.20
8.21 use "ML-Systems/polyml_common.ML";
8.22 -
8.23 -if ml_system = "polyml-5.2"
8.24 -then (use "ML-Systems/thread_dummy.ML"; use "ML-Systems/multithreading.ML")
8.25 -else use "ML-Systems/multithreading_polyml.ML";
8.26 +use "ML-Systems/multithreading_polyml.ML";
8.27
8.28 val pointer_eq = PolyML.pointerEq;
8.29
8.30 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
8.31
8.32 -use "ML-Systems/compiler_polyml-5.2.ML";
8.33 -use "ML-Systems/pp_polyml.ML";
8.34 +use "ML-Systems/compiler_polyml-5.3.ML";
8.35 +PolyML.Compiler.reportUnreferencedIds := true;
8.36
8.37 +
8.38 +(* toplevel pretty printing *)
8.39 +
8.40 +val pretty_ml =
8.41 + let
8.42 + fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
8.43 + let
8.44 + fun property name default =
8.45 + (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
8.46 + SOME (PolyML.ContextProperty (_, b)) => b
8.47 + | NONE => default);
8.48 + val bg = property "begin" "";
8.49 + val en = property "end" "";
8.50 + val len' = property "length" len;
8.51 + in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
8.52 + | convert len (PolyML.PrettyString s) =
8.53 + ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
8.54 + | convert _ (PolyML.PrettyBreak (wd, _)) =
8.55 + ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
8.56 + in convert "" end;
8.57 +
8.58 +fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
8.59 + let val context =
8.60 + (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
8.61 + (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
8.62 + in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
8.63 + | ml_pretty (ML_Pretty.String (s, len)) =
8.64 + if len = size s then PolyML.PrettyString s
8.65 + else PolyML.PrettyBlock
8.66 + (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s])
8.67 + | ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
8.68 + | ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0);
8.69 +
8.70 +fun toplevel_pp context (_: string list) pp =
8.71 + use_text context (1, "pp") false
8.72 + ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
8.73 +
9.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Nov 09 20:47:39 2009 +0100
9.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Nov 09 21:30:54 2009 +0100
9.3 @@ -1,7 +1,7 @@
9.4 (* Title: Pure/ML/ml_compiler_polyml-5.3.ML
9.5 Author: Makarius
9.6
9.7 -Advanced runtime compilation for Poly/ML 5.3 (SVN 839).
9.8 +Advanced runtime compilation for Poly/ML 5.3.0.
9.9 *)
9.10
9.11 signature ML_COMPILER =
10.1 --- a/src/Pure/ROOT.ML Mon Nov 09 20:47:39 2009 +0100
10.2 +++ b/src/Pure/ROOT.ML Mon Nov 09 21:30:54 2009 +0100
10.3 @@ -169,7 +169,7 @@
10.4 use "ML/ml_syntax.ML";
10.5 use "ML/ml_env.ML";
10.6 use "Isar/runtime.ML";
10.7 -if ml_system = "polyml-experimental"
10.8 +if ml_system = "polyml-5.3.0"
10.9 then use "ML/ml_compiler_polyml-5.3.ML"
10.10 else use "ML/ml_compiler.ML";
10.11 use "ML/ml_context.ML";
11.1 --- a/src/Pure/pure_setup.ML Mon Nov 09 20:47:39 2009 +0100
11.2 +++ b/src/Pure/pure_setup.ML Mon Nov 09 21:30:54 2009 +0100
11.3 @@ -33,7 +33,7 @@
11.4 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
11.5 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
11.6
11.7 -if ml_system = "polyml-experimental"
11.8 +if ml_system = "polyml-5.3.0"
11.9 then use "ML-Systems/install_pp_polyml-5.3.ML"
11.10 else if String.isPrefix "polyml" ml_system
11.11 then use "ML-Systems/install_pp_polyml.ML"