From 19076a5163eb1437a14ba1bfdf71e10a9b44858a Mon Sep 17 00:00:00 2001
From: Glen Whitney <glen@studioinfinity.org>
Date: Tue, 19 Jan 2021 18:34:00 -0800
Subject: [PATCH] doc: document running strategies with the Sunshine jar

---
 editor/Manual.esv   |  2 +-
 trans/prop-dnf3.str | 53 +++++++++++++++++++++++++++++++++++----------
 2 files changed, 43 insertions(+), 12 deletions(-)

diff --git a/editor/Manual.esv b/editor/Manual.esv
index e91573b..c3a2aea 100644
--- a/editor/Manual.esv
+++ b/editor/Manual.esv
@@ -5,4 +5,4 @@ menus
     action: "prop-dnf"  = do-dnf
     action: "prop-dnf3" = do-dnf3
     action: "prop-cnf3" = do-cnf3
-    action: "both nf3"  = do-dcnf
+    action: "both-nf3"  = do-dcnf
diff --git a/trans/prop-dnf3.str b/trans/prop-dnf3.str
index 6b9d0a3..ec38da7 100644
--- a/trans/prop-dnf3.str
+++ b/trans/prop-dnf3.str
@@ -93,20 +93,51 @@ 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. There's one caveat here, though. The test case for `dcnf`:
-```SPT
-{! ../test/manual-suite.spt extract:
-  start: '^(.*test.*both.*\n?)$'
-!}
-```
-does not actually work, because of what appears to be a bug in SPT: the `to`
-in the expectation line is interpreted as part of the expected AST. However,
-the error message does show that the transformation is operating properly.
+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.
 
 ### Command-line Utilities
 
-[HERE]
-**/
\ No newline at end of file
+The Spoofax project offers an executable jar called
+[Sunshine](http://www.metaborg.org/en/latest/source/release/development.html#command-line-utilities)
+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`:
+```bash
+{! ../bin/spoofax-menu extract:
+- stop: --help
+- start: ';;'
+!}
+```
+(You can also get a usage explanation, elided from the listing above, via
+`bin/spoofax-menu -h`.)
+
+To use this, you must have a Spoofax menu item set up to run the strategy you
+want, but then you can invoke it on an arbitrary file from the command line like
+so:
+```
+spoofax_prop> export SUNSHINE_JAR=~/software/org.metaborg.sunshine2-2.6.0-20210119.175231-1.jar
+spoofax_prop> export ECLIPSE_INSTALL=~/software/spoofax
+spoofax_prop> export SPOOFAX_PROJECT=~/code/neweclipse/spoofax_prop
+spoofax_prop> bin/spoofax-menu syntax/examples/sec5.1.2_test1.spl both-nf3
+( Or(
+    And(Not(Atom("r")), Atom("p"))
+  , And(And(Atom("p"), Atom("q")), Atom("p"))
+  )
+, And(
+    And(
+      Or(Not(Atom("r")), Atom("p"))
+    , Or(Not(Atom("r")), Atom("q"))
+    )
+  , Atom("p")
+  )
+)
+```
+
+In our case, the Sunshine jar doesn't really give us any new capabilities, and
+the ESV menu items still have to be set up, but it could make running examples
+more convenient for you.
+**/