src/Pure/ML-Systems/ml_pretty.ML
author wenzelm
Tue Mar 25 13:18:10 2014 +0100 (2014-03-25 ago)
changeset 56275 600f432ab556
parent 38635 f76ad0771f67
child 61864 e2a9e46ac0fb
permissions -rw-r--r--
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm@30622
     1
(*  Title:      Pure/ML-Systems/ml_pretty.ML
wenzelm@30622
     2
    Author:     Makarius
wenzelm@30622
     3
wenzelm@38635
     4
Minimal support for raw ML pretty printing -- for boot-strapping only.
wenzelm@30622
     5
*)
wenzelm@30622
     6
wenzelm@30622
     7
structure ML_Pretty =
wenzelm@30622
     8
struct
wenzelm@30622
     9
wenzelm@30622
    10
datatype pretty =
wenzelm@30623
    11
  Block of (string * string) * pretty list * int |
wenzelm@30623
    12
  String of string * int |
wenzelm@30623
    13
  Break of bool * int;
wenzelm@30622
    14
wenzelm@38635
    15
fun block prts = Block (("", ""), prts, 2);
wenzelm@38635
    16
fun str s = String (s, size s);
wenzelm@38635
    17
fun brk wd = Break (false, wd);
wenzelm@38635
    18
wenzelm@38635
    19
fun pair pretty1 pretty2 ((x, y), depth: int) =
wenzelm@38635
    20
  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
wenzelm@38635
    21
wenzelm@38635
    22
fun enum sep lpar rpar pretty (args, depth) =
wenzelm@38635
    23
  let
wenzelm@38635
    24
    fun elems _ [] = []
wenzelm@38635
    25
      | elems 0 _ = [str "..."]
wenzelm@38635
    26
      | elems d [x] = [pretty (x, d)]
wenzelm@38635
    27
      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
wenzelm@38635
    28
  in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
wenzelm@38635
    29
wenzelm@30622
    30
end;
wenzelm@30622
    31