src/Pure/ML-Systems/pp_polyml.ML
author haftmann
Mon, 08 Feb 2010 17:12:22 +0100
changeset 35045 a77d200e6503
parent 31313 97800f7e80b4
permissions -rw-r--r--
using code antiquotation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31313
97800f7e80b4 renamed polyml_pp.ML to pp_polyml.ML;
wenzelm
parents: 30672
diff changeset
     1
(*  Title:      Pure/ML-Systems/pp_polyml.ML
30627
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
     2
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
     3
Toplevel pretty printing for Poly/ML before 5.3.
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
     4
*)
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
     5
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
     6
fun ml_pprint (print, begin_blk, brk, end_blk) =
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
     7
  let
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
     8
    fun str "" = ()
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
     9
      | str s = print s;
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
    10
    fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
    11
          (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
    12
      | pprint (ML_Pretty.String (s, _)) = str s
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
    13
      | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
    14
      | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
    15
  in pprint end;
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
    16
30672
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents: 30627
diff changeset
    17
fun toplevel_pp context (_: string list) pp =
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents: 30627
diff changeset
    18
  use_text context (1, "pp") false
31313
97800f7e80b4 renamed polyml_pp.ML to pp_polyml.ML;
wenzelm
parents: 30672
diff changeset
    19
    ("PolyML.install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
30627
fb9e73c01603 added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
diff changeset
    20