src/Pure/ML-Systems/ml_pretty.ML
author wenzelm
Thu Dec 17 17:32:01 2015 +0100 (2015-12-17)
changeset 61862 e2a9e46ac0fb
parent 38635 f76ad0771f67
child 61864 3a5992c3410c
permissions -rw-r--r--
support pretty break indent, like underlying ML systems;
     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 * int;
    14 
    15 fun block prts = Block (("", ""), prts, 2);
    16 fun str s = String (s, size s);
    17 fun brk width = Break (false, width, 0);
    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