src/Pure/ML-Systems/pp_polyml.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 31313 97800f7e80b4
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     1 (*  Title:      Pure/ML-Systems/pp_polyml.ML
     2 
     3 Toplevel pretty printing for Poly/ML before 5.3.
     4 *)
     5 
     6 fun ml_pprint (print, begin_blk, brk, end_blk) =
     7   let
     8     fun str "" = ()
     9       | str s = print s;
    10     fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
    11           (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
    12       | pprint (ML_Pretty.String (s, _)) = str s
    13       | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
    14       | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
    15   in pprint end;
    16 
    17 fun toplevel_pp context (_: string list) pp =
    18   use_text context (1, "pp") false
    19     ("PolyML.install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
    20