src/Pure/ML-Systems/pp_polyml.ML
author wenzelm
Sat Nov 27 16:29:53 2010 +0100 (2010-11-27 ago)
changeset 40748 591b6778d076
parent 31313 97800f7e80b4
permissions -rw-r--r--
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm@31313
     1
(*  Title:      Pure/ML-Systems/pp_polyml.ML
wenzelm@30627
     2
wenzelm@30627
     3
Toplevel pretty printing for Poly/ML before 5.3.
wenzelm@30627
     4
*)
wenzelm@30627
     5
wenzelm@30627
     6
fun ml_pprint (print, begin_blk, brk, end_blk) =
wenzelm@30627
     7
  let
wenzelm@30627
     8
    fun str "" = ()
wenzelm@30627
     9
      | str s = print s;
wenzelm@30627
    10
    fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
wenzelm@30627
    11
          (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
wenzelm@30627
    12
      | pprint (ML_Pretty.String (s, _)) = str s
wenzelm@30627
    13
      | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
wenzelm@30627
    14
      | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
wenzelm@30627
    15
  in pprint end;
wenzelm@30627
    16
wenzelm@30672
    17
fun toplevel_pp context (_: string list) pp =
wenzelm@30672
    18
  use_text context (1, "pp") false
wenzelm@31313
    19
    ("PolyML.install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
wenzelm@30627
    20