# HG changeset patch # User wenzelm # Date 1237662023 -3600 # Node ID fb9e73c01603b721b86c4e25710fd10d9642f159 # Parent 248de8dd839e19330902f4abd20f2ce0938f14cd added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3; diff -r 248de8dd839e -r fb9e73c01603 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sat Mar 21 19:58:45 2009 +0100 +++ b/src/Pure/IsaMakefile Sat Mar 21 20:00:23 2009 +0100 @@ -27,10 +27,10 @@ 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/polyml_old_compiler4.ML \ - ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML \ - ML-Systems/smlnj.ML ML-Systems/system_shell.ML \ - ML-Systems/thread_dummy.ML ML-Systems/time_limit.ML \ - ML-Systems/universal.ML + ML-Systems/polyml_old_compiler5.ML ML-Systems/polyml_pp.ML \ + ML-Systems/proper_int.ML ML-Systems/smlnj.ML \ + ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \ + ML-Systems/time_limit.ML ML-Systems/universal.ML RAW: $(OUT)/RAW diff -r 248de8dd839e -r fb9e73c01603 src/Pure/ML-Systems/polyml-4.1.3.ML --- a/src/Pure/ML-Systems/polyml-4.1.3.ML Sat Mar 21 19:58:45 2009 +0100 +++ b/src/Pure/ML-Systems/polyml-4.1.3.ML Sat Mar 21 20:00:23 2009 +0100 @@ -8,6 +8,7 @@ use "ML-Systems/thread_dummy.ML"; use "ML-Systems/polyml_common.ML"; use "ML-Systems/polyml_old_compiler4.ML"; +use "ML-Systems/polyml_pp.ML"; val pointer_eq = Address.wordEq; diff -r 248de8dd839e -r fb9e73c01603 src/Pure/ML-Systems/polyml-4.1.4.ML --- a/src/Pure/ML-Systems/polyml-4.1.4.ML Sat Mar 21 19:58:45 2009 +0100 +++ b/src/Pure/ML-Systems/polyml-4.1.4.ML Sat Mar 21 20:00:23 2009 +0100 @@ -8,6 +8,7 @@ use "ML-Systems/thread_dummy.ML"; use "ML-Systems/polyml_common.ML"; use "ML-Systems/polyml_old_compiler4.ML"; +use "ML-Systems/polyml_pp.ML"; val pointer_eq = Address.wordEq; diff -r 248de8dd839e -r fb9e73c01603 src/Pure/ML-Systems/polyml-4.2.0.ML --- a/src/Pure/ML-Systems/polyml-4.2.0.ML Sat Mar 21 19:58:45 2009 +0100 +++ b/src/Pure/ML-Systems/polyml-4.2.0.ML Sat Mar 21 20:00:23 2009 +0100 @@ -7,6 +7,7 @@ use "ML-Systems/thread_dummy.ML"; use "ML-Systems/polyml_common.ML"; use "ML-Systems/polyml_old_compiler4.ML"; +use "ML-Systems/polyml_pp.ML"; val pointer_eq = Address.wordEq; diff -r 248de8dd839e -r fb9e73c01603 src/Pure/ML-Systems/polyml-5.0.ML --- a/src/Pure/ML-Systems/polyml-5.0.ML Sat Mar 21 19:58:45 2009 +0100 +++ b/src/Pure/ML-Systems/polyml-5.0.ML Sat Mar 21 20:00:23 2009 +0100 @@ -7,6 +7,7 @@ use "ML-Systems/thread_dummy.ML"; use "ML-Systems/polyml_common.ML"; use "ML-Systems/polyml_old_compiler5.ML"; +use "ML-Systems/polyml_pp.ML"; val pointer_eq = PolyML.pointerEq; diff -r 248de8dd839e -r fb9e73c01603 src/Pure/ML-Systems/polyml-5.1.ML --- a/src/Pure/ML-Systems/polyml-5.1.ML Sat Mar 21 19:58:45 2009 +0100 +++ b/src/Pure/ML-Systems/polyml-5.1.ML Sat Mar 21 20:00:23 2009 +0100 @@ -6,6 +6,7 @@ use "ML-Systems/thread_dummy.ML"; use "ML-Systems/polyml_common.ML"; use "ML-Systems/polyml_old_compiler5.ML"; +use "ML-Systems/polyml_pp.ML"; val pointer_eq = PolyML.pointerEq; diff -r 248de8dd839e -r fb9e73c01603 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Sat Mar 21 19:58:45 2009 +0100 +++ b/src/Pure/ML-Systems/polyml.ML Sat Mar 21 20:00:23 2009 +0100 @@ -68,3 +68,6 @@ in use_text tune str_of_pos name_space (1, name) output verbose txt end; end; + +use "ML-Systems/polyml_pp.ML"; + diff -r 248de8dd839e -r fb9e73c01603 src/Pure/ML-Systems/polyml_pp.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/polyml_pp.ML Sat Mar 21 20:00:23 2009 +0100 @@ -0,0 +1,20 @@ +(* Title: Pure/ML-Systems/polyml_pp.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 tune str_of_pos output (_: string list) pp = + use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false + ("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))"); +