# HG changeset patch
# User haftmann
# Date 1263143669 -3600
# Node ID d91c3fce478eb1909dedb04a70f0b3819589a621
# Parent  3f2e25dc99ab91690178bade1b32c96aa933865d# Parent  394fc3cce91561f7ef971e51e9f6c885564f1daf
merged

diff -r 3f2e25dc99ab -r d91c3fce478e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Jan 09 23:22:56 2010 +0100
+++ b/src/HOL/HOL.thy	Sun Jan 10 18:14:29 2010 +0100
@@ -1925,9 +1925,9 @@
   (Haskell "True" and "False" and "not"
     and infixl 3 "&&" and infixl 2 "||"
     and "!(if (_)/ then (_)/ else (_))")
-
-code_const True and False
-  (Scala "true" and "false")
+  (Scala "true" and "false" and "'! _"
+    and infixl 3 "&&" and infixl 1 "||"
+    and "!(if ((_))/ (_)/ else (_))")
 
 code_reserved SML
   bool true false not
diff -r 3f2e25dc99ab -r d91c3fce478e src/HOL/ex/Codegenerator_Pretty_Test.thy
--- a/src/HOL/ex/Codegenerator_Pretty_Test.thy	Sat Jan 09 23:22:56 2010 +0100
+++ b/src/HOL/ex/Codegenerator_Pretty_Test.thy	Sun Jan 10 18:14:29 2010 +0100
@@ -10,5 +10,6 @@
 export_code * in SML module_name CodegenTest
   in OCaml module_name CodegenTest file -
   in Haskell file -
+  in Scala file -
 
 end
diff -r 3f2e25dc99ab -r d91c3fce478e src/HOL/ex/Codegenerator_Test.thy
--- a/src/HOL/ex/Codegenerator_Test.thy	Sat Jan 09 23:22:56 2010 +0100
+++ b/src/HOL/ex/Codegenerator_Test.thy	Sun Jan 10 18:14:29 2010 +0100
@@ -10,5 +10,6 @@
 export_code * in SML module_name CodegenTest
   in OCaml module_name CodegenTest file -
   in Haskell file -
+  in Scala file -
 
 end
diff -r 3f2e25dc99ab -r d91c3fce478e src/Pure/name.ML
--- a/src/Pure/name.ML	Sat Jan 09 23:22:56 2010 +0100
+++ b/src/Pure/name.ML	Sun Jan 10 18:14:29 2010 +0100
@@ -156,7 +156,7 @@
           if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs
           else "x" :: xs;
         fun is_valid x =
-          Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x orelse x = "'";
+          Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x;
         fun sep [] = []
           | sep (xs as "_" :: _) = xs
           | sep xs = "_" :: xs;
diff -r 3f2e25dc99ab -r d91c3fce478e src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sat Jan 09 23:22:56 2010 +0100
+++ b/src/Tools/Code/code_scala.ML	Sun Jan 10 18:14:29 2010 +0100
@@ -60,7 +60,7 @@
                 then print_case tyvars thm vars fxy cases
                 else print_app tyvars is_pat thm vars fxy c_ts
             | NONE => print_case tyvars thm vars fxy cases)
-    and print_app tyvars is_pat thm vars fxy (app as ((c, ((tys, _), _)), ts)) =
+    and print_app tyvars is_pat thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
       let
         val k = length ts;
         val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
@@ -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));
+              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take k 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)