# HG changeset patch # User haftmann # Date 1261564328 -3600 # Node ID a78b8d5b91cbc8086c7484502d31a5954f348914 # Parent 412cf41a92a0b00c8d672c448bd2896ad80f79cf take care for destructive print mode properly using dedicated pretty builders diff -r 412cf41a92a0 -r a78b8d5b91cb src/Tools/Code/code_haskell.ML --- 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 diff -r 412cf41a92a0 -r a78b8d5b91cb src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Wed Dec 23 10:09:06 2009 +0100 +++ b/src/Tools/Code/code_ml.ML Wed Dec 23 11:32:08 2009 +0100 @@ -51,11 +51,11 @@ fun print_product _ [] = NONE | print_product print [x] = SOME (print x) - | print_product print xs = (SOME o Pretty.enum " *" "" "") (map print xs); + | print_product print xs = (SOME o enum " *" "" "") (map print xs); fun print_tuple _ _ [] = NONE | print_tuple print fxy [x] = SOME (print fxy x) - | print_tuple print _ xs = SOME (Pretty.list "(" ")" (map (print NOBR) xs)); + | print_tuple print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs)); (** SML serializer **) @@ -66,13 +66,13 @@ | print_tyco_expr fxy (tyco, [ty]) = concat [print_typ BR ty, (str o deresolve) tyco] | print_tyco_expr fxy (tyco, tys) = - concat [Pretty.list "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] + concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco of NONE => print_tyco_expr fxy (tyco, tys) | SOME (i, print) => print print_typ fxy tys) | print_typ fxy (ITyVar v) = str ("'" ^ v); fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]); - fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" "" + fun print_typscheme_prefix (vs, p) = enum " ->" "" "" (map_filter (fn (v, sort) => (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); @@ -89,7 +89,7 @@ of [] => v_p | [classrel] => brackets [(str o deresolve) classrel, v_p] | classrels => brackets - [Pretty.enum " o" "(" ")" (map (str o deresolve) classrels), v_p] + [enum " o" "(" ")" (map (str o deresolve) classrels), v_p] end and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR @@ -145,9 +145,9 @@ val (ps, vars') = fold_map print_match binds vars; in Pretty.chunks [ - Pretty.block [str ("let"), Pretty.fbrk, Pretty.chunks ps], - Pretty.block [str ("in"), Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body], - str ("end") + Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps], + Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body], + str "end" ] end | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) = @@ -174,7 +174,7 @@ let fun print_co (co, []) = str (deresolve co) | print_co (co, tys) = concat [str (deresolve co), str "of", - Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; + enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; in concat ( str definer @@ -196,7 +196,7 @@ (insert (op =)) ts []); val prolog = if needs_typ then concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty] - else Pretty.strs [definer, deresolve name]; + else (concat o map str) [definer, deresolve name]; in concat ( prolog @@ -240,7 +240,7 @@ :: (if is_pseudo_fun inst then [str "()"] else print_dict_args vs) @ str "=" - :: Pretty.list "{" "}" + :: enum "," "{" "}" (map print_superinst superinsts @ map print_classparam classparams) :: str ":" @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs]) @@ -328,7 +328,7 @@ str ("type '" ^ v), (str o deresolve) class, str "=", - Pretty.list "{" "};" ( + enum "," "{" "};" ( map print_superclass_field superclasses @ map print_classparam_field classparams ) @@ -344,7 +344,7 @@ else Pretty.chunks2 ( Pretty.chunks ( str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " =")) - :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls + :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls @| (if is_some some_decls then str "end = struct" else str "struct") ) :: body @@ -357,7 +357,7 @@ literal_numeral = fn unbounded => fn k => if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)" else string_of_int k, - literal_list = Pretty.list "[" "]", + literal_list = enum "," "[" "]", infix_cons = (7, "::") }; @@ -370,13 +370,13 @@ | print_tyco_expr fxy (tyco, [ty]) = concat [print_typ BR ty, (str o deresolve) tyco] | print_tyco_expr fxy (tyco, tys) = - concat [Pretty.list "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] + concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco of NONE => print_tyco_expr fxy (tyco, tys) | SOME (i, print) => print print_typ fxy tys) | print_typ fxy (ITyVar v) = str ("'" ^ v); fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]); - fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" "" + fun print_typscheme_prefix (vs, p) = enum " ->" "" "" (map_filter (fn (v, sort) => (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); @@ -465,7 +465,7 @@ let fun print_co (co, []) = str (deresolve co) | print_co (co, tys) = concat [str (deresolve co), str "of", - Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; + enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; in concat ( str definer @@ -543,7 +543,7 @@ end; val prolog = if needs_typ then concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty] - else Pretty.strs [definer, deresolve name]; + else (concat o map str) [definer, deresolve name]; in pair (print_val_decl print_typscheme (name, vs_ty)) (concat ( @@ -670,7 +670,7 @@ else Pretty.chunks2 ( Pretty.chunks ( str ("module " ^ name ^ (if is_some some_decls then " : sig" else " =")) - :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls + :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls @| (if is_some some_decls then str "end = struct" else str "struct") ) :: body @@ -693,15 +693,15 @@ then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")" else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")" in Literals { - literal_char = enclose "'" "'" o char_ocaml, + literal_char = Library.enclose "'" "'" o char_ocaml, literal_string = quote o translate_string char_ocaml, literal_numeral = fn unbounded => fn k => if k >= 0 then if unbounded then bignum_ocaml k else string_of_int k else if unbounded then "(Big_int.minus_big_int " ^ bignum_ocaml (~ k) ^ ")" - else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k, - literal_list = Pretty.enum ";" "[" "]", + else (Library.enclose "(" ")" o prefix "-" o string_of_int o op ~) k, + literal_list = enum ";" "[" "]", infix_cons = (6, "::") } end; diff -r 412cf41a92a0 -r a78b8d5b91cb src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Wed Dec 23 10:09:06 2009 +0100 +++ b/src/Tools/Code/code_printer.ML Wed Dec 23 11:32:08 2009 +0100 @@ -18,9 +18,12 @@ val str: string -> Pretty.T val concat: Pretty.T list -> Pretty.T val brackets: Pretty.T list -> Pretty.T + val enclose: string -> string -> Pretty.T list -> Pretty.T + val enum: string -> string -> string -> Pretty.T list -> Pretty.T + val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T val semicolon: Pretty.T list -> Pretty.T val doublesemicolon: Pretty.T list -> Pretty.T - val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T + val indent: int -> Pretty.T -> Pretty.T val string_of_pretty: int -> Pretty.T -> string val writeln_pretty: int -> Pretty.T -> unit @@ -99,11 +102,14 @@ fun xs @| y = xs @ [y]; val str = PrintMode.setmp [] Pretty.str; val concat = Pretty.block o Pretty.breaks; -val brackets = Pretty.enclose "(" ")" o Pretty.breaks; +fun enclose l r = PrintMode.setmp [] (Pretty.enclose l r); +val brackets = enclose "(" ")" o Pretty.breaks; +fun enum sep l r = PrintMode.setmp [] (Pretty.enum sep l r); +fun enum_default default sep l r [] = str default + | enum_default default sep l r xs = enum sep l r xs; fun semicolon ps = Pretty.block [concat ps, str ";"]; fun doublesemicolon ps = Pretty.block [concat ps, str ";;"]; -fun enum_default default sep opn cls [] = str default - | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs; +fun indent i = PrintMode.setmp [] (Pretty.indent i); fun string_of_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.string_of) p ^ "\n"; fun writeln_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.writeln) p; @@ -198,7 +204,7 @@ | fixity _ _ = true; fun gen_brackify _ [p] = p - | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps + | gen_brackify true (ps as _::_) = enclose "(" ")" ps | gen_brackify false (ps as _::_) = Pretty.block ps; fun brackify fxy_ctxt = @@ -210,7 +216,7 @@ fun brackify_block fxy_ctxt p1 ps p2 = let val p = Pretty.block_enclose (p1, p2) ps in if fixity BR fxy_ctxt - then Pretty.enclose "(" ")" [p] + then enclose "(" ")" [p] else p end;