--- a/src/Tools/Code/code_haskell.ML Wed Dec 23 10:09:06 2009 +0100
+++ b/src/Tools/Code/code_haskell.ML Wed Dec 23 11:32:08 2009 +0100
@@ -32,7 +32,7 @@
| SOME class => class;
fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
of [] => []
- | classbinds => Pretty.list "(" ")" (
+ | classbinds => enum "," "(" ")" (
map (fn (v, class) =>
str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds)
@@ str " => ";
@@ -412,11 +412,11 @@
val s = ML_Syntax.print_char c;
in if s = "'" then "\\'" else s end;
in Literals {
- literal_char = enclose "'" "'" o char_haskell,
+ literal_char = Library.enclose "'" "'" o char_haskell,
literal_string = quote o translate_string char_haskell,
literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
- else enclose "(" ")" (signed_string_of_int k),
- literal_list = Pretty.enum "," "[" "]",
+ else Library.enclose "(" ")" (signed_string_of_int k),
+ literal_list = enum "," "[" "]",
infix_cons = (5, ":")
} end;
@@ -451,7 +451,7 @@
val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
(bind :: binds) vars;
in
- (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks)
+ (brackify fxy o single o enclose "do {" "}" o Pretty.breaks)
(ps @| print_term vars' NOBR t'')
end
| NONE => brackify_infix (1, L) fxy