# HG changeset patch
# User haftmann
# Date 1263487659 -3600
# Node ID 9b12b0824bfe376dbd4fdf40c5bc8e2e0e86497e
# Parent  8674bb6f727b203812f2fecf4d18bb1f9ca8eb01
tuned for products vs. tupled functions

diff -r 8674bb6f727b -r 9b12b0824bfe src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Jan 14 17:47:39 2010 +0100
+++ b/src/HOL/Product_Type.thy	Thu Jan 14 17:47:39 2010 +0100
@@ -1000,7 +1000,7 @@
   (SML infix 2 "*")
   (OCaml infix 2 "*")
   (Haskell "!((_),/ (_))")
-  (Scala "!((_),/ (_))")
+  (Scala "((_),/ (_))")
 
 code_instance * :: eq
   (Haskell -)
diff -r 8674bb6f727b -r 9b12b0824bfe src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Jan 14 17:47:39 2010 +0100
+++ b/src/Tools/Code/code_scala.ML	Thu Jan 14 17:47:39 2010 +0100
@@ -71,7 +71,7 @@
               (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
                 (map (print_term tyvars is_pat thm vars NOBR) ts))
           | SOME (_, print) => (false, fn ts =>
-              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take k tys_args));
+              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take l tys_args));
       in if k = l then print' ts
       else if k < l then
         print_term tyvars is_pat thm vars fxy (Code_Thingol.eta_expand l app)
@@ -404,11 +404,17 @@
     let
       val s = ML_Syntax.print_char c;
     in if s = "'" then "\\'" else s end;
+  fun bigint_scala k = "(" ^ (if k <= 2147483647
+    then string_of_int k else quote (string_of_int k)) ^ ")"
 in Literals {
   literal_char = Library.enclose "'" "'" o char_scala,
   literal_string = quote o translate_string char_scala,
-  literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
-    else Library.enclose "(" ")" (signed_string_of_int k),
+  literal_numeral = fn unbounded => fn k => if k >= 0 then
+      if unbounded then bigint_scala k
+      else Library.enclose "(" ")" (string_of_int k)
+    else
+      if unbounded then "(- " ^ bigint_scala (~ k) ^ ")"
+      else Library.enclose "(" ")" (signed_string_of_int k),
   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   infix_cons = (6, "::")
 } end;
@@ -424,7 +430,7 @@
   Code_Target.add_target (target, (isar_seri_scala, literals))
   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy [
-        print_typ (INFX (1, X)) ty1,
+        print_typ BR ty1 (*product type vs. tupled arguments!*),
         str "=>",
         print_typ (INFX (1, R)) ty2
       ]))