# HG changeset patch
# User haftmann
# Date 1275393131 -7200
# Node ID 97097e589715893e051454fcb35b8c7992c78831
# Parent  32c5251f78cdd5a2c42ae9dac9309d2032f5cdcb
brackify_infix etc.: no break before infix operator -- eases survival in Scala

diff -r 32c5251f78cd -r 97097e589715 src/HOL/Tools/list_code.ML
--- a/src/HOL/Tools/list_code.ML	Tue Jun 01 11:18:51 2010 +0200
+++ b/src/HOL/Tools/list_code.ML	Tue Jun 01 13:52:11 2010 +0200
@@ -31,11 +31,11 @@
   end;
 
 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
-  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
+  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
     pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
     Code_Printer.str target_cons,
     pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
-  ];
+  );
 
 fun add_literal_list target =
   let
diff -r 32c5251f78cd -r 97097e589715 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Tue Jun 01 11:18:51 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Tue Jun 01 13:52:11 2010 +0200
@@ -447,7 +447,7 @@
             (ps @| print_term vars' NOBR t'')
         end
       | NONE => brackify_infix (1, L) fxy
-          [print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2]
+          (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
   in (2, ([c_bind], pretty)) end;
 
 fun add_monad target' raw_c_bind thy =
@@ -477,11 +477,11 @@
 val setup =
   Code_Target.add_target (target, (isar_seri_haskell, literals))
   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
-      brackify_infix (1, R) fxy [
+      brackify_infix (1, R) fxy (
         print_typ (INFX (1, X)) ty1,
         str "->",
         print_typ (INFX (1, R)) ty2
-      ]))
+      )))
   #> fold (Code_Target.add_reserved target) [
       "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
       "import", "default", "forall", "let", "in", "class", "qualified", "data",
diff -r 32c5251f78cd -r 97097e589715 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Jun 01 11:18:51 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Jun 01 13:52:11 2010 +0200
@@ -963,17 +963,17 @@
   Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
   #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
   #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
-      brackify_infix (1, R) fxy [
+      brackify_infix (1, R) fxy (
         print_typ (INFX (1, X)) ty1,
         str "->",
         print_typ (INFX (1, R)) ty2
-      ]))
+      )))
   #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
-      brackify_infix (1, R) fxy [
+      brackify_infix (1, R) fxy (
         print_typ (INFX (1, X)) ty1,
         str "->",
         print_typ (INFX (1, R)) ty2
-      ]))
+      )))
   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   #> fold (Code_Target.add_reserved target_SML)
       ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*), "IntInf"]
diff -r 32c5251f78cd -r 97097e589715 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Tue Jun 01 11:18:51 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Tue Jun 01 13:52:11 2010 +0200
@@ -61,7 +61,7 @@
   val INFX: int * lrx -> fixity
   val APP: fixity
   val brackify: fixity -> Pretty.T list -> Pretty.T
-  val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
+  val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
   val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
   val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
 
@@ -219,8 +219,9 @@
 fun brackify fxy_ctxt =
   gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
 
-fun brackify_infix infx fxy_ctxt =
-  gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
+fun brackify_infix infx fxy_ctxt (l, m, r) =
+  (if fixity (INFX infx) fxy_ctxt then enclose "(" ")" else Pretty.block)
+    ([l, str " ", m, Pretty.brk 1, r]);
 
 fun brackify_block fxy_ctxt p1 ps p2 =
   let val p = Pretty.block_enclose (p1, p2) ps
@@ -304,7 +305,7 @@
     val r = case x of R => INFX (i, R) | _ => INFX (i, X);
   in
     mk_mixfix prep_arg (INFX (i, x),
-      [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
+      [Arg l, (Pretty o str) " ", (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
   end;
 
 fun parse_mixfix prep_arg s =