try to improve the examples for typesetting styles

and other small improvements to the redex docs

redex-doc/redex/scribblings/ref.scrbl

@@ -1,11 +1,11 @@
 #lang scribble/doc
 @(require scribble/manual)
-@title[#:tag "reference"]{The Redex Reference}
+@title[#:style 'toc #:tag "reference"]{The Redex Reference}
 
 @defmodule*/no-declare[(redex)]
 
 The @racketmodname[redex] library provides all of
-the names documented here.
+the names documented in this section.
 
 Alternatively, use the @racketmodname[redex/reduction-semantics] and 
 @racketmodname[redex/pict] libraries, which provide only non-GUI 

redex-doc/redex/scribblings/ref/typesetting.scrbl

@@ -110,8 +110,10 @@ sets @racket[dc-for-text-size] and the latter does not.
  @ex[(define-language nums
        (AE K
            (+ AE AE))
+       (code:comment "binary digits")
+       (k 1 0)
        (code:comment "binary constants")
-       (K · (1 K) (0 K)))
+       (K · (k K)))
      (render-term nums (+ (1 (0 (1 ·))) (+ (1 (1 (1 ·))) (1 (0 (0 ·))))))]
 
  The @racket[term] argument must be a literal; it is not an 
@@ -237,15 +239,18 @@ The following forms of arrows can be typeset:
 @arrows[--> -+> ==> -> => ..> >-> ~~> ~> :-> :--> c->
         -->> >-- --< >>-- --<<]
 
-@ex[(render-reduction-relation
-     (reduction-relation
-      nums
-      (--> (+ AE ())
-           AE)
-      (--> (+ AE_1
-              AE_2)
-           (+ AE_2
-              AE_1))))]
+ @ex[
+ (define simplify-ae
+   (reduction-relation
+    nums
+    (--> (+ AE ())
+         AE)
+    (--> (+ AE_1
+            AE_2)
+         (+ AE_2
+            AE_1))))
+ (render-reduction-relation
+  simplify-ae)]
 
 }
 
@@ -284,8 +289,10 @@ Similarly, @racket[render-metafunctions] accepts multiple
 metafunctions and renders them together, lining up all of the
 clauses together.
 
-Parameters that affect rendering include
-@racket[metafunction-pict-style], @racket[linebreaks], @racket[sc-linebreaks], and
+There are a number of different styles that affect the overall rendering
+of the metafunction, controlled by @racket[metafunction-pict-style].
+Other parameters that affect rendering include
+@racket[linebreaks], @racket[sc-linebreaks], and
 @racket[metafunction-cases].
 
 If the metafunctions have contracts, they are typeset as the first
