# HG changeset patch
# User haftmann
# Date 1275381053 -7200
# Node ID 4d984bc33c6681a34ac2a414c4c850128bf86ff0
# Parent  9d9205e31767a857ad087f10a6b8c1e522c72376
added Scala code setup

diff -r 9d9205e31767 -r 4d984bc33c66 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Tue Jun 01 10:30:53 2010 +0200
+++ b/src/HOL/Library/Code_Char.thy	Tue Jun 01 10:30:53 2010 +0200
@@ -12,9 +12,10 @@
   (SML "char")
   (OCaml "char")
   (Haskell "Char")
+  (Scala "Char")
 
 setup {*
-  fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"] 
+  fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] 
   #> String_Code.add_literal_list_string "Haskell"
 *}
 
@@ -27,10 +28,14 @@
 code_reserved OCaml
   char
 
+code_reserved Scala
+  char
+
 code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (SML "!((_ : char) = _)")
   (OCaml "!((_ : char) = _)")
   (Haskell infixl 4 "==")
+  (Scala infixl 5 "==")
 
 code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
   (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
@@ -53,10 +58,12 @@
   (SML "String.implode")
   (OCaml "failwith/ \"implode\"")
   (Haskell "_")
+  (Scala "List.toString((_))")
 
 code_const explode
   (SML "String.explode")
   (OCaml "failwith/ \"explode\"")
   (Haskell "_")
+  (Scala "List.fromString((_))")
 
 end
diff -r 9d9205e31767 -r 4d984bc33c66 src/HOL/Library/Code_Char_chr.thy
--- a/src/HOL/Library/Code_Char_chr.thy	Tue Jun 01 10:30:53 2010 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy	Tue Jun 01 10:30:53 2010 +0200
@@ -22,23 +22,10 @@
   "char_of_nat = char_of_int o int"
   unfolding char_of_int_def by (simp add: expand_fun_eq)
 
-lemmas [code del] = char.recs char.cases char.size
-
-lemma [code, code_unfold]:
-  "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
-  by (cases c) (auto simp add: nibble_pair_of_nat_char)
-
-lemma [code, code_unfold]:
-  "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
-  by (cases c) (auto simp add: nibble_pair_of_nat_char)
-
-lemma [code]:
-  "size (c\<Colon>char) = 0"
-  by (cases c) auto
-
 code_const int_of_char and char_of_int
   (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
   (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
-  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
+  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | (0 <= k && k < 256) = toEnum k :: Char in chr . fromInteger)")
+  (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
 
-end
\ No newline at end of file
+end