added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
authorwenzelm
Sat Mar 21 20:00:23 2009 +0100 (2009-03-21)
changeset 30627fb9e73c01603
parent 30626 248de8dd839e
child 30628 4078276bcace
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
src/Pure/IsaMakefile
src/Pure/ML-Systems/polyml-4.1.3.ML
src/Pure/ML-Systems/polyml-4.1.4.ML
src/Pure/ML-Systems/polyml-4.2.0.ML
src/Pure/ML-Systems/polyml-5.0.ML
src/Pure/ML-Systems/polyml-5.1.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/polyml_pp.ML
     1.1 --- a/src/Pure/IsaMakefile	Sat Mar 21 19:58:45 2009 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Sat Mar 21 20:00:23 2009 +0100
     1.3 @@ -27,10 +27,10 @@
     1.4    ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML			\
     1.5    ML-Systems/polyml-experimental.ML ML-Systems/polyml.ML		\
     1.6    ML-Systems/polyml_common.ML ML-Systems/polyml_old_compiler4.ML	\
     1.7 -  ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML		\
     1.8 -  ML-Systems/smlnj.ML ML-Systems/system_shell.ML			\
     1.9 -  ML-Systems/thread_dummy.ML ML-Systems/time_limit.ML			\
    1.10 -  ML-Systems/universal.ML
    1.11 +  ML-Systems/polyml_old_compiler5.ML ML-Systems/polyml_pp.ML		\
    1.12 +  ML-Systems/proper_int.ML ML-Systems/smlnj.ML				\
    1.13 +  ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML			\
    1.14 +  ML-Systems/time_limit.ML ML-Systems/universal.ML
    1.15  
    1.16  RAW: $(OUT)/RAW
    1.17  
     2.1 --- a/src/Pure/ML-Systems/polyml-4.1.3.ML	Sat Mar 21 19:58:45 2009 +0100
     2.2 +++ b/src/Pure/ML-Systems/polyml-4.1.3.ML	Sat Mar 21 20:00:23 2009 +0100
     2.3 @@ -8,6 +8,7 @@
     2.4  use "ML-Systems/thread_dummy.ML";
     2.5  use "ML-Systems/polyml_common.ML";
     2.6  use "ML-Systems/polyml_old_compiler4.ML";
     2.7 +use "ML-Systems/polyml_pp.ML";
     2.8  
     2.9  val pointer_eq = Address.wordEq;
    2.10  
     3.1 --- a/src/Pure/ML-Systems/polyml-4.1.4.ML	Sat Mar 21 19:58:45 2009 +0100
     3.2 +++ b/src/Pure/ML-Systems/polyml-4.1.4.ML	Sat Mar 21 20:00:23 2009 +0100
     3.3 @@ -8,6 +8,7 @@
     3.4  use "ML-Systems/thread_dummy.ML";
     3.5  use "ML-Systems/polyml_common.ML";
     3.6  use "ML-Systems/polyml_old_compiler4.ML";
     3.7 +use "ML-Systems/polyml_pp.ML";
     3.8  
     3.9  val pointer_eq = Address.wordEq;
    3.10  
     4.1 --- a/src/Pure/ML-Systems/polyml-4.2.0.ML	Sat Mar 21 19:58:45 2009 +0100
     4.2 +++ b/src/Pure/ML-Systems/polyml-4.2.0.ML	Sat Mar 21 20:00:23 2009 +0100
     4.3 @@ -7,6 +7,7 @@
     4.4  use "ML-Systems/thread_dummy.ML";
     4.5  use "ML-Systems/polyml_common.ML";
     4.6  use "ML-Systems/polyml_old_compiler4.ML";
     4.7 +use "ML-Systems/polyml_pp.ML";
     4.8  
     4.9  val pointer_eq = Address.wordEq;
    4.10  
     5.1 --- a/src/Pure/ML-Systems/polyml-5.0.ML	Sat Mar 21 19:58:45 2009 +0100
     5.2 +++ b/src/Pure/ML-Systems/polyml-5.0.ML	Sat Mar 21 20:00:23 2009 +0100
     5.3 @@ -7,6 +7,7 @@
     5.4  use "ML-Systems/thread_dummy.ML";
     5.5  use "ML-Systems/polyml_common.ML";
     5.6  use "ML-Systems/polyml_old_compiler5.ML";
     5.7 +use "ML-Systems/polyml_pp.ML";
     5.8  
     5.9  val pointer_eq = PolyML.pointerEq;
    5.10  
     6.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Sat Mar 21 19:58:45 2009 +0100
     6.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Sat Mar 21 20:00:23 2009 +0100
     6.3 @@ -6,6 +6,7 @@
     6.4  use "ML-Systems/thread_dummy.ML";
     6.5  use "ML-Systems/polyml_common.ML";
     6.6  use "ML-Systems/polyml_old_compiler5.ML";
     6.7 +use "ML-Systems/polyml_pp.ML";
     6.8  
     6.9  val pointer_eq = PolyML.pointerEq;
    6.10  
     7.1 --- a/src/Pure/ML-Systems/polyml.ML	Sat Mar 21 19:58:45 2009 +0100
     7.2 +++ b/src/Pure/ML-Systems/polyml.ML	Sat Mar 21 20:00:23 2009 +0100
     7.3 @@ -68,3 +68,6 @@
     7.4    in use_text tune str_of_pos name_space (1, name) output verbose txt end;
     7.5  
     7.6  end;
     7.7 +
     7.8 +use "ML-Systems/polyml_pp.ML";
     7.9 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/ML-Systems/polyml_pp.ML	Sat Mar 21 20:00:23 2009 +0100
     8.3 @@ -0,0 +1,20 @@
     8.4 +(*  Title:      Pure/ML-Systems/polyml_pp.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 tune str_of_pos output (_: string list) pp =
    8.21 +  use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
    8.22 +    ("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
    8.23 +