diff --git a/redex-doc/redex/scribblings/long-tut/code/common.rkt b/redex-doc/redex/scribblings/long-tut/code/common.rkt
index 648b68dc..f7dcc537 100644
--- a/redex-doc/redex/scribblings/long-tut/code/common.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/common.rkt
@@ -27,13 +27,13 @@
  subst)
 
 ;; -----------------------------------------------------------------------------
-(require redex)
+(require redex/reduction-semantics)
 
 (define-language Lambda
   (e ::=
      x 
-     (lambda (x_!_ ...) e)
-     (e e ...))
+     (lambda (x) e)
+     (e e))
   (x ::= variable-not-otherwise-mentioned))
 
 (define lambda? (redex-match? Lambda e))
@@ -41,7 +41,7 @@
 (module+ test
   (define e1 (term y))
   (define e2 (term (lambda (y) y)))
-  (define e3 (term (lambda (x y) y)))
+  (define e3 (term (lambda (x) (lambda (y) y))))
   (define e4 (term (,e2 e3)))
 
   (test-equal (lambda? e1) #true)
@@ -49,8 +49,8 @@
   (test-equal (lambda? e3) #true)
   (test-equal (lambda? e4) #true)
 
-  (define eb1 (term (lambda (x x) y)))
-  (define eb2 (term (lambda (x y) 3)))
+  (define eb1 (term (lambda () y)))
+  (define eb2 (term (lambda (x) (lambda (y) 3))))
 
   (test-equal (lambda? eb1) #false)
   (test-equal (lambda? eb2) #false))
@@ -74,7 +74,11 @@
 (module+ test
   (test-equal (term (=α (lambda (x) x) (lambda (y) y))) #true)
   (test-equal (term (=α (lambda (x) (x 1)) (lambda (y) (y 1)))) #true)
-  (test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false))
+  (test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false)
+  (test-equal (term (=α (lambda (x) x) (lambda (x) (lambda (x) x)))) #false)
+  (test-equal (term (=α (lambda (x) x) (lambda (x) (x x)))) #false)
+  (test-equal (term (=α (lambda (x) (lambda (y) (x y))) (lambda (x) (lambda (y) (y x))))) #false)
+  (test-equal (term (=α (lambda (x) (lambda (y) (x y))) (lambda (a) (lambda (b) (a b))))) #true))
 
 (define-metafunction Lambda
   =α : any any -> boolean
@@ -85,45 +89,44 @@
 
 ;; (sd e) computes the static distance version of e
 (define-extended-language SD Lambda
-  (e ::= .... (K n))
+  (e ::= .... (K n) (lambda e))
   (n ::= natural))
 
 (define SD? (redex-match? SD e))
 
 (module+ test
   (define sd1 (term (K 1)))
-  (define sd2 (term 1))
 
   (test-equal (SD? sd1) #true))
 
 (define-metafunction SD
   sd : any -> any
-  [(sd any_1) (sd/a any_1 ())])
+  [(sd any) (sd/a any ())])
 
 (module+ test
   (test-equal (term (sd/a x ())) (term x))
-  (test-equal (term (sd/a x ((y) (z) (x)))) (term (K 2 0)))
+  (test-equal (term (sd/a x (y z x))) (term (K 2)))
   (test-equal (term (sd/a ((lambda (x) x) (lambda (y) y)) ()))
-              (term ((lambda () (K 0 0)) (lambda () (K 0 0)))))
+              (term ((lambda (K 0)) (lambda (K 0)))))
   (test-equal (term (sd/a (lambda (x) (x (lambda (y) y))) ()))
-              (term (lambda () ((K 0 0) (lambda () (K 0 0))))))
-  (test-equal (term (sd/a (lambda (z x) (x (lambda (y) z))) ()))
-              (term (lambda () ((K 0 1) (lambda () (K 1 0)))))))
+              (term (lambda ((K 0) (lambda (K 0))))))
+  (test-equal (term (sd/a (lambda (z) (lambda (x) (x (lambda (y) z)))) ()))
+              (term (lambda (lambda ((K 0) (lambda (K 2))))))))
 
 (define-metafunction SD
-  sd/a : any ((x ...) ...) -> any
-  [(sd/a x ((x_1 ...) ... (x_0 ... x x_2 ...) (x_3 ...) ...))
+  sd/a : any (x ...) -> any
+  [(sd/a x (x_1 ... x x_2 ...))
    ;; bound variable 
-   (K n_rib n_pos)
-   (where n_rib ,(length (term ((x_1 ...) ...))))
-   (where n_pos ,(length (term (x_0 ...))))
-   (where #false (in x (x_1 ... ...)))]
-  [(sd/a (lambda (x ...) any_1) (any_rest ...))
-   (lambda () (sd/a any_1 ((x ...) any_rest ...)))]
-  [(sd/a (any_fun any_arg ...) (any_rib ...))
-   ((sd/a any_fun (any_rib ...)) (sd/a any_arg (any_rib ...)) ...)]
-  [(sd/a any_1 any)
-   ;; free variable, constant, etc 
+   (K n)
+   (where n ,(length (term (x_1 ...))))
+   (where #false (in x (x_1 ...)))]
+  [(sd/a (lambda (x) any_body) (x_rest ...))
+   (lambda (sd/a any_body (x x_rest ...)))
+   (where n ,(length (term (x_rest ...))))]
+  [(sd/a (any_fun any_arg) (x_rib ...))
+   ((sd/a any_fun (x_rib ...)) (sd/a any_arg (x_rib ...)))]
+  [(sd/a any_1 (x ...))
+   ;; free variable or constant, etc
    any_1])
 
 
@@ -134,10 +137,10 @@
   (test-equal (term (subst ([1 x][2 y]) x)) 1)
   (test-equal (term (subst ([1 x][2 y]) y)) 2)
   (test-equal (term (subst ([1 x][2 y]) z)) (term z))
-  (test-equal (term (subst ([1 x][2 y]) (lambda (z w) (x y))))
-              (term (lambda (z w) (1 2))))
-  (test-equal (term (subst ([1 x][2 y]) (lambda (z w) (lambda (x) (x y)))))
-              (term (lambda (z w) (lambda (x) (x 2))))
+  (test-equal (term (subst ([1 x][2 y]) (lambda (z) (lambda (w) (x y)))))
+              (term (lambda (z) (lambda (w) (1 2)))))
+  (test-equal (term (subst ([1 x][2 y]) (lambda (z) (lambda (w) (lambda (x) (x y))))))
+              (term (lambda (z) (lambda (w) (lambda (x) (x 2)))))
               #:equiv =α/racket)
   (test-equal (term (subst ((2 x)) ((lambda (x) (1 x)) x)))
               (term ((lambda (x) (1 x)) 2))
@@ -150,23 +153,23 @@
   subst : ((any x) ...) any -> any
   [(subst [(any_1 x_1) ... (any_x x) (any_2 x_2) ...] x) any_x]
   [(subst [(any_1 x_1) ... ] x) x]
-  [(subst [(any_1 x_1) ... ] (lambda (x ...) any_body))
-   (lambda (x_new ...)
+  [(subst [(any_1 x_1) ... ] (lambda (x) any_body))
+   (lambda (x_new)
      (subst ((any_1 x_1) ...)
-            (subst-raw ((x_new x) ...) any_body)))
-   (where  (x_new ...)  ,(variables-not-in (term (any_body any_1 ...)) (term (x ...)))) ]
+            (subst-raw (x_new x) any_body)))
+   (where  x_new ,(variable-not-in (term (any_body any_1 ...)) (term x)))]
   [(subst [(any_1 x_1) ... ] (any ...)) ((subst [(any_1 x_1) ... ] any) ...)]
   [(subst [(any_1 x_1) ... ] any_*) any_*])
 
 (define-metafunction Lambda
-  subst-raw : ((x x) ...) any -> any
-  [(subst-raw ((x_n1 x_o1) ... (x_new x) (x_n2 x_o2) ...) x) x_new]
-  [(subst-raw ((x_n1 x_o1) ... ) x) x]
-  [(subst-raw ((x_n1 x_o1) ... ) (lambda (x ...) any))
-   (lambda (x ...) (subst-raw ((x_n1 x_o1) ... ) any))]
-  [(subst-raw [(any_1 x_1) ... ] (any ...))
-   ((subst-raw [(any_1 x_1) ... ] any) ...)]
-  [(subst-raw [(any_1 x_1) ... ] any_*) any_*])
+  subst-raw : (x x) any -> any
+  [(subst-raw (x_new x_) x_) x_new]
+  [(subst-raw (x_new x_) x) x]
+  [(subst-raw (x_new x_) (lambda (x) any))
+   (lambda (x) (subst-raw (x_new x_) any))]
+  [(subst-raw (x_new x_) (any ...))
+   ((subst-raw (x_new x_) any) ...)]
+  [(subst-raw (x_new x_) any_*) any_*])
 
 ;; -----------------------------------------------------------------------------
 (module+ test
diff --git a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
index cb0589fd..af952793 100644
--- a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
@@ -22,31 +22,17 @@ subst (if time, otherwise it's provide)
 ;; -----------------------------------------------------------------------------
 (require redex)
 
-(define-language Lambda0
-  (e ::=
-     x 
-     (lambda (x ...) e)
-     (e e ...))
-  (x ::= variable-not-otherwise-mentioned))
-
-(define-language Lambda-bad
-  (e ::=
-     x 
-     (side-condition (lambda (x_ ...) e) (term (unique-vars (x_ ...))))
-     (e e ...))
-  (x ::= variable-not-otherwise-mentioned))
-
 (define-language Lambda
   (e ::=
      x 
-     (lambda (x_!_ ...) e)
-     (e e ...))
+     (lambda (x) e)
+     (e e))
   (x ::= variable-not-otherwise-mentioned))
 
 (define e1 (term y))
 (define e2 (term (lambda (y) y)))
-(define e3 (term (lambda (x y) y)))
-(define e4 (term (,e2 e3)))
+(define e3 (term (lambda (x) (lambda (y) y))))
+(define e4 (term (,e2 ,e3)))
 
 (define in-Lambda? (redex-match? Lambda e))
 
@@ -56,20 +42,23 @@ subst (if time, otherwise it's provide)
   (test-equal (in-Lambda? e3) #true)
   (test-equal (in-Lambda? e4) #true))
 
-(define eb1 (term (lambda (x x) y)))
-(define eb2 (term (lambda (x y) 3)))
+(define eb1 (term (lambda (y) (lambda () y))))
+(define eb2 (term (lambda (x) (lambda (y) 3))))
 
 (module+ test
   (test-equal (in-Lambda? eb1) #false)
-  (test-equal (in-Lambda? eb2) #false))
+  (test-equal (in-Lambda? eb2) #false)
+  ) ;; close paren must be on this line or else mon-aft.scrbl won't run properly
 
 ;; -----------------------------------------------------------------------------
 ;; (unique-vars x ...) is the sequence of variables x ... free of duplicates?
 
+;; unique-vars tests start
 (module+ test 
   (test-equal (term (unique-vars x y)) #true)
   (test-equal (term (unique-vars x y x)) #false))
 
+;; unique-vars metafunction start
 (define-metafunction Lambda 
   unique-vars : x ... -> boolean 
   [(unique-vars) #true]
@@ -95,19 +84,19 @@ subst (if time, otherwise it's provide)
 (module+ test
   (test-equal (term (fv x)) (term (x)))
   (test-equal (term (fv (lambda (x) x))) (term ()))
-  (test-equal (term (fv (lambda (x) (y z x)))) (term (y z))))
+  (test-equal (term (fv (lambda (x) ((y z) x)))) (term (y z))))
 
+;; fv metafunction start
 (define-metafunction Lambda
-  fv : any -> (x ...)
+  fv : e -> (x ...)
   [(fv x) (x)]
-  [(fv (lambda (x ...) any_body))
-   (subtract (x_e ...) x ...)
-   (where (x_e ...) (fv any_body))]
-  [(fv (any_f any_a ...))
-   (x_f ... x_a ... ...)
-   (where (x_f ...) (fv any_f))
-   (where ((x_a ...) ...) ((fv any_a) ...))]
-  [(fv any) ()])
+  [(fv (lambda (x) e_body))
+   (subtract (x_e ...) x)
+   (where (x_e ...) (fv e_body))]
+  [(fv (e_f e_a))
+   (x_f ... x_a ...)
+   (where (x_f ...) (fv e_f))
+   (where (x_a ...) (fv e_a))])
 
 ;; -----------------------------------------------------------------------------
 ;; (subtract (x ...) x_1 ...) removes x_1 ... from (x ...)
@@ -137,108 +126,60 @@ subst (if time, otherwise it's provide)
 ;; (sd e) computes the static distance version of e
 
 (define-extended-language SD Lambda
-  (e ::= .... (K n n) (lambda n e))
+  (e ::= .... (K n) (lambda e) n)
   (n ::= natural))
 
-(define sd1 (term (K 0 1)))
-(define sd2 (term 1))
+(define sd1 (term (K 0)))
 
 (define SD? (redex-match? SD e))
 
+;; SD? test case
 (module+ test
   (test-equal (SD? sd1) #true))
 
+;; SD metafunction
 (define-metafunction SD
-  sd : any -> any
-  [(sd any_1) (sd/a any_1 ())])
+  sd : e -> e
+  [(sd e) (sd/a e ())])
 
 (module+ test
   (test-equal (term (sd/a x ())) (term x))
-  (test-equal (term (sd/a x ((y) (z) (x)))) (term (K 2 0)))
+  (test-equal (term (sd/a x (y z x))) (term (K 2)))
   (test-equal (term (sd/a ((lambda (x) x) (lambda (y) y)) ()))
-              (term ((lambda 1 (K 0 0)) (lambda 1 (K 0 0)))))
+              (term ((lambda (K 0)) (lambda (K 0)))))
   (test-equal (term (sd/a (lambda (x) (x (lambda (y) y))) ()))
-              (term (lambda 1 ((K 0 0) (lambda 1 (K 0 0))))))
-  (test-equal (term (sd/a (lambda (z x) (x (lambda (y) z))) ()))
-              (term (lambda 2 ((K 0 1) (lambda 1 (K 1 0)))))))
+              (term (lambda ((K 0) (lambda (K 0))))))
+  (test-equal (term (sd/a (lambda (z) (lambda (x) (x (lambda (y) z)))) ()))
+              (term (lambda (lambda ((K 0) (lambda (K 2))))))))
 
 (define-metafunction SD
-  sd/a : any ((x ...) ...) -> any
-  [(sd/a x ((x_1 ...) ... (x_0 ... x x_2 ...) (x_3 ...) ...))
+  sd/a : e (x ...) -> any
+  [(sd/a x (x_1 ... x x_2 ...))
    ;; bound variable 
-   (K n_rib n_pos)
-   (where n_rib ,(length (term ((x_1 ...) ...))))
-   (where n_pos ,(length (term (x_0 ...))))
-   (where #false (in x (x_1 ... ...)))]
-  [(sd/a (lambda (x ...) any_1) (any_rest ...))
-   (lambda n (sd/a any_1 ((x ...) any_rest ...)))
-   (where n ,(length (term (x ...))))]
-  [(sd/a (any_fun any_arg ...) (any_rib ...))
-   ((sd/a any_fun (any_rib ...)) (sd/a any_arg (any_rib ...)) ...)]
-  [(sd/a any_1 any)
-   ;; free variable, constant, etc 
+   (K n)
+   (where n ,(length (term (x_1 ...))))
+   (where #false (in x (x_1 ...)))]
+  [(sd/a (lambda (x) e_body) (x_rest ...))
+   (lambda (sd/a e_body (x x_rest ...)))
+   (where n ,(length (term (x_rest ...))))]
+  [(sd/a (e_fun e_arg) (x ...))
+   ((sd/a e_fun (x ...)) (sd/a e_arg (x ...)))]
+  [(sd/a any_1 (x ...))
    any_1])
 
 ;; -----------------------------------------------------------------------------
 ;; (=α e_1 e_2) determines whether e_1 and e_2 are α equivalent
 
-(define-extended-language Lambda/n Lambda
-  (e ::= .... n)
-  (n ::= natural))
-
-(define in-Lambda/n? (redex-match? Lambda/n e))
-
 (module+ test
   (test-equal (term (=α (lambda (x) x) (lambda (y) y))) #true)
   (test-equal (term (=α (lambda (x) (x 1)) (lambda (y) (y 1)))) #true)
   (test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false))
 
 (define-metafunction SD
-  =α : any any -> boolean
-  [(=α any_1 any_2) ,(equal? (term (sd any_1)) (term (sd any_2)))])
+  =α : e e -> boolean
+  [(=α e_1 e_2) ,(equal? (term (sd e_1)) (term (sd e_2)))])
 
 (define (=α/racket x y) (term (=α ,x ,y)))
 
-;; -----------------------------------------------------------------------------
-;; (subst ([e x] ...) e_*) substitutes e ... for x ... in e_* (hygienically)
-
-(module+ test
-  (test-equal (term (subst ([1 x][2 y]) x)) 1)
-  (test-equal (term (subst ([1 x][2 y]) y)) 2)
-  (test-equal (term (subst ([1 x][2 y]) z)) (term z))
-  (test-equal (term (subst ([1 x][2 y]) (lambda (z w) (x y))))
-              (term (lambda (z w) (1 2))))
-  (test-equal (term (subst ([1 x][2 y]) (lambda (z w) (lambda (x) (x y)))))
-              (term (lambda (z w) (lambda (x) (x 2))))
-              #:equiv =α/racket)
-  (test-equal (term (subst ((2 x)) ((lambda (x) (1 x)) x)))
-              (term ((lambda (x) (1 x)) 2))
-              #:equiv =α/racket))
-              
-              
-
-(define-metafunction Lambda
-  subst : ((any x) ...) any -> any
-  [(subst [(any_1 x_1) ... (any_x x) (any_2 x_2) ...] x) any_x]
-  [(subst [(any_1 x_1) ... ] x) x]
-  [(subst [(any_1 x_1) ... ] (lambda (x ...) any_body))
-   (lambda (x_new ...)
-     (subst ((any_1 x_1) ...)
-            (subst-raw ((x_new x) ...) any_body)))
-   (where  (x_new ...)  ,(variables-not-in (term any_body) (term (x ...)))) ]
-  [(subst [(any_1 x_1) ... ] (any ...)) ((subst [(any_1 x_1) ... ] any) ...)]
-  [(subst [(any_1 x_1) ... ] any_*) any_*])
-
-(define-metafunction Lambda
-  subst-raw : ((x x) ...) any -> any
-  [(subst-raw ((x_n1 x_o1) ... (x_new x) (x_n2 x_o2) ...) x) x_new]
-  [(subst-raw ((x_n1 x_o1) ... ) x) x]
-  [(subst-raw ((x_n1 x_o1) ... ) (lambda (x ...) any))
-   (lambda (x ...) (subst-raw ((x_n1 x_o1) ... ) any))]
-  [(subst-raw [(any_1 x_1) ... ] (any ...))
-   ((subst-raw [(any_1 x_1) ... ] any) ...)]
-  [(subst-raw [(any_1 x_1) ... ] any_*) any_*])
-
-;; -----------------------------------------------------------------------------
 (module+ test
   (test-results))
diff --git a/redex-doc/redex/scribblings/long-tut/code/tue-mor.rkt b/redex-doc/redex/scribblings/long-tut/code/tue-mor.rkt
index 1d5cf088..1b4b8ecd 100644
--- a/redex-doc/redex/scribblings/long-tut/code/tue-mor.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/tue-mor.rkt
@@ -1,12 +1,12 @@
 #lang racket
-(require redex "common.rkt" (only-in "mon-aft.rkt" fv))
 (provide eval-value)
+(require redex "common.rkt" (only-in "mon-aft.rkt" fv))
 
 (define-extended-language Lambda-calculus Lambda
   (e ::= .... n)
-  (v ::= n (lambda (x ...) e))
+  (v ::= n (lambda (x) e))
   (n ::= number)
-  (C ::= hole (e ... C e ...) (lambda (x_!_ ...) C)))
+  (C ::= hole (e ... C e ...) (lambda (x) C)))
 
 (define lambda? (redex-match? Lambda-calculus e))
 (define context? (redex-match? Lambda-calculus C))
@@ -16,25 +16,32 @@
 (define-metafunction Lambda-calculus
   ;;  let : ((x e) ...) e -> e but e plus hole 
   let : ((x any) ...) any -> any
-  [(let ([x_lhs any_rhs] ...) any_body)
-   ((lambda (x_lhs ...) any_body) any_rhs ...)])
+  [(let () any_body) any_body]
+  [(let ([x_lhs any_rhs] [x_lhs-more any_rhs-more] ...) any_body)
+   ((lambda (x_lhs)
+      (let ([x_lhs-more any_rhs-more] ...)
+        any_body))
+    any_rhs)])
 
 (module+ test
-  (define C1 (term ((lambda (x y) x) hole 1)))
-  (define C2 (term ((lambda (x y) hole) 0 1)))
-  (define C3 (term (let ([x hole][y 3]) (lambda (a) (a (x 1 y 2))))))
+  ;; context tests
+  (define C1 (term (((lambda (x) (lambda (y) x)) hole) 1)))
+  (define C2 (term (((lambda (x) (lambda (y) hole)) 0) 1)))
+  (define C3 (term (let ([x hole][y 3]) (lambda (a) (a (((x 1) y) 2))))))
   
   (test-equal (context? C1) #true)
   (test-equal (context? C2) #true)
   (test-equal (context? C3) #true)
   
+  ;; plugging tests
   (define e1 (term (in-hole ,C1 1)))
   (define e2 (term (in-hole ,C2 x)))
-  (define e3 (term (in-hole ,C3 (lambda (x y z) x))))
+  (define e3 (term (in-hole ,C3 (lambda (x) (lambda (y) (lambda (z) x))))))
   
   (test-equal (lambda? e1) #true)
   (test-equal (lambda? e2) #true)
-  (test-equal (lambda? e3) #true))
+  (test-equal (lambda? e3) #true)
+  )
 
 ;; -----------------------------------------------------------------------------
 ;; model the λβv calculus, reductions only 
@@ -48,23 +55,26 @@
   ;; reduces to TWO expressions 
   (define e4 ;; a term that contains TWO βv redexes 
     (term
-     ((lambda (x y)
-        [(lambda (f) (f (x 1 y 2)))
-         (lambda (w) 42)])
-      [(lambda (x) x) (lambda (a b c) a)]
+     (((lambda (x)
+         (lambda (y)
+           [(lambda (f) (f (((x 1) y) 2)))
+            (lambda (w) 42)]))
+       [(lambda (x) x) (lambda (a) (lambda (b) (lambda (c) a)))])
       3)))
   (define e4-one-step
     (term
-     ((lambda (x y)
-        ((lambda (f) (f (x 1 y 2)))
-         (lambda (w) 42)))
-      (lambda (a b c) a)
+     (((lambda (x)
+         (lambda (y)
+           ((lambda (f) (f (((x 1) y) 2)))
+            (lambda (w) 42))))
+       (lambda (a) (lambda (b) (lambda (c) a))))
       3)))
   (define e4-other-step
     (term
-     ((lambda (x y)
-        ((lambda (w) 42) (x 1 y 2)))
-      ((lambda (x) x) (lambda (a b c) a))
+     (((lambda (x)
+         (lambda (y)
+           ((lambda (w) 42) (((x 1) y) 2))))
+       ((lambda (x) x) (lambda (a) (lambda (b) (lambda (c) a)))))
       3)))
   
   (test--> -->βv #:equiv =α/racket e4 e4-other-step e4-one-step)
@@ -73,8 +83,8 @@
 (define -->βv 
   (reduction-relation
    Lambda-calculus
-   (--> (in-hole C ((lambda (x_1 ..._n) e) v_1 ..._n))
-        (in-hole C (subst ([v_1 x_1] ...) e))
+   (--> (in-hole C ((lambda (x) e) v))
+        (in-hole C (subst ([v x]) e))
         βv)))
 
 #;
@@ -94,8 +104,8 @@
 (define s-->βv
   (reduction-relation
    Standard
-   (--> (in-hole E ((lambda (x_1 ..._n) e) v_1 ..._n))
-        (in-hole E (subst ((v_1 x_1) ...) e)))))
+   (--> (in-hole E ((lambda (x) e) v))
+        (in-hole E (subst ([v x]) e)))))
 
 ;; -----------------------------------------------------------------------------
 ;; a semantics
diff --git a/redex-doc/redex/scribblings/long-tut/lab-mon-aft.scrbl b/redex-doc/redex/scribblings/long-tut/lab-mon-aft.scrbl
index 5f0d30b7..341f2ab3 100644
--- a/redex-doc/redex/scribblings/long-tut/lab-mon-aft.scrbl
+++ b/redex-doc/redex/scribblings/long-tut/lab-mon-aft.scrbl
@@ -39,7 +39,7 @@ Here is the definition of @deftech{environment}:
 Before you get started, make sure you can create examples of
 @tech{environment}s and confirm their well-formedness.}
 
-@exercise["ex:let"]{Develop the metafunction @racket[let], which extends
+@exercise["ex:let"]{Develop the metafunction @racket[let*], which extends
  the language with a notational shorthand, also known as syntactic sugar. 
 
  Once you have this metafunction, you can write expressions such as 
@@ -48,12 +48,12 @@ Before you get started, make sure you can create examples of
 #reader scribble/comment-reader
 (racketblock
 (term 
-  (let ((x (lambda (a b c) a))
+ (let* ((x (lambda (a b c) a))
         (y (lambda (x) x)))
     (x y y y)))
 ))
 @;%
- Like Racket's @racket[let], the function elaborates surface syntax into
+ Like Racket's @racket[let*], the function elaborates surface syntax into
  core syntax:
 @;%
 @(begin
@@ -74,8 +74,8 @@ Before you get started, make sure you can create examples of
 (racketblock
 (term 
  (fv 
-  (let ((x (lambda (a b c) a))
-        (y (lambda (x) x)))
+  (let* ((x (lambda (a b c) a))
+         (y (lambda (x) x)))
     (x y y y))))
 ))
 @;%
@@ -86,8 +86,8 @@ Before you get started, make sure you can create examples of
 (racketblock
 (term 
  (bv
-  (let ((x (lambda (a b c) a))
-        (y (lambda (x) x)))
+  (let* ((x (lambda (a b c) a))
+         (y (lambda (x) x)))
     (x y y y))))
 ))
 @;%
diff --git a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
index dbfe876b..b98e2ad7 100644
--- a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
+++ b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
@@ -25,18 +25,10 @@ To start a program with Redex, start your file with
 @codeblock{#lang racket
            (require redex)}
 
-The @racket[define-language] from specifies syntax trees via tree grammars: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(define-language Lambda 
-  (e ::= x 
-         (lambda (x ...) e)
-         (e e ...))
-  (x ::= variable-not-otherwise-mentioned))
-))
-@;%
+The @racket[define-language] from specifies syntax trees via tree grammars:
+
+@code-from-file["code/mon-aft.rkt" #rx"define-language Lambda" #:eval redex-eval]
+
 The trees are somewhat concrete, which makes it easy to work with them, but
 it is confusing on those incredibly rare occasions when we want truly
 abstract syntax. 
@@ -46,54 +38,28 @@ or integers (all of Racket's integers) or naturals (all of Racket's natural
 numbers)---and many other things. 
 
 After you have a syntax, use the grammar to generate instances and check
-them (typos do sneak in). Instances are generated with @racket[term]: 
-@;
-@examples[#:label #f #:eval redex-eval
-(define e1 (term y))
-(define e2 (term (lambda (y) y)))
-(define e3 (term (lambda (x y) y)))
-(define e4 (term (,e2 ,e3)))
+them (typos do sneak in). Instances are generated with @racket[term]:
+@code-from-file["code/mon-aft.rkt"
+                #rx"define e1 [(]term"
+                #:eval redex-eval
+                #:exp-count 4
+                #:extra-code ("e4")]
 
-e4
-]
 Mouse over @racket[define]. It is @emph{not} a Redex form, it comes from
 Racket. Take a close look at the last definition. Comma anyone? 
 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(redex-match? Lambda e e4)
-))
-@;%
-
 Define yourself a predicate that tests membership: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(define lambda? (redex-match? Lambda e))
-))
-@;%
-Now you can formulate language tests: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(test-equal (lambda? e1) #true)
-(test-equal (lambda? e2) #true)
-(test-equal (lambda? e3) #true)
-(test-equal (lambda? e4) #true)
+@code-from-file["code/mon-aft.rkt" #rx"define in-Lambda[?]" #:eval redex-eval]
 
-(define eb1 (term (lambda (x x) y)))
-(define eb2 (term (lambda (x y) 3)))
+Now you can formulate language tests:
+@code-from-file["code/mon-aft.rkt" #rx"test-equal [(]in-Lambda[?] e1"
+                #:eval redex-eval #:exp-count 4]
+@code-from-file["code/mon-aft.rkt" #rx"define eb1"
+                #:eval redex-eval #:exp-count 2]
+@code-from-file["code/mon-aft.rkt" #rx"test-equal [(]in-Lambda[?] eb1"
+                #:eval redex-eval #:exp-count 2
+                #:extra-code ("(test-results)")]
 
-(test-equal (lambda? eb1) #false)
-(test-equal (lambda? eb2) #false)
-
-(test-results)
-))
-@;%
 Make sure your language contains the terms that you want and does
 @emph{not} contain those you want to exclude. Why should @racket[eb1] and
 @racket[eb2] not be in @racket[Lambda]'s set of expressions? 
@@ -105,147 +71,59 @@ To make basic statements about (parts of) your language, define
 metafunctions. Roughly, a metafunction is a function on the terms of a
 specific language. 
 
-We don't want parameter sequences with repeated variables. Can we say this
-with a metafunction?
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(define-metafunction Lambda 
-  unique-vars : x ... -> boolean)
-))
-@;%
- The second line is a Redex contract, not a type. It says
+A first meta-function might determine whether or not some sequence
+of variables has any duplicates. The second line is a Redex contract, not a type. It says
  @racket[unique-vars] consumes a sequence of @racket[x]s and produces a
  @racket[boolean]. 
 
-How do we say we don't want repeated variables? With patterns. 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(define-metafunction Lambda 
-  unique-vars : x ... -> boolean 
-  [(unique-vars) #true]
-  [(unique-vars x x_1 ... x x_2 ...) #false]
-  [(unique-vars x x_1 ...) (unique-vars x_1 ...)])
-))
-@;%
- Patterns are powerful. More later. 
+The remaining lines say that we don't want repeated variables with patterns.
+@code-from-file["code/mon-aft.rkt"
+                #rx";; unique-vars metafunction start"
+                #:eval redex-eval
+                #:skip-lines 1]
+Patterns are powerful. More later. 
 
 But, don't just define metafunctions, develop them properly: state what
 they are about, work through examples, write down the latter as tests,
 @emph{then} define the function. 
 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-;; are the identifiers in the given sequence unique?
-
-(module+ test 
-  (test-equal (term (unique-vars x y)) #true)
-  (test-equal (term (unique-vars x y x)) #false))
 
-(define-metafunction Lambda 
-  unique-vars : x ... -> boolean 
-  [(unique-vars) #true]
-  [(unique-vars x x_1 ... x x_2 ...) #false]
-  [(unique-vars x x_1 ...) (unique-vars x_1 ...)])
-
-(module+ test
-  (test-results))
-))
-@;%
-Submodules delegate the tests to where they belong and they allow us to
-  document functions by example. 
+Wrap the tests in a @racket[module+] with the name @racketidfont{test}
+to delegate the tests to a submodule where they belong, allowing us to
+document functions by example without introducing tests into client modules
+that require the module for the definitions:
+@;
+@code-from-file["code/mon-aft.rkt"
+                #rx";; unique-vars tests start"
+                #:skip-lines 1]
 
-Sadly, our language definition cannot use the @racket[unique-vars] metafunction.
-(In order to define the metafunction, we first need to define the language.)
+Here are two more metafunctions that use patterns in interesting ways:
 
-Fortunately, language definitions can employ more than Kleene patterns: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(define-language Lambda
-  (e ::=
-     x 
-     (lambda (x_!_ ...) e)
-     (e e ...))
-  (x ::= variable-not-otherwise-mentioned))
-))
-@;%
-@racket[x_!_ ...] means @racket[x] must differ from all other elements of
-this sequence 
-
-Here are two more metafunctions that use patterns in interesting ways: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-;; (subtract (x ...) x_1 ...) removes x_1 ... from (x ...)
-
-(module+ test
-  (test-equal (term (subtract (x y z x) x z)) (term (y))))
-
-(define-metafunction Lambda
-  subtract : (x ...) x ... -> (x ...)
-  [(subtract (x ...)) (x ...)]
-  [(subtract (x ...) x_1 x_2 ...)
-   (subtract (subtract1 (x ...) x_1) x_2 ...)])
-
-;; (subtract1 (x ...) x_1) removes x_1  from (x ...)
-(module+ test
-  (test-equal (term (subtract1 (x y z x) x)) (term (y z))))
-
-(define-metafunction Lambda
-  subtract1 : (x ...) x -> (x ...)
-  [(subtract1 (x_1 ... x x_2 ...) x)
-   (x_1 ... x_2new ...)
-   (where (x_2new ...) (subtract1 (x_2 ...) x))
-   (where #false (in x (x_1 ...)))]
-  [(subtract1 (x ...) x_1) (x ...)])
-
-(define-metafunction Lambda
-  in : x (x ...) -> boolean
-  [(in x (x_1 ... x x_2 ...)) #true]
-  [(in x (x_1 ...)) #false])
-
-))
-@;%
+@code-from-file["code/mon-aft.rkt"
+                #rx"[(]subtract [(]x [.][.][.][)] x_1 [.][.][.][)] removes"
+                #:exp-count 4
+                #:skip-lines 2]
 
 @; -----------------------------------------------------------------------------
 @section{Developing a Language 2}
 
 One of the first things a language designer ought to specify is
 @deftech{scope}. People often do so with a free-variables function that
-specifies which language constructs bind and which ones don't:
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-;; (fv e) computes the sequence of free variables of e
-;; a variable occurrence of @racket[x] is free in @racket[e] 
-;; if no @racket[(lambda (... x ...) ...)] @emph{dominates} its occurrence 
-
-(module+ test
-  (test-equal (term (fv x)) (term (x)))
-  (test-equal (term (fv (lambda (x) x))) (term ()))
-  (test-equal (term (fv (lambda (x) (y z x)))) (term (y z))))
-
-(define-metafunction Lambda
-  fv : e -> (x ...)
-  [(fv x) (x)]
-  [(fv (lambda (x ...) e))
-   (subtract (x_e ...) x ...)
-   (where (x_e ...) (fv e))]
-  [(fv (e_f e_a ...))
-   (x_f ... x_a ... ...)
-   (where (x_f ...) (fv e_f))
-   (where ((x_a ...) ...) ((fv e_a) ...))])
-))
-@;%
+specifies which language constructs bind and which ones don't.
+
+@racket[(fv e)] computes the sequence of free variables of e
+a variable occurrence of @racket[x] is free in @racket[e] 
+if no @racket[(lambda (x) ...)] @emph{dominates} its occurrence 
+
+
+@code-from-file["code/mon-aft.rkt"
+                #rx"[(]fv e[)] computes the sequence of free variables of e"
+                #:skip-lines 1]
+
+@code-from-file["code/mon-aft.rkt"
+                #rx";; fv metafunction start"
+                #:eval redex-eval
+                #:skip-lines 1]
 
 @margin-note{You may know it as the de Bruijn index representation.}
 @;
@@ -253,97 +131,38 @@ The best approach is to specify an α equivalence relation, that is, the
 relation that virtually eliminates variables from phrases and replaces them
 with arrows to their declarations. In the world of lambda calculus-based
 languages, this transformation is often a part of the compiler, the
-so-called static-distance phase.
-
-The function is a good example of accumulator-functions in Redex: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-;; (sd e) computes the static distance version of e
-
-(define-extended-language SD Lambda
-  (e ::= .... (K n))
-  (n ::= natural))
-
-(define sd1 (term (K 1)))
-(define sd2 (term 1))
+so-called static-distance phase. The function is a good example of
+accumulator-functions in Redex.
 
-(define SD? (redex-match? SD e))
-
-(module+ test
-  (test-equal (SD? sd1) #true))
-))
-@;%
   We have to add a means to the language to say ``arrow back to the variable
   declaration.'' We do @emph{not} edit the language definition but
   @emph{extend} the language definition instead. 
 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(define-metafunction SD
-  sd : e -> e
-  [(sd e_1) (sd/a e_1 ())])
-
-(module+ test
-  (test-equal (term (sd/a x ())) (term x))
-  (test-equal (term (sd/a x ((y) (z) (x)))) (term (K 2 0)))
-  (test-equal (term (sd/a ((lambda (x) x) (lambda (y) y)) ()))
-              (term ((lambda () (K 0 0)) (lambda () (K 0 0)))))
-  (test-equal (term (sd/a (lambda (x) (x (lambda (y) y))) ()))
-              (term (lambda () ((K 0 0) (lambda () (K 0 0))))))
-  (test-equal (term (sd/a (lambda (z x) (x (lambda (y) z))) ()))
-              (term (lambda () ((K 0 1) (lambda () (K 1 0)))))))
-
-(define-metafunction SD
-  sd/a : e ((x ...) ...) -> e
-  [(sd/a x ((x_1 ...) ... (x_0 ... x x_2 ...) (x_3 ...) ...))
-   ;; bound variable 
-   (K n_rib n_pos)
-   (where n_rib ,(length (term ((x_1 ...) ...))))
-   (where n_pos ,(length (term (x_0 ...))))
-   (where #false (in x (x_1 ... ...)))]
-  [(sd/a (lambda (x ...) e_1) (e_rest ...))
-   (lambda () (sd/a e_1 ((x ...) e_rest ...)))]
-  [(sd/a (e_fun e_arg ...) (e_rib ...))
-   ((sd/a e_fun (e_rib ...)) (sd/a e_arg (e_rib ...)) ...)]
-  [(sd/a e_1 any)
-   ;; a free variable is left alone 
-   e_1])
-))
-@;%
+@code-from-file["code/mon-aft.rkt"
+                #rx"define-extended-language SD Lambda"
+                #:eval redex-eval
+                #:exp-count 3]
+@code-from-file["code/mon-aft.rkt"
+                #rx";; SD[?] test case"
+                #:skip-lines 1]
 
-Now α equivalence is straightforward: 
 @;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-;; (=α e_1 e_2) determines whether e_1 and e_2 are α equivalent
 
-(define-extended-language Lambda/n Lambda
-  (e ::= .... n)
-  (n ::= natural))
+@code-from-file["code/mon-aft.rkt"
+                #rx";; SD metafunction"
+                #:exp-count 3]
 
-(define in-Lambda/n? (redex-match? Lambda/n e))
-
-(module+ test
-  (test-equal (term (=α (lambda (x) x) (lambda (y) y))) #true)
-  (test-equal (term (=α (lambda (x) (x 1)) (lambda (y) (y 1)))) #true)
-  (test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false))
+Now α equivalence is straightforward: 
 
-(define-metafunction SD
-  =α : e e -> boolean
-  [(=α e_1 e_2) ,(equal? (term (sd e_1)) (term (sd e_2)))])
+@code-from-file["code/mon-aft.rkt"
+                #rx"determines whether e_1 and e_2 are α equivalent"
+                #:exp-count 3]
 
-(define (=α/racket x y) (term (=α ,x ,y)))
-))
-@;%
 
 @; -----------------------------------------------------------------------------
 @section{Extending a Language: @racket[any]}
 
+
 Suppose we wish to extend @racket[Lambda] with @racket[if] and Booleans,
 like this: 
 @;%
@@ -357,7 +176,7 @@ like this:
      (if e e e)))
 ))
 @;%
- Guess what? @racket[(term (fv (lambda (x y) (if x y false))))] doesn't
+ Guess what? @racket[(term (sd (lambda (x y) (if x y false))))] doesn't
  work because @racket[false] and @racket[if] are not covered. 
 
 We want metafunctions that are as generic as possible for computing such
@@ -366,45 +185,11 @@ equivalences.
 
 Redex contracts come with @racket[any] and Redex patterns really are over
 Racket's S-expressions. This definition now works for extensions that don't
-add binders: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(module+ test
-  (test-equal (SD? sd1) #true))
-
-(define-metafunction SD
-  sd : any -> any
-  [(sd any_1) (sd/a any_1 ())])
-
-(module+ test
-  (test-equal (term (sd/a x ())) (term x))
-  (test-equal (term (sd/a x ((y) (z) (x)))) (term (K 2 0)))
-  (test-equal (term (sd/a ((lambda (x) x) (lambda (y) y)) ()))
-              (term ((lambda () (K 0 0)) (lambda () (K 0 0)))))
-  (test-equal (term (sd/a (lambda (x) (x (lambda (y) y))) ()))
-              (term (lambda () ((K 0 0) (lambda () (K 0 0))))))
-  (test-equal (term (sd/a (lambda (z x) (x (lambda (y) z))) ()))
-              (term (lambda () ((K 0 1) (lambda () (K 1 0)))))))
-
-(define-metafunction SD
-  sd/a : any ((x ...) ...) -> any
-  [(sd/a x ((x_1 ...) ... (x_0 ... x x_2 ...) (x_3 ...) ...))
-   ;; bound variable 
-   (K n_rib n_pos)
-   (where n_rib ,(length (term ((x_1 ...) ...))))
-   (where n_pos ,(length (term (x_0 ...))))
-   (where #false (in x (x_1 ... ...)))]
-  [(sd/a (lambda (x ...) any_1) (any_rest ...))
-   (lambda () (sd/a any_1 ((x ...) any_rest ...)))]
-  [(sd/a (any_fun any_arg ...) (any_rib ...))
-   ((sd/a any_fun (any_rib ...)) (sd/a any_arg (any_rib ...)) ...)]
-  [(sd/a any_1 any)
-   ;; free variable, constant, etc 
-   any_1])
-))
-@;%
+add binders:
+
+@code-from-file["code/common.rkt"
+                #rx"define-extended-language SD Lambda"
+                #:exp-count 6]
 
 @; -----------------------------------------------------------------------------
 @section{Substitution}
@@ -413,51 +198,6 @@ The last thing we need is substitution, because it @emph{is} the syntactic
 equivalent of function application. We define it with @emph{any} having
 future extensions in mind.  
 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-;; (subst ([e x] ...) e_*) substitutes e ... for x ... in e_* (hygienically)
-
-(module+ test
-  (test-equal (term (subst ([1 x][2 y]) x)) 1)
-  (test-equal (term (subst ([1 x][2 y]) y)) 2)
-  (test-equal (term (subst ([1 x][2 y]) z)) (term z))
-  (test-equal (term (subst ([1 x][2 y]) (lambda (z w) (x y))))
-              (term (lambda (z w) (1 2))))
-  (test-equal (term (subst ([1 x][2 y]) (lambda (z w) (lambda (x) (x y)))))
-              (term (lambda (z w) (lambda (x) (x 2))))
-              #:equiv =α/racket)
-  (test-equal (term (subst ((2 x)) ((lambda (x) (1 x)) x)))
-              (term ((lambda (x) (1 x)) 2))
-              #:equiv =α/racket))
-              
-              
-
-(define-metafunction Lambda
-  subst : ((any x) ...) any -> any
-  [(subst [(any_1 x_1) ... (any_x x) (any_2 x_2) ...] x) any_x]
-  [(subst [(any_1 x_1) ... ] x) x]
-  [(subst [(any_1 x_1) ... ] (lambda (x ...) any_body))
-   (lambda (x_new ...)
-     (subst ((any_1 x_1) ...)
-            (subst-raw ((x_new x) ...) any_body)))
-   (where  (x_new ...)  ,(variables-not-in (term any_body) (term (x ...)))) ]
-  [(subst [(any_1 x_1) ... ] (any ...)) ((subst [(any_1 x_1) ... ] any) ...)]
-  [(subst [(any_1 x_1) ... ] any_*) any_*])
-
-(define-metafunction Lambda
-  subst-raw : ((x x) ...) any -> any
-  [(subst-raw ((x_n1 x_o1) ... (x_new x) (x_n2 x_o2) ...) x) x_new]
-  [(subst-raw ((x_n1 x_o1) ... ) x) x]
-  [(subst-raw ((x_n1 x_o1) ... ) (lambda (x ...) any))
-   (lambda (x ...) (subst-raw ((x_n1 x_o1) ... ) any))]
-  [(subst-raw [(any_1 x_1) ... ] (any ...))
-   ((subst-raw [(any_1 x_1) ... ] any) ...)]
-  [(subst-raw [(any_1 x_1) ... ] any_*) any_*])
-
-))
-@;%
-
-
-}
+@code-from-file["code/common.rkt"
+                #rx"substitutes e [.][.][.] for x [.][.][.] in e_[*]"
+                #:exp-count 3]
diff --git a/redex-doc/redex/scribblings/long-tut/mon-mor.scrbl b/redex-doc/redex/scribblings/long-tut/mon-mor.scrbl
index 2a6d6fe1..ffff876e 100644
--- a/redex-doc/redex/scribblings/long-tut/mon-mor.scrbl
+++ b/redex-doc/redex/scribblings/long-tut/mon-mor.scrbl
@@ -74,8 +74,9 @@ All of the above is mathematics but it is just that,
 mathematics. It might be considered theory of computation,
 but it is not theory of programming languages. But we can
 use these ideas to create a theory of programming languages.
-Plotkin's 1974 TCS paper on call-by-name versus
-call-by-value shows how to create a theory of programming
+@link["https://homepages.inf.ed.ac.uk/gdp/publications/cbn_cbv_lambda.pdf"]{
+ Plotkin's 1974 TCS paper on call-by-name versus
+ call-by-value} shows how to create a theory of programming
 languages.
 
 In addition, Plotkin's paper also sketches several research programs,
diff --git a/redex-doc/redex/scribblings/long-tut/shared.rkt b/redex-doc/redex/scribblings/long-tut/shared.rkt
index 85621583..487ccc58 100644
--- a/redex-doc/redex/scribblings/long-tut/shared.rkt
+++ b/redex-doc/redex/scribblings/long-tut/shared.rkt
@@ -10,16 +10,21 @@
     scribble/example
     racket/sandbox
     scribble/core
-    scriblib/figure))
+    scriblib/figure)
+  code-from-file)
 
 ;; -----------------------------------------------------------------------------
 (require
   "exercise/ex.rkt"
   (for-label racket/base redex/reduction-semantics)
+  (for-syntax racket/base racket/match racket/list racket/port
+              syntax/parse syntax/strip-context compiler/cm-accomplice)
   scribble/manual
   scribble/core
   scribble/example
   racket/sandbox
+  racket/runtime-path
+  racket/list
   scriblib/figure)
 
 
@@ -51,3 +56,133 @@ to the top of your file:
 @;%
  }
 )
+
+;; codeblock-from-file pulls a specific hunk of lines from
+;; one of the files in code/ and generates a use of `examples`
+;; with that code in it.
+;;
+;; Supply:
+;; - the name of the file as a relative path to the source
+;;   location of the use of codeblock-from-file,
+;; - a regular expression that the first line to include must match
+;; - the evaluator to evaluate the program, with #:eval; if #:eval
+;;   is not present, the code is not evaluated and instead of `examples`
+;;   being used, `codeblock` is used.
+;; - the number of expressions that should follow (according to the
+;;   rules of read) with #:exp-count, which defaults to 1
+;; - the number of lines to skip, counting the matching line
+;;   (useful to add comments to give the regexp something to grab onto)
+;;   with #:skip-lines
+;; - and a sequence of strings to tack onto the end of the expression
+;;   these are treated as if they are extra lines in the file with
+;;   #:extra-code
+;;
+;; if the expression begins with define, define-language or a few
+;; other keywords (see the match expression below), then the code
+;; is wrapped with eval:no-prompt (see examples for docs)
+;; the highlighting and linking is based on the for-label bindings
+;; that are at the use of codeblock-from-file
+(define-syntax (code-from-file stx)
+  (syntax-parse stx
+    [(_ file:string rx-start:regexp 
+        (~optional (~seq #:eval eval))
+        (~optional (~seq #:exp-count number-of-expressions:integer))
+        (~optional (~seq #:skip-lines number-of-lines-to-skip:nat))
+        (~optional (~seq #:extra-code (extra-code:string ...))))
+     (define doing-eval? (attribute eval))
+     (define code
+       (get-code (syntax-e #'file)
+                 (syntax-e #'rx-start)
+                 (if (attribute number-of-expressions)
+                     (syntax-e #'number-of-expressions)
+                     1)
+                 (if (attribute number-of-lines-to-skip)
+                     (syntax-e #'number-of-lines-to-skip)
+                     0)
+                 (if (attribute extra-code)
+                     (map
+                      syntax-e
+                      (syntax->list #'(extra-code ...)))
+                     '())
+                 doing-eval?
+                 stx))
+     (if doing-eval?
+         #`(examples #:label #f
+                     #:eval eval
+                     #,@code)
+         #`(codeblock #:context #'#,stx
+                      #,@code))]))
+
+(begin-for-syntax
+  (define (get-code file rx:start number-of-expressions number-of-lines-to-skip extra-code doing-eval? stx)
+    (define src (syntax-source stx))
+    (define-values (src-dir _1 _2) (split-path src))
+    (define file-with-code-to-show (build-path src-dir file))
+    (register-external-file file-with-code-to-show)
+    (define-values (in out) (make-pipe))
+    (define-values (start-pos start-line end-line no-prompt?s)
+      (get-start-and-end-lines file rx:start
+                               number-of-expressions
+                               stx
+                               src-dir))
+    (set! start-line (+ start-line number-of-lines-to-skip))
+    (call-with-input-file file-with-code-to-show
+      (λ (port)
+        (for/list ([l (in-lines port)]
+                   [i (in-range end-line)]
+                   #:unless (< i start-line))
+          (displayln l out))))
+    (for ([extra-code-item (in-list extra-code)])
+      (displayln extra-code-item out))
+    (close-output-port out)
+    (port-count-lines! in)
+    (set-port-next-location! in start-line 0 start-pos)
+    (cond
+      [doing-eval?
+       (for/list ([no-prompt? (in-list (append no-prompt?s
+                                               (make-list (length extra-code)
+                                                          #f)))])
+         (define e (replace-context stx (read-syntax file-with-code-to-show in)))
+         (if no-prompt?
+             `(eval:no-prompt ,e)
+             e))]
+      [else
+       (define sp (open-output-string))
+       (copy-port in sp)
+       (list (get-output-string sp))]))
+
+  (define (get-start-and-end-lines file rx:start number-of-expressions stx src-dir)
+    (define-values (start-line start-pos)
+      (call-with-input-file (build-path src-dir file)
+        (λ (port)
+          (define count 0)
+          (let/ec escape
+            (for ([l (in-lines port)])
+              (when (regexp-match? rx:start l)
+                (escape))
+              (set! count (+ count 1)))
+            (raise-syntax-error 'codeblock-from-file
+                                (format "didn't find a line matching ~s" rx:start)
+                                stx))
+          (define-values (line col pos) (port-next-location port))
+          (values count pos))))
+    (define-values (no-prompt?s end-line)
+      (call-with-input-file (build-path src-dir file)
+        (λ (port)
+          (port-count-lines! port)
+          (for ([i (in-range start-line)])
+            (read-line port))
+          (define no-prompt?s
+            (for/list ([i (in-range number-of-expressions)])
+              (define exp (read port))
+              (when (eof-object? exp) (error 'codeblock-from-file "expression #~a not present in file" i))
+              (match exp
+                [`(define . ,stuff) #t]
+                [`(define-language . ,stuff) #t]
+                [`(define-extended-language . ,stuff) #t]
+                [`(define-metafunction . ,stuff) #t]
+                [`(test-equal . ,stuff) #t]
+                [_ #f])))
+          (define-values (line col pos) (port-next-location port))
+          (values no-prompt?s line))))
+    (values start-pos start-line end-line no-prompt?s)))
diff --git a/redex-doc/redex/scribblings/long-tut/tue-mor.scrbl b/redex-doc/redex/scribblings/long-tut/tue-mor.scrbl
index 86468ea8..474bc732 100644
--- a/redex-doc/redex/scribblings/long-tut/tue-mor.scrbl
+++ b/redex-doc/redex/scribblings/long-tut/tue-mor.scrbl
@@ -3,6 +3,10 @@
 @(require "shared.rkt"
           racket/runtime-path)
 @(define-runtime-path traces.png "traces.png")
+@(define redex-eval (let ([e (make-base-eval)])
+                      (e '(require redex/reduction-semantics
+                                   redex/scribblings/long-tut/code/common))
+                      e))
 
 @; ---------------------------------------------------------------------------------------------------
 @title[#:tag "tue-mor"]{Reductions and Semantics}
@@ -43,45 +47,21 @@ compatible with all syntactic constructions.
 An alternative and equivalent method is to introduce the notion of a
 context and to use it to generate the reduction relation (or equivalence)
 from the notion of reduction:
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(require "common.rkt")
-
-(define-extended-language Lambda-calculus Lambda
-  (e ::= .... n)
-  (n ::= natural)
-  (v ::= (lambda (x ...) e))
-   
-  ;; a context is an expression with one hole in lieu of a sub-expression 
-  (C ::=
-     hole
-     (e ... C e ...)
-     (lambda (x_!_ ...) C)))
 
-(define Context? (redex-match? Lambda-calculus C))
+@code-from-file["code/tue-mor.rkt"
+                #rx"define-extended-language"
+                #:eval redex-eval
+                #:exp-count 3]
+@code-from-file["code/tue-mor.rkt"
+                #rx";; context tests"
+                #:exp-count 6]
 
-(module+ test
-  (define C1 (term ((lambda (x y) x) hole 1)))
-  (define C2 (term ((lambda (x y) hole) 0 1)))
-  (test-equal (Context? C1) #true)
-  (test-equal (Context? C2) #true))
-))
 @;%
 Filling the hole of context with an expression yields an expression: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(module+ test
-  (define e1 (term (in-hole ,C1 1)))
-  (define e2 (term (in-hole ,C2 x)))
+@code-from-file["code/tue-mor.rkt"
+                #rx";; plugging tests"
+                #:exp-count 6]
 
-  (test-equal (in-Lambda/n? e1) #true)
-  (test-equal (in-Lambda/n? e2) #true))
-))
-@;%
 What does filling the hole of a context with a context yield?
 
 @; -----------------------------------------------------------------------------