[sphinx] Add abort and restart options to directive coqtop.

3 files changed, 21 insertions, 11 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index a341cd9401..accba737fd 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -220,7 +220,7 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
           Definition a := 1.
 
     The blank line after the directive is required.  If you begin a proof,
-    include an ``Abort`` afterwards to reset coqtop for the next example.
+    use the ``abort`` option to reset coqtop for the next example.
 
     Here is a list of permissible options:
 
@@ -234,7 +234,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
     - Behavior options
 
       - ``reset``: Send a ``Reset Initial`` command before running this block
-      - ``fail``: Don't die if a command fails.
+      - ``fail``: Don't die if a command fails
+      - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode)
+      - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any)
 
     ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
     of the same document (``coqrst`` creates a single ``coqtop`` process per
@@ -508,7 +510,7 @@ Tips and tricks
 Nested lemmas
 -------------
 
-The ``.. coqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas::
+The ``.. coqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas (which by default results in a failure)::
 
    .. coqtop:: all
 
@@ -518,7 +520,7 @@ The ``.. coqtop::`` directive does *not* reset Coq after running its contents.
 
       Lemma l2: 2 + 2 <> 1.
 
-Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas.
+Add either ``abort`` to the first block or ``reset`` to the second block to avoid nesting lemmas.
 
 Abbreviations and macros
 ------------------------
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 81f25bf274..78803a927f 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -265,7 +265,7 @@ Tips and tricks
 Nested lemmas
 -------------
 
-The ``.. coqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas::
+The ``.. coqtop::`` directive does *not* reset Coq after running its contents.  That is, the following will create two nested lemmas (which by default results in a failure)::
 
    .. coqtop:: all
 
@@ -275,7 +275,7 @@ The ``.. coqtop::`` directive does *not* reset Coq after running its contents.
 
       Lemma l2: 2 + 2 <> 1.
 
-Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas.
+Add either ``abort`` to the first block or ``reset`` to the second block to avoid nesting lemmas.
 
 Abbreviations and macros
 ------------------------
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 2d8bb43e62..36b842d347 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -566,7 +566,7 @@ class CoqtopDirective(Directive):
           Definition a := 1.
 
     The blank line after the directive is required.  If you begin a proof,
-    include an ``Abort`` afterwards to reset coqtop for the next example.
+    use the ``abort`` option to reset coqtop for the next example.
 
     Here is a list of permissible options:
 
@@ -580,7 +580,9 @@ class CoqtopDirective(Directive):
     - Behavior options
 
       - ``reset``: Send a ``Reset Initial`` command before running this block
-      - ``fail``: Don't die if a command fails.
+      - ``fail``: Don't die if a command fails
+      - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode)
+      - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any)
 
     ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
     of the same document (``coqrst`` creates a single ``coqtop`` process per
@@ -831,16 +833,18 @@ class CoqtopBlocksTransform(Transform):
         """Parse options according to the description in CoqtopDirective."""
         opt_reset = 'reset' in options
         opt_fail = 'fail' in options
+        opt_restart = 'restart' in options
+        opt_abort = 'abort' in options
         opt_all, opt_none = 'all' in options, 'none' in options
         opt_input, opt_output = opt_all or 'in' in options, opt_all or 'out' in options
 
-        unexpected_options = list(set(options) - set(('reset', 'fail', 'all', 'none', 'in', 'out')))
+        unexpected_options = list(set(options) - set(('reset', 'fail', 'restart', 'abort', 'all', 'none', 'in', 'out')))
         if unexpected_options:
             raise ValueError("Unexpected options for .. coqtop:: {}".format(unexpected_options))
         elif (opt_input or opt_output) and opt_none:
             raise ValueError("Inconsistent options for .. coqtop:: ‘none’ with ‘in’, ‘out’, or ‘all’")
 
-        return opt_reset, opt_fail, opt_input and not opt_none, opt_output and not opt_none
+        return opt_reset, opt_fail, opt_restart, opt_abort, opt_input and not opt_none, opt_output and not opt_none
 
     @staticmethod
     def block_classes(should_show, contents=None):
@@ -866,10 +870,12 @@ class CoqtopBlocksTransform(Transform):
 
     def add_coq_output_1(self, repl, node):
         options = node['coqtop_options']
-        opt_reset, opt_fail, opt_input, opt_output = self.parse_options(options)
+        opt_reset, opt_fail, opt_restart, opt_abort, opt_input, opt_output = self.parse_options(options)
 
         pairs = []
 
+        if opt_restart:
+            repl.sendone("Restart.")
         if opt_reset:
             repl.sendone("Reset Initial.")
             repl.sendone("Set Coqtop Exit On Error.")
@@ -877,6 +883,8 @@ class CoqtopBlocksTransform(Transform):
             repl.sendone("Unset Coqtop Exit On Error.")
         for sentence in self.split_sentences(node.rawsource):
             pairs.append((sentence, repl.sendone(sentence)))
+        if opt_abort:
+            repl.sendone("Abort All.")
         if opt_fail:
             repl.sendone("Set Coqtop Exit On Error.")