diff --git a/collects/macro-debugger/model/debug.ss b/collects/macro-debugger/model/debug.ss
new file mode 100644
index 0000000..1426e5d
--- /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 0cfec4a..bca3848 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 6cc9ed9..efd1406 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 e6539b4..f3e8305 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/hiding-policies.ss b/collects/macro-debugger/model/hiding-policies.ss
index 5529cc9..2278379 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 18aa266..9ae287b 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 aa05de6..d47d78d 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 0000000..a8e3a3b
--- /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/syntax-browser/prefs.ss b/collects/macro-debugger/syntax-browser/prefs.ss
index 31ab72d..1a7c69e 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 866d127..4f62b9b 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 a8f5643..2f0eceb 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/widget.ss b/collects/macro-debugger/syntax-browser/widget.ss
index 8b9c9cb..eb3d5fd 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)))