diff --git a/collects/macro-debugger/model/debug.ss b/collects/macro-debugger/model/debug.ss
new file mode 100644
index 0000000000..1426e5d314
--- /dev/null
+++ b/collects/macro-debugger/model/debug.ss
@@ -0,0 +1,104 @@
+
+(module debug mzscheme
+  (require (lib "plt-match.ss"))
+  (require "trace.ss"
+           "deriv-util.ss"
+           "hiding-policies.ss"
+           "deriv.ss")
+
+  (provide (all-from "trace.ss")
+           (all-from "deriv.ss")
+           (all-from "deriv-util.ss")
+           (all-from "hiding-policies.ss")
+           (all-from (lib "plt-match.ss"))
+           find-deriv)
+
+  (define (find-deriv pred d)
+    (define (loop d)
+      (match d
+        [(? pred d) (list d)]
+        [(AnyQ mrule (_ _ tx next))
+         (append (loop tx) (loop next))]
+        [(AnyQ lift-deriv (_ _ first lift second))
+         (append (loop first) (loop lift) (loop second))]
+        [(AnyQ transformation (_ _ _ _ _ locals))
+         (loops locals)]
+        [(struct local-expansion (_ _ _ _ deriv))
+         (loop deriv)]
+        [(struct local-bind (deriv))
+         (loop deriv)]
+        [(AnyQ p:define-syntaxes (_ _ _ rhs))
+         (loop rhs)]
+        [(AnyQ p:define-values (_ _ _ rhs))
+         (loop rhs)]
+        [(AnyQ p:if (_ _ _ _ test then else))
+         (append (loop test) (loop then) (loop else))]
+        [(AnyQ p:wcm (_ _ _ key value body))
+         (append (loop key) (loop value) (loop body))]
+        [(AnyQ p:set! (_ _ _ _ rhs))
+         (loop rhs)]
+        [(AnyQ p:set!-macro (_ _ _ deriv))
+         (loop deriv)]
+        [(AnyQ p:begin (_ _ _ lderiv))
+         (loop lderiv)]
+        [(AnyQ p:begin0 (_ _ _ first lderiv))
+         (append (loop first) (loop lderiv))]
+        [(AnyQ p:#%app (_ _ _ _ lderiv))
+         (loop lderiv)]
+        [(AnyQ p:lambda (_ _ _ _ body))
+         (loop body)]
+        [(AnyQ p:case-lambda (_ _ _ rbs))
+         (apply append (map loop (map cdr (or rbs null))))]
+        [(AnyQ p:let-values (_ _ _ _ rhss body))
+         (append (loops rhss) (loop body))]
+        [(AnyQ p:let*-values (_ _ _ inner))
+         (loop inner)]
+        [(AnyQ p:letrec-values (_ _ _ _ rhss body))
+         (append (loops rhss) (loop body))]
+        [(AnyQ p:letrec-syntaxes+values (_ _ _ _ srhss _ vrhss body))
+         (append (loops srhss) (loops vrhss) (loop body))]
+        [(AnyQ p:module (_ _ _ body))
+         (loop body)]
+        [(AnyQ p:#%module-begin (_ _ _ pass1 pass2))
+         (append (loops pass1) (loops pass2))]
+        [(AnyQ p:rename (_ _ _ _ inner))
+         (loop inner)]
+        [(AnyQ p:synth (_ _ _ subterms))
+         (loops (map s:subterm-deriv subterms))]
+
+        [(AnyQ lderiv (_ _ derivs))
+         (loops derivs)]
+        [(AnyQ bderiv (_ _ pass1 _ pass2))
+         (append (loops pass1) (loop pass2))]
+        [(AnyQ b:defvals (_ head))
+         (loop head)]
+        [(AnyQ b:defstx (_ deriv rhs))
+         (append (loop deriv) (loop rhs))]
+        [(AnyQ b:splice (_ head _))
+         (loop head)]
+        [(AnyQ b:expr (_ head))
+         (loop head)]
+        [(AnyQ b:begin (_ head inner))
+         (append (loop head) (loop inner))]
+        [(AnyQ mod:cons (head))
+         (loop head)]
+        [(AnyQ mod:prim (head prim))
+         (append (loop head) (loop prim))]
+        [(AnyQ mod:splice (head _))
+         (loop head)]
+        [(AnyQ mod:lift (head tail))
+         (append (loop head) (loop tail))]
+        [(AnyQ mod:lift-end (tail))
+         (loop tail)]
+        [(AnyQ mod:begin (head inner))
+         (append (loop head) (loop inner))]
+
+        [else null]))
+
+    (define (loops ds)
+      (if (list? ds)
+          (apply append (map loop ds))
+          null))
+
+    (loop d))
+  )
diff --git a/collects/macro-debugger/model/deriv-c.ss b/collects/macro-debugger/model/deriv-c.ss
index 0cfec4a0f9..bca3848373 100644
--- a/collects/macro-debugger/model/deriv-c.ss
+++ b/collects/macro-debugger/model/deriv-c.ss
@@ -23,6 +23,7 @@
   (define-struct local-expansion (e1 e2 me1 me2 deriv) #f)
   (define-struct local-lift (expr id) #f)
   (define-struct local-lift-end (decl) #f)
+  (define-struct local-bind (deriv) #f)
   
   ;; A PRule is one of ...
   (define-struct (prule deriv) (resolves) #f)
@@ -107,7 +108,7 @@
   ;; A BlockRename is (cons syntax syntax)
   ;; It always applies only to the current block element
 
-  (define-struct brule (renames))
+  (define-struct brule (renames) #f)
   (define-struct (b:defvals brule) (head) #f)
   (define-struct (b:defstx brule) (deriv rhs) #f)
   (define-struct (b:splice brule) (head tail) #f)
@@ -136,7 +137,7 @@
   ;;   - (make-mod:cons Derivation)
   ;;   - (make-mod:lift Derivation syntaxes)
 
-  (define-struct modrule ())
+  (define-struct modrule () #f)
   (define-struct (mod:cons modrule) (head) #f)
   (define-struct (mod:prim modrule) (head prim) #f)
   (define-struct (mod:skip modrule) () #f)
diff --git a/collects/macro-debugger/model/deriv-parser.ss b/collects/macro-debugger/model/deriv-parser.ss
index 6cc9ed9880..efd14066ad 100644
--- a/collects/macro-debugger/model/deriv-parser.ss
+++ b/collects/macro-debugger/model/deriv-parser.ss
@@ -125,13 +125,16 @@
        [((? LocalAction) (? LocalActions)) (cons $1 $2)])
 
       (LocalAction
+       (#:no-wrap)
        [(enter-local local-pre (? EE) local-post exit-local)
         (make-local-expansion $1 $5 $2 $4 $3)]
        [(lift)
         (make-local-lift (car $1) (cdr $1))]
        [(lift-statement)
-        (make-local-lift-end $1)])
-      
+        (make-local-lift-end $1)]
+       [(phase-up (? EE/Lifts))
+        (make-local-bind $2)])
+
       ;; Multiple calls to local-expand
       ;; EEs Answer = (listof Derivation)
       (EEs
@@ -236,7 +239,7 @@
       (ModulePass1/Prim
        [(enter-prim prim-define-values ! exit-prim)
         (make-p:define-values $1 $4 null #f)]
-       [(enter-prim prim-define-syntaxes ! phase-up (? EE) exit-prim)
+       [(enter-prim prim-define-syntaxes ! phase-up (? EE/Lifts) exit-prim)
         (make-p:define-syntaxes $1 $6 null $5)]
        [(enter-prim prim-require ! exit-prim)
         (make-p:require $1 $4 null)]
diff --git a/collects/macro-debugger/model/deriv.ss b/collects/macro-debugger/model/deriv.ss
index e6539b46ba..f3e8305ff5 100644
--- a/collects/macro-debugger/model/deriv.ss
+++ b/collects/macro-debugger/model/deriv.ss
@@ -6,11 +6,10 @@
 
   ;; NO CONTRACTS
   
-;  (provide (all-from "deriv-c.ss"))
-
-
+  (provide (all-from "deriv-c.ss"))
   ;; CONTRACTS
 
+#;  (begin
   (define (stx-list-like? x)
     (or (syntax? x)
         (null? x)
@@ -58,11 +57,17 @@
             [resolves resolves/c]
             [me1 syntax?]
             [me2 syntax/f]
-            [locals (listof (or/c local-expansion? local-lift? local-lift-end?))]))
+            [locals (listof (or/c local-expansion? local-lift? local-lift-end? local-bind?))]))
    (struct (prule deriv)
            ([e1 syntax?]
             [e2 syntax/f]
             [resolves resolves/c]))
+   (struct (p:#%app prule)
+           ([e1 syntax?]
+            [e2 syntax/f]
+            [resolves resolves/c]
+            [tagged-stx syntax?]
+            [lderiv (anyq (maybe lderiv?))]))
 
    (struct lderiv
            ([es1 syntaxes/c]
@@ -87,6 +92,7 @@
            (struct local-expansion (e1 e2 me1 me2 deriv))
            (struct local-lift (expr id))
            (struct local-lift-end (decl))
+           (struct local-bind (deriv))
 
            ;(struct prule (resolves))
            (struct p:variable ())
@@ -98,7 +104,7 @@
            (struct p:set!-macro (deriv))
            (struct p:begin (lderiv))
            (struct p:begin0 (first lderiv))
-           (struct p:#%app (tagged-stx lderiv))
+           ;(struct p:#%app (tagged-stx lderiv))
            (struct p:lambda (renames body))
            (struct p:case-lambda (renames+bodies))
            (struct p:let-values (renames body))
@@ -307,5 +313,5 @@
   #;
   (define (wf-exn-deriv? x)
     #f)
-  
+  )
   )
diff --git a/collects/macro-debugger/model/hide.ss b/collects/macro-debugger/model/hide.ss
index 8f35028b18..a16ea15bd8 100644
--- a/collects/macro-debugger/model/hide.ss
+++ b/collects/macro-debugger/model/hide.ss
@@ -20,6 +20,19 @@
     (parameterize ((macro-policy show-macro?))
       (hide deriv)))
 
+  ;; current-hiding-warning-handler : (parameter-of (symbol string -> void))
+  (define current-hiding-warning-handler
+    (make-parameter
+     (lambda (tag message) (printf "~a: ~a~n" tag message))))
+
+  (define (warn tag message) ((current-hiding-warning-handler) tag message))
+
+  ;; machinery for reporting things that macro hiding can't handle
+  (define-struct nonlinearity (message paths))
+  (define-struct localactions ())
+
+
+
 ;   +@   ++           -                    
 ;   *@+  ++           @-                   
 ;   *@@  ++  -+@+-  -+@+++   -+@+-   -+@@+ 
@@ -90,7 +103,7 @@
         [(AnyQ p:variable (e1 e2 rs))
          (values d e2)]
         [(AnyQ p:module (e1 e2 rs body))
-         (>>Prim d #t (make-p:module body)
+         (>>Prim d e1 #t (make-p:module body)
                  (module name lang . _BODY)
                  (module name lang BODY)
                  ([for-deriv BODY body]))]
@@ -148,22 +161,25 @@
               ([for-deriv FIRST first]
                [for-lderiv LDERIV lderiv]))]
         [(AnyQ p:#%app (e1 e2 rs tagged-stx ld))
-         (>>P d (make-p:#%app tagged-stx ld)
-              (#%app . LDERIV)
-              ([for-lderiv LDERIV ld])
-              #:with2
-              (lambda (pr* stx*)
-                (if (or (eq? tagged-stx e1) (show-macro? #'#%app))
-                    (values pr* stx*)
+         (if (or (eq? e1 tagged-stx) (show-macro? #'#%app))
+             ;; If explicitly tagged, simple
+             (>>Prim d tagged-stx #t (make-p:#%app tagged-stx ld)
+                  (#%app . LDERIV) (#%app . LDERIV)
+                  ([for-lderiv LDERIV ld]))
+             ;; If implicitly tagged:
+             (>>P d (make-p:#%app tagged-stx ld)
+                  LDERIV
+                  ([for-lderiv LDERIV ld])
+                  #:with2
+                  (lambda (pr* stx*)
                     (match pr*
                       [(struct p:#%app (_ _ rs tagged-stx (IntQ lderiv (es1 es2 derivs*))))
-                       (let ([stx* (and stx* (stx-cdr stx*))])
-                         (values (make-p:synth e1 stx* rs
-                                               (map (lambda (n d)
-                                                      (make-s:subterm (list (make-ref n)) d))
-                                                    (iota (length derivs*))
-                                                    derivs*))
-                                 stx*))]
+                       (values (make-p:synth e1 stx* rs
+                                             (map (lambda (n d)
+                                                    (make-s:subterm (list (make-ref n)) d))
+                                                  (iota (length derivs*))
+                                                  derivs*))
+                               stx*)]
                       [(struct p:#%app (_ _ rs tagged-stx (struct error-wrap (exn _ _))))
                        (values (make-error-wrap exn #f (make-p:synth e1 #f rs null))
                                #f)]))))]
@@ -223,13 +239,27 @@
         ;; Macros
 
         [(AnyQ mrule (e1 e2 tx next))
-         (if (show-transformation? tx)
-             ;; FIXME: Not handling local expansions now
-             (recv [(next e2) (for-deriv next)]
-                   (values (rewrap d (make-mrule e1 e2 tx next))
-                           e2))
-             (seek/deriv d))]
-        
+         (let ([show-k
+                (lambda ()
+                  (recv [(next e2) (for-deriv next)]
+                        (values (rewrap d (make-mrule e1 e2 tx next))
+                                e2)))])
+           (if (show-transformation? tx)
+               (show-k)
+               (with-handlers ([nonlinearity?
+                                (lambda (nl)
+                                  (warn 'nonlinearity
+                                        (format "~a: ~s"
+                                                (nonlinearity-message nl)
+                                                (nonlinearity-paths nl)))
+                                  (show-k))]
+                               [localactions?
+                                (lambda (nl)
+                                  (warn 'localactions
+                                        "opaque macro called local-expand or lifted expression")
+                                  (show-k))])
+                 (seek/deriv d))))]
+
         ;; Lift
 
         [($$ lift-deriv (e1 e2 first lifted-stx second))
@@ -442,7 +472,7 @@
         [(AnyQ p:letrec-values (e1 e2 rs renames rhss body))
          (let ([new-table (table-restrict/let e1 renames)])
            (parameterize ((subterms-table new-table))
-             (append (apply append (map for-deriv new-table))
+             (append (apply append (map for-deriv rhss))
                      (for-bderiv body))))]
         [(AnyQ p:letrec-syntaxes+values (e1 e2 rs srenames srhss vrenames vrhss body))
          (let ([new-table (table-restrict/lsv1 e1 srenames)])
@@ -483,13 +513,27 @@
         [(struct transformation (e1 e2 rs me1 me2 locals))
          ;; FIXME: We'll need to use e1/e2/me1/me2 to synth locals, perhaps
          ;; FIXME: and we'll also need to account for *that* marking, too...
+         (unless (null? locals)
+           (raise (make-localactions)))
          (parameterize ((subterms-table (table-restrict/rename e1 me1)))
            (let ([sss (map for-local locals)])
              (values (apply append sss)
                      (table-restrict/rename me2 e2))))]))
 
+    ;; for-local : LocalAction -> (list-of Subterm)
     (define (for-local local)
-      '...)
+      (match local
+        [(IntQ local-expansion (e1 e2 me1 me2 deriv))
+         (parameterize ((subterms-table (table-restrict/rename e1 me1)))
+           (let ([ss (for-deriv deriv)])
+             ;; 
+             '(for-each (lambda (s) (s:subterm-deriv s))
+                        ss)
+             '(table-restrict/rename me2 e2)
+             ss))]
+        ;; Also need to handle local-bind
+        ;; ...
+        [else null]))
 
     ;; for-lderiv : ListDerivation -> (list-of Subterm)
     (define (for-lderiv ld)
@@ -534,18 +578,20 @@
                  (or (> (length null-paths) 1)
                      (pair? tail-paths)
                      (pair? ref-paths)))
-        (error 'check-nonlinear-paths "self path plus others: ~s" paths))
+        (raise (make-nonlinearity "self path plus others" paths)))
       (when (pair? tail-paths)
         (when (> (length tail-paths) 1)
-          (error 'check-nonlinear-paths "multiple tail paths"))
+          (raise (make-nonlinearity "multiple tail paths" paths)))
         (let ([n (tail-n (car (car tail-paths)))])
           (for-each (lambda (p)
                       (when (> (ref-n (car p)) n)
-                        (error 'check-nonlinear-paths "ref path after tail path")))
+                        (raise (make-nonlinearity
+                                "ref path after tail path"
+                                paths))))
                     ref-paths)))
       (let ([ref-path-partitions (partition&cdr-ref-paths ref-paths)])
         (for-each check-nonlinear-paths ref-path-partitions))))
-  
+
   ;; partition&cdr-ref-paths : (list-of Path) -> (list-of (list-of Path))
   (define (partition&cdr-ref-paths paths)
     (let ([t (make-hash-table 'equal)]
diff --git a/collects/macro-debugger/model/hiding-policies.ss b/collects/macro-debugger/model/hiding-policies.ss
index 5529cc99ae..2278379f66 100644
--- a/collects/macro-debugger/model/hiding-policies.ss
+++ b/collects/macro-debugger/model/hiding-policies.ss
@@ -67,28 +67,29 @@
                               opaque-kernel
                               opaque-libs
                               transparent-identifiers))
-       (let ([binding (identifier-binding id)])
-         (if (list? binding)
-             (let-values ([(srcmod srcname nommod nomname _) (apply values binding)])
-               (inline ([opaque-srcmod (hash-table-get opaque-modules srcmod /false)]
-                        [opaque-nommod (hash-table-get opaque-modules nommod /false)]
-                        ;; FIXME
-                        [in-kernel?
-                         (and (symbol? srcmod)
-                              (eq? #\# (string-ref (symbol->string srcmod) 0)))]
-                        [in-lib-module?
-                         (lib-module? srcmod)]
-                        [not-opaque-id
-                         (not (module-identifier-mapping-get opaque-identifiers id /false))]
-                        [transparent-id
-                         (module-identifier-mapping-get transparent-identifiers id /false)])
-                       (or transparent-id
-                           (and (not opaque-srcmod)
-                                (not opaque-nommod)
-                                (not (and in-kernel? opaque-kernel))
-                                (not (and in-lib-module? opaque-libs))
-                                not-opaque-id))))
-             #f))]))
+       (inline ([not-opaque-id
+                 (not (module-identifier-mapping-get opaque-identifiers id /false))]
+                [transparent-id
+                 (module-identifier-mapping-get transparent-identifiers id /false)])
+         (let ([binding (identifier-binding id)])
+           (if (list? binding)
+               (let-values ([(srcmod srcname nommod nomname _) (apply values binding)])
+                 (inline ([opaque-srcmod (hash-table-get opaque-modules srcmod /false)]
+                          [opaque-nommod (hash-table-get opaque-modules nommod /false)]
+                          ;; FIXME
+                          [in-kernel?
+                           (and (symbol? srcmod)
+                                (eq? #\# (string-ref (symbol->string srcmod) 0)))]
+                          [in-lib-module?
+                           (lib-module? srcmod)])
+                   (or transparent-id
+                       (and (not opaque-srcmod)
+                            (not opaque-nommod)
+                            (not (and in-kernel? opaque-kernel))
+                            (not (and in-lib-module? opaque-libs))
+                            not-opaque-id))))
+               (or transparent-id
+                   not-opaque-id))))]))
 
   (define (lib-module? mpi)
     (and (module-path-index? mpi)
diff --git a/collects/macro-debugger/model/reductions-engine.ss b/collects/macro-debugger/model/reductions-engine.ss
index 18aa2666c5..9ae287b12c 100644
--- a/collects/macro-debugger/model/reductions-engine.ss
+++ b/collects/macro-debugger/model/reductions-engine.ss
@@ -1,19 +1,10 @@
 
 (module reductions-engine mzscheme
   (require "deriv.ss"
-           "stx-util.ss")
-  (provide (all-defined))
-  
-  ;; A ReductionSequence is a (list-of Reduction)
-  
-  ;; A Reduction is one of 
-  ;;   - (make-step Syntaxes Syntaxes Syntax Syntax BigContext)
-  ;;   - (make-misstep Syntax Syntax Exception)
-  (define-struct step (redex contractum e1 e2 note lctx) #f)
-  ;(define-struct lift-step (expr id note lctxt) #t)
-  (define-struct misstep (redex e1 exn) #f)
-  
-  ;; -------------------------
+           "stx-util.ss"
+           "steps.ss")
+  (provide (all-defined)
+           (all-from "steps.ss"))
   
   ;; A Context is (syntax -> syntax)
   ;; A BigContext is (list-of (cons Syntaxes Syntax))
@@ -84,6 +75,14 @@
                          (values form2 foci1 foci2 description))])
            (cons (walk/foci/E foci1-var foci2-var f form2-var description-var)
                  (R** form2-var p . more)))]
+      [(R** f p [#:rename form2 foci1 foci2 description] . more)
+       #'(let-values ([(form2-var foci1-var foci2-var description-var)
+                       (with-syntax ([p f])
+                         (values form2 foci1 foci2 description))])
+           (cons (walk-rename/foci/E foci1-var foci2-var
+                                     f form2-var
+                                     description-var)
+                 (R** form2-var p . more)))]
       [(R** f p [#:walk form2 description] . more)
        #'(let-values ([(form2-var description-var)
                        (with-syntax ([p f])
@@ -129,7 +128,8 @@
       ;; Implementation for (hole ...) sequences
       [(R** form-var pattern
             [f0 get-e1 get-e2 (hole0 :::) fill0s] . more)
-       (module-identifier=? #'::: (quote-syntax ...))
+       (and (identifier? #':::)
+            (module-identifier=? #'::: (quote-syntax ...)))
        #'(let ([ctx0 (CC (hole0 :::) form-var pattern)])
            (let ([e1s (with-syntax ([pattern form-var]) (syntax->list #'(hole0 :::)))])
              (let loop ([fills fill0s] [prefix null] [suffix e1s])
@@ -173,15 +173,19 @@
   (define walk
     (case-lambda
       [(e1 e2) (walk e1 e2 #f)]
-      [(e1 e2 note) (make-step e1 e2 (E e1) (E e2) note (big-context))]))
+      [(e1 e2 note) (make-rewrite-step e1 e2 (E e1) (E e2) note (big-context))]))
   
   ;; walk/foci/E : syntax(s) syntax(s) syntax syntax string -> Reduction
   (define (walk/foci/E focus1 focus2 e1 e2 note)
     (walk/foci focus1 focus2 (E e1) (E e2) note))
-  
+
+  ;; walk-rename/foci/E : syntax(s) syntax(s) syntax syntax string -> Reduction
+  (define (walk-rename/foci/E focus1 focus2 e1 e2 note)
+    (make-rename-step focus1 focus2 (E e1) (E e2) note (big-context)))
+
   ;; walk/foci : syntax(s) syntax(s) syntax syntax string -> Reduction
   (define (walk/foci focus1 focus2 Ee1 Ee2 note)
-    (make-step focus1 focus2 Ee1 Ee2 note (big-context)))
+    (make-rewrite-step focus1 focus2 Ee1 Ee2 note (big-context)))
 
   ;; stumble : syntax exception -> Reduction
   (define (stumble stx exn)
diff --git a/collects/macro-debugger/model/reductions.ss b/collects/macro-debugger/model/reductions.ss
index aa05de6d75..d47d78dae5 100644
--- a/collects/macro-debugger/model/reductions.ss
+++ b/collects/macro-debugger/model/reductions.ss
@@ -6,9 +6,7 @@
            "context.ss"
            "deriv.ss"
            "reductions-engine.ss")
-  (provide reductions
-           (struct step (redex contractum e1 e2 note lctx))
-           (struct misstep (redex e1 exn)))
+  (provide reductions)
 
   ;; Setup for reduction-engines
 
@@ -106,45 +104,21 @@
           [! exni]
           [#:bind (?formals* . ?body*) renames]
           [#:pattern (?lambda ?formals . ?body)]
-          [#:walk (syntax/skeleton e1 (?lambda ?formals* . ?body*))
-                  #'?formals #'?formals*
-                  "Rename formal parameters"]
-          [Block ?body body])
-       #;
-       (R e1 _1
-          [! exni]
-          => 
-          (lambda (stx)
-            (with-syntax ([(?lambda ?formals . ?body) stx]
-                          [(?formals* . ?body*) renames])
-              (let ([mid (syntax/skeleton e1 (?lambda ?formals* . ?body*))])
-                (append 
-                 (if (stx-pair? #'?formals)
-                     (list (walk/foci/E #'?formals #'?formals* e1 mid
-                                        "Rename formal parameters"))
-                     null)
-                 (R mid (LAMBDA FORMALS . BODY)
-                    [Block BODY body]))))))
-       #;(with-syntax ([(?lambda ?formals . ?body) e1]
-                       [(?formals* . ?body*) renames])
-           (let ([mid (syntax/skeleton e1 (?lambda ?formals* . ?body*))])
-             (append
-              (if (stx-pair? #'?formals)
-                  (list (walk/foci/E #'?formals #'?formals* e1 mid
-                                     "Rename formal parameters"))
-                  null)
-              (R mid (LAMBDA FORMALS . BODY)
-                 [Block BODY body]))))]
+          [#:rename (syntax/skeleton e1 (?lambda ?formals* . ?body*))
+                         #'?formals #'?formals*
+                         "Rename formal parameters"]
+          [Block ?body body])]
       [(struct p:case-lambda (e1 e2 rs renames+bodies))
        #;
        (R e1 _
           [! exni]
           [#:pattern (?case-lambda [?formals . ?body] ...)]
           [#:bind [(?formals* . ?body*) ...] (map car renames+bodies)]
-          [#:walk (syntax/skeleton e1 (?case-lambda [?formals* . ?body*] ...))
-                  (syntax->list #'(?formals ...))
-                  (syntax->list #'(?formals* ...))
-                  "Rename formal parameters"]
+          [#:rename
+           (syntax/skeleton e1 (?case-lambda [?formals* . ?body*] ...))
+           (syntax->list #'(?formals ...))
+           (syntax->list #'(?formals* ...))
+           "Rename formal parameters"]
           [Block (?body ...) (map cdr renames+bodies)])
        (with-syntax ([(?case-lambda [?formals . ?body] ...) e1]
                      [((?formals* . ?body*) ...) (map car renames+bodies)])
@@ -159,88 +133,55 @@
           [! exni]
           [#:pattern (?let-values ([?vars ?rhs] ...) . ?body)]
           [#:bind (([?vars* ?rhs*] ...) . ?body*) renames]
-          [#:walk (syntax/skeleton e1 (?let-values ([?vars* ?rhs*] ...) . ?body*))
-                  (syntax->list #'(?vars ...))
-                  (syntax->list #'(?vars* ...))
-                  "Rename bound variables"]
+          [#:rename
+           (syntax/skeleton e1 (?let-values ([?vars* ?rhs*] ...) . ?body*))
+           (syntax->list #'(?vars ...))
+           (syntax->list #'(?vars* ...))
+           "Rename bound variables"]
           [Expr (?rhs ...) rhss]
-          [Block ?body body])
-       #;
-       (with-syntax ([(?let-values ([?vars ?rhs] ...) . ?body) e1]
-                     [(([?vars* ?rhs*] ...) . ?body*) renames])
-         (let ([mid (syntax/skeleton e1 (?let-values ([?vars* ?rhs*] ...) . ?body*))])
-           (cons (walk/foci/E (syntax->list #'(?vars ...))
-                              (syntax->list #'(?vars* ...))
-                              e1 mid "Rename let-bound variables")
-                 (R mid (LET-VALUES ([VARS RHS] ...) . BODY)
-                    [Expr (RHS ...) rhss]
-                    [Block BODY body]))))]
+          [Block ?body body])]
       [(AnyQ p:letrec-values (e1 e2 rs renames rhss body) exni)
        (R e1 _
           [! exni]
           [#:pattern (?letrec-values ([?vars ?rhs] ...) . ?body)]
           [#:bind (([?vars* ?rhs*] ...) . ?body*) renames]
-          [#:walk (syntax/skeleton e1 (?letrec-values ([?vars* ?rhs*] ...) . ?body*))
-                  (syntax->list #'(?vars ...))
-                  (syntax->list #'(?vars* ...))
-                  "Rename bound variables"]
+          [#:rename
+           (syntax/skeleton e1 (?letrec-values ([?vars* ?rhs*] ...) . ?body*))
+           (syntax->list #'(?vars ...))
+           (syntax->list #'(?vars* ...))
+           "Rename bound variables"]
           [Expr (?rhs ...) rhss]
-          [Block ?body body])
-       #;
-       (with-syntax ([(?letrec-values ([?vars ?rhs] ...) . ?body) e1]
-                     [(([?vars* ?rhs*] ...) . ?body*) renames])
-         (let ([mid (syntax/skeleton e1 (?letrec-values ([?vars* ?rhs*] ...) . ?body*))])
-           (cons (walk/foci/E (syntax->list #'(?vars ...))
-                              (syntax->list #'(?vars* ...))
-                              e1 mid "Rename letrec-bound variables")
-                 (R mid (LETREC-VALUES ([VARS RHS] ...) . BODY)
-                    [Expr (RHS ...) rhss]
-                    [Block BODY body]))))]
-
-      [(AnyQ p:letrec-syntaxes+values (e1 e2 rs srenames srhss vrenames vrhss body) exni)
+          [Block ?body body])]
+      [(AnyQ p:letrec-syntaxes+values
+             (e1 e2 rs srenames srhss vrenames vrhss body) exni)
        (R e1 _
           [! exni]
           [#:pattern (?lsv ([?svars ?srhs] ...) ([?vvars ?vrhs] ...) . ?body)]
           [#:bind (([?svars* ?srhs*] ...) ([?vvars* ?vrhs] ...) . ?body*) srenames]
-          [#:walk (syntax/skeleton e1 (?lsv ([?svars* ?srhs*] ...) ([?vvars* ?vrhs*] ...) . ?body*))
-                  (syntax->list #'(?svars ...))
-                  (syntax->list #'(?svars* ...))
-                  "Rename bound variables"]
+          [#:rename
+           (syntax/skeleton e1
+                            (?lsv ([?svars* ?srhs*] ...) ([?vvars* ?vrhs*] ...)
+                              . ?body*))
+           (syntax->list #'(?svars ...))
+           (syntax->list #'(?svars* ...))
+           "Rename bound variables"]
           [Expr (?srhs ...) srhss]
           ;; If vrenames is #f, no var bindings to rename
           [#:if vrenames
                 [#:bind (([?vvars** ?vrhs**] ...) . ?body**) vrenames]
-                [#:walk (syntax/skeleton e1 (?lsv ([?svars* ?srhs*] ...) ([?vars** ?vrhs**] ...) . ?body**))
-                        (syntax->list #'(?vvars* ...))
-                        (syntax->list #'(?vvars** ...))
-                        "Rename bound variables"]]
+                [#:rename
+                 (syntax/skeleton e1 (?lsv ([?svars* ?srhs*] ...)
+                                           ([?vars** ?vrhs**] ...)
+                                        . ?body**))
+                 (syntax->list #'(?vvars* ...))
+                 (syntax->list #'(?vvars** ...))
+                 "Rename bound variables"]]
           [Expr (?vrhs ...) vrhss]
           [Block ?body body]
           => (lambda (mid)
                (if (eq? mid e2)
                    null
-                   (list (walk mid e2 "Remove syntax bindings")))))
-       #;
-       (with-syntax ([(?lsv ([?svars ?srhs] ...) ([?vvars ?vrhs] ...) . ?body) e1]
-                     [(([?svars* ?srhs*] ...) ?vpart* . ?body*) srenames])
-         (with-syntax ([(([?vvars* ?vrhs*] ...) . ?body**) 
-                        (or vrenames #'(?vpart* . ?body*))])
-           (let ([mid (syntax/skeleton
-                       e1
-                       (?lsv ([?svars* ?srhs*] ...) ([?vvars* ?vrhs] ...) . ?body**))])
-             (cons 
-              (walk/foci/E (syntax->list #'(?svars ... ?vvars ...))
-                           (syntax->list #'(?svars* ... ?vvars* ...))
-                           e1 mid "Rename local variables")
-              (R mid (LETREC-SYNTAXES+VALUES ([SVARS SRHS] ...) ([VVARS VRHS] ...) . BODY)
-                 [Expr (SRHS ...) srhss]
-                 [Expr (VRHS ...) vrhss]
-                 [Block BODY body]
-                 => (lambda (mid)
-                      (if (eq? mid e2)
-                          null
-                          (list (walk mid e2 "Finish letrec-syntaxes+values")))))))))]
-
+                   (list (walk mid e2 "Remove syntax bindings")))))]
       ;; The auto-tagged atomic primitives
       [(AnyQ p:#%datum (e1 e2 rs tagged-stx) exni)
        (append (if (eq? e1 tagged-stx)
@@ -298,15 +239,6 @@
 
       ;; Error
 
-;      [(struct error-wrap (exn tag (? prule? prule)))
-;       ;; Let's take the attitude that all primitive syntax errors
-;       ;; occur "at the beginning"
-;       (list (make-misstep (deriv-e1 prule) (E (deriv-e1 prule)) exn))]
-;      
-;      #;
-;      [($$ interrupted-wrap (tag prule))
-;       (reductions prule orig-stx)]
-
       ;; Macros
       [(IntQ mrule (e1 e2 transformation next))
        (append (reductions-transformation transformation)
@@ -343,12 +275,14 @@
   ;; reductions-local : LocalAction -> ReductionSequence
   (define (reductions-local local)
     (match local
-      [(IntQ local-expansion (e1 e2 me1 me2 deriv))
+      [(struct local-expansion (e1 e2 me1 me2 deriv))
        (reductions deriv)]
       [(struct local-lift (expr id))
        (list (walk expr id "Macro lifted expression to top-level"))]
       [(struct local-lift-end (decl))
-       (list (walk decl decl "Declaration lifted to end of module"))]))
+       (list (walk decl decl "Declaration lifted to end of module"))]
+      [(struct local-bind (deriv))
+       (reductions deriv)]))
 
   ;; list-reductions : ListDerivation -> ReductionSequence
   (define (list-reductions ld)
diff --git a/collects/macro-debugger/model/steps.ss b/collects/macro-debugger/model/steps.ss
new file mode 100644
index 0000000000..a8e3a3bb7d
--- /dev/null
+++ b/collects/macro-debugger/model/steps.ss
@@ -0,0 +1,16 @@
+
+(module steps mzscheme
+  (provide (all-defined))
+
+  ;; A ReductionSequence is a (list-of Reduction)
+  
+  ;; A Reduction is one of 
+  ;;   - (make-step Syntaxes Syntaxes Syntax Syntax BigContext)
+  ;;   - (make-misstep Syntax Syntax Exception)
+  (define-struct step (redex contractum e1 e2 note lctx) #f)
+  (define-struct misstep (redex e1 exn) #f)
+
+  (define-struct (rewrite-step step) () #f)
+  (define-struct (rename-step step) () #f)
+  
+  )
diff --git a/collects/macro-debugger/model/synth-engine.ss b/collects/macro-debugger/model/synth-engine.ss
index ba3ca44587..3a06f86f6a 100644
--- a/collects/macro-debugger/model/synth-engine.ss
+++ b/collects/macro-debugger/model/synth-engine.ss
@@ -26,29 +26,35 @@
   (define-syntax recv
     (syntax-rules ()
       [(recv body)
-       body]
+       (begin body)]
       [(recv [(var ...) expr] . more)
        (let-values ([(var ...) expr]) (recv . more))]))
 
   (define-syntax (>>P stx)
     (syntax-case stx ()
       [(>>P pr (constructor var ...) pattern . clauses)
-       #'(>>Prim pr #t (constructor var ...) pattern pattern . clauses)]))
+       #'(>>PrimI pr #t (constructor var ...) pattern pattern . clauses)]))
 
   ;; >>P with no restamping
   (define-syntax (>>Pn stx)
     (syntax-case stx ()
       [(>>Pn pr (constructor var ...) pattern . clauses)
-       #'(>>Prim pr #f (constructor var ...) pattern pattern . clauses)]))
+       #'(>>PrimI pr #f (constructor var ...) pattern pattern . clauses)]))
+
+  (define-syntax (>>PrimI stx)
+    (syntax-case stx ()
+      [(>>PrimI pr restamp? cons+vars inp outp . clauses)
+       #'(let ([prvar pr])
+           (>>Prim prvar (deriv-e1 prvar) restamp? cons+vars inp outp . clauses))]))
 
   (define-syntax (>>Prim stx)
     (syntax-case stx ()
-      [(>>Prim pr restamp? cons+vars inp outp clauses)
-       #'(>>Prim pr restamp? cons+vars inp outp clauses #:with values)]
-      [(>>Prim pr restamp? cons+vars inp outp clauses #:with transform)
-       #'(>>Prim pr restamp? cons+vars inp outp clauses
-                 #:with2 (lambda (pr stx) (values pr (transform stx))))]
-      [(>>Prim pr restamp? (constructor var ...)
+      [(>>Prim pr e1 restamp? cons+vars inp outp clauses)
+       #'(>>Prim pr e1 restamp? cons+vars inp outp clauses #:with values)]
+      [(>>Prim pr e1 restamp? cons+vars inp outp clauses #:with transform)
+       #'(>>Prim pr e1 restamp? cons+vars inp outp clauses
+                 #:with2 (lambda (prvar stx) (values prvar (transform stx))))]
+      [(>>Prim pr given-e1 restamp? (constructor var ...)
                in-pattern
                out-pattern
                ([recur hole fill/bind] ...)
@@ -61,7 +67,7 @@
                                (if fbvar (recur fbvar) (values fbvar #f)))] ...)
                  (let ([new-e2 (if (or (interrupted-wrap? prule-var) (error-wrap? prule-var))
                                    #f
-                                   (with-syntax ([in-pattern (deriv-e1 prule-var)])
+                                   (with-syntax ([in-pattern given-e1])
                                      (with-syntax ([hole s-tmp] ...)
                                        #,(if restamp?
                                              #'(syntax/restamp out-pattern #'out-pattern
@@ -69,7 +75,7 @@
                                              #'#'out-pattern))))])
                    (let ([new-pr
                           (match prule-var
-                            [($$ prule (e1 _ rs) _exni)
+                            [(AnyQ prule (e1 _ rs))
                              (constructor e1 new-e2 rs var ...)])])
                      (let-values ([(new-pr new-e2) (transform new-pr new-e2)])
                        (values (rewrap prule-var new-pr)
diff --git a/collects/macro-debugger/syntax-browser/prefs.ss b/collects/macro-debugger/syntax-browser/prefs.ss
index 31ab72d72a..1a7c69e1fa 100644
--- a/collects/macro-debugger/syntax-browser/prefs.ss
+++ b/collects/macro-debugger/syntax-browser/prefs.ss
@@ -3,7 +3,7 @@
   (require (lib "framework.ss" "framework"))
   (provide (all-defined))
 
-  (define current-syntax-font-size (make-parameter 16))
+  (define current-syntax-font-size (make-parameter #f #;16))
   (define current-default-columns (make-parameter 40))
 
   (define-syntax pref:get/set
diff --git a/collects/macro-debugger/syntax-browser/pretty-helper.ss b/collects/macro-debugger/syntax-browser/pretty-helper.ss
index 866d127b0b..4f62b9b0a4 100644
--- a/collects/macro-debugger/syntax-browser/pretty-helper.ss
+++ b/collects/macro-debugger/syntax-browser/pretty-helper.ss
@@ -3,8 +3,6 @@
            "partition.ss")
   (provide (all-defined))
   
-  ;; Fixme: null object still confusable.
-  
   ;; Problem: If stx1 and stx2 are two distinguishable syntax objects, it
   ;; still may be the case that (syntax-e stx1) and (syntax-e stx2) are 
   ;; indistinguishable.
@@ -14,6 +12,10 @@
   ;;   - stx is identifier : map it to an uninterned symbol w/ same rep
   ;;     (Symbols are useful: see pretty-print's style table)
   ;;   - else : map it to a syntax-dummy object
+
+  ;; NOTE: Nulls are only wrapped when *not* list-terminators.  
+  ;; If they were always wrapped, the pretty-printer would screw up
+  ;; list printing (I think).
   
   (define-struct syntax-dummy (val))
   
@@ -45,37 +47,45 @@
     (let/ec escape
       (let ([flat=>stx (make-hash-table)]
             [stx=>flat (make-hash-table)])
-        (values (let loop ([obj stx])
-                  (cond
-                    [(hash-table-get stx=>flat obj (lambda _ #f))
-                     => (lambda (datum) datum)]
-                    [(and partition (identifier? obj))
-                     (let ([lp-datum (make-identifier-proxy obj)])
-                       (when (and limit (> (send partition count) limit))
-                         (call-with-values (lambda () (table stx partition #f #t))
-                                           escape))
-                       (hash-table-put! flat=>stx lp-datum obj)
-                       (hash-table-put! stx=>flat obj lp-datum)
-                       lp-datum)]
-                    [(syntax? obj)
-                     (void (send partition get-partition obj))
-                     (let ([lp-datum (loop (syntax-e obj))])
-                       (hash-table-put! flat=>stx lp-datum obj)
-                       (hash-table-put! stx=>flat obj lp-datum)
-                       lp-datum)]
-                    [(pair? obj) 
-                     (cons (loop (car obj))
-                           (loop (cdr obj)))]
-                    [(vector? obj) 
-                     (list->vector (map loop (vector->list obj)))]
-                    [(symbol? obj)
-                     #;(make-syntax-dummy obj)
-                       (string->uninterned-symbol (symbol->string obj))]
-                    [(number? obj)
-                     (make-syntax-dummy obj)]
-                    #;[(null? obj)
-                       (make-syntax-dummy obj)]
-                      [else obj]))
+        (define (loop obj)
+          (cond [(hash-table-get stx=>flat obj (lambda _ #f))
+                 => (lambda (datum) datum)]
+                [(and partition (identifier? obj))
+                 (let ([lp-datum (make-identifier-proxy obj)])
+                   (when (and limit (> (send partition count) limit))
+                     (call-with-values (lambda () (table stx partition #f #t))
+                       escape))
+                   (hash-table-put! flat=>stx lp-datum obj)
+                   (hash-table-put! stx=>flat obj lp-datum)
+                   lp-datum)]
+                [(syntax? obj)
+                 (void (send partition get-partition obj))
+                 (let ([lp-datum (loop (syntax-e obj))])
+                   (hash-table-put! flat=>stx lp-datum obj)
+                   (hash-table-put! stx=>flat obj lp-datum)
+                   lp-datum)]
+                [(pair? obj)
+                 (pairloop obj)]
+                [(vector? obj) 
+                 (list->vector (map loop (vector->list obj)))]
+                [(symbol? obj)
+                 ;(make-syntax-dummy obj)
+                 (string->uninterned-symbol (symbol->string obj))]
+                [(number? obj)
+                 (make-syntax-dummy obj)]
+                [(box? obj)
+                 (box (loop (unbox obj)))]
+                [(null? obj)
+                 (make-syntax-dummy obj)]
+                [else obj]))
+        (define (pairloop obj)
+          (cond [(pair? obj)
+                 (cons (loop (car obj))
+                       (pairloop (cdr obj)))]
+                [(null? obj)
+                 null]
+                [else (loop obj)]))
+        (values (loop stx)
                 flat=>stx
                 stx=>flat))))
   )
diff --git a/collects/macro-debugger/syntax-browser/pretty-printer.ss b/collects/macro-debugger/syntax-browser/pretty-printer.ss
index a8f5643085..2f0ecebff9 100644
--- a/collects/macro-debugger/syntax-browser/pretty-printer.ss
+++ b/collects/macro-debugger/syntax-browser/pretty-printer.ss
@@ -1,4 +1,6 @@
 
+;; FIXME: Need to disable printing of structs with custom-write property
+
 (module pretty-printer mzscheme
   (require (lib "list.ss")
            (lib "class.ss")
@@ -76,7 +78,15 @@
              [pretty-print-size-hook pp-size-hook]
              [pretty-print-print-hook pp-print-hook]
              [pretty-print-columns columns]
-             [pretty-print-current-style-table (pp-extend-style-table)])
+             [pretty-print-current-style-table (pp-extend-style-table)]
+             ;; Printing parameters (mzscheme manual 7.9.1.4)
+             [print-unreadable #t]
+             [print-graph #f]
+             [print-struct #f]
+             [print-box #t]
+             [print-vector-length #t]
+             [print-hash-table #f]
+             [print-honu #f])
           (pretty-print datum (send typesetter get-output-port))
           (set! -range range)))
 
diff --git a/collects/macro-debugger/syntax-browser/typesetter.ss b/collects/macro-debugger/syntax-browser/typesetter.ss
index 6c48e6cb23..bfc136822d 100644
--- a/collects/macro-debugger/syntax-browser/typesetter.ss
+++ b/collects/macro-debugger/syntax-browser/typesetter.ss
@@ -27,17 +27,18 @@
 
       ;; Internals
 
-      (define start-anchor (new snip%))
-      (define end-anchor (new snip%))
+      (define start-anchor (new anchor-snip%))
+      (define end-anchor (new anchor-snip%))
       (send text insert start-anchor)
       (send text insert end-anchor)
 
       (define output-port (make-text-port text end-anchor))
 
       (define base-style
-        (let ([sd (make-object style-delta% 'change-family 'modern)])
-          (when (current-syntax-font-size)
-            (send sd set-delta 'change-size (current-syntax-font-size)))
+        (send (send text get-style-list) find-named-style "Standard")
+        #;(let ([sd (make-object style-delta% 'change-family 'modern)])
+            (when (current-syntax-font-size)
+              (send sd set-delta 'change-size (current-syntax-font-size)))
           sd))
 
       (define/private (get-start-position)
@@ -93,8 +94,8 @@
     (make-output-port #f
                       always-evt
                       (lambda (s start end flush? enable-break?)
-                        (send text insert 
-                              (substring (bytes->string/utf-8 s) start end)
+                        (send text insert
+                              (bytes->string/utf-8 s #f start end)
                               (send text get-snip-position end-anchor))
                         (- end start))
                       void
@@ -103,4 +104,9 @@
                               (send text get-snip-position end-anchor))
                         #t)))
 
+  (define anchor-snip%
+    (class snip%
+      (define/override (copy)
+        (make-object string-snip% ""))
+      (super-instantiate ())))
   )
diff --git a/collects/macro-debugger/syntax-browser/widget.ss b/collects/macro-debugger/syntax-browser/widget.ss
index 8b9c9cb601..eb3d5fdae8 100644
--- a/collects/macro-debugger/syntax-browser/widget.ss
+++ b/collects/macro-debugger/syntax-browser/widget.ss
@@ -16,6 +16,8 @@
            syntax-widget%
            syntax-browser-frame%)
 
+  (define browser-text% (editor:standard-style-list-mixin text:basic%))
+
   ;; syntax-widget%
   ;; A syntax-widget creates its own syntax-controller.
   (define syntax-widget%
@@ -24,17 +26,17 @@
 
       (define -main-panel (new vertical-panel% (parent parent)))
       (define -split-panel (new panel:horizontal-dragable% (parent -main-panel)))
-      (define -text (new text%))
+      (define -text (new browser-text%))
       (define -ecanvas (new editor-canvas% (parent -split-panel) (editor -text)))
       (define -props-panel (new horizontal-panel% (parent -split-panel)))
       (define props (new properties-view% (parent -props-panel)))
       (define -saved-panel-percentages #f)
+      (define canvas-width #f)
 
       (define controller
         (new syntax-controller%
              (properties-controller this)))
 
-      #;(send -text hide-caret #t)
       (send -text lock #t)
       (send -split-panel set-percentages 
             (let ([pp (pref:props-percentage)]) (list (- 1 pp) pp)))
@@ -110,17 +112,24 @@
 
       (define/private (internal-add-syntax stx hi-stxs hi-color)
         (with-unlock -text
-          (let ([current-position (send -text last-position)])
-            (let* ([new-ts (new typesetter-for-text%
-                                (controller controller)
-                                (syntax stx)
-                                (text -text))]
-                   [new-colorer (send new-ts get-colorer)])
-              (send* -text
-                (insert "\n")
-                (scroll-to-position current-position))
-              (unless (null? hi-stxs)
-                (send new-colorer highlight-syntaxes hi-stxs hi-color))))))
+          (parameterize ((current-default-columns (calculate-columns)))
+            (let ([current-position (send -text last-position)])
+              (let* ([new-ts (new typesetter-for-text%
+                                  (controller controller)
+                                  (syntax stx)
+                                  (text -text))]
+                     [new-colorer (send new-ts get-colorer)])
+                (send* -text
+                  (insert "\n")
+                  (scroll-to-position current-position))
+                (unless (null? hi-stxs)
+                  (send new-colorer highlight-syntaxes hi-stxs hi-color)))))))
+
+      (define/private (calculate-columns)
+        (define style-list (send -text get-style-list))
+        (define standard (send style-list find-named-style "Standard"))
+        (define char-width (send standard get-text-width (send -ecanvas get-dc)))
+        (inexact->exact (floor (/ (send -ecanvas get-width) char-width))))
 
       (super-new)))
 
diff --git a/collects/macro-debugger/tool.ss b/collects/macro-debugger/tool.ss
index 88d8a73e6e..8ae3c5f8d8 100644
--- a/collects/macro-debugger/tool.ss
+++ b/collects/macro-debugger/tool.ss
@@ -1,7 +1,9 @@
 
 (module tool mzscheme
   (require "model/trace.ss"
-           (prefix view: "view/gui.ss"))
+           "model/hiding-policies.ss"
+           (prefix view: "view/gui.ss")
+           (prefix prefs: "syntax-browser/prefs.ss"))
   (require (lib "class.ss")
            (lib "list.ss")
            (lib "unitsig.ss")
@@ -23,6 +25,7 @@
       (define drscheme-eventspace (current-eventspace))
 
       (define-local-member-name check-language)
+      (define-local-member-name get-debug-button)
       
       (define (macro-debugger-unit-frame-mixin %)
         (class %
@@ -49,6 +52,8 @@
             (send (get-interactions-text) enable-macro-debugging debugging?)
             (super execute-callback))
 
+          (define/public (get-debug-button) macro-debug-button)
+
           ;; Hide button for inappropriate languages
 
           (define/augment (on-tab-change old new)
@@ -75,12 +80,22 @@
 
       (define (macro-debugger-definitions-text-mixin %)
         (class %
-          (super-new)
           (inherit get-top-level-window)
-
           (define/augment (after-set-next-settings s)
 	    (send (get-top-level-window) check-language)
-	    (inner (void) after-set-next-settings s))))
+	    (inner (void) after-set-next-settings s))
+          (super-new)))
+
+      (define (macro-debugger-tab-mixin %)
+        (class %
+          (inherit get-frame)
+          (define/override (enable-evaluation)
+            (super enable-evaluation)
+            (send (send (get-frame) get-debug-button) enable #t))
+          (define/override (disable-evaluation)
+            (super disable-evaluation)
+            (send (send (get-frame) get-debug-button) enable #f))
+          (super-new)))
 
       (define (macro-debugger-interactions-text-mixin %)
         (class %
@@ -95,20 +110,23 @@
             (super reset-console)
             (run-in-evaluation-thread
              (lambda ()
-               (let-values ([(e mnr) (make-handlers (current-eval) (current-module-name-resolver))])
+               (let-values ([(e mnr) 
+                             (make-handlers (current-eval)
+                                            (current-module-name-resolver))])
                  (current-eval e)
                  (current-module-name-resolver mnr)))))
 
           (define/private (make-handlers original-eval-handler original-module-name-resolver)
-            (let ([stepper (delay (view:make-macro-stepper))]
+            (let ([stepper (delay (view:make-macro-stepper (new-standard-hiding-policy)))]
                   [debugging? debugging?])
               (values
                (lambda (expr)
-                 (if debugging?
+                 (if (and debugging? (and (syntax? expr) (syntax-source expr)))
                      (let-values ([(e-expr deriv) (trace/result expr)])
                        (show-deriv deriv stepper)
                        (if (syntax? e-expr)
-                           (original-eval-handler e-expr)
+                           (parameterize ((current-eval original-eval-handler))
+                             (original-eval-handler e-expr))
                            (raise e-expr)))
                      (original-eval-handler expr)))
                (lambda args
@@ -145,12 +163,13 @@
           (and (equal? main-group (string-constant professional-languages))
                (or (member second 
                            (list (string-constant r5rs-lang-name)
+                                 "(module ...)"
                                  "Swindle"))
                    (member third
                            (list (string-constant mzscheme-w/debug)
                                  (string-constant mred-w/debug)
                                  (string-constant pretty-big-scheme)))))))
-
+      
       ;; Macro debugger code
 
       (drscheme:get/extend:extend-unit-frame
@@ -159,5 +178,7 @@
        macro-debugger-interactions-text-mixin)
       (drscheme:get/extend:extend-definitions-text
        macro-debugger-definitions-text-mixin)
+      (drscheme:get/extend:extend-tab
+       macro-debugger-tab-mixin)
 
       )))
diff --git a/collects/macro-debugger/view/gui.ss b/collects/macro-debugger/view/gui.ss
index 3d911b9d4b..e672058500 100644
--- a/collects/macro-debugger/view/gui.ss
+++ b/collects/macro-debugger/view/gui.ss
@@ -15,6 +15,7 @@
            "../model/trace.ss"
            "../model/hide.ss"
            "../model/hiding-policies.ss"
+           "../model/steps.ss"
            "cursor.ss"
            "util.ss")
 
@@ -22,7 +23,7 @@
 
   ;; Configuration
 
-  (define catch-errors? (make-parameter #t))
+  (define catch-errors? (make-parameter #f))
 
   ;; Macro Stepper
 
@@ -32,6 +33,8 @@
 
   (define macro-stepper-frame%
     (class base-frame%
+      (init policy
+            macro-hiding?)
       (inherit get-menu%
                get-menu-item%
                get-menu-bar
@@ -43,6 +46,9 @@
                  (width (sb:pref:width))
                  (height (sb:pref:height)))
 
+      (define/override (on-size w h)
+        (send widget update/preserve-view))
+
       (override/return-false file-menu:create-new?
                              file-menu:create-open?
                              file-menu:create-open-recent?
@@ -96,7 +102,9 @@
         (new macro-stepper-widget%
              (register-syntax-action (mk-register-action syntax-menu))
              (register-stepper-action (mk-register-action stepper-menu))
-             (parent (send this get-area-container))))
+             (parent (send this get-area-container))
+             (policy policy)
+             (macro-hiding? macro-hiding?)))
 
       (define/public (get-widget) widget)
       (frame:reorder-menus this)
@@ -108,6 +116,8 @@
       (init-field parent)
       (init-field register-syntax-action)
       (init-field register-stepper-action)
+      (init policy)
+      (init macro-hiding?)
 
       ;; derivs : (list-of Derivation)
       (define derivs null)
@@ -157,7 +167,11 @@
       (define control-pane
         (new vertical-panel% (parent area) (stretchable-height #f)))
       (define macro-hiding-prefs
-        (new macro-hiding-prefs-widget% (parent control-pane) (stepper this)))
+        (new macro-hiding-prefs-widget%
+             (policy policy)
+             (parent control-pane)
+             (stepper this)
+             (enabled? macro-hiding?)))
       (send sbc add-selection-listener
             (lambda (stx) (send macro-hiding-prefs set-syntax stx)))
 
@@ -229,6 +243,15 @@
         (send sbview add-text text)
         (send sbview add-text "\n\n"))
 
+      ;; update/preserve-view : -> void
+      (define/public (update/preserve-view)
+        (define text (send sbview get-text))
+        (define start-box (box 0))
+        (define end-box (box 0))
+        (send text get-visible-position-range start-box end-box)
+        (update)
+        (send text scroll-to-position (unbox start-box) #f (unbox end-box)))
+
       ;; update : -> void
       ;; Updates the terms in the syntax browser to the current step
       (define/private (update)
@@ -340,7 +363,7 @@
                              (set! synth-deriv #f)
                              (set! steps (cursor:new null)))])
             (let ([d (synthesize deriv)])
-              (let ([s (cursor:new (reductions d))])
+              (let ([s (cursor:new (reduce d))])
                 (set! synth-deriv d)
                 (set! steps s)))))
         #;(navigate-to-start)
@@ -352,8 +375,13 @@
           (if show-macro?
               (with-handlers ([(lambda (e) (catch-errors?))
                                (lambda (e) (no-synthesize deriv))])
-                (let-values ([(d s) (hide/policy deriv show-macro?)])
-                  d))
+                (parameterize ((current-hiding-warning-handler
+                                (let ([warnings (delay (new warnings-frame%))])
+                                  (lambda (tag message)
+                                    (send (force warnings)
+                                          add-warning tag)))))
+                  (let-values ([(d s) (hide/policy deriv show-macro?)])
+                    d)))
               deriv)))
 
       (define/private (no-synthesize deriv)
@@ -365,6 +393,13 @@
         (send macro-hiding-prefs enable-hiding #f)
         (synthesize deriv))
 
+      ;; reduce : Derivation -> ReductionSequence
+      (define/private (reduce d)
+        (if (get-show-macro?)
+            (filter (lambda (x) (not (rename-step? x)))
+                    (reductions d))
+            (reductions d)))
+      
       (define/private (foci x) (if (list? x) x (list x)))
 
       ;; Hiding policy
@@ -383,10 +418,9 @@
     (class object%
       (init parent)
       (init-field stepper)
-      (init-field (policy (new-hiding-policy)))
-          ;; (new-standard-hiding-policy)))
+      (init-field policy)
+      (init-field (enabled? #f))
 
-      (define enabled? #f)
       (define stx #f)
       (define stx-name #f)
       (define stx-module #f)
@@ -510,14 +544,8 @@
 
       (define/private (update-add-text)
         (send add-editor lock #f)
-        (if stx-module
-            (send add-editor insert
-                  (format "'~s' from module ~a"
-                          stx-name
-                          (mpi->string stx-module)))
-            (send add-editor insert
-                  (format "lexically-bound ~s"
-                          stx-name)))
+        (when (identifier? stx)
+          (send add-editor insert (identifier-text "" stx)))
         (send add-editor lock #t))
 
       (define/private (add-hide-module)
@@ -545,6 +573,22 @@
                   (send look-ctl get-selections))
         (update-list-view))
 
+      (define/private (identifier-text prefix id)
+        (let ([b (identifier-binding id)])
+          (cond [(pair? b)
+                 (let ([name (cadr b)]
+                       [mod (car b)])
+                   (format "~a'~s' from module ~a"
+                           prefix
+                           name
+                           (mpi->string mod)))]
+                [(eq? b 'lexical)
+                 (format "~alexically bound '~s'"
+                         prefix
+                         (syntax-e id))]
+                [(not b)
+                 (format "~aglobal or unbound '~s'" prefix (syntax-e id))])))
+
       (define/private (update-list-view)
         (let ([opaque-modules
                (hash-table-map (hiding-policy-opaque-modules policy)
@@ -563,20 +607,10 @@
             (cons (format "hide from module ~a" (mpi->string s))
                   (cons 'module s)))
           (define (*i prefix tag id)
-            (cons (let ([b (identifier-binding id)])
-                    (if (pair? b)
-                        (let ([name (cadr b)]
-                              [mod (car b)])
-                          (format "~a '~s' from module ~a"
-                                  prefix
-                                  name
-                                  (mpi->string mod)))
-                        (format "~a lexically bound macro '~s'"
-                                prefix
-                                (syntax-e id))))
+            (cons (identifier-text prefix id)
                   (cons tag id)))
-          (define (oid id) (*i "hide" 'identifier id))
-          (define (tid id) (*i "show" 'show-identifier id))
+          (define (oid id) (*i "hide " 'identifier id))
+          (define (tid id) (*i "show " 'show-identifier id))
           (let ([choices
                  (sort (append (map om opaque-modules)
                                (map oid opaque-ids)
@@ -589,14 +623,48 @@
 
       (super-new)))
 
+  ;; warnings-frame%
+  (define warnings-frame%
+    (class frame%
+      (super-new (label "Macro stepper warnings") (width 400) (height 300))
+
+      (define text (new text% (auto-wrap #t)))
+      (define ec (new editor-canvas% (parent this) (editor text)))
+      (send text lock #t)
+
+      (define/private (add-text . strs)
+        (send text lock #f)
+        (for-each (lambda (s) (send text insert s)) strs)
+        (send text insert "\n\n")
+        (send text lock #t))
+
+      (define/public (add-warning tag)
+        (case tag
+          ((nonlinearity)
+           (add-text
+            "An opaque macro duplicated one of its subterms. "
+            "Macro hiding requires opaque macros to use their subterms linearly. "
+            "The macro stepper is showing the expansion of that macro use."))
+          ((localactions)
+           (add-text
+            "An opaque macro called local-expand, syntax-local-lift-expression, "
+            "etc. Macro hiding cannot currently handle local actions. "
+            "The macro stepper is showing the expansion of that macro use."))))
+      (send this show #t)))
 
   ;; Main entry points
 
-  (define (make-macro-stepper)
-    (let ([f (new macro-stepper-frame%)])
-      (send f show #t)
-      (send f get-widget)))
-  
+  (define make-macro-stepper
+    (case-lambda
+      [(policy hiding?)
+       (let ([f (new macro-stepper-frame% (policy policy) (macro-hiding? hiding?))])
+         (send f show #t)
+         (send f get-widget))]
+      [(policy)
+       (make-macro-stepper policy #t)]
+      [()
+       (make-macro-stepper (new-hiding-policy) #f)]))
+
   (define (go . stxs)
     (let ([stepper (make-macro-stepper)])
       (let loop ([stxs stxs])