diff --git a/README.md b/README.md
index 3d07474..e968990 100644
--- a/README.md
+++ b/README.md
@@ -12,18 +12,9 @@ of those facilities can be created from more primitive operations of
 term matching and replacement. Every step of the way is illustrated with actual,
 working Stratego programs.
 
-There are, however, two catches for a newcomer trying to learn Spoofax and
-Stratego for the first time:
-
-1. All of the examples are worked in an older framework ("Stratego/XT") which
-   has a rather different collection of tools than the current implementation
-   of Spoofax in the Eclipse IDE.
-1. Unlike with the Calc example language used for the explication of the
-   Syntax Definition Language SDF3, there does not seem to be any publicly
-   available repository containing the worked examples to follow along with.
-
-This [Gitea repository](https://code.studioinfinity.org/glen/spoofax_prop) aims
-to fill both gaps. It can be cloned as an Eclipse project (note the git root
+This [Gitea repository](https://code.studioinfinity.org/glen/spoofax_prop)
+provides a working implementation of most of the examples in the manual.
+It can be cloned as an Eclipse project (note the git root
 is at the project level rather than in the directory above the project, as may
 be more common; in other words, this repository should be cloned within
 an existing Eclipse workspace, rather than as the workspace itself). Within that
@@ -34,19 +25,15 @@ dealing with an arithmetical/imperative language (except in a couple of
 isolated instances in which the relevant phenomenon is recast in the
 propositional language).
 
-This (Mkdocs-generated) documentation seeks to clarify the ways that Stratego
-transformations may be run in the Spoofax/Eclipse IDE environment, serving as
-a supplement/replacement for the portions of the manual that are
-specific to Stratego/XT.
-
 ## Preliminaries
 
 I recommend working with a complete pre-built Eclipse installation of Spoofax
 as provided by the Spoofax project,
 for example one that you can download from their
 [development release page](https://www.metaborg.org/en/latest/source/release/development.html).
-I have been unable to get the examples in this repository working starting from
-plain Eclipse and installing Spoofax in it using the Spoofax update site.
+Sometimes I have had difficulty getting the examples in this repository working
+starting from plain Eclipse and installing Spoofax in it using the Spoofax
+update site.
 
 If at any point in using the examples things appear to stop working, and
 especially if the Spoofax menu item disappears or the Spoofax menu turns into
@@ -68,9 +55,10 @@ operation at some point in the above process.
 
 ## Abstract syntax
 
-With the preliminaries out of the way, let's begin delving into Stratego
-transformations by recalling the abstract syntax of the
-Spoofax Propositional Language (SPL), as defined 
+With the preliminaries out of the way, note that the examples in the Stratego
+manual deal exclusively with Abstract Syntax Trees (ASTs). The trees used
+are primarily for a language concerning propositional logic, which we dub the
+Spoofax Propositional Language (SPL). It is defined
 at the top of {! docrefs/sec4.1.md !} of the manual.
 It consists of the following signature of constructors:
 
diff --git a/docrefs/sec4.2.md b/docrefs/sec4.2.md
index 8328565..1722d82 100644
--- a/docrefs/sec4.2.md
+++ b/docrefs/sec4.2.md
@@ -1 +1 @@
-[Section 4.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/04-term-rewriting.html#adding-rules-to-a-rewrite-system)
+[Section 4.3](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/04-term-rewriting.html#adding-rules-to-a-rewrite-system)
diff --git a/mkdocs.yml b/mkdocs.yml
index 4f979df..3ea4902 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -21,3 +21,4 @@ markdown_extensions:
 - pymdownx.superfences
 - pymdownx.highlight:
     use_pygments: true
+- smarty
diff --git a/syntax/Spoofax-Propositional-Language.sdf3 b/syntax/Spoofax-Propositional-Language.sdf3
index 8bf0eaa..3ce63ea 100644
--- a/syntax/Spoofax-Propositional-Language.sdf3
+++ b/syntax/Spoofax-Propositional-Language.sdf3
@@ -68,7 +68,4 @@ you can visit the file `syntax/examples/sec4.1_A.spl` (or ...`_B.spl`) and from
 Spoofax menu select "Syntax > Show parsed AST" to see the AST generation
 in action.)
 
-This concrete syntax actually makes it easier to construct the example
-expressions used throughout the tutorial manual as examples for Stratego
-processing.
 **/
diff --git a/test/manual-suite.spt b/test/manual-suite.spt
index 57a2297..348120a 100644
--- a/test/manual-suite.spt
+++ b/test/manual-suite.spt
@@ -267,40 +267,6 @@ test chap9_cnf7_ex [[
                        Or(Not(Atom("r")), Atom("q"))),
                    Atom("p"))
 
-/** md
-The key point to know about
-[Chapter 9](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/09-traversal-strategies.html),
-however, is that there is a mistake that affects examples `prop-dnf8` through
-`prop-dnf10`. The difficulty is in this definition:
-```Stratego
-strategies
-  propbu(s) = proptr(propbu(s)); s
-```
-
-Recall that `proptr` is defined as follows: (Note that our implementation calls
-it `proptr7` to distinguish it from different definitions for `proptr` in other
-examples.)
-```Stratego
-{! ../trans/prop-dnf7.str extract:
-  start: '(rules\n*)'
-  stop: strategies
-!}
-```
-
-So `propbu` must be defined as:
-```Stratego
-{! ../trans/prop-dnf8.str extract:
-  start: strategies
-  stop: '(.*propbu8.*)'
-!}
-```
-
-The point is that `proptr` cannot apply to `Atom`s and logical constants, and so
-fails when it reaches such nodes in the AST. Without the `try` in the definition
-of the `propbu` traversal, any such failure propagates to a failure of the entire
-strategy.
-**/
-
 test chap9_dnf8_ex [[
   (r -> p & q) & p
 ]] run dnf8 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
@@ -311,10 +277,6 @@ test chap9_cnf8_ex [[
                        Or(Not(Atom("r")), Atom("q"))),
                    Atom("p"))
 
-/** md
-Example `prop-dnf9` simply re-uses `propbu8`.
-**/
-
 test chap9_dnf9_ex [[
   (r -> p & q) & p
 ]] run dnf9 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
@@ -325,14 +287,6 @@ test chap9_cnf9_ex [[
                        Or(Not(Atom("r")), Atom("q"))),
                    Atom("p"))
 
-/** md
-And a similar fix is made to `prop-dnf10`:
-```Stratego
-{! ../trans/prop-dnf10.str !}
-```
-
-**/
-
 test sec9_1_dnf10_ex [[
   (r -> p & q) & p
 ]] run dnf10 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
@@ -343,22 +297,6 @@ test sec9_1_cnf10_ex [[
                        Or(Not(Atom("r")), Atom("q"))),
                    Atom("p"))
 
-/** md
-There is another issue in the "Format Checking" example in section 9.1. It lies
-with the strategy used to determine if an expression is an atom or the negation
-of an atom. The expression shown is `Not(Atom(x)) <+ Atom(x)`. This appears to
-be a left choice of two congruences. But a congruence expects a strategy as an
-argument, whereas here `x` is simply a free variable. There are a couple of
-fixes to write an expression that checks whether a term is just an `Atom()` call
-or the negation of one. The first possibility is to use match expressions, e.g.
-`?Not(Atom(x)) <+ ?Atom(x)`. However, as that can run into issues with the scoping
-of the variable `x`, we opted for sticking with the congruences, just using a
-strategy that always succeeds in the inner position, namely `id`:
-```Stratego
-{! ../trans/sec9_1.str terminate: exercise !}
-```
-**/
-
 test sec9_1_disj-nf_fails [[
   (r -> p & q) & p
 ]] run disj-nf fails
@@ -386,7 +324,7 @@ test sec9_1_cnf11_ex [[
                     Atom("p"))
 
 /** md
-Also note that the repository does not include `prop-dnf12` because at this
+Note that this repository does not include `prop-dnf12` because at this
 point the strategies there have become identical to the ones
 in {! ../docrefs/sec6.2.md !} used to introduce the idea of splitting
 transformations into local rewrite rules applied via a traversal strategy. So
@@ -454,8 +392,7 @@ test sec9_2_impl-nf_once [[
 ]] run impl-nf2 to Impl(Impl(Atom("p"),Impl(Atom("q"),False())),False())
 
 /** md
-I couldn't think of a natural application of paramorphism in the context of
-the Spoofax Propositional Language, so there is no solution provided for the
+On the other hand there is no solution provided for the
 exercise just before
 [Section 9.2.1](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/09-traversal-strategies.html#cascading-transformations).
 
diff --git a/trans/prop-dnf-rules.str b/trans/prop-dnf-rules.str
index dcf6a86..9e2203e 100644
--- a/trans/prop-dnf-rules.str
+++ b/trans/prop-dnf-rules.str
@@ -5,11 +5,29 @@ Title: Running a Strategy, continued
 
 The next Stratego example, in {! ../docrefs/sec4.2.md !}, extends
 `prop-eval-rules` to convert SPL propositions into disjunctive normal form (DNF).
-Once again, we can place the Stratego code in `trans/prop-dnf-rules.str`:
+As the manual notes, another way to see what the `dnf` strategy does to a given
+AST is to add a Spoofax Test Language test that claims it transforms to
+something that it definitely does **not** parse to, e.g.
+```SPT
+{! ../test/manual-suite.spt extract:
+  start: '\*\*[/]'
+terminate: '(.*run dnf.*)$' !}
+```
 
+The difficulty is that in a standard Spoofax language project, the error popup
+showing what the transformation actually does is nearly unreadable due to
+a tremendous amount of annotation produced by the default static analysis process.
+
+Since in this repository we are not actually doing any (meaningful) static
+analysis, it includes a hack which makes the editor popup much more readable.
+Namely, it strips the annotation, by modifying the
+`editor-analyze` rule in `trans/analysis.str` like so:
 ```Stratego
+{! ../trans/analysis.str terminate: Debugging!}  [rest of file omitted]
+```
+
 **/
-/** md Include this code in documentation: */
+
 module prop-dnf-rules
 imports prop-eval-rules
 rules
@@ -23,121 +41,3 @@ rules
 
   E : And(Or(x, y), z) -> Or(And(x, z), And(y, z))
   E : And(z, Or(x, y)) -> Or(And(z, x), And(z, y))
-/* end of code inclusion **/
-/** md rest of documentation
-```
-and create a `trans/prop-dnf.str` that defines a strategy for applying the
-DNF rules and supplies the glue needed between ESV and Stratego:
-```Stratego
-{! prop-dnf.str !}
-```
-Now just importing `prop-dnf` in `trans/spoofax-propositional-language.str`
-and adding a menu item to `editor/Manual.esv`:
-```ESV
- ...
-{! ../editor/Manual.esv extract: {start: menus, stop: dnf3} !}
-```
-should suffice to make the dnf strategy available in the "Spoofax > Manual"
-menu.
-
-Indeed, we can try it out on `syntax/examples/sec4.2_test3.spl`:
-```SPL
-{! ../syntax/examples/sec4.2_test3.spl !}
-```
-to produce
-```
-{! ../syntax/examples/sec4.2_test3.dnf.aterm !}
-```
-as verified in the manual (again, modulo the "ATom" typo in the manual).
-
-However, we also want to use this second example to show another method of
-running Stratego strategies from the Eclipse IDE.
-
-### Spoofax Testing Language
-
-The
-[Spoofax Testing Language](http://www.metaborg.org/en/latest/source/langdev/meta/lang/spt/index.html)
-(SPT) is a declarative language that provides for a full range of tests
-for a Spoofax language project. As such, it includes the ability to run an
-arbitrary Stratego strategy on the results of parsing an arbitrary piece of
-the language you're working with -- seemingly perfect for our interest in
-trying our different Stratego transformations.
-
-So, we can just take our `test3` expression above and make it a part of
-an SPT test suite, which we will call `test/manual-suite.spt`:
-```SPT
-{! ../test/manual-suite.spt extract:
-  start: '\*\*[/]'
-terminate: '(.*run dnf)' !}
-```
-
-Once we have saved this file, the tests run automatically. What does this mean?
-The file seems to be just "sitting there;" there's no indication that anything
-is happening. That's because this test we've just written **succeeds**. All we
-asked is that Spoofax run the `dnf` transformation on the results of parsing
-the test expression. It did that, and the transformation succeeded. So all is
-well, and no output is generated.
-
-But of course, we want to see what the _result_ of the transformation was. One
-way of arranging that is to ask that SPT compare that result to a given AST.
-If we use an AST like `Atom("x")` that can't possibly be the actual output
-(since "x" does not occur in the input), then the error message will show
-what the transformation actually produced. So we add just a bit to
-`test/manual-suite.spt`:
-```SPT
-{! ../test/manual-suite.spt extract:
-  start: '\*\*[/]'
-terminate: '(.*run dnf.*)$' !}
-```
-
-and now sure enough a little error symbol appears next to the test. If you hover
-over it, a popup will show up, indicating that SPT was expecting `Atom("x")`,
-but got... wait! What's this monstrosity?
-```
-Got: Or(And(Not(Atom("r"{TermIndex("test/manual-suite.spt",1)}){TermIndex
- ("test/manual-suite.spt",2)}),Atom("p"{TermIndex("test/manual-suite.spt",9)})
- {TermIndex("test/manual-suite.spt",10)}),And(And(Atom("p"{TermIndex("test/manual-
- suite.spt",3)}){TermIndex("test/manual-suite.spt",4)},Atom("q"{TermIndex
- ("test/manual-suite.spt",5)}){TermIndex("test/manual-suite.spt",6)}){TermIndex
- ("test/manual-suite.spt",7)},Atom("p"{TermIndex("test/manual-suite.spt",9)})
- {TermIndex("test/manual-suite.spt",10)}))
-```
-
-Well, it is actually the result of running the `dnf` strategy on the result of
-parsing ` {! ../syntax/examples/sec4.2_test3.spl !} `. It's just that Spoofax
-automatically annotates every subterm of the parsed term with its location in
-the input, and those annotations are carried through the Stratego
-transformation. While this can be very helpful in figuring out exactly what
-happened in the course of the transformation, it can also make the output
-practically unreadable.
-
-Fortunately, we can strip this annotation if we like, by modifying the
-`editor-analyze` rule in `trans/analysis.str` like so:
-```Stratego
-{! ../trans/analysis.str terminate: Debugging!}  [rest of file omitted]
-```
-
-Now rebuild the project and re-run the SPT manual suite. (You may need to
-do an irrelevant edit and save of the `test/manual-suite.spt` file, or
-you can select this file in the project explorer and select the menu item
-"Spoofax (meta) > Run all selected tests" to pop up a convenient window of
-all test results.) Now you should see the much more readable
-```
-Got: Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
-```
-in the error message for the `sec4_2_test3` test.
-
-Of course, if you know the AST you expect to generate with your transformation,
-you can also just tell SPT to compare against that, for example in our case
-by adding a test to the manual suite like this:
-```SPT
-{! ../test/manual-suite.spt extract:
-  start: '(test sec4_2_test3_ex.*\n?)$'
-  stop: '^(.*run.*)$'
-!}
-```
-
-Now if there is no error or warning on this test then you know the
-`dnf` strategy produced the result shown in the `to` clause, and otherwise,
-the actual result will be shown in the error popup.
-**/
diff --git a/trans/prop-dnf3.str b/trans/prop-dnf3.str
index ec38da7..cc1f2c5 100644
--- a/trans/prop-dnf3.str
+++ b/trans/prop-dnf3.str
@@ -4,7 +4,7 @@ Title: Running a Strategy: the command line
 ## Functionalizing reduction rules
 
 The {! ../docrefs/manual.md !} next goes on, in Chapter 5, to consider ways to
-add the ability to also compute conjunctive normal forms for propositional
+add the ability to also compute conjunctive normal forms (CNF) for propositional
 ASTs. The rules for this form cannot simply be added to those from the prior
 chapter for disjunctive normal form, as they would produce a non-terminating
 rewrite system.
@@ -12,13 +12,26 @@ rewrite system.
 The first method for which working examples are provided is the method of
 "functionalization" in {! ../docrefs/sec5.1.2.md !}. Although an anti-pattern
 in the views of the Spoofax designers, the examples are still instructive and
-of course we want to implement them here.
+of course they are implemented here.
+
+In fact, the Stratego code
+for the CNF is not given explicitly in the manual, but it consists of:
+```
+{! prop-cnf3.str !}
+```
+
+Note in particular we have not repeated the `make-nf` strategy from
+`trans/prop-dnf3.str` here --- that's the
+entire point of functionalization; we can use the same top-level reduction
+scheme because the introduced function symbols keep track of what operations
+are being performed. We also introduce a strategy `dcnf` for the simultaneous
+construction of DNF and CNF, as noted in the manual.
+
+Again, there are menu items and SPT cases for the `cnf3` and `dcnf` strategies
+as well. All operate just as in the previous sections.
 
-So, we can grab the Stratego code given in the section as our
-`trans/prop-dnf3.str`:
-```Stratego
 **/
-/** md  Include this code in docs: */
+
 module prop-dnf3
 imports libstrategolib signatures/-
 signature
@@ -50,53 +63,8 @@ strategies
   do-dnf3: (selected, _, _, path, project-path) -> (filename, result)
     with filename := <guarantee-extension(|"dnf.aterm")> path
        ; result   := <dnf3> selected
-/* End of code inclusion **/
-/** md  Conclusion of documentation:
-```
 
-Notice the few minor differences from the manual. We import `signatures/-` as
-before. We've used a fresh identifier for the `E` and `D` rules, because unlike
-in the manual, all of our Stratego files are imported into the same main
-`trans/spoofax_propositional_language.str` module. So they must live together,
-but as noted in the manual, these functionalized rules do not "play together"
-nicely with the evaluation `E` rules introduced [earlier](prop-eval-rules.md).
-And we've renamed the `dnf` rule to `make-nf` -- for a reason that will
-become clear in a moment -- but incorporated the wrapping by `Dnf` of the AST
-we want to compute the DNF of into the `dnf3` strategy, since our concrete
-syntax has no way of specifying such a wrapping.
-
-Also as before, we've created a `syntax/examples/sec_5_1_2_test1.spl`
-(which it turns out is just the same as `sec_4_2_test3.spl`)
-and a menu item and a `test/manual-suite.spt` case called `sec5_1_2_test1_ex` to
-see that all is working well. Applying `dnf3` to the test file produces
-```
-{! ../syntax/examples/sec5.1.2_test1.dnf.aterm !}
-```
-which is correct. (Note the contrast with what's shown in
-{! ../docrefs/sec5.1.2.md !} as the output of the `prop-dnf3` program,
-in which the recurring "ATom" typo has blocked
-the reductive elimination of some of the occurrences of the Dnf function
-symbol. Of course, as the manual itself points out, in proper operation of
-this functionalization approach, all of the function symbols must reduce away
-to end up back in an AST of the subject language.)
-
-So now we can move on to the conjunctive normal form. The Stratego code
-for the CNF is not given explicitly in the manual, but it consists of:
-```
-{! prop-cnf3.str !}
-```
-
-Note in particular we have not repeated the `make-nf` strategy -- that's the
-entire point of functionalization; we can use the same top-level reduction
-scheme because the introduced function symbols keep track of what operations
-are being performed. We also introduce a strategy `dcnf` for the simultaneous
-construction of DNF and CNF, as noted in the manual.
-
-Again, there are menu items and SPT cases for the `cnf3` and `dcnf` strategies
-as well. All operate just as in the previous two sections.
-
-We can now use this example to show yet another way to try Stratego stragies
-with the Spoofax IDE implementation.
+/** md
 
 ### Command-line Utilities
 
@@ -105,7 +73,8 @@ The Spoofax project offers an executable jar called
 that allows several different Spoofax actions to be invoked from the command line.
 Let's say you have downloaded it to the path `SUNSHINE_JAR`. Then you can see a
 summary of the available actions with `java -jar $SUNSHINE_JAR -h`. In the
-repository there's a convenience bash script `bin/spoofax-menu`:
+repository there's a convenience bash script `bin/spoofax-menu` you can use to
+run the Sunshine jar:
 ```bash
 {! ../bin/spoofax-menu extract:
 - stop: --help
diff --git a/trans/prop-eval-rules.str b/trans/prop-eval-rules.str
index d5da8cc..21723b5 100644
--- a/trans/prop-eval-rules.str
+++ b/trans/prop-eval-rules.str
@@ -5,17 +5,60 @@ Title: Running a Strategy
 
 The first example of running a Stratego strategy
 in the {! ../docrefs/manual.md !} is that of _evaluating_ an AST,
-via the `prop-eval-rules` module in {! ../docrefs/sec4.1.md !}. This page
-describes the most straightforward way to run this same strategy
-in the Spoofax Eclipse IDE.
+via the `prop-eval-rules` module in {! ../docrefs/sec4.1.md !}. In this
+repository, we've placed those rules in `trans/prop-eval-rules.str`,
+and the glue strategies that call them in `trans/prop-eval.str`. This latter
+module is imported by `trans/spoofax_propositional_language.str`.
 
-In the current project structure, Stratego transformations and strategies go in
-the `trans` directory. So, you can place the Stratego code for
-this module in `trans/prop-eval-rules.str`, with the following contents:
+(I am unclear on what triggers Editor Services to use this particular Stratego
+file, but in any automatically-generated Spoofax project there will be a
+main language Stratego file in the `trans` directory, and that's the file
+from which the rule specified in an ESV `action` has to be visible.)
+
+There's an Editor Services module `editor/Manual.esv` to invoke the eval strategy,
+and it's included in in `editor/Main.esv.`
+
+With all of these elements in place, you should now be able to invoke
+the `eval` rule from the "Spoofax" menu. For example, to execute the "test1"
+example from the Spoofax Tutorial/Reference
+{! ../docrefs/sec4.1.md !}, navigate to the
+file `syntax/examples/sec4.1_test1.spl`:
+```SPL
+{! ../syntax/examples/sec4.1_test1.spl !}
+```
+and select "Spoofax > Manual > prop-eval" from the menu bar to produce:
+```
+{! ../syntax/examples/sec4.1_test1.eval.aterm !}
+```
+You can do the same with test2:
+```SPL
+{! ../syntax/examples/sec4.1_test2.spl !}
+```
+to produce
+```
+{! ../syntax/examples/sec4.1_test2.eval.aterm !}
+```
+
+Both of these results match the expected output of the `eval` transformation
+as shown in {! ../docrefs/sec4.1.md !}.
+
+One other note about the files provided in this repository. The "do-XXX" rule
+used as boilerplate glue between ESV and a Stratego strategy in
+`trans/prop-eval.str` is:
 
 ```Stratego
-[End the documentation block to avoid the comment close in the code] **/
-/** md [restart processing to include the code in the documentation] */
+{! prop-eval.str extract: {start: '^(.*Interface.*\s*)$'} !}
+```
+
+The version of this glue being used here corresponds to what's used in the example
+[Calc language project](https://github.com/MetaBorgCube/metaborg-calc),
+but is slightly different from what is described in the
+[Menus section](http://www.metaborg.org/en/latest/source/langdev/meta/lang/esv.html#menus)
+of the ESV Manual. I am unclear on the significance of this difference or which
+form is "better" -- I simply modeled this Stratego code after the code in the
+working Calc repository, and all seems to be well.
+**/
+
 module prop-eval-rules
 imports signatures/-
 rules
@@ -37,116 +80,3 @@ rules
   E : Eq(x, False())   -> Not(x)
   E : Eq(True(), x)    -> x
   E : Eq(x, True())    -> x
-/* [stop to avoid the open-comment in the code block] **/
-/** md [conclusion of the documentation]
-```
-
-Note an important difference between this code and the `prop-eval-rules` block
-in {! ../docrefs/sec4.1.md !}: here, we import `signatures/-` rather than `prop`.
-That's because the Spoofax IDE automatically generates the Spoofax Propositional
-Language AST signature for us, from its concrete syntax definition. (The
-evaluation rules in {! ../docrefs/sec4.1.md !} also happen to be missing the
-fourth `Impl` rule, but that's less material; unsurprisingly, none of the examples
-given in the manual happen to rely on that rule, but we include it here for the
-sake of completeness.)
-
-As in the {! ../docrefs/manual.md !}, we need an additional module, which we can
-place in `trans/prop-eval.str`, to describe the strategy by which we want
-to apply the above evaluation rules and to facilitate actually invoking
-the strategy on an AST. This file starts out much like its counterpart in
-{! ../docrefs/sec4.1.md !}:
-
-```Stratego
-{! prop-eval.str {terminate:  '^\s*$'} !}
-```
-
-So far, we've included the evaluation rules and defined a strategy `eval` to
-apply them exhaustively to an AST starting with inner subterms. Now we want to
-be able to "run" this strategy on an actual AST.
-
-### Editor Services
-
-The most straightforward mechanism to execute a Stratego transformation
-in the Spoofax IDE is by use of Editor Services (ESV). ESV is actually a full
-declarative language in its own right, covering syntax coloring, menu items,
-hover texts, and more, and with its own
-[manual](http://www.metaborg.org/en/latest/source/langdev/meta/lang/esv.html).
-We will not delve into the details of ESV here, but merely provide a recipe
-for using it to add an item to the "Spoofax" Eclipse menu for running Stratego.
-
-Actually, we'll create a submenu "Manual" for our examples. It's
-cleanest to put our additions in a separate ESV module, which then must be
-included into the `editor/Main.esv` file, like so:
-```esv
-{! ../editor/Main.esv extract:
-  replace: ['^\s*$']
-terminate: 'provider\s*:' !}  [ ... rest of file suppressed for brevity. ]
-```
-It's just the one line "Manual" in the `imports` section that we have added. The
-`editor/Manual.esv` implementing the submenu is also very simple:
-```esv
-{! ../editor/Manual.esv terminate: dnf !}
-```
-Note that the quoted string on the `action` line is the text label of the menu
-item in the "Manual" submenu, and the identifier on its right-hand side is the
-Stratego action to call. But note that `do-eval` is not the same identifier as
-`eval` in our last Stratego file above. That's because the Stratego invocation
-caused by an ESV action item has a specific, multi-item argument list, whereas
-`eval` above expects only a single Spoofax Propositional Language AST to operate
-on. To bridge this gap, we must add one more item to `trans/prop-eval.str`,
-namely:
-```Stratego
-{! prop-eval.str extract: {start: '^(.*Interface.*\s*)$'} !}
-```
-This "do-XXX" rule is pretty much boilerplate glue between ESV and your Stratego
-strategy of interest. (Note that this "glue" being used here corresponds to
-what's used in the example
-[Calc language project](https://github.com/MetaBorgCube/metaborg-calc),
-but is slightly different from what is described in the
-[Menus section](http://www.metaborg.org/en/latest/source/langdev/meta/lang/esv.html#menus)
-of the ESV Manual. I am unclear on the significance of this difference or which
-form is "better" -- I simply modeled this Stratego code after the code in the
-working Calc repository, and all seems to be well.)
-
-There's one last step before you can run `eval` from inside the IDE.
-Editor Services has to be able to find the `do-eval` rule. You can enable that
-by importing the `prop-eval` module in the main Stratego file for our language,
-in this case `trans/spoofax_propositional_language.str`:
-```Stratego
-{! spoofax_propositional_language.str extract:
-  - stop: 'prop-dnf'
-  - start: '^(.*rule.*)$'
-terminate: debug-show
-!}
-  [ ... rest of file suppressed. ]
-```
-(I am unclear on what triggers ESV to use this particular Stratego file, but
-in any automatically-generated Spoofax project there will be a main language
-Stratego file in the `trans` directory, and that's the file from which
-the rule specified in an ESV `action` has to be visible.)
-
-Ok, with all of these elements in place, you should now be able to invoke
-the `eval` rule from the "Spoofax" menu. For example, to execute the next example
-from the Spoofax Tutorial/Reference
-{! ../docrefs/sec4.1.md !}, navigate to the
-file `syntax/examples/sec4.1_test1.spl`:
-```SPL
-{! ../syntax/examples/sec4.1_test1.spl !}
-```
-and select "Spoofax > Manual > prop-eval" from the menu bar to produce:
-```
-{! ../syntax/examples/sec4.1_test1.eval.aterm !}
-```
-You can do the same with test2:
-```SPL
-{! ../syntax/examples/sec4.1_test2.spl !}
-```
-to produce
-```
-{! ../syntax/examples/sec4.1_test2.eval.aterm !}
-```
-
-Both of these results match the expected output of the `eval` transformation
-as shown in {! ../docrefs/sec4.1.md !} (allowing for the typo "ATom" in the
-manual in the latter case).
-**/