1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Fri Jul 16 14:11:08 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jul 16 15:28:22 2010 +0200
     1.3 @@ -345,7 +345,7 @@
     1.4    "new n x = make n (\<lambda>_. x)"
     1.5    by (rule Heap_eqI) (simp add: map_replicate_trivial execute_simps)
     1.6  
     1.7 -lemma array_of_list_make:
     1.8 +lemma array_of_list_make [code]:
     1.9    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
    1.10    by (rule Heap_eqI) (simp add: map_nth execute_simps)
    1.11  
    1.12 @@ -482,11 +482,10 @@
    1.13  
    1.14  text {* Scala *}
    1.15  
    1.16 -code_type array (Scala "!Array[_]")
    1.17 +code_type array (Scala "!collection.mutable.ArraySeq[_]")
    1.18  code_const Array (Scala "!error(\"bare Array\")")
    1.19 -code_const Array.new' (Scala "('_: Unit)/ => / Array.fill((_))((_))")
    1.20 -code_const Array.of_list (Scala "('_: Unit)/ =>/ _.toArray")
    1.21 -code_const Array.make' (Scala "('_: Unit)/ =>/ Array.tabulate((_),/ (_))")
    1.22 +code_const Array.new' (Scala "('_: Unit)/ => / collection.mutable.ArraySeq.fill((_))((_))")
    1.23 +code_const Array.make' (Scala "('_: Unit)/ =>/ collection.mutable.ArraySeq.tabulate((_))((_))")
    1.24  code_const Array.len' (Scala "('_: Unit)/ =>/ _.length")
    1.25  code_const Array.nth' (Scala "('_: Unit)/ =>/ _((_))")
    1.26  code_const Array.upd' (Scala "('_: Unit)/ =>/ _.update((_),/ (_))")

     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 14:11:08 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 15:28:22 2010 +0200
     2.3 @@ -489,7 +489,7 @@
     2.4  code_type Heap (Scala "Unit/ =>/ _")
     2.5  code_const bind (Scala "!Heap.bind((_), (_))")
     2.6  code_const return (Scala "('_: Unit)/ =>/ _")
     2.7 -code_const Heap_Monad.raise' (Scala "!error(_)")
     2.8 +code_const Heap_Monad.raise' (Scala "!error((_))")
     2.9  
    2.10  
    2.11  subsubsection {* Target variants with less units *}

     3.1 --- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Fri Jul 16 14:11:08 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Fri Jul 16 15:28:22 2010 +0200
     3.3 @@ -14,6 +14,6 @@
     3.4    Array.upd, Array.map_entry, Array.swap, Array.freeze,
     3.5    ref, Ref.lookup, Ref.update, Ref.change)"
     3.6  
     3.7 -export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell?
     3.8 +export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
     3.9  
    3.10  end

     4.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 16 14:11:08 2010 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 16 15:28:22 2010 +0200
     4.3 @@ -303,3 +303,4 @@
     4.4  code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.update((_), (_))")
     4.5  
     4.6  end
     4.7 +

     5.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jul 16 14:11:08 2010 +0200
     5.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jul 16 15:28:22 2010 +0200
     5.3 @@ -655,6 +655,6 @@
     5.4  
     5.5  ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
     5.6  
     5.7 -export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell?
     5.8 +export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
     5.9  
    5.10 -end
    5.11 \ No newline at end of file
    5.12 +end

     6.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Jul 16 14:11:08 2010 +0200
     6.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Jul 16 15:28:22 2010 +0200
     6.3 @@ -110,6 +110,6 @@
     6.4        subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
     6.5    (drule sym[of "List.length (Array.get h a)"], simp)
     6.6  
     6.7 -export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell?
     6.8 +export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
     6.9  
    6.10  end