1.1 --- a/src/HOL/Tools/list_code.ML	Tue Jun 01 11:18:51 2010 +0200
     1.2 +++ b/src/HOL/Tools/list_code.ML	Tue Jun 01 13:52:11 2010 +0200
     1.3 @@ -31,11 +31,11 @@
     1.4    end;
     1.5  
     1.6  fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
     1.7 -  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
     1.8 +  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
     1.9      pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
    1.10      Code_Printer.str target_cons,
    1.11      pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
    1.12 -  ];
    1.13 +  );
    1.14  
    1.15  fun add_literal_list target =
    1.16    let

     2.1 --- a/src/Tools/Code/code_haskell.ML	Tue Jun 01 11:18:51 2010 +0200
     2.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Jun 01 13:52:11 2010 +0200
     2.3 @@ -447,7 +447,7 @@
     2.4              (ps @| print_term vars' NOBR t'')
     2.5          end
     2.6        | NONE => brackify_infix (1, L) fxy
     2.7 -          [print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2]
     2.8 +          (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
     2.9    in (2, ([c_bind], pretty)) end;
    2.10  
    2.11  fun add_monad target' raw_c_bind thy =
    2.12 @@ -477,11 +477,11 @@
    2.13  val setup =
    2.14    Code_Target.add_target (target, (isar_seri_haskell, literals))
    2.15    #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    2.16 -      brackify_infix (1, R) fxy [
    2.17 +      brackify_infix (1, R) fxy (
    2.18          print_typ (INFX (1, X)) ty1,
    2.19          str "->",
    2.20          print_typ (INFX (1, R)) ty2
    2.21 -      ]))
    2.22 +      )))
    2.23    #> fold (Code_Target.add_reserved target) [
    2.24        "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
    2.25        "import", "default", "forall", "let", "in", "class", "qualified", "data",

     3.1 --- a/src/Tools/Code/code_ml.ML	Tue Jun 01 11:18:51 2010 +0200
     3.2 +++ b/src/Tools/Code/code_ml.ML	Tue Jun 01 13:52:11 2010 +0200
     3.3 @@ -963,17 +963,17 @@
     3.4    Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
     3.5    #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
     3.6    #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
     3.7 -      brackify_infix (1, R) fxy [
     3.8 +      brackify_infix (1, R) fxy (
     3.9          print_typ (INFX (1, X)) ty1,
    3.10          str "->",
    3.11          print_typ (INFX (1, R)) ty2
    3.12 -      ]))
    3.13 +      )))
    3.14    #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    3.15 -      brackify_infix (1, R) fxy [
    3.16 +      brackify_infix (1, R) fxy (
    3.17          print_typ (INFX (1, X)) ty1,
    3.18          str "->",
    3.19          print_typ (INFX (1, R)) ty2
    3.20 -      ]))
    3.21 +      )))
    3.22    #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
    3.23    #> fold (Code_Target.add_reserved target_SML)
    3.24        ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*), "IntInf"]

     4.1 --- a/src/Tools/Code/code_printer.ML	Tue Jun 01 11:18:51 2010 +0200
     4.2 +++ b/src/Tools/Code/code_printer.ML	Tue Jun 01 13:52:11 2010 +0200
     4.3 @@ -61,7 +61,7 @@
     4.4    val INFX: int * lrx -> fixity
     4.5    val APP: fixity
     4.6    val brackify: fixity -> Pretty.T list -> Pretty.T
     4.7 -  val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
     4.8 +  val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
     4.9    val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
    4.10    val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
    4.11  
    4.12 @@ -219,8 +219,9 @@
    4.13  fun brackify fxy_ctxt =
    4.14    gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
    4.15  
    4.16 -fun brackify_infix infx fxy_ctxt =
    4.17 -  gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
    4.18 +fun brackify_infix infx fxy_ctxt (l, m, r) =
    4.19 +  (if fixity (INFX infx) fxy_ctxt then enclose "(" ")" else Pretty.block)
    4.20 +    ([l, str " ", m, Pretty.brk 1, r]);
    4.21  
    4.22  fun brackify_block fxy_ctxt p1 ps p2 =
    4.23    let val p = Pretty.block_enclose (p1, p2) ps
    4.24 @@ -304,7 +305,7 @@
    4.25      val r = case x of R => INFX (i, R) | _ => INFX (i, X);
    4.26    in
    4.27      mk_mixfix prep_arg (INFX (i, x),
    4.28 -      [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
    4.29 +      [Arg l, (Pretty o str) " ", (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
    4.30    end;
    4.31  
    4.32  fun parse_mixfix prep_arg s =