1.1 --- a/src/Pure/IsaMakefile Thu Jun 04 18:00:47 2009 +0200
1.2 +++ b/src/Pure/IsaMakefile Thu Jun 04 19:15:54 2009 +0200
1.3 @@ -68,15 +68,14 @@
1.4 ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML \
1.5 ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
1.6 ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
1.7 - ML-Systems/install_pp_polyml-experimental.ML \
1.8 - ML-Systems/use_context.ML Proof/extraction.ML \
1.9 - Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
1.10 - Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML \
1.11 - ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \
1.12 - ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML \
1.13 - ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML \
1.14 - ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML \
1.15 - ProofGeneral/proof_general_emacs.ML \
1.16 + ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \
1.17 + Proof/extraction.ML Proof/proof_rewrite_rules.ML \
1.18 + Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
1.19 + ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
1.20 + ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \
1.21 + ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \
1.22 + ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \
1.23 + ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML \
1.24 ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \
1.25 Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
1.26 Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \
2.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Thu Jun 04 18:00:47 2009 +0200
2.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Thu Jun 04 19:15:54 2009 +0200
2.3 @@ -1,6 +1,6 @@
2.4 (* Title: Pure/ML-Systems/compiler_polyml-5.3.ML
2.5
2.6 -Runtime compilation for Poly/ML 5.3 (SVN experimental).
2.7 +Runtime compilation for Poly/ML 5.3.
2.8 *)
2.9
2.10 local
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Thu Jun 04 19:15:54 2009 +0200
3.3 @@ -0,0 +1,17 @@
3.4 +(* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML
3.5 +
3.6 +Extra toplevel pretty-printing for Poly/ML 5.3.
3.7 +*)
3.8 +
3.9 +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
3.10 + (case Future.peek x of
3.11 + NONE => PolyML.PrettyString "<future>"
3.12 + | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
3.13 + | SOME (Exn.Result y) => pretty (y, depth)));
3.14 +
3.15 +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
3.16 + (case Lazy.peek x of
3.17 + NONE => PolyML.PrettyString "<lazy>"
3.18 + | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
3.19 + | SOME (Exn.Result y) => pretty (y, depth)));
3.20 +
4.1 --- a/src/Pure/ML-Systems/install_pp_polyml-experimental.ML Thu Jun 04 18:00:47 2009 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,17 +0,0 @@
4.4 -(* Title: Pure/ML-Systems/install_pp_polyml-experimental.ML
4.5 -
4.6 -Extra toplevel pretty-printing for Poly/ML 5.3 (SVN experimental).
4.7 -*)
4.8 -
4.9 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
4.10 - (case Future.peek x of
4.11 - NONE => PolyML.PrettyString "<future>"
4.12 - | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
4.13 - | SOME (Exn.Result y) => pretty (y, depth)));
4.14 -
4.15 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
4.16 - (case Lazy.peek x of
4.17 - NONE => PolyML.PrettyString "<lazy>"
4.18 - | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
4.19 - | SOME (Exn.Result y) => pretty (y, depth)));
4.20 -
5.1 --- a/src/Pure/ML-Systems/polyml-experimental.ML Thu Jun 04 18:00:47 2009 +0200
5.2 +++ b/src/Pure/ML-Systems/polyml-experimental.ML Thu Jun 04 19:15:54 2009 +0200
5.3 @@ -1,6 +1,6 @@
5.4 (* Title: Pure/ML-Systems/polyml-experimental.ML
5.5
5.6 -Compatibility wrapper for Poly/ML 5.3 (SVN experimental).
5.7 +Compatibility wrapper for Poly/ML 5.3.
5.8 *)
5.9
5.10 open Thread;
6.1 --- a/src/Pure/pure_setup.ML Thu Jun 04 18:00:47 2009 +0200
6.2 +++ b/src/Pure/pure_setup.ML Thu Jun 04 19:15:54 2009 +0200
6.3 @@ -42,8 +42,8 @@
6.4 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
6.5 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
6.6
6.7 -if File.exists (Path.explode ("ML-Systems/install_pp_" ^ ml_system ^ ".ML"))
6.8 -then use ("ML-Systems/install_pp_" ^ ml_system ^ ".ML")
6.9 +if ml_system = "polyml-experimental"
6.10 +then use "ML-Systems/install_pp_polyml-5.3.ML"
6.11 else if String.isPrefix "polyml" ml_system
6.12 then use "ML-Systems/install_pp_polyml.ML"
6.13 else ();