1.1 --- a/src/HOL/Library/Char_nat.thy	Tue Jun 01 09:12:12 2010 +0200
     1.2 +++ b/src/HOL/Library/Char_nat.thy	Tue Jun 01 11:18:51 2010 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4    unfolding nibble_of_nat_def by auto
     1.5  
     1.6  lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
     1.7 -  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
     1.8 +  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc One_nat_def]
     1.9  
    1.10  lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
    1.11    by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
    1.12 @@ -193,12 +193,12 @@
    1.13  text {* Code generator setup *}
    1.14  
    1.15  code_modulename SML
    1.16 -  Char_nat List
    1.17 +  Char_nat String
    1.18  
    1.19  code_modulename OCaml
    1.20 -  Char_nat List
    1.21 +  Char_nat String
    1.22  
    1.23  code_modulename Haskell
    1.24 -  Char_nat List
    1.25 +  Char_nat String
    1.26  
    1.27  end
    1.28 \ No newline at end of file

     2.1 --- a/src/HOL/Library/Code_Char.thy	Tue Jun 01 09:12:12 2010 +0200
     2.2 +++ b/src/HOL/Library/Code_Char.thy	Tue Jun 01 11:18:51 2010 +0200
     2.3 @@ -12,9 +12,10 @@
     2.4    (SML "char")
     2.5    (OCaml "char")
     2.6    (Haskell "Char")
     2.7 +  (Scala "Char")
     2.8  
     2.9  setup {*
    2.10 -  fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"] 
    2.11 +  fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] 
    2.12    #> String_Code.add_literal_list_string "Haskell"
    2.13  *}
    2.14  
    2.15 @@ -27,10 +28,14 @@
    2.16  code_reserved OCaml
    2.17    char
    2.18  
    2.19 +code_reserved Scala
    2.20 +  char
    2.21 +
    2.22  code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    2.23    (SML "!((_ : char) = _)")
    2.24    (OCaml "!((_ : char) = _)")
    2.25    (Haskell infixl 4 "==")
    2.26 +  (Scala infixl 5 "==")
    2.27  
    2.28  code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
    2.29    (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
    2.30 @@ -53,10 +58,12 @@
    2.31    (SML "String.implode")
    2.32    (OCaml "failwith/ \"implode\"")
    2.33    (Haskell "_")
    2.34 +  (Scala "List.toString((_))")
    2.35  
    2.36  code_const explode
    2.37    (SML "String.explode")
    2.38    (OCaml "failwith/ \"explode\"")
    2.39    (Haskell "_")
    2.40 +  (Scala "List.fromString((_))")
    2.41  
    2.42  end

     3.1 --- a/src/HOL/Library/Code_Char_chr.thy	Tue Jun 01 09:12:12 2010 +0200
     3.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Tue Jun 01 11:18:51 2010 +0200
     3.3 @@ -22,23 +22,10 @@
     3.4    "char_of_nat = char_of_int o int"
     3.5    unfolding char_of_int_def by (simp add: expand_fun_eq)
     3.6  
     3.7 -lemmas [code del] = char.recs char.cases char.size
     3.8 -
     3.9 -lemma [code, code_unfold]:
    3.10 -  "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
    3.11 -  by (cases c) (auto simp add: nibble_pair_of_nat_char)
    3.12 -
    3.13 -lemma [code, code_unfold]:
    3.14 -  "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
    3.15 -  by (cases c) (auto simp add: nibble_pair_of_nat_char)
    3.16 -
    3.17 -lemma [code]:
    3.18 -  "size (c\<Colon>char) = 0"
    3.19 -  by (cases c) auto
    3.20 -
    3.21  code_const int_of_char and char_of_int
    3.22    (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
    3.23    (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
    3.24 -  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
    3.25 +  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | (0 <= k && k < 256) = toEnum k :: Char in chr . fromInteger)")
    3.26 +  (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
    3.27  
    3.28 -end
    3.29 \ No newline at end of file
    3.30 +end

     4.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 01 09:12:12 2010 +0200
     4.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 01 11:18:51 2010 +0200
     4.3 @@ -317,7 +317,7 @@
     4.4      else error("Int value too big:" + this.value.toString)
     4.5  
     4.6    def +(that: Nat): Nat = new Nat(this.value + that.value)
     4.7 -  def -(that: Nat): Nat = Nat(this.value + that.value)
     4.8 +  def -(that: Nat): Nat = Nat(this.value - that.value)
     4.9    def *(that: Nat): Nat = new Nat(this.value * that.value)
    4.10  
    4.11    def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)

     5.1 --- a/src/Tools/Code/code_scala.ML	Tue Jun 01 09:12:12 2010 +0200
     5.2 +++ b/src/Tools/Code/code_scala.ML	Tue Jun 01 11:18:51 2010 +0200
     5.3 @@ -400,10 +400,11 @@
     5.4    end;
     5.5  
     5.6  val literals = let
     5.7 -  fun char_scala c =
     5.8 -    let
     5.9 -      val s = ML_Syntax.print_char c;
    5.10 -    in if s = "'" then "\\'" else s end;
    5.11 +  fun char_scala c = if c = "'" then "\\'"
    5.12 +    else if c = "\"" then "\\\""
    5.13 +    else if c = "\\" then "\\\\"
    5.14 +    else let val k = ord c
    5.15 +    in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
    5.16    fun numeral_scala k = if k < 0
    5.17      then if k <= 2147483647 then "- " ^ string_of_int (~ k)
    5.18        else quote ("- " ^ string_of_int (~ k))