diff --git a/collects/profj/check.ss b/collects/profj/check.ss
index 75e1e9e09b..0def6c1af0 100644
--- a/collects/profj/check.ss
+++ b/collects/profj/check.ss
@@ -161,6 +161,22 @@
                       (environment-labels base-env)
                       (environment-local-inners base-env)))
   
+  (define (remove-set-vars to-remove sets)
+    (cond
+      ((null? sets) sets)
+      ((member (car sets) to-remove) (remove-set-vars to-remove (cdr sets)))
+      (else (cons (car sets) (remove-set-vars to-remove (cdr sets))))))
+  
+  (define (unnest-var base-env context+)
+    (let ((adds 
+           (map var-type-var
+                (srfi:lset-difference equal? (environment-types context+) (environment-types base-env)))))
+    (make-environment (environment-types base-env)
+                      (remove-set-vars adds (environment-set-vars context+))
+                      (environment-exns base-env)
+                      (environment-labels base-env)
+                      (environment-local-inners base-env))))
+  
   ;;add-exn-to-env: type env -> env
   (define (add-exn-to-env exn env)
     (make-environment (environment-types env)
@@ -1063,7 +1079,8 @@
   ;check-while: type/env  src -> void
   (define (check-while cond/env src check-s loop-body)
     ((check-cond 'while) (type/env-t cond/env) src)
-    (check-s loop-body (type/env-e cond/env) #t #f))
+    (check-s loop-body (type/env-e cond/env) #t #f)
+    (make-type/env 'void cond/env))
         
   ;check-do: (exp env -> type/env) exp src type/env -> type/env
   (define (check-do check-e exp src loop/env)
@@ -1079,12 +1096,13 @@
                           (check-for-exps init env check-e)))
            (cond/env (check-e cond inits-env)))
       ((check-cond 'for) (type/env-t cond/env) (expr-src cond))
-      (check-s loop (check-for-exps incr inits-env check-e) #t in-switch?)))
+      (check-s loop (check-for-exps incr inits-env check-e) #t in-switch?))
+    (make-type/env 'void env))
 
   ;check-for-vars: (list field) env (expression env -> type/env) symbol (list string) type-records -> env
   (define (check-for-vars vars env check-e level c-class types)
     (or (and (null? vars) env)
-        (check-for-vars (cdr vars) 
+        (check-for-vars (cdr vars)
                         (check-local-var (car vars) env check-e level c-class types) 
                         check-e level c-class types)))
   
@@ -1139,8 +1157,8 @@
                         (check-s (catch-body catch)
                                  (add-var-to-env name (field-type-spec field) parm env)))))
                 catches)
-      (when finally (check-s finally env)
-        body-res)))
+      (when finally (check-s finally env))
+      (make-type/env 'void (unnest-var (type/env-e body-res)))))
 
   ;INCORRECT!!! This doesn't properly type check and I'm just raising an error for now
   ;Skipping proper checks of the statements + proper checking that constants aren't repeated
@@ -1164,7 +1182,7 @@
   (define (check-block stmts env check-s check-e level c-class type-recs)
     (let loop ((stmts stmts) (block-env env))
       (cond 
-        ((null? stmts) (make-type/env 'void block-env))
+        ((null? stmts) (make-type/env 'void (unnest-var env block-env)))
         ((field? (car stmts))
          (loop (cdr stmts) 
                (check-local-var (car stmts) block-env check-e level c-class type-recs)))
diff --git a/collects/profj/tool.ss b/collects/profj/tool.ss
index 59096ff309..e94f108567 100644
--- a/collects/profj/tool.ss
+++ b/collects/profj/tool.ss
@@ -875,8 +875,8 @@
       ((boolean? value) (list (if value "true" "false")))
       ((is-java-array? value)
        (if full-print?
-           (array->string value (send value length) -1 #t style already-printed newline? num-tabs)
-           (array->string value 3 (- (send value length) 3) #f style already-printed newline? num-tabs)))
+           (format-array->list value (send value length) -1 #t style already-printed newline? num-tabs)
+           (format-array->list value 3 (- (send value length) 3) #f style already-printed newline? num-tabs)))
       ((is-a? value String) (list (format "~v" (send value get-mzscheme-string))))
       ((string? value) (list (format "~v" value)))
       ((or (is-a? value ObjectI) (supports-printable-interface? value))
@@ -922,6 +922,27 @@
             (else (list (send value my-name)))))))
           (else (list value))))
 
+  ;format-array->list: java-value int int bool symbol (list value) -> (list val)
+  (define (format-array->list value stop restart full-print? style already-printed nl? nt)
+    (letrec ((len (send value length))
+             (make-partial-string
+              (lambda (idx first-test second-test)
+                (cond
+                  ((first-test idx) "")
+                  ((second-test idx)
+                   (string-append (format-java (send value access idx) full-print? style already-printed nl? nt)
+                                  (make-partial-string (add1 idx) first-test second-test)))
+                  (else
+                   (string-append (format-java (send value access idx) full-print? style already-printed nl? nt)
+                                  " "
+                                  (make-partial-string (add1 idx) first-test second-test)))))))
+      (if (or full-print? (< restart stop))
+          (list (format "[~a]" (make-partial-string 0 (lambda (i) (>= i len)) (lambda (i) (= i (sub1 len))))))
+          (list (format "[~a~a~a]"                      
+                  (make-partial-string 0 (lambda (i) (or (>= i stop) (>= i len))) (lambda (i) (= i (sub1 stop))))
+                  " ... "
+                  (make-partial-string restart (lambda (i) (>= i len)) (lambda (i) (= i (sub1 len)))))))))
+  
   
   ;array->string: java-value int int bool symbol (list value) -> string
   (define (array->string value stop restart full-print? style already-printed nl? nt)