src/Pure/ML-Systems/ml_pretty.ML
author wenzelm
Sat Nov 27 16:29:53 2010 +0100 (2010-11-27 ago)
changeset 40748 591b6778d076
parent 38635 f76ad0771f67
child 61864 e2a9e46ac0fb
permissions -rw-r--r--
removed bash from ML system bootstrap, and past the Secure ML barrier;
     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