diff --git a/collects/scribble/manual.ss b/collects/scribble/manual.ss
index 287d86d429..13f766baf4 100644
--- a/collects/scribble/manual.ss
+++ b/collects/scribble/manual.ss
@@ -172,7 +172,10 @@
            [s (regexp-replace* #px"[-\\s]+" 
                                (regexp-replace 
                                 #rx"s$" 
-                                (string-foldcase (content->string c))
+                                (regexp-replace 
+                                 #rx"ies$" 
+                                 (string-foldcase (content->string c))
+                                 "y")
                                 "")
                                " ")])
       (make-elem style
diff --git a/collects/scribblings/guide/certificates.scrbl b/collects/scribblings/guide/certificates.scrbl
new file mode 100644
index 0000000000..285a679c63
--- /dev/null
+++ b/collects/scribblings/guide/certificates.scrbl
@@ -0,0 +1,253 @@
+#reader(lib "docreader.ss" "scribble")
+@require[(lib "manual.ss" "scribble")]
+@require[(lib "eval.ss" "scribble")]
+@require["guide-utils.ss"]
+
+@require-for-syntax[mzscheme]
+
+@title[#:style 'quiet]{Syntax Certificates}
+
+A use of a macro can expand into a use of an identifier that is not
+exported from the module that binds the macro. In general, such an
+identifier must not be extracted from the expanded expression and used
+in a different context, because using the identifier in a different
+context may break invariants of the macro's module.
+
+For example, the following module exports a macro @scheme[go] that
+expands to a use of @scheme[unchecked-go]:
+
+@schemeblock[
+(module m mzscheme
+  (provide go)
+  (define (unchecked-go n x) 
+    ;; to avoid disaster, @scheme[n] must be a number
+    (+ n 17))
+  (define-syntaxKW (go stx)
+    (syntax-case stx ()
+     [(_ x)
+      #'(unchecked-go 8 x)])))
+]
+
+If the reference to @scheme[unchecked-go] is extracted from the
+expansion of @scheme[(go 'a)], then it might be inserted into a new
+expression, @scheme[(unchecked-go #f 'a)], leading to disaster. The
+@scheme[datum->syntax] procedure can be used similarly to construct
+references to an unexported identifier, even when no macro expansion
+includes a reference to the identifier.
+
+To prevent such abuses of unexported identifiers, the expander rejects
+references to unexported identifiers unless they appear in
+@defterm{certified} syntax objects. The macro expander always
+certifies a syntax object that is produced by a transformer. For
+example, when @scheme[(go 'a)] is expanded to @scheme[(unchecked-go 8
+'a)], a certificate is attached to the result @scheme[(unchecked-go 8
+'a)]. Extracting just @scheme[unchecked-go] removes the identifier
+from the certified expression, so that the reference is disallowed
+when it is inserted into @scheme[(unchecked-go #f 'a)].
+
+In addition to checking module references, the macro expander
+disallows references to local bindings where the binding identifier is
+less certified than the reference. Otherwise, the expansion of
+@scheme[(go 'a)] could be wrapped with a local binding that redirects
+@scheme[#%app] to @scheme[values], thus obtaining the value of
+@scheme[unchecked-go]. Note that a capturing @scheme[#%app] would have
+to be extracted from the expansion of @scheme[(go 'a)], since lexical
+scope would prevent an arbitrary @scheme[#%app] from capturing.  The
+act of extracting @scheme[#%app] removes its certification, whereas
+the @scheme[#%app] within the expansion is still certified; comparing
+these certifications, the macro expander rejects the local-binding
+reference, and @scheme[unchecked-go] remains protected.
+
+In much the same way that the macro expander copies properties from a
+syntax transformer's input to its output (see @secref["mz:stxprops"]),
+the expander copies certificates from a transformer's input to its
+output. Building on the previous example,
+
+@schemeblock[
+(module n mzscheme
+  (require m)
+  (provide go-more)
+  (define y 'hello)
+  (define-syntaxKW (go-more stx)
+    #'(go y)))
+]
+
+the expansion of @scheme[(go-more)] introduces a reference to the
+unexported @scheme[y] in @scheme[(go y)], and a certificate allows the
+reference to @scheme[y]. As @scheme[(go y)] is expanded to
+@scheme[(unchecked-go 8 y)], the certificate that allows @scheme[y] is
+copied over, in addition to the certificate that allows the reference
+to @scheme[unchecked-go].
+
+When a protected identifier becomes inaccessible by direct reference
+(i.e., when the current code inspector is changed so that it does not
+control the module's invocation; see @secref["mz:modprotect"]), the
+protected identifier is treated like an unexported identifier.
+
+@;------------------------------------------------------------------------
+@section[#:tag "mz:stxinactivecerts"]{Certificate Propagation}
+
+When the result of a macro expansion contains a @scheme[quote-syntax]
+form, the macro expansion's certificate must be attached to the
+resulting syntax object to support macro-generating macros. In
+general, when the macro expander encounters @scheme[quote-syntax], it
+attaches all certificates from enclosing expressions to the quoted
+syntax constant. However, the certificates are attached to the syntax
+constant as @defterm{inactive} certificates, and inactive certificates
+do not count directly for certifying identifier access. Inactive
+certificates become active when the macro expander certifies the
+result of a macro expansion; at that time, the expander removes all
+inactive certificates within the expansion result and attaches active
+versions of the certificates to the overall expansion result.
+
+For example, suppose that the @scheme[go] macro is implemented through
+a macro:
+
+@schemeblock[
+(module m mzscheme
+  (provide def-go)
+  (define (unchecked-go n x) 
+    (+ n 17))
+  (define-syntaxKW (def-go stx)
+   (syntax-case stx ()
+     [(_ go)
+      #'(define-syntaxKW (go stx)
+          (syntax-case stx ()
+           [(_ x)
+            #'(unchecked-go 8 x)]))])))
+]
+
+When @scheme[def-go] is used inside another module, the generated
+macro should legally generate expressions that use
+@scheme[unchecked-go], since @scheme[def-go] in @scheme[m] had
+complete control over the generated macro.
+
+@schemeblock[
+(module n mzscheme
+  (require m)
+  (def-go go)
+  (go 10)) ; access to @scheme[unchecked-go] is allowed
+]
+
+This example works because the expansion of @scheme[(def-go go)] is
+certified to access protected identifiers in @scheme[m], including
+@scheme[unchecked-go]. Specifically, the certified expansion is a
+definition of the macro @scheme[go], which includes a syntax-object
+constant @scheme[unchecked-go]. Since the enclosing macro declaration
+is certified, the @scheme[unchecked-go] syntax constant gets an
+inactive certificate to access protected identifiers of
+@scheme[m]. When @scheme[(go 10)] is expanded, the inactive
+certificate on @scheme[unchecked-go] is activated for the macro result
+@scheme[(unchecked-go 8 10)], and the access of @scheme[unchecked-go]
+is allowed.
+
+To see why @scheme[unchecked-go] as a syntax constant must be given an
+inactive certificate instead of an active one, it's helpful to write
+the @scheme[def-go] macro as follows:
+
+@schemeblock[
+(define-syntaxKW (def-go stx)
+ (syntax-case stx ()
+   [(_ go)
+    #'(define-syntaxKW (go stx)
+        (syntax-case stx ()
+         [(_ x)
+          (with-syntax ([ug (quote-syntax unchecked-go)])
+            #'(ug 8 x))]))]))
+]
+
+In this case, @scheme[unchecked-go] is clearly quoted as an immediate
+syntax object in the expansion of @scheme[(def-go go)]. If this syntax
+object were given an active certificate, then it would keep the
+certificate---directly on the identifier @scheme[unchecked-go]---in
+the result @scheme[(unchecked-go 8 10)]. Consequently, the
+@scheme[unchecked-go] identifier could be extracted and used with its
+certificate intact. Attaching an inactive certificate to
+@scheme[unchecked-go] and activating it only for the complete result
+@scheme[(unchecked-go 8 10)] ensures that @scheme[unchecked-go] is
+used only in the way intended by the implementor of @scheme[def-go].
+
+The @scheme[datum->syntax] procedure allows inactive certificates to
+be transferred from one syntax object to another. Such transfers are
+allowed because a macro transformer with access to the syntax object
+could already wrap it with an arbitrary context before activating the
+certificates. In practice, transferring inactive certificates is
+useful mainly to macros that implement to new template forms, such as
+@scheme[syntax/loc].
+
+@;------------------------------------------------------------------------
+@section{Internal Certificates}
+
+In some cases, a macro implementor intends to allow limited
+destructuring of a macro result without losing the result's
+certificate. For example, given the following @scheme[define-like-y]
+macro,
+
+@schemeblock[
+(module q mzscheme
+  (provide define-like-y)
+  (define y 'hello)
+  (define-syntax (define-like-y stx)
+    (syntax-case stx ()
+      [(_ id) #'(define-values (id) y)])))
+]
+
+someone may use the macro in an internal definition:
+
+@schemeblock[
+(let ()
+  (define-like-y x)
+  x)
+]
+
+The implementor of the @scheme[q] module most likely intended to allow
+such uses of @scheme[define-like-y]. To convert an internal definition
+into a @scheme[letrec] binding, however, the @scheme[define] form
+produced by @scheme[define-like-y] must be deconstructed, which would
+normally lose the certificate that allows the reference to @scheme[y].
+
+The internal use of @scheme[define-like-y] is allowed because the
+macro expander treats specially a transformer result that is a syntax
+list beginning with @scheme[define-values]. In that case, instead of
+attaching the certificate to the overall expression, the certificate
+is instead attached to each individual element of the syntax list,
+pushing the certificates into the second element of the list so that
+they are attached to the defined identifiers. Thus, a certificate is
+attached to @scheme[define-values], @scheme[x], and @scheme[y] in the
+expansion result @scheme[(define-values (x) y)], and the definition
+can be deconstructed for conversion to @scheme[letrec].
+
+Just like the new certificate that is added to a transformer result,
+old certificates from the input are similarly moved to syntax-list
+elements when the result starts with @scheme[define-values]. Thus,
+@scheme[define-like-y] could have been implemented to produce
+@scheme[(define id y)], using @scheme[define] instead of
+@scheme[define-values]. In that case, the certificate to allow
+reference to @scheme[y] would be attached initially to the expansion
+result @scheme[(define x y)], but as the @scheme[define] is expanded
+to @scheme[define-values], the certificate would be moved to the
+parts.
+
+The macro expander treats syntax-list results starting with
+@scheme[define-syntaxes] in the same way that it treats results
+starting with @scheme[define-values]. Syntax-list results starting
+with @scheme[begin] are treated similarly, except that the second
+element of the syntax list is treated like all the other elements
+(i.e., the certificate is attached to the element instead of its
+content). Furthermore, the macro expander applies this special
+handling recursively, in case a macro produces a @scheme[begin] form
+that contains nested @scheme[define-values] forms.
+
+The default application of certificates can be overridden by attaching
+a @scheme['certify-mode] property (see @secref["mz:stxprops"]) to the
+result syntax object of a macro transformer. If the property value is
+@scheme['opaque], then the certificate is attached to the syntax
+object and not its parts. If the property value is
+@scheme['transparent], then the certificate is attached to the syntax
+object's parts. If the property value is
+@scheme['transparent-binding], then the certificate is attached to the
+syntax object's parts and to the sub-parts of the second part (as for
+@scheme[define-values] and @scheme[define-syntaxes]). The
+@scheme['transparent] and @scheme['transparent-binding] modes triggers
+recursive property checking at the parts, so that the certificate can
+be pushed arbitrarily deep into a transformer's result.
diff --git a/collects/scribblings/guide/guide.scrbl b/collects/scribblings/guide/guide.scrbl
index 6d3d5bf6c7..aa9c2c4669 100644
--- a/collects/scribblings/guide/guide.scrbl
+++ b/collects/scribblings/guide/guide.scrbl
@@ -80,7 +80,7 @@ of an expression to the values for the clause:
 @section[#:tag "threads"]{Threads}
 
 @; ----------------------------------------------------------------------
-@section[#:tag "guide:macros"]{Syntactic Extension@aux-elem{ (Macros)}}
+@include-section["macros.scrbl"]
 
 
 @; ----------------------------------------------------------------------
diff --git a/collects/scribblings/guide/macros.scrbl b/collects/scribblings/guide/macros.scrbl
new file mode 100644
index 0000000000..de01493f59
--- /dev/null
+++ b/collects/scribblings/guide/macros.scrbl
@@ -0,0 +1,11 @@
+#reader(lib "docreader.ss" "scribble")
+@require[(lib "manual.ss" "scribble")]
+@require[(lib "eval.ss" "scribble")]
+@require["guide-utils.ss"]
+
+@title[#:tag "guide:macros" #:style 'toc]{Syntactic Extension@aux-elem{ (Macros)}}
+
+@local-table-of-contents[]
+
+@;------------------------------------------------------------------------
+@include-section["certificates.scrbl"]
diff --git a/collects/scribblings/reference/bytes.scrbl b/collects/scribblings/reference/bytes.scrbl
index 963521e951..1149f0c647 100644
--- a/collects/scribblings/reference/bytes.scrbl
+++ b/collects/scribblings/reference/bytes.scrbl
@@ -27,6 +27,12 @@ See also: @scheme[immutable].
 @; ----------------------------------------
 @section{Byte String Constructors, Selectors, and Mutators}
 
+@defproc[(bytes? [v any/c]) boolean?]{ Returns @scheme[#t] if @scheme[v]
+ is a byte string, @scheme[#f] otherwise.
+
+@examples[(bytes? #"Apple") (bytes? "Apple")]}
+
+
 @defproc[(make-bytes [k exact-nonnegative-integer?] [b byte? 0])
 bytes?]{ Returns a new mutable byte string of length @scheme[k] where each
 position in the byte string is initialized with the byte @scheme[b].
@@ -49,12 +55,6 @@ positions are initialized with the given @scheme[b]s.
  immutable.}
 
 
-@defproc[(bytes? [v any/c]) boolean?]{ Returns @scheme[#t] if @scheme[v]
- is a byte string, @scheme[#f] otherwise.
-
-@examples[(bytes? #"Apple") (bytes? "Apple")]}
-
-
 @defproc[(byte? [v any/c]) boolean?]{ Returns @scheme[#t] if @scheme[v] is
  a byte (i.e., an exact integer between @scheme[0] and @scheme[255]
  inclusive), @scheme[#f] otherwise.
diff --git a/collects/scribblings/reference/control.scrbl b/collects/scribblings/reference/control.scrbl
index 7876e9f3c8..1f2c3bc025 100644
--- a/collects/scribblings/reference/control.scrbl
+++ b/collects/scribblings/reference/control.scrbl
@@ -9,3 +9,4 @@
 @include-section["cont.scrbl"]
 @include-section["cont-marks.scrbl"]
 @include-section["breaks.scrbl"]
+@include-section["exit.scrbl"]
diff --git a/collects/scribblings/reference/custodians.scrbl b/collects/scribblings/reference/custodians.scrbl
index 7353d66492..bb5820350e 100644
--- a/collects/scribblings/reference/custodians.scrbl
+++ b/collects/scribblings/reference/custodians.scrbl
@@ -7,6 +7,12 @@
 See @secref["mz:custodian-model"] for basic information on the PLT
 Scheme custodian model.
 
+@defproc[(custodian? [v any/c]) boolean?]{
+
+Returns @scheme[#t] if @scheme[v] is a @tech{custodian} value,
+@scheme[#f] otherwise.}
+
+
 @defproc[(make-custodian [cust custodian? (current-custodian)]) custodian?]{
 
 Creates a new custodian that is subordinate to @scheme[cust]. When
@@ -14,6 +20,7 @@ Creates a new custodian that is subordinate to @scheme[cust]. When
 shut down all of its managed values, the new subordinate custodian is
 automatically directed to shut down its managed values as well.}
 
+
 @defproc[(custodian-shutdown-all [cust custodian?]) void?]{
 
 Closes all open ports and closes all active TCP listeners and UDP
@@ -24,11 +31,6 @@ a thread has no managers, it is killed (or suspended; see
 killed, all other shut-down actions take place before killing the
 thread.}
 
-@defproc[(custodian? [v any/c]) boolean?]{
-
-Returns @scheme[#t] if @scheme[v] is a @tech{custodian} value,
-@scheme[#f] otherwise.}
-
 
 @defparam[current-custodian cust custodian?]{
 
diff --git a/collects/scribblings/reference/data.scrbl b/collects/scribblings/reference/data.scrbl
index b1f94b4b60..deaaefeae3 100644
--- a/collects/scribblings/reference/data.scrbl
+++ b/collects/scribblings/reference/data.scrbl
@@ -166,14 +166,19 @@ of the sequence. See also @scheme[in-list].
 @; ----------------------------------------
 @subsection{Pair Constructors, Selectors, and Mutators}
 
-@defproc[(cons [a any/c] [d any/c]) pair?]{Returns a pair whose first
-element is @scheme[a] and second element is @scheme[d].}
-
 @defproc[(pair? [v any/c]) boolean?]{Returns @scheme[#t] if @scheme[v] is
 a pair, @scheme[#f] otherwise.}
 
 @defproc[(cons? [v any/c]) boolean?]{The same as @scheme[(pair? v)].}
 
+@defproc[(null? [v any/c]) boolean?]{Returns @scheme[#t] if @scheme[v] is
+the empty list, @scheme[#f] otherwise.}
+
+@defproc[(empty? [v any/c]) boolean?]{The same as @scheme[(null? v)].}
+
+@defproc[(cons [a any/c] [d any/c]) pair?]{Returns a pair whose first
+element is @scheme[a] and second element is @scheme[d].}
+
 @defproc[(car [p pair?]) any/c]{Returns the first element of the
 pair @scheme[p].}
 
@@ -188,11 +193,6 @@ pair @scheme[p].}
 
 @defthing[empty null?]{The empty list.}
 
-@defproc[(null? [v any/c]) boolean?]{Returns @scheme[#t] if @scheme[v] is
-the empty list, @scheme[#f] otherwise.}
-
-@defproc[(empty? [v any/c]) boolean?]{The same as @scheme[(null? v)].}
-
 @defproc[(list [v any/c] ...) list?]{Returns a newly allocated list
 containing the @scheme[v]s as its elements.}
 
@@ -299,10 +299,10 @@ that have a side-effect and no useful result. The constant
 @|undefined-const| is used as the initial value for @scheme[letrec]
 bindings.
 
-@defproc[(void [v any/c] ...) void?]{Returns the constant @|void-const|. Each
- @scheme[v] argument is ignored.}
-
 @defproc[(void? [v any/c]) void?]{Returns @scheme[#t] if @scheme[v] is the
  constant @|void-const|, @scheme[#f] otherwise.}
 
 
+@defproc[(void [v any/c] ...) void?]{Returns the constant @|void-const|. Each
+ @scheme[v] argument is ignored.}
+
diff --git a/collects/scribblings/reference/define-struct.scrbl b/collects/scribblings/reference/define-struct.scrbl
index a50968cab6..ecfad802f6 100644
--- a/collects/scribblings/reference/define-struct.scrbl
+++ b/collects/scribblings/reference/define-struct.scrbl
@@ -59,7 +59,7 @@ up to @math{4+2n} names:
        value. The structure is destructively updated with the new
        value, and @|void-const| is returned.}
 
- @item{@scheme[id], a transformer binding that encapsulates
+ @item{@scheme[id], a @tech{transformer binding} that encapsulates
        information about the structure type declaration. This binding
        is used to define subtypes, and it also works with the
        @scheme[shared] and @scheme[match] forms. For detailed
diff --git a/collects/scribblings/reference/eval.scrbl b/collects/scribblings/reference/eval.scrbl
new file mode 100644
index 0000000000..ed1fed1f2e
--- /dev/null
+++ b/collects/scribblings/reference/eval.scrbl
@@ -0,0 +1,368 @@
+#reader(lib "docreader.ss" "scribble")
+@require["mz.ss"]
+
+@title{Evaluation and Compilation}
+
+
+@defparam[current-eval proc (any/c . -> . any)]{
+
+A parameter that determines the current @deftech{evaluation handler}.
+The evaluation handler is a procedure that takes a top-level form and
+evaluates it, returning the resulting values. The @tech{evaluation
+handler} is called by @scheme[eval], @scheme[eval-syntax], the default
+load handler, and @scheme[read-eval-print-loop] to evaluate a
+top-level form. The handler should evaluate its argument in tail
+position.
+
+The @scheme[_top-level-form] provided to the handler can be a
+@tech{syntax object}, a compiled form, a compiled form wrapped as a
+syntax object, or an arbitrary datum.
+
+The default handler converts an arbitrary datum to a syntax object
+using @scheme[datum->syntax], and then enriches its @tech{lexical
+information} in the same way as @scheme[eval]. (If
+@scheme[_top-level-form] is a syntax object, then its @tech{lexical
+information} is not enriched.)  The default evaluation handler
+partially expands the form to splice the body of top-level
+@scheme[begin] forms into the top level (see
+@scheme[expand-to-top-form]), and then individually compiles and
+evaluates each spliced form before continuing to expand, compile, and
+evaluate later forms.}
+
+
+@defproc[(eval [top-level-form any/c]
+               [namespace namespace? (current-namespace)])
+         any]{
+
+Calls the current @tech{evaluation handler} to evaluate
+@scheme[top-level-form]. The @tech{evaluation handler} is called in
+tail position with respect to the @scheme[eval] call, and
+@scheme[parameterize]d to set @scheme[current-namespace] to
+@scheme[namespace].
+
+If @scheme[top-level-form] is a syntax object whose datum is not a
+compiled form, then its @tech{lexical information} is enriched before
+it is sent to the @tech{evaluation handler}:
+
+@itemize{
+
+ @item{If @scheme[top-level-form] is a pair whose @scheme[car] is a symbol or
+       identifier, and if applying @scheme[namespace-syntax-introduce]
+       to the (@scheme[datum->syntax]-converted) identifier produces
+       an identifier bound to @scheme[module], then only that
+       identifier is enriched.}
+
+ @item{For any other @scheme[top-level-form],
+       @scheme[namespace-syntax-introduce] is applied to the entire
+       syntax object.}
+
+}}
+
+
+@defproc[(eval-syntax [stx syntax?]
+                      [namespace namespace? (current-namespace)])
+         any]{
+
+Like @scheme[eval], except that @scheme[stx] must be a syntax object,
+and its lexical context is not enriched before it is passed to the
+@tech{evaluation handler}.}
+
+
+@defparam[current-load proc (path? (or/c symbol? false/c) . -> . any)]{
+
+A parameter that determines the current @deftech{load handler} to load
+top-level forms from a file. The @tech{load handler} is called by
+@scheme[load], @scheme[load-relative], @scheme[load/cd], and the
+default @tech{compiled-load handler}.
+
+A load handler takes two arguments: a path (see
+@secref["mz:pathutils"]) and an expected module name. The expected
+module name is a symbol when the call is to load a module declaration
+in response to a @scheme[require] (in which case the file should
+contain a module declaration), or @scheme[#f] for any other load.
+ 
+The default load handler reads forms from the file in
+@scheme[read-syntax] mode with line-counting enabled for the file
+port. It also @scheme[parameterize]s each read to set both
+@scheme[read-accept-compiled] and @scheme[read-accept-reader] to
+@scheme[#t]. After reading a single form, the form is passed to the
+current evaluation handler, wrapping the evaluation in a continuation
+prompt (see @scheme[call-with-continuation-prompt]) for the default
+continuation prompt tag with handler that propagates the abort to the
+continuation of the @scheme[load] call.
+
+If the second argument to the load handler is a symbol, then:
+
+@itemize{
+
+ @item{The @scheme[read-syntax] from the file is additionally
+       @tech{parameterize}d as follows (to provide consistent reading
+       of module source):
+
+       @schemeblock[
+       (current-readtable #f)
+       (read-case-sensitive #t)
+       (read-square-bracket-as-paren #t)
+       (read-curly-brace-as-paren #t)
+       (read-accept-box #t)
+       (read-accept-compiled #t)
+       (read-accept-bar-quote #t)
+       (read-accept-graph #t)
+       (read-decimal-as-inexact #t)
+       (read-accept-dot #t)
+       (read-accept-infix-dot #t)
+       (read-accept-quasiquote #t)
+       (read-accept-reader #t)
+       ]}
+
+ @item{If the read result is not a @schemeidfont{module} form with the
+       expected name, or if a second @scheme[read-syntax] does not
+       produce an end-of-file, then the @exnraise[exn:fail] without
+       evaluating the form that was read from the file.}
+
+ @item{The @tech{lexical information} of the initial
+       @schemeidfont{module} identifier is enriched with a binding for
+       @scheme[module], so that the form corresponds to a module
+       declaration independent of the current namespace's bindings.}
+
+}
+
+The return value from the default @tech{load handler} is the value of
+the last form from the loaded file, or @|void-const| if the file
+contains no forms. If the given path is a relative path, then it is
+resolved using the value of @scheme[current-directory].}
+
+
+@defproc[(load [file path-string?]) any]{
+
+Calls the current @tech{load handler} in tail position. The call is
+@scheme[parameterized] to set @scheme[current-load-relative-directory]
+to the directory of @scheme[file], which is resolved relative to
+the value of @scheme[current-directory].}
+
+
+@defproc[(load-relative [file path-string?]) any]{
+
+Like @scheme[load/use-compiled], but when @scheme[file] is a relative
+path, it is resolved using the value of
+@scheme[current-load-relative-directory] instead of the value of
+@scheme[current-directory] if the former is not @scheme[#f], otherwise
+@scheme[current-directory] is used.}
+
+
+@defproc[(load/cd [file path-string?]) any]{
+
+Like @scheme[load], but @scheme[load/cd] sets both
+@scheme[current-directory] and
+@scheme[current-load-relative-directory] before calling the @tech{load
+handler}.}
+
+
+@defparam[current-load-extension proc (path? (or/c symbol? false/c) . -> . any)]{
+
+A parameter that determines a @deftech{extension-load handler}, which is
+called by @scheme[load-extension] and the default @tech{compiled-load
+handler}.
+
+An @tech{extension-load handler} takes the same arguments as a
+@tech{load handler}, but the file should be a platform-specific
+@deftech{dynamic extension}, typically with the file suffix @file{.so}
+(Unix), @file{.dll} (Windows), or @file{.dylib} (Mac OS X).  The file
+is loaded using internal, OS-specific primitives. See
+@secref["inside-mzscheme"] for more information on @tech{dynamic
+extensions}.}
+
+
+@defproc[(load-extension [file path-string?]) any]{
+
+Sets @scheme[current-load-relative-directory] like @scheme[load], and
+calls the @tech{extension-load handler} in tail position.}
+
+
+@defproc[(load-relative-extension [file path-string?]) any]{
+
+Like @scheme[load-exension], but resolves @scheme[file] using
+@scheme[current-load-relative-directory] like @scheme[load-relative].}
+
+
+@defparam[current-load/use-compiled proc (path? (or/c symbol? false/c) . -> . any)]{
+
+A parameter that determines the current @deftech{compiled-load
+handler} to load from a file that may have a compiled form. The
+@tech{compiled-load handler} is called by @scheme[load/use-compiled].
+
+The protocol for a @tech{compiled-load handler} is the same as for the
+@scheme{load handler} (see @scheme[current-load]), except that a
+@tech{compiled-load handler} is expected to set
+@scheme[current-load-relative-directory] itself. The default
+@tech{compiled-load handler}, however, checks for @file{.zo} files
+(usually produced with @scheme[compile-file]) and @file{.so} (Unix),
+@file{.dll} (Windows), or @file{.dylib} (Mac OS X) files.
+
+The check for a compiled file occurs whenever the given path
+@scheme[_file] ends with any extension (e.g., @file{.ss} or
+@file{.scm}), and the check consults the subdirectories indicated by
+the @scheme[use-compiled-file-paths] parameter relative to
+@scheme[_file].  The subdirectories are checked in order. A @file{.zo}
+version of the file is loaded if it exists directly in one of the
+indicated subdirectories, or a @file{.so}/@file{.dll}/@file{.dylib}
+version of the file is loaded if it exists within a @file{native}
+subdirectory of a @scheme[use-compiled-file-paths] directory, in an
+even deeper subdirectory as named by
+@scheme[system-library-subpath]. A compiled file is loaded only if its
+modification date is not older than the date for @scheme[_file]. If
+both @file{.zo} and @file{.so}/@file{.dll}/@file{.dylib} files are
+available, the @file{.so}/@file{.dll}/@file{.dylib} file is used.
+
+Multiple files can be combined into a single
+@file{.so}/@file{.dll}/@file{.dylib} file by creating a special file
+@file{_loader.so}, @file{_loader.dll}, or
+@file{_loader.dylib}. When such a file is present where a normal
+@file{.so}/@file{.dll}/@file{.dylib} would be loaded, then the
+@file{_loader} file is first loaded via @scheme[load-extension]. The
+result returned by @file{_loader} must be a procedure that accepts a
+symbol. This procedure will be called with a symbol matching the base
+part of @scheme[_file] (without the directory path part of the name
+and without the filename extension), and the result must be two
+values; if @scheme[#f] is returned as the first result, then
+@scheme[load/use-compiled] ignores @file{_loader} for @scheme[_file]
+and continues as normal. Otherwise, the first return value is yet
+another procedure. When this procedure is applied to no arguments, it
+should have the same effect as loading @scheme[_file]. The second
+return value is either a symbol or @scheme[#f]; a symbol indicates
+that calling the returned procedure has the effect of declaring the
+module named by the symbol (which is potentially useful information to
+a @tech{load handler}).
+
+While a @file{.zo}, @file{.so}, @file{.dll}, or @file{.dylib} file is
+loaded (or while a thunk returned by @file{_loader} is invoked), the
+current @scheme[load-relative] directory is set to the directory of
+the original @scheme[_file].
+
+If the original @scheme[_file] is loaded or a @file{.zo} variant is
+loaded, the @tech{load handler} is called to load the file. If any
+other kind of file is loaded, the @tech{extension-load handler} is
+called.}
+
+
+@defproc[(load/use-compiled [file path-string?]) any]{
+
+Calls the current @tech{compiled-load handler} in tail position.}
+
+
+@defparam[current-load-relative-directory path 
+          (and/c path-string?
+                 complete-path?)]{     
+
+A parameter that is set by @scheme[load], @scheme[load-relative],
+@scheme[load-extension], @scheme[load-relative-extension], and the
+default @tech{compiled-load handler}, and used by
+@scheme[load-relative], @scheme[load-relative-extension], and the
+default @tech{compiled-load handler}.
+
+When a new path or string is provided as the parameter's value, it is
+immediately expanded (see @secref["mz:pathutils"]) and converted to a
+path. (The directory need not exist.)}
+
+
+@defparam[use-compiled-file-paths paths (listof path?)]{
+
+A list of relative paths, which defaults to @scheme[(list
+(string->path "compiled"))]. It is used by the @tech{compiled-load
+handler} (see @scheme[current-load/use-compiled]).}
+
+
+@defproc[(read-eval-print-loop) any]{
+
+Starts a new REPL using the current input, output, and error
+ports. The REPL wraps each evaluation with a continuation prompt using
+the default continuation prompt tag and prompt handler (see
+@scheme[call-with-continuation-prompt]). The REPL also wraps the read
+and print operations with a prompt for the default tag whose handler
+ignores abort arguments and continues the loop. The
+@scheme[read-eval-print-loop] procedure does not return until
+@scheme[eof] is read, at which point it returns @|void-const|.
+
+The @scheme[read-eval-print-loop] procedure can be configured through
+the @scheme[current-prompt-read], @scheme[current-eval], and
+@scheme[current-print] parameters.}
+
+
+@defparam[current-prompt-read proc (-> any)]{
+
+A parameter that determines a procedure that takes no arguments,
+displays a prompt string, and returns a top-level form to
+evaluate. This procedure is called by the read phase of
+@scheme[read-eval-print-loop].  The default prompt read handler prints
+@litchar{> } and returns the result of
+
+@schemeblock[
+(parameterize ((read-accept-reader #t))
+  (read-syntax))
+]}
+
+
+@defparam[current-compile proc (any/c boolean? . -> . compiled-expression?)]{
+
+A parameter that determines the current @deftech{compilation handler}.
+The @tech{compilation handler} is a procedure that takes a top-level form and
+returns a compiled form; see see @secref["mz:compilation-model"] for
+more information on compilation.
+
+The @tech{compilation handler} is called by @scheme[compile], and
+indirectly by the default @tech{evaluation handler} and the default
+@tech{load handler}.
+
+The handler's second argument is @scheme[#t] if the compiled form will
+be used only for immediate evaluation, or @scheme[#f] if the compiled
+form may be saved for later use; the default compilation handler is
+optimized for the special case of immediate evaluation.
+
+When a compiled form is written to an output port, the written form
+starts with @litchar{#~}.  These forms are essentially assembly code
+for PLT Scheme, and reading such an form produces a compiled form (as
+long as the @scheme[read-accept-compiled] parameter is set to
+@scheme[#t]).
+
+When a compiled form contains syntax object constants, the
+@litchar{#~}-marshaled form drops location information and properties
+(@secref["mz:stxprops"]) for the @tech{syntax objects}.
+
+Compiled code parsed from @litchar{#~} may contain references to
+unexported or protected bindings from a module. At read time, such
+references are associated with the current code inspector (see
+@scheme[current-code-inspector]), and the code will only execute if
+that inspector controls the relevant module invocation (see
+@secref["mz:modprotect"]).
+
+A compiled-form object may contain @tech{uninterned} symbols (see
+@secref["mz:symbols"]) that were created by @scheme[gensym] or
+@scheme[string->uninterned-symbol]. When the compiled object is read
+via @litchar{#~}, each uninterned symbol in the original form is
+mapped to a new uninterned symbol, where multiple instances of a
+single symbol are consistently mapped to the same new symbol. The
+original and new symbols have the same printed representation.
+
+Due to the above restrictions, do not use @scheme[gensym] or
+@scheme[string->uninterned-symbol] to construct an identifier for a
+top-level or module binding. Instead, generate distinct identifiers
+either with @scheme[generate-temporaries] or by applying the result of
+@scheme[make-syntax-introducer] to an existing identifier.}
+
+
+@defproc[(compile [top-level-form any/c]) compiled-expression?]{
+
+Like @scheme[eval], but calls the current @tech{compilation handler} in
+tail position with @scheme[top-level-form].}
+
+
+@defproc[(compile-syntax [stx syntax?]) compiled-expression?]{
+
+Like @scheme[eval-syntax], but calls the current @tech{compile
+handler} in tail position with @scheme[stx].}
+
+
+@defproc[(compiled-expression? [v any/c]) boolean?]{
+
+Returns @scheme[#t] if @scheme[v] is a compiled form, @scheme[#f]
+otherwise.}
diff --git a/collects/scribblings/reference/evts.scrbl b/collects/scribblings/reference/evts.scrbl
index 673ebcf341..a416a97cf4 100644
--- a/collects/scribblings/reference/evts.scrbl
+++ b/collects/scribblings/reference/evts.scrbl
@@ -178,6 +178,12 @@ types can generate events (see @scheme[prop:evt]).
 
 @;------------------------------------------------------------------------
 
+@defproc[(evt? [v any/c]) boolean?]{
+
+Returns @scheme[#t] if @scheme[v] is a @tech{synchronizable event},
+@scheme[#f] otherwise.}
+
+
 @defproc[(sync [evt evt?] ...+) any]{
 
 Blocks as long as none of the @tech{synchronizable events}
@@ -292,11 +298,6 @@ less than @scheme[msecs], and it is ready when
 more than @scheme[msecs].}
 
 
-@defproc[(evt? [v any/c]) boolean?]{
-
-Returns @scheme[#t] if @scheme[v] is a @tech{synchronizable event},
-@scheme[#f] otherwise.}
-
 @defproc[(handle-evt? [evt evt?]) boolean?]{
 
 Returns @scheme[#t] if @scheme[evt] was created by @scheme[handle-evt]
diff --git a/collects/scribblings/reference/exit.scrbl b/collects/scribblings/reference/exit.scrbl
new file mode 100644
index 0000000000..c9275c1dc4
--- /dev/null
+++ b/collects/scribblings/reference/exit.scrbl
@@ -0,0 +1,23 @@
+#reader(lib "docreader.ss" "scribble")
+@require["mz.ss"]
+
+@title{Exiting}
+
+@defproc[(exit [v any/c #t]) any]{
+
+Passes @scheme[v] to the current @tech{exit handler}. If the exit
+handler does not escape or terminate the thread, @|void-const| is
+returned.}
+
+
+@defparam[exit-handler proc (any/c . -> . any)]{
+
+A parameter that determines the current @deftech{exit handler}. The
+@tech{exit handler} is called by @scheme[exit].
+
+The default @tech{exit handler} in the @exec{mzscheme} executable
+takes any argument and shuts down the OS-level Scheme process. The
+argument is used as the OS-level exit code if it is an exact integer
+between @scheme[1] and @scheme[255] (which normally means
+``failure''); otherwise, the exit code is @scheme[0], (which normally
+means ``success'').}
diff --git a/collects/scribblings/reference/macros.scrbl b/collects/scribblings/reference/macros.scrbl
index 620af05635..a6e7388d19 100644
--- a/collects/scribblings/reference/macros.scrbl
+++ b/collects/scribblings/reference/macros.scrbl
@@ -15,3 +15,6 @@ called.
 @include-section["stx-ops.scrbl"]
 @include-section["stx-comp.scrbl"]
 @include-section["stx-trans.scrbl"]
+@include-section["stx-props.scrbl"]
+@include-section["stx-certs.scrbl"]
+@include-section["stx-expand.scrbl"]
diff --git a/collects/scribblings/reference/module-reflect.scrbl b/collects/scribblings/reference/module-reflect.scrbl
new file mode 100644
index 0000000000..3a619e7d3e
--- /dev/null
+++ b/collects/scribblings/reference/module-reflect.scrbl
@@ -0,0 +1,301 @@
+#reader(lib "docreader.ss" "scribble")
+@require["mz.ss"]
+
+@title{Module Names and Loading}
+
+@;------------------------------------------------------------------------
+@section[#:tag "mz:modnameresolver"]{Resolving Module Names}
+
+The name of a declared module is either a symbol or a @deftech{resolved
+module path}. A symbol normally refers to a predefined module or
+module declared through reflective evaluation (e.g., @scheme[eval]). A
+@tech{resolved module path} encapsulates a filesystem path (see
+@secref["mz:pathutils"]) and normally refers to a module declaration
+that was loaded on demand via @scheme[require] or other forms.
+
+@defproc[(resolved-module-path? [v any/c]) boolean?]{
+
+Returns @scheme[#f] if @scheme[v] is a @tech{resolved module path},
+@scheme[#f] otherwise.}
+
+@defproc[(make-resolved-module-path [path path-string?])
+         resolved-module-path?]{
+
+Returns a @tech{resolved module path} that encapsulates @scheme[path]
+as relative to @scheme[current-directory] and expanded (see
+@scheme[expand-path]), simplified (see @scheme[simplify-path]), and
+with all but the last path element case-normalized (see
+@scheme[normal-case-path]).
+
+A @tech{resolved module path} is interned. That is, if two
+@tech{resolved module path} values encapsulate paths that are
+@scheme{equal?}, then the @tech{resolved module path} values are
+@scheme{eq?}.}
+
+@defproc[(resolved-module-path->path [module-path resolved-module-path?])
+         path?]{
+
+Returns the path encapsulated by a @tech{resolved module path}.}
+
+
+@defproc[(module-path? [v any/c]) boolean?]{
+
+Returns @scheme[#t] if @scheme[v] corresponds to a datum that matches
+the grammar for @scheme[_module-path] for @scheme[require],
+@scheme[#f] otherwise.}
+
+
+@defparam[current-module-name-resolver proc 
+           (case->
+            ((or/c symbol? resolved-module-path?)
+             . -> . 
+             any)
+            ((or/c module-path? path?)
+             (or/c false/c symbol? resolved-module-path?) 
+             boolean?
+             . -> . 
+             (or/c symbol? resolved-module-path?)))]{
+
+A parameter that determines the current @deftech{module name
+resolver}, which manages the conversion from other kinds of module
+references to a symbol or @tech{resolved module path}. For example,
+when the expander encounters @scheme[(require _module-path)] where
+@scheme[_module-path] is not an identifier, then the expander passes
+@scheme['_module-path] to the module name resolver to obtain a symbol
+or resolved module path. When such a @scheme[require] appears within a
+module, the @deftech{module path resolver} is also given the name of
+the enclosing module, so that a relative reference can be converted to
+an absolute symbol or @tech{resolved module path}.
+
+A @tech{module name resolver} takes one and three arguments:
+%
+@itemize{
+
+  @item{When given one argument, it is a name for a module declaration
+  that is already loaded. Such a call to the module name resolver is a
+  notification that the corresponding module does not need to be
+  loaded (for the current namespace, or any other namespace that
+  shares the same module registry). The module name resolver's result
+  is ignored.}
+ 
+  @item{When given three arguments, the first is a module path, either
+  equivalent to a quoted @scheme[module-path] for @scheme[require] or
+  a file system path.  The second is name for the source module, if
+  any, to which the path is relative; f the second argument is
+  @scheme[#f], the module path is relative to @scheme[(or
+  (current-load-relative-directory) (current-directory))].  If the
+  argument is @scheme[#t], then the module declaration should be
+  loaded (if it is not already), otherwise the module path should be
+  simply resolved to a name. The result is the resolved name.}
+
+}
+
+For the second case, the standard module name resolver keeps a
+per-registry table of loaded module name. If a resolved module path is
+not in the table, and @scheme[#f] is not provided as the third
+argument to the @tech{module name resolver}, then the name is put into
+the table and the corresponding file is loaded with a variant of
+@scheme[load/use-compiled] that passes the expected module name to the
+@tech{compiled-load handler}.
+
+While loading a file, the default @tech{module name resolver} sets the
+@scheme[current-module-name-prefix] parameter, so that the name of any
+module declared in the loaded file is given a prefix. The resolver
+sets the prefix to the resolved module name, minus the de-suffixed
+file name. Also, the default @tech{module name resolver} records in a
+private @tech{continuation mark} the filename being loaded, and it
+checks whether such a mark already exists; if such a continuation mark
+does exist in the current continuation, then the @exnraise[exn:fail]
+with a message about a dependency cycle.
+
+Module loading is suppressed (i.e., @scheme[#f] is supplied as a third
+argument to the module name resolver) when resolving module paths in
+syntax objects (see @secref["mz:stxobj"]). When a syntax object is
+manipulated, the current namespace might not match the original
+namespace for the syntax object, and the module should not necessarily
+be loaded in the current namespace.
+
+The current module name resolver is called with a single argument by
+@scheme[namespace-attach-module] to notify the resolver that a module
+was attached to the current namespace (and should not be loaded in the
+future for the namespace's registry). No other Scheme operation
+invokes the module name resolver with a single argument, but other
+tools (such as DrScheme) might call this resolver in this mode to
+avoid redundant module loads.}
+
+
+@defparam[current-module-name-prefix prefix (or/c path? false/c)]{
+
+A parameter that determines a prefix used when evaluating a
+@scheme[module] declaration when the prefix is not @scheme[#f]. In
+that case, the quoted form of the @scheme[_id] from the
+@scheme[module] declaration is converted to a path element (via
+@scheme[symbol->string] and @scheme[string->path-element]), combined
+with the prefix (via @scheme[build-path]), and then converted to a
+@tech{resolved module path} (via @scheme[make-resolved-module-path])
+which is used as the name of the declared module.}
+
+@;------------------------------------------------------------------------
+@section[#:tag "mz:modpathidx"]{Compiled Modules and References}
+
+While expanding a @scheme[module] declaration, the expander resolves
+module paths for imports to load module declarations as necessary and
+to determine imported bindings, but the compiled form of a
+@scheme[module] declaration preserves the original module path.
+Consequently, a compiled module can be moved to another filesystem,
+where the module name resolver can resolve inter-module references
+among compiled code.
+
+When a module reference is extracted from compiled form (see
+@scheme[module-compiled-imports]) or from syntax objects in macro
+expansion (see @secref["mz:stxops"]), the module reference is
+typically reported in the form of a @deftech{module path index}. A
+@tech{module path index} is a semi-interned (multiple references to
+the same relative module tend to use the same @tech{module path index}
+value, but not always) opaque value that encodes a module path (see
+@scheme[module-path?])  and another @tech{module path index} to which
+it is relative.
+
+A @tech{module path index} that uses both @scheme[#f] for its path and
+base @tech{module path index} represents ``self''---i.e., the module
+declaration that was the source of the @tech{module path index}---and
+such a @tech{module path index} is always used as the root for a chain
+of @tech{module path index}. For example, when extracting information
+about an identifier's binding within a module, if the identifier is
+bound by a definition within the same module, the identifier's source
+module is reported using the ``self'' @tech{module path index}. If the
+identifier is instead defined in a module that is imported via a
+module path (as opposed to a literal module name), then the
+identifier's source module will be reported using a @tech{module path
+index} that contains the @scheme[require]d module path and the
+``self'' @tech{module path index}.
+
+
+A @tech{module path index} has state. When it is @deftech{resolved} to
+a symbolic module name, then the symbol or @tech{resolved module path}
+is stored with the @tech{module path index}. In particular, when a
+module is loaded, its root @tech{module path index} is resolved to
+match the module's declaration-time name. This resolved path is
+forgotten, however, in identifiers that the module contributes to the
+compiled and marshaled form of other modules. This transient nature of
+resolved names allows the module code to be loaded with a different
+resolved name than the name when it was compiled.
+
+Where a @tech{module path index} is expected, a symbol can usually
+take its place, representing a literal module name. A symbol is used
+instead of a @tech{module path index} when a module is imported using
+its name directly with @scheme[require] instead of a module path (in
+which case the symbol is also the resolved name of the module).
+
+@defproc[(module-path-index? [v any/c]) boolean?]{
+
+Returns @scheme[#t] if @scheme[v] is a @tech{module path index},
+@scheme[#f] otherwise.}
+
+
+@defproc[(module-path-index-resolve [mpi module-path-index?])
+         (or/c symbol? resolved-module-path?)]{
+
+Returns a symbol or @tech{resolved module path} for the resolved
+module name, computing the resolved name (and storing it in
+@scheme[mpi]) if it has not been computed before.
+
+Resolving a @tech{module path index} uses the current @tech{module
+name resolver} (see @scheme[current-module-name-resolver]). Depending
+on the kind of module paths encapsulated by @scheme[mpi], the computed
+resolved name can depend on the value of
+@scheme[current-load-relative-directory] or
+@scheme[current-directory].}
+
+
+@defproc[(module-path-index-split [mpi module-path-index?])
+         (values (or/c (and/c module-path? (not/c symbol?)) false/c)
+                 (or/c module-path-index? false/c))]{
+
+Returns two values: a module path, and a base @tech{module path
+index}, symbol, or @scheme[#f] to which the module path is relative.
+
+A @scheme[#f] second result means that the path is relative to an
+unspecified directory (i.e., its resolution depends on the value of
+@scheme[current-load-relative-directory] and/or
+@scheme[current-directory]).
+
+A @scheme[#f] for the first result implies a @scheme[#f] for the
+second result, and means that @scheme[mpi] represents ``self'' (see
+above).}
+
+@defproc[(module-path-index-join [path (or/c (and/c module-path? (not/c symbol?))
+                                             false/c)]
+                                 [mpi (or/c module-path-index? false/c)])
+         module-path-index?]{
+
+Combines @scheme[path] and @scheme[mpi] to create a new @tech{module
+path index}. The @scheme[path] argument can @scheme[#f] only if
+@scheme[mpi] i also @scheme[false].}
+
+@defproc[(compiled-module-expression? [v any/c]) boolean?]{
+
+Returns @scheme[#t] if @scheme[v] is a compiled @scheme[module]
+declaration, @scheme[#f] otherwise. See also
+@secref["mz:compilation"].}
+
+
+@defproc[(module-compiled-name [compiled-module-code compiled-module-expression?])
+         symbol?]{
+
+Takes a module declaration in compiled form and returns a symbol for
+the module's declared name.}
+
+
+@defproc[(module-compiled-imports [compiled-module-code compiled-module-expression?])
+         (values (listof (or/c module-path-index? symbol?))
+                 (listof (or/c module-path-index? symbol?))
+                 (listof (or/c module-path-index? symbol?)))]{
+
+Takes a module declaration in compiled form and returns three values:
+a list of module references for the module's explicit imports, a list
+of module references for the module's explicit for-syntax imports, and
+a list of module references for the module's explicit for-template
+imports.}
+
+@defproc[(module-compiled-exports [compiled-module-code compiled-module-expression?])
+         (values (listof symbol?)
+                 (listof symbol?))]{
+
+Takes a module declaration in compiled form and returns two values: a
+list of symbols for the module's explicit variable exports, a list
+symbols for the module's explicit syntax exports.}
+
+@;------------------------------------------------------------------------
+@section[#:tag "mz:dynreq"]{Dynamic Module Access}
+
+@defproc[(dynamic-require [mod module-path?][provided (or/c symbol? false/c void?)]) 
+         any]{
+
+Dynamically instantiates the module specified by @scheme[mod] for
+@tech{phase} 0 in the current namespace's registry, if it is not yet
+instantiated. If @scheme[mod] is not a symbol, the current
+@tech{module name resolver} may load a module declaration to resolve
+it (see @scheme[current-module-name-resolver]); the path is resolved
+relative to @scheme[current-load-relative-directory] and/or
+@scheme[current-directory].
+
+If @scheme[provided] is @scheme[#f], then the result is
+@|void-const|. Otherwise, when @scheme[provided] is a symbol, the
+value of the module's export with the given name is returned. If the
+module exports @scheme[provide] as syntax, then a use of the binding
+is expanded and evaluated (in a fresh namespace to which the module is
+attached). If the module has no such exported variable or syntax, or
+if the variable is protected (see @secref["mz:modprotect"]), the
+@exnraise[exn:fail:contract].
+
+If @scheme[provided] is @|void-const|, then the module is
+@tech{visit}ed (see @secref["mz:mod-parse"]), but not
+@tech{instantiate}d. The result is @|void-const|.}
+
+
+@defproc[(dynamic-require-for-syntax [mod module-path?]
+                                     [provided (or/c symbol? false/c)])
+         any]{
+
+Like @scheme[dynamic-require], but in @tech{phase} 1.}
diff --git a/collects/scribblings/reference/namespaces.scrbl b/collects/scribblings/reference/namespaces.scrbl
index 2c58c1c2ac..5766c8b01e 100644
--- a/collects/scribblings/reference/namespaces.scrbl
+++ b/collects/scribblings/reference/namespaces.scrbl
@@ -14,6 +14,13 @@ providing the namespace to procedures such as @scheme[eval] and
 
 [FIXME: define the initial namespace.]
 
+
+@defproc[(namespace? [v any/c]) boolean?]{
+
+Returns @scheme[#t] if @scheme[v] is a namespace value, @scheme[#f]
+otherwise.}
+
+
 @defproc[(make-namespace [flag (one-of/c 'initial 'empty) 'initial]) namespace?]{
 
 Creates a new namespace with a new module registry. The @scheme[flag]
@@ -32,11 +39,6 @@ is an option that determines the initial bindings in the namespace:
 
 }}
 
-@defproc[(namespace? [v any/c]) boolean?]{
-
-Returns @scheme[#t] if @scheme[v] is a namespace value, @scheme[#f]
-otherwise.}
-
 
 @defproc[(namespace-symbol->identifier [sym symbol?]) identifier?]{
 
diff --git a/collects/scribblings/reference/reference.scrbl b/collects/scribblings/reference/reference.scrbl
index f126d6165a..fe80899f5f 100644
--- a/collects/scribblings/reference/reference.scrbl
+++ b/collects/scribblings/reference/reference.scrbl
@@ -22,8 +22,8 @@ language.
 @include-section["control.scrbl"]
 @include-section["concurrency.scrbl"]
 @include-section["macros.scrbl"]
-@include-section["security.scrbl"]
 @include-section["io.scrbl"]
+@include-section["security.scrbl"]
 @include-section["os.scrbl"]
 @include-section["memory.scrbl"]
 
diff --git a/collects/scribblings/reference/regexps.scrbl b/collects/scribblings/reference/regexps.scrbl
index 3e921262db..d930e7c618 100644
--- a/collects/scribblings/reference/regexps.scrbl
+++ b/collects/scribblings/reference/regexps.scrbl
@@ -101,6 +101,31 @@ arbitrarily large sequence).
 @;------------------------------------------------------------------------
 @section{Regexp Constructors}
 
+@defproc[(regexp? [v any/c]) boolean?]{
+
+Returns @scheme[#t] if @scheme[v] is a regexp value created by
+@scheme[regexp] or @scheme[pregexp], @scheme[#f] otherwise.}
+
+
+@defproc[(pregexp? [v any/c]) boolean?]{
+
+Returns @scheme[#t] if @scheme[v] is a regexp value created by
+@scheme[pregexp] (not @scheme[regexp]), @scheme[#f] otherwise.}
+
+
+@defproc[(byte-regexp? [v any/c]) boolean?]{
+
+Returns @scheme[#t] if @scheme[v] is a regexp value created by
+@scheme[byte-regexp] or @scheme[byte-pregexp], @scheme[#f] otherwise.}
+
+
+@defproc[(byte-pregexp? [v any/c]) boolean?]{
+
+Returns @scheme[#t] if @scheme[v] is a regexp value created by
+@scheme[byte-pregexp] (not @scheme[byte-regexp]), @scheme[#f]
+otherwise.}
+
+
 @defproc[(regexp [str string?]) regexp?]{
 
 Takes a string representation of a regular expression (using the
@@ -131,16 +156,6 @@ Like @scheme[regexp], except that it uses a slightly different syntax
 (regexp? #px"ap*le")
 ]}
 
-@defproc[(regexp? [v any/c]) boolean?]{
-
-Returns @scheme[#t] if @scheme[v] is a regexp value created by
-@scheme[regexp] or @scheme[pregexp], @scheme[#f] otherwise.}
-
-@defproc[(pregexp? [v any/c]) boolean?]{
-
-Returns @scheme[#t] if @scheme[v] is a regexp value created by
-@scheme[pregexp] (not @scheme[regexp]), @scheme[#f] otherwise.}
-
 @defproc[(byte-regexp [bstr bytes?]) byte-regexp?]{
 
 Takes a byte-string representation of a regular expression (using the
@@ -166,22 +181,11 @@ syntax (see @secref["mz:regexp-syntax"]). The result can be used with
 (byte-pregexp #"ap*le")
 ]}
 
-@defproc[(byte-regexp? [v any/c]) boolean?]{
-
-Returns @scheme[#t] if @scheme[v] is a regexp value created by
-@scheme[byte-regexp] or @scheme[byte-pregexp], @scheme[#f] otherwise.}
-
-@defproc[(byte-pregexp? [v any/c]) boolean?]{
-
-Returns @scheme[#t] if @scheme[v] is a regexp value created by
-@scheme[byte-pregexp] (not @scheme[byte-regexp]), @scheme[#f]
-otherwise.}
-
 
 @;------------------------------------------------------------------------
 @section{Regexp Matching}
 
-@defproc[(regexp-match [pattern (or/c string? bytes? regexp? bytes-regexp?)]
+@defproc[(regexp-match [pattern (or/c string? bytes? regexp? byte-regexp?)]
                        [input (or/c string? bytes? input-port?)]
                        [start-pos nonnegative-exact-integer? 0]
                        [end-pos (or/c nonnegative-exact-integer? false/c) #f]
@@ -271,7 +275,7 @@ bytes. To avoid such interleaving, use @scheme[regexp-match-peek]
 (with a @scheme[progress-evt] argument) followed by
 @scheme[port-commit-peeked].}
 
-@defproc[(regexp-match-positions [pattern (or/c string? bytes? regexp? bytes-regexp?)]
+@defproc[(regexp-match-positions [pattern (or/c string? bytes? regexp? byte-regexp?)]
                         [input (or/c string? bytes? input-port?)]
                         [start-pos nonnegative-exact-integer? 0]
                         [end-pos (or/c nonnegative-exact-integer? false/c) #f]
@@ -295,7 +299,7 @@ Range results are returned in a @scheme[substring]- and
 positions indicate the number of bytes that were read, including
 @scheme[start-pos], before the first matching byte.}
 
-@defproc[(regexp-match? [pattern (or/c string? bytes? regexp? bytes-regexp?)]
+@defproc[(regexp-match? [pattern (or/c string? bytes? regexp? byte-regexp?)]
                         [input (or/c string? bytes? input-port?)]
                         [start-pos nonnegative-exact-integer? 0]
                         [end-pos (or/c nonnegative-exact-integer? false/c) #f]
@@ -305,7 +309,7 @@ positions indicate the number of bytes that were read, including
 Like @scheme[regexp-match], but returns merely @scheme[#t] when the
 match succeeds, @scheme[#f] otherwise.}
 
-@defproc[(regexp-match-peek [pattern (or/c string? bytes? regexp? bytes-regexp?)]
+@defproc[(regexp-match-peek [pattern (or/c string? bytes? regexp? byte-regexp?)]
                             [input input-port?]
                             [start-pos nonnegative-exact-integer? 0]
                             [end-pos (or/c nonnegative-exact-integer? false/c) #f]
@@ -324,7 +328,7 @@ and returns @scheme[#f]. The @scheme[progress] argument can be
 information if another process meanwhile reads from
 @scheme[input-port].}
 
-@defproc[(regexp-match-peek-positions [pattern (or/c string? bytes? regexp? bytes-regexp?)]
+@defproc[(regexp-match-peek-positions [pattern (or/c string? bytes? regexp? byte-regexp?)]
                             [input input-port?]
                             [start-pos nonnegative-exact-integer? 0]
                             [end-pos (or/c nonnegative-exact-integer? false/c) #f]
@@ -338,7 +342,7 @@ Like @scheme[regexp-match-positions] on input ports, but only peeks
 bytes from @scheme[input-port] instead of reading them, and with a
 @scheme[progress] argument like @scheme[regexp-match-peek].}
 
-@defproc[(regexp-match-peek-immediate [pattern (or/c string? bytes? regexp? bytes-regexp?)]
+@defproc[(regexp-match-peek-immediate [pattern (or/c string? bytes? regexp? byte-regexp?)]
                             [input input-port?]
                             [start-pos nonnegative-exact-integer? 0]
                             [end-pos (or/c nonnegative-exact-integer? false/c) #f]
@@ -352,7 +356,7 @@ that are available from @scheme[input-port] without blocking.  The
 match fails if not-yet-available characters might be used to match
 @scheme[pattern].}
 
-@defproc[(regexp-match-peek-positions-immediate [pattern (or/c string? bytes? regexp? bytes-regexp?)]
+@defproc[(regexp-match-peek-positions-immediate [pattern (or/c string? bytes? regexp? byte-regexp?)]
                             [input input-port?]
                             [start-pos nonnegative-exact-integer? 0]
                             [end-pos (or/c nonnegative-exact-integer? false/c) #f]
diff --git a/collects/scribblings/reference/security-guards.scrbl b/collects/scribblings/reference/security-guards.scrbl
index 0897f9e776..83b21533aa 100644
--- a/collects/scribblings/reference/security-guards.scrbl
+++ b/collects/scribblings/reference/security-guards.scrbl
@@ -4,6 +4,12 @@
 
 @title[#:tag "mz:securityguards"]{Security Guards}
 
+@defproc[(security-guard? [v any/c]) boolean?]{
+
+Returns @scheme[#t] if @scheme[v] is a security guard value as created
+by @scheme[make-security-guard], @scheme[#f] otherwise.}
+
+
 A @deftech{security guard} provides a set of access-checking
 procedures to be called when a thread initiates access of a file,
 directory, or network connection through a primitive procedure. For
@@ -141,12 +147,6 @@ into or out of the @scheme[file-guard] or @scheme[network-guard] call
 (see @secref["mz:prompt-model"]).}
 
 
-@defproc[(security-guard? [v any/c]) boolean?]{
-
-Returns @scheme[#t] if @scheme[v] is a security guard value as created
-by @scheme[make-security-guard], @scheme[#f] otherwise.}
-
-
 @defparam[current-security-guard guard security-guard?]{
 
 A parameter that determines the current security guard that controls
diff --git a/collects/scribblings/reference/security.scrbl b/collects/scribblings/reference/security.scrbl
index 3defe9e456..d5b0548e8e 100644
--- a/collects/scribblings/reference/security.scrbl
+++ b/collects/scribblings/reference/security.scrbl
@@ -1,18 +1,16 @@
 #reader(lib "docreader.ss" "scribble")
 @require["mz.ss"]
 
-@title[#:style 'toc]{Security and Reflection}
-
-MzScheme offers several mechanisms for managing security, each of
-which relies on @tech{thread}- and @tech{continuation}-specific
-@tech{parameters} (see @secref["mz:parameters"]).
+@title[#:style 'toc]{Reflection and Security}
 
 @local-table-of-contents[]
 
 @;------------------------------------------------------------------------
+@include-section["namespaces.scrbl"]
+@include-section["eval.scrbl"]
 @include-section["security-guards.scrbl"]
 @include-section["custodians.scrbl"]
 @include-section["thread-groups.scrbl"]
 @include-section["struct-inspectors.scrbl"]
 @include-section["code-inspectors.scrbl"]
-@include-section["namespaces.scrbl"]
+@include-section["module-reflect.scrbl"]
diff --git a/collects/scribblings/reference/strings.scrbl b/collects/scribblings/reference/strings.scrbl
index 6071183c3c..e284da6319 100644
--- a/collects/scribblings/reference/strings.scrbl
+++ b/collects/scribblings/reference/strings.scrbl
@@ -28,6 +28,12 @@ See also: @scheme[immutable], @scheme[symbol->string],
 @; ----------------------------------------
 @section{String Constructors, Selectors, and Mutators}
 
+@defproc[(string? [v any/c]) boolean?]{ Returns @scheme[#t] if @scheme[v]
+ is a string, @scheme[#f] otherwise.
+
+@examples[(string? "Apple") (string? 'apple)]}
+
+
 @defproc[(make-string [k exact-nonnegative-integer?] [char char?
 #\nul]) string?]{ Returns a new mutable string of length @scheme[k] where
 each position in the string is initialized with the character
@@ -49,12 +55,6 @@ Returns an immutable string with the same content as
  immutable.}
 
 
-@defproc[(string? [v any/c]) boolean?]{ Returns @scheme[#t] if @scheme[v]
- is a string, @scheme[#f] otherwise.
-
-@examples[(string? "Apple") (string? 'apple)]}
-
-
 @defproc[(string-length [str string?]) exact-nonnegative-integer?]{
  Returns the length of @scheme[str].
 
diff --git a/collects/scribblings/reference/struct-inspectors.scrbl b/collects/scribblings/reference/struct-inspectors.scrbl
index a1a60093a2..8ccbec068a 100644
--- a/collects/scribblings/reference/struct-inspectors.scrbl
+++ b/collects/scribblings/reference/struct-inspectors.scrbl
@@ -3,7 +3,7 @@
 
 @title[#:tag "mz:inspectors"]{Structure Inspectors}
 
-An @pidefterm{inspector} provides access to structure fields and
+An @deftech{inspector} provides access to structure fields and
 structure type information without the normal field accessors and
 mutators. (Inspectors are also used to control access to module
 bindings; see @secref["mz:modprotect"].) Inspectors are primarily
@@ -22,6 +22,11 @@ be provided though the @scheme[#:inspector] option of the
 through an optional @scheme[inspector] argument to
 @scheme[make-struct-type].
 
+
+@defproc[(inspector? [v any/c]) boolean?]{Returns @scheme[#t] if
+@scheme[v] is an inspector, @scheme[#f] otherwise.}
+
+
 @defproc[(make-inspector [inspector inspector? (current-inspector)])
          inspector?]{
 
@@ -30,9 +35,6 @@ Returns a new inspector that is a subinspector of
 is also controlled by its ancestor inspectors, but no other
 inspectors.}
 
-@defproc[(inspector? [v any/c]) boolean?]{Returns @scheme[#t] if
-@scheme[v] is an inspector, @scheme[#f] otherwise.}
-
 
 @defparam[current-inspector insp inspector?]{
 
diff --git a/collects/scribblings/reference/struct.scrbl b/collects/scribblings/reference/struct.scrbl
index 61dba1fd6f..0e47d9c4f1 100644
--- a/collects/scribblings/reference/struct.scrbl
+++ b/collects/scribblings/reference/struct.scrbl
@@ -342,3 +342,75 @@ is inaccessible.)}
  @scheme[#t] if @scheme[v] is a mutator procedure generated by
  @scheme[define-struct], @scheme[make-struct-type], or
  @scheme[make-struct-field-mutator], @scheme[#f] otherwise.}
+
+@;------------------------------------------------------------------------
+@section[#:tag "mz:structinfo"]{Structure Type Transformer Binding}
+
+The @scheme[define-struct] form binds the name of a structure type as
+a @tech{transformer binding} that records the other identifiers bound
+to the structure type, the constructor procedure, the predicate
+procedure, and the field accessor and mutator procedures. This
+information can be used during the expansion of other expressions via
+@scheme[syntax-local-value].
+
+For example, the @scheme[define-struct] variant for subtypes uses the
+base type name @scheme[t] to find the variable
+@scheme[struct@scheme[:t]] containing the base type's descriptor; it
+also folds the field accessor and mutator information for the base
+type into the information for the subtype. As another example, the
+@scheme[match] form uses a type name to find the predicates and field
+accessors for the structure type. The @scheme[struct] form in an
+imported signature for @scheme[unit] causes the @scheme[unit]
+transformer to generate information about imported structure types, so
+that @scheme[match] and subtyping @scheme[define-struct] forms work
+within the unit.
+
+The expansion-time information for a structure type is represented as
+a list of six elements:
+
+@itemize{
+
+ @item{an identifier that is bound to the structure type's descriptor,
+ or @scheme[#f] it none is known;}
+
+ @item{an identifier that is bound to the structure type's constructor,
+ or @scheme[#f] it none is known;}
+
+ @item{an identifier that is bound to the structure type's predicate,
+ or @scheme[#f] it none is known;}
+
+ @item{a list of identifiers bound to the field accessors of the
+ structure type, optionally with @scheme[#f] as the list's last
+ element. A @scheme[#f] as the last element indicates that the
+ structure type may have additional fields, otherwise the list is a
+ reliable indicator of the number of fields in the structure
+ type. Furthermore, the accessors are listed in reverse order for the
+ corresponding constructor arguments. (The reverse order enables
+ sharing in the lists for a subtype and its base type.)}
+
+ @item{a list of identifiers bound to the field mutators of
+ the structure type, or @scheme[#f] for each field that has no known
+ mutator, and optionally with an extra @scheme[#f] as the list's last
+ element (if the accessor list has such a @scheme[#f]). The list's
+ order and the meaning of a final @scheme[#f] are the same as for the
+ accessor identifiers, and the length of the mutator list is the same
+ as the accessor list's length.}
+
+ @item{an identifier that determines a super-type for the structure
+ type, @scheme[#f] if the super-type (if any) is unknown, or
+ @scheme[#t] if there is no super-type. If a super-type is specified,
+ the identifier is also bound to structure-type expansion-time
+ information.}
+
+}
+
+The implementor of a syntactic form can expect users of the form to
+know what kind of information is available about a structure type. For
+example, the @scheme[match] implementation works with structure
+information containing an incomplete set of accessor bindings, because
+the user is assumed to know what information is available in the
+context of the @scheme[match] expression. In particular, the
+@scheme[match] expression can appear in a @scheme[unit] form with an
+imported structure type, in which case the user is expected to know
+the set of fields that are listed in the signature for the structure
+type.
diff --git a/collects/scribblings/reference/stx-certs.scrbl b/collects/scribblings/reference/stx-certs.scrbl
new file mode 100644
index 0000000000..139768d64a
--- /dev/null
+++ b/collects/scribblings/reference/stx-certs.scrbl
@@ -0,0 +1,135 @@
+#reader(lib "docreader.ss" "scribble")
+@require["mz.ss"]
+
+@require-for-syntax[mzscheme]
+
+@title[#:tag "mz:stxcerts"]{Syntax Certificates}
+
+A @deftech{syntax certificate} combines a @tech{syntax mark} (see
+@secref["mz:transformer-model"]), a @tech{module path index} or symbol
+module name (see @secref["mz:modpathidx"]), an @tech{inspector} (see
+@secref["mz:modprotect"]), and an arbitrary key object. A certificate
+is attached as either an @deftech{active certificate} or an
+@deftech{inactive certificate}.
+
+The @scheme[datum->syntax] procedure never transfers an
+@deftech{active certificate} from one syntax object to another. The
+@scheme[syntax-recertify] procedure can be used to transfer a
+certificate from one syntax object to another, but only if the
+certificate's key is provided, or if a sufficiently powerful inspector
+is provided. Thus, a certificate's inspector serves two roles: it
+determines the certificate's power to grant access, and also allows
+the certificate to be moved arbitrarily by anyone with a more powerful
+inspector.
+
+The expander generates a certificate when it applies a syntax
+transformer. The @tech{syntax mark} in the certificate is fresh, the
+certificate's module reference corresponds to the module that defined
+the @tech{transformer binding}, the inspector is the inspector for the
+module's declaration (see @secref["mz:modprotect"]), and the key
+object is hidden. (Applying the result of
+@scheme[syntax-local-certifier] can introduce certificates with other
+keys.) The certificate's mark is applied to both the input and output
+of the syntax transformer, so that it identifies every piece of syntax
+that was introduced by the transformer (see
+@secref["mz:transformer-mode"]). The expander attaches this
+certificate to parts of the transformer's result, depending on the
+shape and properties of the result:
+
+@itemize{
+
+ @item{If the result has a @scheme['certify-mode] property (see
+          @secref["mz:stxprops"]) that is @scheme['opaque], then the
+          certificate is attached to the immediate syntax object.}
+
+ @item{If the result has a @scheme['certify-mode] property that is
+          @scheme['transparent], then the certificate is also
+          propagated recursively to syntax object that corresponds to
+          elements of the syntax object's datum as a list (or, more
+          precisely, to the @scheme[car]s of the datum as reached by
+          any number of @scheme[cdr]s). This recursive propagation
+          uses syntax properties and shapes, as for the immediate
+          attachment.}
+
+ @item{If the result has a @scheme['certify-mode] property that is
+          @scheme['transparent-binding], then the certificate is
+          attached to similar to @scheme['transparent], but further
+          treating the syntax object corresponding to the second list
+          element as having a @scheme['transparent] value for the
+          @scheme['certify-mode] property if it does not already have
+          a @scheme['certify-mode] property value.}
+
+ @item{If the result has no @scheme['certify-mode] property value,
+          but its datum is a pair, and if the syntax object
+          corresponding to the @scheme[car] of the pair is an
+          identifier bound to @scheme[begin], then the certificate is
+          propagated as if the syntax object had the
+          @scheme['transparent] property value.}
+
+ @item{If the result has no @scheme['certify-mode] property value,
+          but its datum is a pair, and if the syntax object
+          corresponding to the @scheme[car] of the pair is an
+          identifier bound to @scheme[define-values] or
+          @scheme[define-syntaxes], then the certificate is propagated
+          as if the syntax object had the @scheme['transparent-binding]
+          property value.}
+
+}
+
+The the expander attaches a new active certificate to a syntax object,
+it also removes any @tech{inactive certificates} attached to any
+@tech{syntax object} within the one where the certificate is attached,
+and it re-attaches the formerly @tech{inactive certificates} as
+@tech{active certificates} along with the new one.
+
+As the expander processes a form, it accumulates @tech{active
+certificates} that are attached to enclosing forms as part of the
+expansion context:
+
+@itemize{
+
+ @item{To check access to an unexported identifier, the expander
+   checks each of the identifier's marks and module bindings; if, for
+   some mark, the identifier's enclosing expressions include a
+   certificate with the mark, the identifier's binding module, and
+   with an inspector that controls the module's invocation (as opposed
+   to the module's declaration; see again @secref["mz:modprotect"]),
+   then the access is allowed. To check access to a protected
+   identifier, only the certificate's mark and inspector are used
+   (i.e., the module that bound the transformer is irrelevant, as long
+   as it was evaluated with a sufficiently powerful inspector). The
+   certificate key is not used in checking references.}
+
+ @item{To check access to a locally bound identifier, the expander
+   checks the marks of the binding and reference identifiers; for
+   every mark that they have in common, if the reference identifier
+   has a certificate for the mark from an enclosing expression, the
+   binding identifier must have a certificate for the mark from an
+   enclosing expression, otherwise the reference is disallowed. (The
+   reference identifier can have additional certificates for marks
+   that are not attached to the binding identifier.) The binding
+   module (if any) and the certificate key are not used for checking a
+   local reference.}
+
+ @item{When the expander encounters a @scheme[quote-syntax] form, it
+   attaches all accumulated @tech{active certificates} from the
+   expressions's context to the quoted syntax objects. The
+   certificates are attached as @tech{inactive certificates}.}
+
+}
+
+
+@defproc[(syntax-recertify [new-stx syntax?]
+                           [old-stx syntax?]
+                           [inspector inspector?]
+                           [key any/c])
+         syntax?]{
+
+Copies certain certificates of @scheme[old-stx] to @scheme[new-stx]: a
+certificate is copied if its inspector is either @scheme[inspector] or
+controlled by @scheme[inspector], or if the certificate's key is
+@scheme[key]; otherwise the certificate is not copied.  The result is
+a syntax object like @scheme[new-stx], but with the copied
+certificates. (The @scheme[new-stx] object itself is not modified.)
+Both @tech{active certificates} and @tech{inactive certificates} are
+copied.}
diff --git a/collects/scribblings/reference/stx-expand.scrbl b/collects/scribblings/reference/stx-expand.scrbl
new file mode 100644
index 0000000000..711b8f685b
--- /dev/null
+++ b/collects/scribblings/reference/stx-expand.scrbl
@@ -0,0 +1,121 @@
+#reader(lib "docreader.ss" "scribble")
+@require["mz.ss"]
+
+@title[#:tag "mz:expansion"]{Expanding Top-Level Forms}
+
+
+@defproc[(expand [top-level-form any/c]) syntax?]{
+
+Expands all non-primitive syntax in @scheme[top-level-form], and
+returns a syntax object for the expanded form that contains only core
+forms, matching the grammar specified by @secref["mz:fully-expanded"].
+
+Before @scheme[top-level-form] is expanded, its lexical context is
+enriched with @scheme[namespace-syntax-introduce], just as for
+@scheme[eval]. Use @scheme[syntax->datum] to convert the returned
+syntax object into a printable datum.}
+
+
+@defproc[(expand-syntax [stx syntax?]) syntax?]{
+
+Like @scheme[(expand stx)], except that the argument must be a
+@tech{syntax object}, and its lexical context is not enriched before
+expansion.}
+
+
+@defproc[(expand-once [top-level-form any/c]) syntax?]{
+
+Partially expands @scheme[form-level-form] and returns a syntax object
+for the partially-expanded expression. Due to limitations in the
+expansion mechanism, some context information may be lost. In
+particular, calling @scheme[expand-once] on the result may produce a
+result that is different from expansion via @scheme[expand].  
+
+Before @scheme[top-level-form] is expanded, its lexical context is
+enriched with @scheme[namespace-syntax-introduce], as for
+@scheme[eval].}
+
+
+@defproc[(expand-syntax-once [stx syntax?]) syntax?]{
+
+Like @scheme[(expand-once stx)], except that the argument
+must be a @tech{syntax object}, and its lexical context is not
+enriched before expansion.}
+
+
+@defproc[(expand-to-top-form [top-level-form any/c]) syntax?]{
+
+Partially expands @scheme[top-level-form] to reveal the outermost
+syntactic form. This partial expansion is mainly useful for detecting
+top-level uses of @scheme[begin]. Unlike the result of
+@scheme[expand-once], expanding the result of
+@scheme[expand-to-top-form] with @scheme[expand] produces the same
+result as using @scheme[expand] on the original syntax.
+
+Before @scheme[stx-or-sexpr] is expanded, its lexical context is
+enriched with @scheme[namespace-syntax-introduce], as for
+@scheme[eval].}
+
+
+@defproc[(expand-syntax-to-top-form [stx syntax?]) syntax?]{
+
+Like @scheme[(expand-to-top-form stx)], except that the argument must
+be a @tech{syntax object}, and its lexical context is not enriched
+before expansion.}
+
+@;------------------------------------------------------------------------
+@section[#:tag "mz:modinfo"]{Information on Expanded Modules}
+
+Information for an expanded @scheme[module] declaration is stored in a
+set of @tech{syntax properties} (see @secref["mz:stxprops"]) attached
+to the syntax object:
+
+@itemize{
+
+ @item{@scheme['module-direct-requires] --- a list of
+ @tech{module path index}es (or symbols) representing the modules explicitly
+ imported into the module.}
+
+ @item{@scheme['module-direct-for-syntax-requires] --- a list of
+ @tech{module path index}es (or symbols) representing the modules explicitly
+ for-syntax imported into the module.}
+
+ @item{@scheme['module-direct-for-template-requires] --- a list of
+ @tech{module path index}es (or symbols) representing the modules
+ explicitly for-template imported into the module.}
+
+ @item{@scheme['module-variable-provides] --- a list of provided
+ items, where each item is one of the following:
+ 
+  @itemize{
+
+  @item{@scheme[symbol] --- represents a locally defined variable that
+  is provided with its defined name.}
+
+  @item{@scheme[(cons _provided-sym _defined-sym)] --- represents a
+  locally defined variable that is provided with renaming; the first
+  symbol is the exported name, and the second symbol is the defined
+  name.}
+
+  @item{@scheme[(list* module-path-index _provided-sym _defined-sym)]
+  --- represents a re-exported and possibly re-named variable from the
+  specified module; @scheme[module-path-index] is either a
+  @tech{module path index} or symbol (see @secref["mz:modpathidx"]),
+  indicating the source module for the binding. The
+  @scheme[_provided-sym] is the external name for the re-export, and
+  @scheme[_defined-sym] is the originally defined name in the module
+  specified by @scheme[module-path-index].}
+
+  }}
+
+ @item{@scheme['module-syntax-provides] --- like
+ @scheme['module-variable-provides], but for syntax exports instead of
+ variable exports.}
+
+ @item{@scheme['module-indirect-provides] --- a list of symbols for
+ variables that are defined in the module but not exported; they may
+ be exported indirectly through macro expansions.  Definitions of
+ macro-generated identifiers create uninterned symbols in this list.}
+
+}
+
diff --git a/collects/scribblings/reference/stx-ops.scrbl b/collects/scribblings/reference/stx-ops.scrbl
index 11f59b0c8a..f5c23ef8a2 100644
--- a/collects/scribblings/reference/stx-ops.scrbl
+++ b/collects/scribblings/reference/stx-ops.scrbl
@@ -143,8 +143,8 @@ in @scheme[v] are given the lexical context information of
 @scheme[ctxt] and the source-location information of
 @scheme[srcloc]. If @scheme[v] is not already a syntax object, then
 the resulting immediate syntax object it is given the properties (see
-@secref["mz:stxprops"]) of @scheme[prop] and the inactive certificates
-(see @secref["mz:stxprotect"]) of @scheme[cert].  Any of
+@secref["mz:stxprops"]) of @scheme[prop] and the @tech{inactive certificates}
+(see @secref["mz:stxcerts"]) of @scheme[cert].  Any of
 @scheme[ctxt], @scheme[srcloc], @scheme[prop], or @scheme[cert] can be
 @scheme[#f], in which case the resulting syntax has no lexical
 context, source information, new properties, and/or certificates.
diff --git a/collects/scribblings/reference/stx-props.scrbl b/collects/scribblings/reference/stx-props.scrbl
new file mode 100644
index 0000000000..2b74ff59e1
--- /dev/null
+++ b/collects/scribblings/reference/stx-props.scrbl
@@ -0,0 +1,158 @@
+#reader(lib "docreader.ss" "scribble")
+@require["mz.ss"]
+
+@title[#:tag "mz:stxprops"]{Syntax Object Properties}
+
+Every syntax object has an associated @deftech{syntax property} list,
+which can be queried or extended with
+@scheme[syntax-property]. Properties are not preserved for a
+@scheme[syntax-quoted] syntax object in a compiled form that is
+marshaled to a byte string.
+
+In @scheme[read-syntax], the reader attaches a @scheme['paren-shape]
+property to any pair or vector syntax object generated from parsing a
+pair @litchar["["] and @litchar["]"] or @litchar["{"] and
+@litchar["}"]; the property value is @scheme[#\[] in the former case,
+and @scheme[#\{] in the latter case. The @scheme[syntax] form copies
+any @scheme['paren-shape] property from the source of a template to
+corresponding generated syntax.
+
+Both the syntax input to a transformer and the syntax result of a
+transformer may have associated properties. The two sets of properties
+are merged by the syntax expander: each property in the original and
+not present in the result is copied to the result, and the values of
+properties present in both are combined with @scheme[cons] (result
+value first, original value second).
+
+Before performing the merge, however, the syntax expander
+automatically adds a property to the original syntax object using the
+key @scheme['origin]. If the source syntax has no @scheme['origin]
+property, it is set to the empty list.  Then, still before the merge,
+the identifier that triggered the macro expansion (as syntax) is
+@scheme[cons-immutable]d onto the @scheme['origin] property so far.
+The @scheme['origin] property thus records (in reverse order) the
+sequence of macro expansions that produced an expanded
+expression. Usually, the @scheme['origin] value is an immutable list
+of identifiers. However, a transformer might return syntax that has
+already been expanded, in which case an @scheme['origin] list can
+contain other lists after a merge. The @scheme[syntax-track-origin]
+procedure implements this tracking.
+
+Besides @scheme['origin] tracking for general macro expansion,
+MzScheme adds properties to expanded syntax (often using
+@scheme[syntax-track-origin]) to record additional expansion details:
+
+@itemize{
+
+ @item{When a @scheme[begin] form is spliced into a sequence with
+ internal definitions (see @secref["mz:intdef-body"]),
+ @scheme[syntax-track-origin] is applied to every spliced element from
+ the @scheme[begin] body. The second argument to
+ @scheme[syntax-track-origin] is the @scheme[begin] form, and the
+ third argument is the @scheme[begin] keyword (extracted from the
+ spliced form).}
+
+ @item{When an internal @scheme[define-values] or
+ @scheme[define-syntaxes] form is converted into a
+ @scheme[letrec-values+syntaxes] form (see @secref["mz:intdef-body"]),
+ @scheme[syntax-track-origin] is applied to each generated binding
+ clause.  The second argument to @scheme[syntax-track-origin] is the
+ converted form, and the third argument is the @scheme[define-values]
+ or @scheme[define-syntaxes] keyword form the converted form.}
+
+ @item{When a @scheme[letrec-values+syntaxes] expression is fully
+ expanded, syntax bindings disappear, and the result is either a
+ @scheme[letrec-values] form (if the unexpanded form contained
+ non-syntax bindings), or only the body of the
+ @scheme[letrec-values+syntaxes] form (wrapped with @scheme[begin] if
+ the body contained multiple expressions). To record the disappeared
+ syntax bindings, a property is added to the expansion result: an
+ immutable list of identifiers from the disappeared bindings, as a
+ @scheme['disappeared-binding] property.}
+
+ @item{When a subtyping @scheme[define-struct] form is expanded, the
+ identifier used to reference the base type does not appear in the
+ expansion. Therefore, the @scheme[define-struct] transformer adds the
+ identifier to the expansion result as a @scheme['disappeared-use]
+ property.}
+
+ @item{When a reference to an unexported or protected identifier from
+ a module is discovered (and the reference is certified; see
+ @secref["mz:stxprotect"]), the @scheme['protected] property is added
+ to the identifier with a @scheme[#t] value.}
+
+ @item{When or @scheme[read-syntax] or @scheme[read-honu-syntax]
+ generates a syntax object, it attaches a property to the object
+ (using a private key) to mark the object as originating from a
+ read. The @scheme[syntax-original?]  predicate looks for the property
+ to recognize such syntax objects. (See @secref["mz:stxops"] for more
+ information.)}
+
+}
+
+See @secref["mz:modinfo"] for information about properties generated
+by the expansion of a module declaration. See @secref["mz:arity"] and
+@secref["mz:infernames"] for information about properties recognized
+when compiling a procedure. See @secref["mz:compilation"] for
+information on properties and byte codes.
+
+@;------------------------------------------------------------------------
+
+@defproc[(syntax-property [stx syntax?][key any/c][v any/c])
+         syntax?]{
+
+Extends @scheme[stx] by associating an arbitrary property value
+@scheme[v] with the key @scheme[key]; the result is a new syntax
+object with the association (while @scheme[stx] itself is unchanged).}
+
+
+@defproc[(syntax-property [stx syntax?][key any/c]) any]{
+
+Returns an arbitrary property value associated to @scheme[stx] with
+the key @scheme[key], or @scheme[#f] if no value is associated to
+@scheme[stx] for @scheme[key].}
+
+
+@defproc[(syntax-property-symbol-keys [stx syntax?]) list?]{
+
+Returns a list of all symbols that as keys have associated properties
+in @scheme[stx]. @tech{Uninterned} symbols (see @secref["mz:symbol"])
+are not included in the result list.}
+
+
+@defproc[(syntax-track-origin [new-stx syntax?][orig-stx syntax?][id-stx syntax?]) 
+         any]{
+
+Adds properties to @scheme[new-stx] in the same way that macro
+expansion adds properties to a transformer result. In particular, it
+merges the properties of @scheme[orig-stx] into @scheme[new-stx],
+first adding @scheme[id-stx] as an @scheme['origin] property, and it
+returns the property-extended syntax object. Use the
+@scheme[syntax-track-origin] procedure in a macro transformer that
+discards syntax (corresponding to @scheme[orig-stx] with a keyword
+@scheme[id-stx]) leaving some other syntax in its place (corresponding
+to @scheme[new-stx]).
+
+For example, the expression
+
+@schemeblock[
+(or x y)
+]
+
+expands to
+
+@schemeblock[
+(let ((or-part x)) (if or-part or-part (or y)))
+]
+
+which, in turn, expands to
+
+@schemeblock[
+(let-values ([(or-part) x]) (if or-part or-part y))
+]
+
+The syntax object for the final expression will have an
+@scheme['origin] property whose value is @scheme[(list (quote-syntax
+let) (quote-syntax or))].}
+
+
diff --git a/collects/scribblings/reference/syntax-model.scrbl b/collects/scribblings/reference/syntax-model.scrbl
index b468ea8945..8a456f0f9e 100644
--- a/collects/scribblings/reference/syntax-model.scrbl
+++ b/collects/scribblings/reference/syntax-model.scrbl
@@ -96,10 +96,11 @@ different phase levels.
 @section[#:tag "mz:stxobj-model"]{Syntax Objects}
 
 A @deftech{syntax object} combines a simpler Scheme value, such as a
-symbol or pair, with @deftech{lexical information} about bindings and
-(optionally) source-location information. In particular, an
-@tech{identifier} is represented as a symbol object that combines a
-symbol and lexical/source information.
+symbol or pair, with @deftech{lexical information} about bindings,
+source-location information, @tech{syntax properties}, and
+@tech{syntax certificates}. In particular, an @tech{identifier} is
+represented as a symbol object that combines a symbol and lexical and
+other information.
 
 For example, a @schemeidfont{car} @tech{identifier} might have
 @tech{lexical information} that designates it as the @scheme[car] from
@@ -456,10 +457,11 @@ environment}) instead of @tech{phase level} 0.
 
 The if resulting @scheme[value] is a procedure of one argument or as
 the result of @scheme[make-set!-transformer] on a procedure, then is
-it used as a @deftech{syntax transformer}.  The procedure is expected
-to accept a syntax object and return a syntax object. A use of the
-binding (at @tech{phase level} 0) triggers a call of the @tech{syntax
-transformer} by the expander; see @secref["mz:expand-steps"].
+it used as a @deftech{syntax transformer} (a.k.a. @deftech{macro}).
+The procedure is expected to accept a syntax object and return a
+syntax object. A use of the binding (at @tech{phase level} 0) triggers
+a call of the @tech{syntax transformer} by the expander; see
+@secref["mz:expand-steps"].
 
 Before the expander passes a @tech{syntax object} to a transformer,
 the @tech{syntax object} is extend with a @deftech{syntax mark} (that
@@ -506,7 +508,7 @@ The @scheme[set!] form and the @scheme[make-set!-transformer]
 procedure work together to support @deftech{assignment transformers}
 that transformer @scheme[set!] expression. @tech{Assignment
 transformers} are applied by @scheme[set!] in the same way as a normal
-transformer by the macro expander.
+transformer by the expander.
 
 The @scheme[make-rename-transformer] procedure creates a value that is
 also handled specially by the expander and by @scheme[set!] as a
@@ -517,6 +519,16 @@ passed to @scheme[make-rename-transformer]. Furthermore, the binding
 is also specially handled by @scheme[syntax-local-value] as used by
 @tech{syntax transformer}s.
 
+In addition to using marks to track introduced identifiers, the
+expander tracks the expansion history of a form through @tech{syntax
+properties} such as @scheme['origin]. See @secref["mz:stxprops"] for
+more information.
+
+Finally, the expander uses @tech{syntax certificates} to control the
+way that unexported and protected @tech{module-level bindings} are
+used. See @secref["mz:stxcerts"] for more information on @tech{syntax
+certificates}.
+
 The expander's handling of @scheme[letrec-values+syntaxes] is similar
 to its handling of @scheme[define-syntaxes]. A
 @scheme[letrec-values+syntaxes] mist be expanded in an arbitrary phase
@@ -613,7 +625,7 @@ the required module to be merely visited at @tech{phase} 0, not
 When the expander encounters @scheme[require-for-syntax], it
 immediately instantiates the required module at @tech{phase} 1, in
 addition to adding bindings scheme @tech{phase level} 1 (i.e., the
-@tech{transformer enviornment}).
+@tech{transformer environment}).
 
 When the expander encounters @scheme[require] and
 @scheme[require-for-syntax] within a @tech{module context}, the
@@ -623,7 +635,7 @@ expansion of the enclosing module, and are kept separate from
 @tech{top-level context} or from the expansion of a different module.
 
 @;------------------------------------------------------------------------
-@section{Compilation}
+@section[#:tag "mz:compilation-model"]{Compilation}
 
 Before expanded code is evaluated, it is first @deftech{compiled}. A
 compiled form has essentially the same information as the
diff --git a/collects/scribblings/reference/syntax.scrbl b/collects/scribblings/reference/syntax.scrbl
index beab30aa58..a99b521492 100644
--- a/collects/scribblings/reference/syntax.scrbl
+++ b/collects/scribblings/reference/syntax.scrbl
@@ -903,8 +903,11 @@ information} and source-location information attached to
 
 @defform[(module id require-spec form ...)]{
 
-Declares a module named by @scheme[id]. The @scheme[require-spec] must
-be as for @scheme[require] (see @secref["mz:require"]), and it
+Declares a module named by combining @scheme[(#,(scheme quote) id)]
+with @scheme[(current-module-name-prefix)] if the latter is not
+@scheme[#f], or named @scheme[(#,(scheme quote) id)] otherwise.
+
+The @scheme[require-spec] must be as for @scheme[require], and it
 supplies the initial bindings for the body @scheme[form]s. That is, it
 is treated like a @scheme[(require require-spec)] prefix on
 @scheme[form], where @scheme[require] is the preimitive
@@ -1031,7 +1034,8 @@ be different from the symbolic name of the originally exported
 identifier.
 
  @specsubform[module-path]{ Imports all exported bindings from the
-  named module, using the export identifier as the local identifiers.}
+  named module, using the export identifier as the local identifiers.
+  (See below for information on @scheme[module-path].)}
 
  @specsubform[#:literals (only) (only require-spec id-maybe-renamed ...)]{
   Like @scheme[require-spec], but constrained to those exports for
@@ -1060,7 +1064,11 @@ identifier.
 
 A @scheme[module-path] identifies a module, either through a concrete
 name in the form of an identifier, or through an indirect name that
-can trigger automatic loading of the module declaration:
+can trigger automatic loading of the module declaration. Except for
+the @scheme[id] case below, the actual resolution is up to the current
+@tech{module name resolver} (see
+@scheme[current-module-name-resolver]), and the description below
+corresponds to the default @tech{module name resolver}.
 
  @specsubform[id]{ Refers to a module previously declared with the name
   @scheme[id].}
@@ -1087,8 +1095,7 @@ can trigger automatic loading of the module declaration:
 
  @specsubform[#:literals(planet)
               (planet rel-string (user-string pkg-string vers ...))]{
- Specifies a library available via the @PLaneT server.
- }
+ Specifies a library available via the @PLaneT server.}
 
 No identifier can be bound multiple times by an import, unless all of
 the bindings refer to the same original definition in the same module.