use Pretty.enum convenience;
authorwenzelm
Wed Aug 11 15:17:13 2010 +0200 (2010-08-11 ago)
changeset 3832916bb1e60204b
parent 38328 36afb56ec49e
child 38330 e98236e5068b
use Pretty.enum convenience;
src/HOL/Tools/inductive_codegen.ML
src/Pure/Isar/attrib.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Aug 11 15:00:31 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Aug 11 15:17:13 2010 +0200
     1.3 @@ -830,10 +830,10 @@
     1.4            str "case Seq.pull (testf p) of", Pretty.brk 1,
     1.5            str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"],
     1.6            str " =>", Pretty.brk 1, str "SOME ",
     1.7 -          Pretty.block (str "[" ::
     1.8 -            Pretty.commas (map (fn (s, T) => Pretty.block
     1.9 -              [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args') @
    1.10 -            [str "]"]), Pretty.brk 1,
    1.11 +          Pretty.enum "," "[" "]"
    1.12 +            (map (fn (s, T) => Pretty.block
    1.13 +              [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args'),
    1.14 +          Pretty.brk 1,
    1.15            str "| NONE => NONE);"]) ^
    1.16        "\n\nend;\n";
    1.17      val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
     2.1 --- a/src/Pure/Isar/attrib.ML	Wed Aug 11 15:00:31 2010 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Wed Aug 11 15:17:13 2010 +0200
     2.3 @@ -94,8 +94,7 @@
     2.4  
     2.5  fun pretty_attribs _ [] = []
     2.6    | pretty_attribs ctxt srcs =
     2.7 -      [Pretty.enclose "[" "]"
     2.8 -        (Pretty.commas (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs))];
     2.9 +      [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
    2.10  
    2.11  
    2.12  (* get attributes *)
     3.1 --- a/src/Pure/codegen.ML	Wed Aug 11 15:00:31 2010 +0200
     3.2 +++ b/src/Pure/codegen.ML	Wed Aug 11 15:17:13 2010 +0200
     3.3 @@ -889,9 +889,8 @@
     3.4                mk_app false (str "testf") (map (str o fst) args),
     3.5                Pretty.brk 1, str "then NONE",
     3.6                Pretty.brk 1, str "else ",
     3.7 -              Pretty.block [str "SOME ", Pretty.block (str "[" ::
     3.8 -                Pretty.commas (map (fn (s, _) => str (s ^ "_t ()")) args) @
     3.9 -                  [str "]"])]]),
    3.10 +              Pretty.block [str "SOME ",
    3.11 +                Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
    3.12            str ");"]) ^
    3.13        "\n\nend;\n";
    3.14      val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;