src/Pure/ML-Systems/ml_pretty.ML
author wenzelm
Mon Aug 23 15:11:41 2010 +0200 (2010-08-23)
changeset 38635 f76ad0771f67
parent 30623 9ed1122d6cd2
child 61862 e2a9e46ac0fb
permissions -rw-r--r--
added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
     1 (*  Title:      Pure/ML-Systems/ml_pretty.ML
     2     Author:     Makarius
     3 
     4 Minimal support for raw ML pretty printing -- for boot-strapping only.
     5 *)
     6 
     7 structure ML_Pretty =
     8 struct
     9 
    10 datatype pretty =
    11   Block of (string * string) * pretty list * int |
    12   String of string * int |
    13   Break of bool * int;
    14 
    15 fun block prts = Block (("", ""), prts, 2);
    16 fun str s = String (s, size s);
    17 fun brk wd = Break (false, wd);
    18 
    19 fun pair pretty1 pretty2 ((x, y), depth: int) =
    20   block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
    21 
    22 fun enum sep lpar rpar pretty (args, depth) =
    23   let
    24     fun elems _ [] = []
    25       | elems 0 _ = [str "..."]
    26       | elems d [x] = [pretty (x, d)]
    27       | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
    28   in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
    29 
    30 end;
    31