src/Pure/ML-Systems/ml_pretty.ML
author wenzelm
Sat, 19 Dec 2015 14:47:52 +0100
changeset 61864 3a5992c3410c
parent 61862 e2a9e46ac0fb
child 61869 ba466ac335e3
permissions -rw-r--r--
support for blocks with consistent breaks; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30622
dba663f1afa8 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/ml_pretty.ML
dba663f1afa8 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
dba663f1afa8 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff changeset
     3
38635
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
     4
Minimal support for raw ML pretty printing -- for boot-strapping only.
30622
dba663f1afa8 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff changeset
     5
*)
dba663f1afa8 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff changeset
     6
dba663f1afa8 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff changeset
     7
structure ML_Pretty =
dba663f1afa8 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff changeset
     8
struct
dba663f1afa8 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff changeset
     9
dba663f1afa8 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff changeset
    10
datatype pretty =
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
    11
  Block of (string * string) * pretty list * bool * int |
30623
9ed1122d6cd2 simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
wenzelm
parents: 30622
diff changeset
    12
  String of string * int |
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 38635
diff changeset
    13
  Break of bool * int * int;
30622
dba663f1afa8 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff changeset
    14
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
    15
fun block prts = Block (("", ""), prts, false, 2);
38635
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    16
fun str s = String (s, size s);
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 38635
diff changeset
    17
fun brk width = Break (false, width, 0);
38635
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    18
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    19
fun pair pretty1 pretty2 ((x, y), depth: int) =
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    20
  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    21
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    22
fun enum sep lpar rpar pretty (args, depth) =
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    23
  let
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    24
    fun elems _ [] = []
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    25
      | elems 0 _ = [str "..."]
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    26
      | elems d [x] = [pretty (x, d)]
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    27
      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    28
  in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
f76ad0771f67 added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents: 30623
diff changeset
    29
30622
dba663f1afa8 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff changeset
    30
end;
dba663f1afa8 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff changeset
    31