1.1 --- a/src/Tools/Code/code_scala.ML	Thu Jul 29 09:56:59 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jul 29 09:57:00 2010 +0200
     1.3 @@ -79,24 +79,24 @@
     1.4          val arg_typs' = if is_pat orelse
     1.5            (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
     1.6          val (l, print') = case syntax_const c
     1.7 -         of NONE => (args_num c, fn ts => applify "(" ")"
     1.8 +         of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
     1.9                (print_term tyvars is_pat some_thm vars NOBR) fxy
    1.10                  (applify "[" "]" (print_typ tyvars NOBR)
    1.11                    NOBR ((str o deresolve) c) arg_typs') ts)
    1.12 -          | SOME (Plain_const_syntax (k, s)) => (k, fn ts => applify "(" ")"
    1.13 +          | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
    1.14                (print_term tyvars is_pat some_thm vars NOBR) fxy
    1.15                  (applify "[" "]" (print_typ tyvars NOBR)
    1.16                    NOBR (str s) arg_typs') ts)
    1.17            | SOME (Complex_const_syntax (k, print)) =>
    1.18 -              (k, fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
    1.19 +              (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
    1.20                  (ts ~~ take k function_typs))
    1.21 -      in if k = l then print' ts
    1.22 +      in if k = l then print' fxy ts
    1.23        else if k < l then
    1.24          print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
    1.25        else let
    1.26          val (ts1, ts23) = chop l ts;
    1.27        in
    1.28 -        Pretty.block (print' ts1 :: map (fn t => Pretty.block
    1.29 +        Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
    1.30            [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
    1.31        end end
    1.32      and print_bind tyvars some_thm fxy p =
    1.33 @@ -104,17 +104,19 @@
    1.34      and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
    1.35            let
    1.36              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    1.37 -            fun print_match ((pat, ty), t) vars =
    1.38 -              vars
    1.39 -              |> print_bind tyvars some_thm BR pat
    1.40 -              |>> (fn p => concat [str "val", constraint p (print_typ tyvars NOBR ty),
    1.41 -                  str "=", print_term tyvars false some_thm vars NOBR t])
    1.42 -            val (all_ps, vars') = fold_map print_match binds vars;
    1.43 -            val (ps, p) = split_last all_ps;
    1.44 -          in brackify_block fxy
    1.45 -            (str "{")
    1.46 -            (ps @ Pretty.block [p, str ";"] @@ print_term tyvars false some_thm vars' NOBR body)
    1.47 -            (str "}")
    1.48 +            fun print_match ((IVar NONE, _), t) vars =
    1.49 +                  ((true, print_term tyvars false some_thm vars NOBR t), vars)
    1.50 +              | print_match ((pat, ty), t) vars =
    1.51 +                  vars
    1.52 +                  |> print_bind tyvars some_thm BR pat
    1.53 +                  |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty),
    1.54 +                      str "=", print_term tyvars false some_thm vars NOBR t]))
    1.55 +            val (seps_ps, vars') = fold_map print_match binds vars;
    1.56 +            val all_seps_ps = seps_ps @ [(true, print_term tyvars false some_thm vars' NOBR body)];
    1.57 +            fun insert_seps [(_, p)] = [p]
    1.58 +              | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
    1.59 +                  (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
    1.60 +          in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}")
    1.61            end
    1.62        | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
    1.63            let