src/Pure/ML/ml_pretty.ML
changeset 80814 f06fc05f7c01
parent 80813 9dd4dcb08d37
child 80840 793e490d7bd1
equal deleted inserted replaced
80813:9dd4dcb08d37 80814:f06fc05f7c01
    36 fun brk width = PrettyBreak (width, 0);
    36 fun brk width = PrettyBreak (width, 0);
    37 
    37 
    38 val dots = str "...";
    38 val dots = str "...";
    39 
    39 
    40 fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
    40 fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
    41   block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
    41   if depth = 0 then dots
       
    42   else block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
    42 
    43 
    43 fun enum sep lpar rpar pretty (args, depth: FixedInt.int) =
    44 fun enum sep lpar rpar pretty (args, depth: FixedInt.int) =
    44   let
    45   if depth = 0 then dots
    45     fun elems _ [] = []
    46   else
    46       | elems 0 _ = [dots]
    47     let
    47       | elems d [x] = [pretty (x, d)]
    48       fun elems _ [] = []
    48       | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
    49         | elems 0 _ = [dots]
    49   in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
    50         | elems d [x] = [pretty (x, d)]
       
    51         | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
       
    52     in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
    50 
    53 
    51 
    54 
    52 (* prune *)
    55 (* prune *)
    53 
    56 
    54 fun prune (0: FixedInt.int) (PrettyBlock _) = dots
    57 fun prune (0: FixedInt.int) (PrettyBlock _) = dots