# HG changeset patch # User wenzelm # Date 1257800215 -3600 # Node ID a4dbf0f92d9644eaafff43eb12a7012d79e0a16d # Parent f2d7d4e67447676fdefcbf73f5cfc2c35b85ce79# Parent 84380e6c0b1aa1ce3c5ff3b93d671bc82522f420 merged diff -r f2d7d4e67447 -r a4dbf0f92d96 Admin/isatest/settings/mac-poly --- a/Admin/isatest/settings/mac-poly Mon Nov 09 21:45:24 2009 +0100 +++ b/Admin/isatest/settings/mac-poly Mon Nov 09 21:56:55 2009 +0100 @@ -1,7 +1,7 @@ # -*- shell-script -*- :mode=shellscript: - POLYML_HOME="/home/polyml/polyml-5.2" - ML_SYSTEM="polyml-5.2" + POLYML_HOME="/home/polyml/polyml-5.3.0" + ML_SYSTEM="polyml-5.3.0" ML_PLATFORM="ppc-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="-H 500" diff -r f2d7d4e67447 -r a4dbf0f92d96 Admin/isatest/settings/mac-poly-M4 --- a/Admin/isatest/settings/mac-poly-M4 Mon Nov 09 21:45:24 2009 +0100 +++ b/Admin/isatest/settings/mac-poly-M4 Mon Nov 09 21:56:55 2009 +0100 @@ -1,7 +1,7 @@ # -*- shell-script -*- :mode=shellscript: - POLYML_HOME="/home/polyml/polyml-svn" - ML_SYSTEM="polyml-experimental" + POLYML_HOME="/home/polyml/polyml-5.3.0" + ML_SYSTEM="polyml-5.3.0" ML_PLATFORM="x86-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="--mutable 800 --immutable 2000" diff -r f2d7d4e67447 -r a4dbf0f92d96 Admin/isatest/settings/mac-poly-M8 --- a/Admin/isatest/settings/mac-poly-M8 Mon Nov 09 21:45:24 2009 +0100 +++ b/Admin/isatest/settings/mac-poly-M8 Mon Nov 09 21:56:55 2009 +0100 @@ -1,7 +1,7 @@ # -*- shell-script -*- :mode=shellscript: - POLYML_HOME="/home/polyml/polyml-svn" - ML_SYSTEM="polyml-experimental" + POLYML_HOME="/home/polyml/polyml-5.3.0" + ML_SYSTEM="polyml-5.3.0" ML_PLATFORM="x86-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="--mutable 800 --immutable 2000" diff -r f2d7d4e67447 -r a4dbf0f92d96 Admin/isatest/settings/mac-poly64-M4 --- a/Admin/isatest/settings/mac-poly64-M4 Mon Nov 09 21:45:24 2009 +0100 +++ b/Admin/isatest/settings/mac-poly64-M4 Mon Nov 09 21:56:55 2009 +0100 @@ -1,7 +1,7 @@ # -*- shell-script -*- :mode=shellscript: - POLYML_HOME="/home/polyml/polyml-svn" - ML_SYSTEM="polyml-experimental" + POLYML_HOME="/home/polyml/polyml-5.3.0" + ML_SYSTEM="polyml-5.3.0" ML_PLATFORM="x86_64-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="--mutable 4000 --immutable 2000" diff -r f2d7d4e67447 -r a4dbf0f92d96 Admin/isatest/settings/mac-poly64-M8 --- a/Admin/isatest/settings/mac-poly64-M8 Mon Nov 09 21:45:24 2009 +0100 +++ b/Admin/isatest/settings/mac-poly64-M8 Mon Nov 09 21:56:55 2009 +0100 @@ -1,7 +1,7 @@ # -*- shell-script -*- :mode=shellscript: - POLYML_HOME="/home/polyml/polyml-svn" - ML_SYSTEM="polyml-experimental" + POLYML_HOME="/home/polyml/polyml-5.3.0" + ML_SYSTEM="polyml-5.3.0" ML_PLATFORM="x86_64-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="--mutable 4000 --immutable 2000" diff -r f2d7d4e67447 -r a4dbf0f92d96 Admin/isatest/settings/sun-poly --- a/Admin/isatest/settings/sun-poly Mon Nov 09 21:45:24 2009 +0100 +++ b/Admin/isatest/settings/sun-poly Mon Nov 09 21:56:55 2009 +0100 @@ -1,7 +1,7 @@ # -*- shell-script -*- :mode=shellscript: - POLYML_HOME="/home/polyml/polyml-svn" - ML_SYSTEM="polyml-experimental" + POLYML_HOME="/home/polyml/polyml-5.3.0" + ML_SYSTEM="polyml-5.3.0" ML_PLATFORM="sparc-solaris" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="-H 1000" diff -r f2d7d4e67447 -r a4dbf0f92d96 Admin/polyml/README --- a/Admin/polyml/README Mon Nov 09 21:45:24 2009 +0100 +++ b/Admin/polyml/README Mon Nov 09 21:56:55 2009 +0100 @@ -1,19 +1,18 @@ -This distribution of Poly/ML 5.2.1 has been compiled from the original +This distribution of Poly/ML 5.3 has been compiled from the original sources as follows: - tar xvzf polyml.5.2.1.tar.gz - cd polyml.5.2.1 - ./configure --prefix=/tmp/polyml + tar xvzf polyml.5.3.tar.gz + cd polyml.5.3 + ./configure --prefix="$HOME/tmp/polyml" make make install -Now /tmp/polyml/bin/* and /tmp/polyml/lib/* are moved to the -platform-specific target directory (e.g. polyml-5.2.1/x86-linux). Note -that Isabelle/lib/scripts/polyml-platform identifies your platform. +Now $HOME/tmp/polyml/bin/* and $HOME/tmp/polyml/lib/* are moved to the +platform-specific target directory (e.g. polyml-5.3.0/x86-linux). +Note that Isabelle/lib/scripts/polyml-platform identifies your +platform. Makarius - 22-Oct-2008 - -$Id$ + 09-Nov-2009 diff -r f2d7d4e67447 -r a4dbf0f92d96 etc/settings --- a/etc/settings Mon Nov 09 21:45:24 2009 +0100 +++ b/etc/settings Mon Nov 09 21:56:55 2009 +0100 @@ -29,23 +29,18 @@ ML_OPTIONS="-H 200" ML_SOURCES="$ML_HOME/../src" -# Poly/ML 5.2.1 +# Poly/ML 5.3.0 #ML_PLATFORM=x86-linux #ML_HOME=/usr/local/polyml/x86-linux -#ML_SYSTEM=polyml-5.2.1 +#ML_SYSTEM=polyml-5.3.0 #ML_OPTIONS="-H 500" +#ML_SOURCES="$ML_HOME/../src" -# Poly/ML 5.2.1 (64 bit) +# Poly/ML 5.3.0 (64 bit) #ML_PLATFORM=x86_64-linux #ML_HOME=/usr/local/polyml/x86_64-linux -#ML_SYSTEM=polyml-5.2.1 +#ML_SYSTEM=polyml-5.3.0 #ML_OPTIONS="-H 1000" - -# Poly/ML 5.3 (experimental) -#ML_PLATFORM=x86-linux -#ML_HOME=/usr/local/polyml/x86-linux -#ML_SYSTEM=polyml-experimental -#ML_OPTIONS="-H 500" #ML_SOURCES="$ML_HOME/../src" # Standard ML of New Jersey (slow!) diff -r f2d7d4e67447 -r a4dbf0f92d96 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Nov 09 21:45:24 2009 +0100 +++ b/src/Pure/IsaMakefile Mon Nov 09 21:56:55 2009 +0100 @@ -27,9 +27,10 @@ ML-Systems/ml_pretty.ML ML-Systems/mosml.ML \ ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \ ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \ - ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML \ - ML-Systems/polyml.ML ML-Systems/polyml_common.ML \ - ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \ + ML-Systems/polyml-5.1.ML ML-Systems/polyml-5.2.ML \ + ML-Systems/polyml-5.2.1.ML ML-Systems/polyml.ML \ + ML-Systems/polyml_common.ML ML-Systems/pp_polyml.ML \ + ML-Systems/proper_int.ML ML-Systems/smlnj.ML \ ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \ ML-Systems/timing.ML ML-Systems/time_limit.ML \ ML-Systems/universal.ML ML-Systems/unsynchronized.ML diff -r f2d7d4e67447 -r a4dbf0f92d96 src/Pure/ML-Systems/compiler_polyml-5.3.ML --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Mon Nov 09 21:45:24 2009 +0100 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Mon Nov 09 21:56:55 2009 +0100 @@ -1,6 +1,6 @@ (* Title: Pure/ML-Systems/compiler_polyml-5.3.ML -Runtime compilation for Poly/ML 5.3. +Runtime compilation for Poly/ML 5.3.0. *) local diff -r f2d7d4e67447 -r a4dbf0f92d96 src/Pure/ML-Systems/install_pp_polyml-5.3.ML --- a/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Mon Nov 09 21:45:24 2009 +0100 +++ b/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Mon Nov 09 21:56:55 2009 +0100 @@ -1,6 +1,6 @@ (* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML -Extra toplevel pretty-printing for Poly/ML 5.3. +Extra toplevel pretty-printing for Poly/ML 5.3.0. *) PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => diff -r f2d7d4e67447 -r a4dbf0f92d96 src/Pure/ML-Systems/polyml-5.2.1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML Mon Nov 09 21:56:55 2009 +0100 @@ -0,0 +1,28 @@ +(* Title: Pure/ML-Systems/polyml-5.2.1.ML + +Compatibility wrapper for Poly/ML 5.2.1. +*) + +use "ML-Systems/unsynchronized.ML"; + +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; + +use "ML-Systems/polyml_common.ML"; +use "ML-Systems/multithreading_polyml.ML"; + +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"; + diff -r f2d7d4e67447 -r a4dbf0f92d96 src/Pure/ML-Systems/polyml-5.2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/polyml-5.2.ML Mon Nov 09 21:56:55 2009 +0100 @@ -0,0 +1,30 @@ +(* Title: Pure/ML-Systems/polyml-5.2.ML + +Compatibility wrapper for Poly/ML 5.2. +*) + +use "ML-Systems/unsynchronized.ML"; + +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; + +use "ML-Systems/polyml_common.ML"; + +use "ML-Systems/thread_dummy.ML"; +use "ML-Systems/multithreading.ML"; + +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"; + diff -r f2d7d4e67447 -r a4dbf0f92d96 src/Pure/ML-Systems/polyml-experimental.ML --- a/src/Pure/ML-Systems/polyml-experimental.ML Mon Nov 09 21:45:24 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,68 +0,0 @@ -(* Title: Pure/ML-Systems/polyml-experimental.ML - -Compatibility wrapper for Poly/ML 5.3. -*) - -use "ML-Systems/unsynchronized.ML"; - -open Thread; - -structure ML_Name_Space = -struct - open PolyML.NameSpace; - type T = PolyML.NameSpace.nameSpace; - val global = PolyML.globalNameSpace; -end; - -fun reraise exn = - (case PolyML.exceptionLocation exn of - NONE => raise exn - | SOME location => PolyML.raiseWithLocation (exn, location)); - -use "ML-Systems/polyml_common.ML"; -use "ML-Systems/multithreading_polyml.ML"; - -val pointer_eq = PolyML.pointerEq; - -fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; - -use "ML-Systems/compiler_polyml-5.3.ML"; -PolyML.Compiler.reportUnreferencedIds := true; - - -(* toplevel pretty printing *) - -val pretty_ml = - let - fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) = - let - fun property name default = - (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of - SOME (PolyML.ContextProperty (_, b)) => b - | NONE => default); - val bg = property "begin" ""; - val en = property "end" ""; - val len' = property "length" len; - in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end - | convert len (PolyML.PrettyString s) = - ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s) - | convert _ (PolyML.PrettyBreak (wd, _)) = - ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2)); - in convert "" end; - -fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) = - let val context = - (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @ - (if en = "" then [] else [PolyML.ContextProperty ("end", en)]) - in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end - | ml_pretty (ML_Pretty.String (s, len)) = - if len = size s then PolyML.PrettyString s - else PolyML.PrettyBlock - (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]) - | ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0) - | ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0); - -fun toplevel_pp context (_: string list) pp = - use_text context (1, "pp") false - ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); - diff -r f2d7d4e67447 -r a4dbf0f92d96 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Mon Nov 09 21:45:24 2009 +0100 +++ b/src/Pure/ML-Systems/polyml.ML Mon Nov 09 21:56:55 2009 +0100 @@ -1,6 +1,6 @@ (* Title: Pure/ML-Systems/polyml.ML -Compatibility wrapper for Poly/ML 5.2 and 5.2.1. +Compatibility wrapper for Poly/ML 5.3.0. *) use "ML-Systems/unsynchronized.ML"; @@ -14,18 +14,55 @@ val global = PolyML.globalNameSpace; end; -fun reraise exn = raise exn; +fun reraise exn = + (case PolyML.exceptionLocation exn of + NONE => raise exn + | SOME location => PolyML.raiseWithLocation (exn, location)); use "ML-Systems/polyml_common.ML"; - -if ml_system = "polyml-5.2" -then (use "ML-Systems/thread_dummy.ML"; use "ML-Systems/multithreading.ML") -else use "ML-Systems/multithreading_polyml.ML"; +use "ML-Systems/multithreading_polyml.ML"; 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/compiler_polyml-5.3.ML"; +PolyML.Compiler.reportUnreferencedIds := true; + + +(* toplevel pretty printing *) +val pretty_ml = + let + fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) = + let + fun property name default = + (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of + SOME (PolyML.ContextProperty (_, b)) => b + | NONE => default); + val bg = property "begin" ""; + val en = property "end" ""; + val len' = property "length" len; + in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end + | convert len (PolyML.PrettyString s) = + ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s) + | convert _ (PolyML.PrettyBreak (wd, _)) = + ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2)); + in convert "" end; + +fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) = + let val context = + (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @ + (if en = "" then [] else [PolyML.ContextProperty ("end", en)]) + in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end + | ml_pretty (ML_Pretty.String (s, len)) = + if len = size s then PolyML.PrettyString s + else PolyML.PrettyBlock + (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]) + | ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0) + | ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0); + +fun toplevel_pp context (_: string list) pp = + use_text context (1, "pp") false + ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); + diff -r f2d7d4e67447 -r a4dbf0f92d96 src/Pure/ML/ml_compiler_polyml-5.3.ML --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Nov 09 21:45:24 2009 +0100 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Nov 09 21:56:55 2009 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/ML/ml_compiler_polyml-5.3.ML Author: Makarius -Advanced runtime compilation for Poly/ML 5.3 (SVN 839). +Advanced runtime compilation for Poly/ML 5.3.0. *) signature ML_COMPILER = diff -r f2d7d4e67447 -r a4dbf0f92d96 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Nov 09 21:45:24 2009 +0100 +++ b/src/Pure/ROOT.ML Mon Nov 09 21:56:55 2009 +0100 @@ -169,7 +169,7 @@ use "ML/ml_syntax.ML"; use "ML/ml_env.ML"; use "Isar/runtime.ML"; -if ml_system = "polyml-experimental" +if ml_system = "polyml-5.3.0" then use "ML/ml_compiler_polyml-5.3.ML" else use "ML/ml_compiler.ML"; use "ML/ml_context.ML"; diff -r f2d7d4e67447 -r a4dbf0f92d96 src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Mon Nov 09 21:45:24 2009 +0100 +++ b/src/Pure/pure_setup.ML Mon Nov 09 21:56:55 2009 +0100 @@ -33,7 +33,7 @@ toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode"; toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident"; -if ml_system = "polyml-experimental" +if ml_system = "polyml-5.3.0" then use "ML-Systems/install_pp_polyml-5.3.ML" else if String.isPrefix "polyml" ml_system then use "ML-Systems/install_pp_polyml.ML"