@@ -502,35 +509,41 @@ Defaults to @racket[#f].
 
 @defparam[rule-pict-style style reduction-rule-style/c]{
 
-This parameter controls the style used by default for the reduction
-relation. It can be @racket['horizontal], where the left and
-right-hand sides of the reduction rule are beside each other or
-@racket['vertical], where the left and right-hand sides of the
-reduction rule are above each other.  The @racket['compact-vertical]
-style moves the reduction arrow to the second line and uses less space
-between lines.  The @racket['vertical-overlapping-side-conditions]
-variant, the side-conditions don't contribute to the width of the
-pict, but are just overlaid on the second line of each rule.  The
-@racket['horizontal-left-align] style is like the @racket['horizontal]
-style, but the left-hand sides of the rules are aligned on the left,
-instead of on the right. The @racket['horizontal-side-conditions-same-line]
-is like @racket['horizontal], except that side-conditions
-are on the same lines as the rule, instead of on their own line below.
-
- Each of these styles uses the function
- @racket[rule-pict-info->side-condition-pict] to build the
- side-conditions and where clauses, passing different values
- for the @racket[_max-width] argument. The @racket['vertical]
- and @racket['vertical-overlapping-side-conditions] pass
- @racket[+inf.0], which means that the side-conditions stay
- on a single line. The @racket['horizontal],
- @racket['horizontal-left-align], and
- @racket['horizontal-side-conditions-same-line] pass the
- width of left and right-hand sides combined. The
- @racket['compact-vertical] style offers some configuration,
- passing the larger of the value of
- @racket[compact-vertical-min-width] and the width of the
- left and right-hand sides.
+ This parameter controls the style used by default for the
+ reduction relation. It can be @racket['horizontal], where
+ the left and right-hand sides of the reduction rule are
+ beside each other or @racket['vertical], where the left and
+ right-hand sides of the reduction rule are above each other.
+
+ @ex[#:label #f
+ (parameterize ([rule-pict-style 'horizontal])
+   (render-reduction-relation simplify-ae))
+ (parameterize ([rule-pict-style 'vertical])
+   (render-reduction-relation simplify-ae))]
+
+ The @racket['compact-vertical] style moves the reduction
+ arrow to the second line and uses less space between lines.
+
+ @ex[#:label #f
+ (parameterize ([rule-pict-style 'compact-vertical])
+   (render-reduction-relation simplify-ae))]
+
+ In the @racket['vertical-overlapping-side-conditions] variant,
+ the side-conditions don't contribute to the width of the
+ pict, but are just overlaid on the second line of each rule.
+
+ The @racket['horizontal-left-align] style is like the
+ @racket['horizontal] style, but the left-hand sides of the
+ rules are aligned on the left, instead of on the right.
+
+ @ex[#:label #f
+ (parameterize ([rule-pict-style 'horizontal-left-align])
+   (render-reduction-relation simplify-ae))]
+
+ The @racket['horizontal-side-conditions-same-line] is like
+ @racket['horizontal], except that side-conditions are on the
+ same lines as the rule, instead of on their own line below.
+
 }
 
 @defthing[reduction-rule-style/c contract?]{
@@ -610,25 +623,47 @@ results of calling the metafunction are displayed to the
 right of the arguments and the @racket['up-down] style means that
 the results are displayed below the arguments.
 
+ @ex[#:label #f
+ (parameterize ([metafunction-pict-style 'left-right])
+   (render-metafunction add #:contract? #t))
+ (parameterize ([metafunction-pict-style 'up-down])
+   (render-metafunction add #:contract? #t))]
+
 The @racket['left-right/vertical-side-conditions] and
 @racket['up-down/vertical-side-conditions] variants format side
 conditions each on a separate line, instead of all on the same line.
-
-The @racket['left-right/compact-side-conditions] and
-@racket['up-down/compact-side-conditions] variants move side
-conditions to separate lines to avoid making the rendered form wider
-would be otherwise---except that the rendered form is allowed to be up
-to the width specified by @racket[metafunction-fill-acceptable-width].
-
 The @racket['left-right/beside-side-conditions] variant is like
 @racket['left-right], except it puts the side-conditions on the 
 same line, instead of on a new line below the case.
 
- @ex[(parameterize ([metafunction-pict-style 'left-right])
-       (render-metafunction add #:contract? #t))
-     (parameterize ([metafunction-pict-style 'up-down])
-       (render-metafunction add #:contract? #t))]
-
+ @ex[#:label #f
+ (define-metafunction nums
+   to-nat/sc : K -> natural
+   [(to-nat/sc ·) 0]
+   [(to-nat/sc (k K))
+    ,(* 2 (term natural_K))
+    (where k 0)
+    (where natural_K (term (to-nat/sc K)))]
+   [(to-nat/sc (k K))
+    ,(+ 1 (* 2 (term natural_K)))
+    (where k 1)
+    (where natural_K (term (to-nat/sc K)))])
+ (parameterize ([metafunction-pict-style 'left-right])
+   (render-metafunction to-nat/sc #:contract? #t))
+ (parameterize ([metafunction-pict-style 'left-right/vertical-side-conditions])
+   (render-metafunction to-nat/sc #:contract? #t))
+ (parameterize ([metafunction-pict-style 'left-right/beside-side-conditions])
+   (render-metafunction to-nat/sc #:contract? #t))]
+
+ Sometimes, some cases have side-conditions that are wider
+ than other cases in such a way that they should break across
+ lines differently in different cases. The
+ @racket['left-right/compact-side-conditions] and
+ @racket['up-down/compact-side-conditions] variants move side
+ conditions to separate lines to avoid making the rendered
+ form wider would be otherwise---except that the rendered
+ form is allowed to be up to the width specified by
+ @racket[metafunction-fill-acceptable-width].
 }
 
 @defparam[metafunction-up/down-indent indent (>=/c 0)]{

redex-doc/redex/scribblings/tut.scrbl

@@ -98,7 +98,7 @@ If you are not familiar with Racket, first try
 @other-doc['(lib "quick.scrbl" "scribblings/quick")] or
 @other-doc['(lib "more.scrbl" "scribblings/more")].
 If you wish to follow along with only parts of this tutorial
-but (perhaps using a different IDE or in a text-only
+(perhaps using a different IDE or in a text-only
 context), refer to @secref["reference"] for the full details on
 the constructs presented here.
 
@@ -1059,8 +1059,8 @@ then we can use the pict primitives to combine typeset fragments into a larger w
                  3/2)]
 
 Generally speaking, Redex has reasonable default ways to typeset its
-definitions, except when they escapes to Racket. In that case,
-it typesets the code in a fixed-width font and makes the background pink to call our
+definitions, except when they escape to Racket. In that case,
+it typesets the code in a fixed-width font and makes the background pink to call
 attention to it. While it is possible to use @racket[with-unquote-rewriter] to 
 tell Redex how to typeset those regions, often it is easier to define a metafunction
 and call it. In this case, we can use @racket[different] (defined earlier).
@@ -1115,8 +1115,9 @@ fills as much of the width established by rendering @racket[red].
 
 @exercise[]
 
-Typeset @racket[types]. Use a compound rewriter so a use of @racket[(type Γ e t)]
-is rendered as @racketblock[Γ ⊢ e : t]
+Use @racket[render-judgment-form] to typeset @racket[types].
+Use a compound rewriter so a use of @racket[(type Γ e t)] is
+rendered as @racketblock[Γ ⊢ e : t]
 
 @close-eval[amb-eval]