# HG changeset patch
# User haftmann
# Date 1280390230 -7200
# Node ID a9b52497661caf90455271655a7b4995e690235d
# Parent  6f89490e8eea9074440e7a9471c83b4bfd810239# Parent  72f4630d4c43905ed8416f250dbe2152719cef77
merged

diff -r 6f89490e8eea -r a9b52497661c src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jul 29 08:16:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jul 29 09:57:10 2010 +0200
@@ -521,11 +521,10 @@
     val is_bind = is_const @{const_name bind};
     val is_return = is_const @{const_name return};
     val dummy_name = "";
-    val dummy_type = ITyVar dummy_name;
     val dummy_case_term = IVar NONE;
     (*assumption: dummy values are not relevant for serialization*)
-    val unitt = case lookup_const naming @{const_name Unity}
-     of SOME unit' => IConst (unit', (([], []), []))
+    val (unitt, unitT) = case lookup_const naming @{const_name Unity}
+     of SOME unit' => (IConst (unit', (([], []), [])), the (lookup_tyco naming @{type_name unit}) `%% [])
       | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
     fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
       | dest_abs (t, ty) =
@@ -546,7 +545,7 @@
               then tr_bind' [(x1, ty1), (x2, ty2)]
               else force t
           | _ => force t;
-    fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `|=> ICase (((IVar (SOME dummy_name), dummy_type),
+    fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
       [(unitt, tr_bind' ts)]), dummy_case_term)
     and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys)
        of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
diff -r 6f89490e8eea -r a9b52497661c src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Thu Jul 29 08:16:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Thu Jul 29 09:57:10 2010 +0200
@@ -14,6 +14,6 @@
   Array.upd, Array.map_entry, Array.swap, Array.freeze,
   ref, Ref.lookup, Ref.update, Ref.change)"
 
-export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
 
 end
diff -r 6f89490e8eea -r a9b52497661c src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Jul 29 08:16:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Jul 29 09:57:10 2010 +0200
@@ -655,6 +655,6 @@
 
 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
 
-export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
 
 end
diff -r 6f89490e8eea -r a9b52497661c src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Thu Jul 29 08:16:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Thu Jul 29 09:57:10 2010 +0200
@@ -110,6 +110,8 @@
       subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
   (drule sym[of "List.length (Array.get h a)"], simp)
 
-export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+definition "example = (Array.of_list [1::nat, 2, 3, 4, 5, 6, 7, 8, 9, 10] \<guillemotright>= (\<lambda>a. rev a 0 9))"
+
+export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
 
 end
diff -r 6f89490e8eea -r a9b52497661c src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Jul 29 08:16:49 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Jul 29 09:57:10 2010 +0200
@@ -1014,6 +1014,6 @@
 ML {* @{code test_2} () *}
 ML {* @{code test_3} () *}
 
-export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
+export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? (*Scala_imp?*)
 
 end
diff -r 6f89490e8eea -r a9b52497661c src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Jul 29 08:16:49 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Jul 29 09:57:10 2010 +0200
@@ -79,24 +79,24 @@
         val arg_typs' = if is_pat orelse
           (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
         val (l, print') = case syntax_const c
-         of NONE => (args_num c, fn ts => applify "(" ")"
+         of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
                   NOBR ((str o deresolve) c) arg_typs') ts)
-          | SOME (Plain_const_syntax (k, s)) => (k, fn ts => applify "(" ")"
+          | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
                   NOBR (str s) arg_typs') ts)
           | SOME (Complex_const_syntax (k, print)) =>
-              (k, fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
+              (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
                 (ts ~~ take k function_typs))
-      in if k = l then print' ts
+      in if k = l then print' fxy ts
       else if k < l then
         print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
       else let
         val (ts1, ts23) = chop l ts;
       in
-        Pretty.block (print' ts1 :: map (fn t => Pretty.block
+        Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
           [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
       end end
     and print_bind tyvars some_thm fxy p =
@@ -104,17 +104,19 @@
     and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
-            fun print_match ((pat, ty), t) vars =
-              vars
-              |> print_bind tyvars some_thm BR pat
-              |>> (fn p => concat [str "val", constraint p (print_typ tyvars NOBR ty),
-                  str "=", print_term tyvars false some_thm vars NOBR t])
-            val (all_ps, vars') = fold_map print_match binds vars;
-            val (ps, p) = split_last all_ps;
-          in brackify_block fxy
-            (str "{")
-            (ps @ Pretty.block [p, str ";"] @@ print_term tyvars false some_thm vars' NOBR body)
-            (str "}")
+            fun print_match ((IVar NONE, _), t) vars =
+                  ((true, print_term tyvars false some_thm vars NOBR t), vars)
+              | print_match ((pat, ty), t) vars =
+                  vars
+                  |> print_bind tyvars some_thm BR pat
+                  |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty),
+                      str "=", print_term tyvars false some_thm vars NOBR t]))
+            val (seps_ps, vars') = fold_map print_match binds vars;
+            val all_seps_ps = seps_ps @ [(true, print_term tyvars false some_thm vars' NOBR body)];
+            fun insert_seps [(_, p)] = [p]
+              | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
+                  (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
+          in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}")
           end
       | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
           let