--- a/src/Pure/Tools/codegen_serializer.ML Fri Jan 27 19:03:17 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Fri Jan 27 19:03:19 2006 +0100
@@ -284,7 +284,7 @@
case unfoldr dest_cons e2
of (es, IConst (c, _)) => (writeln (string_of_int (length es));
if c = thingol_nil
- then Pretty.gen_list "," "[" "]" (map (pr NOBR) (e1::es))
+ then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es))
else pretty_default fxy pr e1 e2)
| _ => pretty_default fxy pr e1 e2;
in ((2, 2), pretty_compact) end;
@@ -345,7 +345,7 @@
| ml_from_type _ (IVarT (_, sort)) =
"cannot serialize sort constrained type variable to ML: " ^ commas sort |> error
| ml_from_type _ (IDictT fs) =
- Pretty.gen_list "," "{" "}" (
+ Pretty.enum "," "{" "}" (
map (fn (f, ty) =>
Pretty.block [str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs
);
@@ -360,7 +360,7 @@
else
ps
|> map (ml_from_pat BR)
- |> Pretty.gen_list "," "(" ")"
+ |> Pretty.enum "," "(" ")"
|> single
|> cons ((str o resolv) f)
|> brackify fxy
@@ -433,7 +433,7 @@
| ml_from_expr fxy (IInst _) =
error "cannot serialize poly instant to ML"
| ml_from_expr fxy (IDictE fs) =
- Pretty.gen_list "," "{" "}" (
+ Pretty.enum "," "{" "}" (
map (fn (f, e) =>
Pretty.block [str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs
)
@@ -456,7 +456,7 @@
and ml_mk_app f es =
if is_cons f andalso length es > 1
then
- [(str o resolv) f, Pretty.gen_list " *" "(" ")" (map (ml_from_expr BR) es)]
+ [(str o resolv) f, Pretty.enum " *" "(" ")" (map (ml_from_expr BR) es)]
else
(str o resolv) f :: map (ml_from_expr BR) es
and ml_from_app fxy =
@@ -648,7 +648,7 @@
| from_sctxt vs =
vs
|> map (fn (v, cls) => str ((upper_first o resolv) cls ^ " " ^ lower_first v))
- |> Pretty.gen_list "," "(" ")"
+ |> Pretty.enum "," "(" ")"
|> (fn p => Pretty.block [p, str " => "])
in
vs
--- a/src/Pure/Tools/codegen_thingol.ML Fri Jan 27 19:03:17 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Fri Jan 27 19:03:19 2006 +0100
@@ -317,16 +317,16 @@
(* simple diagnosis *)
fun pretty_itype (IType (tyco, tys)) =
- Pretty.gen_list "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
+ Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
| pretty_itype (IFun (ty1, ty2)) =
- Pretty.gen_list "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
+ Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
| pretty_itype (IVarT (v, sort)) =
Pretty.str (v ^ enclose "|" "|" (space_implode "|" sort))
| pretty_itype (IDictT _) =
Pretty.str "<DictT>";
fun pretty_ipat (ICons ((cons, ps), ty)) =
- Pretty.gen_list " " "(" ")"
+ Pretty.enum " " "(" ")"
(Pretty.str cons :: map pretty_ipat ps @ [Pretty.str ":: ", pretty_itype ty])
| pretty_ipat (IVarP (v, ty)) =
Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty];
@@ -479,10 +479,10 @@
| pretty_def (Prim prims) =
Pretty.str ("<PRIM " ^ (commas o map fst) prims ^ ">")
| pretty_def (Fun (eqs, (_, ty))) =
- Pretty.gen_list " |" "" "" (
+ Pretty.enum " |" "" "" (
map (fn (ps, body) =>
Pretty.block [
- Pretty.gen_list "," "[" "]" (map pretty_ipat ps),
+ Pretty.enum "," "[" "]" (map pretty_ipat ps),
Pretty.str " |->",
Pretty.brk 1,
pretty_iexpr body,
@@ -500,22 +500,22 @@
Pretty.block [
Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
Pretty.str " |=> ",
- Pretty.gen_list " |" "" ""
+ Pretty.enum " |" "" ""
(map (fn (c, tys) => (Pretty.block o Pretty.breaks) (Pretty.str c :: map pretty_itype tys)) cs),
Pretty.str ", instances ",
- Pretty.gen_list "," "[" "]" (map Pretty.str insts)
+ Pretty.enum "," "[" "]" (map Pretty.str insts)
]
| pretty_def (Datatypecons dtname) =
Pretty.str ("cons " ^ dtname)
| pretty_def (Class ((supcls, (v, mems)), insts)) =
Pretty.block [
Pretty.str ("class var " ^ v ^ "extending "),
- Pretty.gen_list "," "[" "]" (map Pretty.str supcls),
+ Pretty.enum "," "[" "]" (map Pretty.str supcls),
Pretty.str " with ",
- Pretty.gen_list "," "[" "]"
+ Pretty.enum "," "[" "]"
(map (fn (m, (_, ty)) => Pretty.block [Pretty.str (m ^ "::"), pretty_itype ty]) mems),
Pretty.str " instances ",
- Pretty.gen_list "," "[" "]" (map Pretty.str insts)
+ Pretty.enum "," "[" "]" (map Pretty.str insts)
]
| pretty_def (Classmember clsname) =
Pretty.block [
@@ -529,7 +529,7 @@
Pretty.str ", (",
Pretty.str tyco,
Pretty.str ", ",
- Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o map Pretty.str o snd) arity),
+ Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o map Pretty.str o snd) arity),
Pretty.str "))"
];