renamed polyml_pp.ML to pp_polyml.ML;
authorwenzelm
Sun May 31 15:03:34 2009 +0200 (2009-05-31)
changeset 3131397800f7e80b4
parent 31312 1c00e4ff3c99
child 31314 b58d6a33b57f
renamed polyml_pp.ML to pp_polyml.ML;
explicit PolyML.install_pp;
src/Pure/IsaMakefile
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
src/Pure/ML-Systems/pp_polyml.ML
     1.1 --- a/src/Pure/IsaMakefile	Sun May 31 14:51:21 2009 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Sun May 31 15:03:34 2009 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML		\
     1.5    ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML		\
     1.6    ML-Systems/polyml.ML ML-Systems/polyml_common.ML			\
     1.7 -  ML-Systems/polyml_pp.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML	\
     1.8 +  ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML	\
     1.9    ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML			\
    1.10    ML-Systems/time_limit.ML ML-Systems/universal.ML
    1.11  
     2.1 --- a/src/Pure/ML-Systems/polyml-5.0.ML	Sun May 31 14:51:21 2009 +0200
     2.2 +++ b/src/Pure/ML-Systems/polyml-5.0.ML	Sun May 31 15:03:34 2009 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  use "ML-Systems/ml_name_space.ML";
     2.5  use "ML-Systems/polyml_common.ML";
     2.6  use "ML-Systems/compiler_polyml-5.0.ML";
     2.7 -use "ML-Systems/polyml_pp.ML";
     2.8 +use "ML-Systems/pp_polyml.ML";
     2.9  
    2.10  val pointer_eq = PolyML.pointerEq;
    2.11  
     3.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Sun May 31 14:51:21 2009 +0200
     3.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Sun May 31 15:03:34 2009 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  use "ML-Systems/ml_name_space.ML";
     3.5  use "ML-Systems/polyml_common.ML";
     3.6  use "ML-Systems/compiler_polyml-5.0.ML";
     3.7 -use "ML-Systems/polyml_pp.ML";
     3.8 +use "ML-Systems/pp_polyml.ML";
     3.9  
    3.10  val pointer_eq = PolyML.pointerEq;
    3.11  
     4.1 --- a/src/Pure/ML-Systems/polyml.ML	Sun May 31 14:51:21 2009 +0200
     4.2 +++ b/src/Pure/ML-Systems/polyml.ML	Sun May 31 15:03:34 2009 +0200
     4.3 @@ -23,5 +23,5 @@
     4.4  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
     4.5  
     4.6  use "ML-Systems/compiler_polyml-5.2.ML";
     4.7 -use "ML-Systems/polyml_pp.ML";
     4.8 +use "ML-Systems/pp_polyml.ML";
     4.9  
     5.1 --- a/src/Pure/ML-Systems/polyml_pp.ML	Sun May 31 14:51:21 2009 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,20 +0,0 @@
     5.4 -(*  Title:      Pure/ML-Systems/polyml_pp.ML
     5.5 -
     5.6 -Toplevel pretty printing for Poly/ML before 5.3.
     5.7 -*)
     5.8 -
     5.9 -fun ml_pprint (print, begin_blk, brk, end_blk) =
    5.10 -  let
    5.11 -    fun str "" = ()
    5.12 -      | str s = print s;
    5.13 -    fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
    5.14 -          (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
    5.15 -      | pprint (ML_Pretty.String (s, _)) = str s
    5.16 -      | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
    5.17 -      | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
    5.18 -  in pprint end;
    5.19 -
    5.20 -fun toplevel_pp context (_: string list) pp =
    5.21 -  use_text context (1, "pp") false
    5.22 -    ("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
    5.23 -
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/ML-Systems/pp_polyml.ML	Sun May 31 15:03:34 2009 +0200
     6.3 @@ -0,0 +1,20 @@
     6.4 +(*  Title:      Pure/ML-Systems/pp_polyml.ML
     6.5 +
     6.6 +Toplevel pretty printing for Poly/ML before 5.3.
     6.7 +*)
     6.8 +
     6.9 +fun ml_pprint (print, begin_blk, brk, end_blk) =
    6.10 +  let
    6.11 +    fun str "" = ()
    6.12 +      | str s = print s;
    6.13 +    fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
    6.14 +          (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
    6.15 +      | pprint (ML_Pretty.String (s, _)) = str s
    6.16 +      | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
    6.17 +      | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
    6.18 +  in pprint end;
    6.19 +
    6.20 +fun toplevel_pp context (_: string list) pp =
    6.21 +  use_text context (1, "pp") false
    6.22 +    ("PolyML.install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
    6.23 +