Sphinx: fail when a command fails

This uses a new coqtop-only option "Coqtop Exit On Error", not sure where
to put the doc for it. It being an option means we can locally turn it
off (.. coqtop:: fail).

1 files changed, 11 insertions, 3 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index f9840dc19a..c9535bd2fc 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -580,6 +580,7 @@ class CoqtopDirective(Directive):
     - Behavior options
 
       - ``reset``: Send a ``Reset Initial`` command before running this block
+      - ``fail``: Don't die if a command fails.
 
     ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
     of the same document (``coqrst`` creates a single ``coqtop`` process per
@@ -829,16 +830,17 @@ class CoqtopBlocksTransform(Transform):
     def parse_options(options):
         """Parse options according to the description in CoqtopDirective."""
         opt_reset = 'reset' in options
+        opt_fail = 'fail' 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', 'all', 'none', 'in', 'out')))
+        unexpected_options = list(set(options) - set(('reset', 'fail', '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_input and not opt_none, opt_output and not opt_none
+        return opt_reset, opt_fail, opt_input and not opt_none, opt_output and not opt_none
 
     @staticmethod
     def block_classes(should_show, contents=None):
@@ -867,15 +869,21 @@ class CoqtopBlocksTransform(Transform):
 
         Finds nodes to process using is_coqtop_block."""
         with CoqTop(color=True) as repl:
+            repl.sendone("Set Coqtop Exit On Error.")
             for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block):
                 options = node['coqtop_options']
-                opt_reset, opt_input, opt_output = self.parse_options(options)
+                opt_reset, opt_fail, opt_input, opt_output = self.parse_options(options)
 
                 if opt_reset:
                     repl.sendone("Reset Initial.")
+                    repl.sendone("Set Coqtop Exit On Error.")
+                if opt_fail:
+                    repl.sendone("Unset Coqtop Exit On Error.")
                 pairs = []
                 for sentence in self.split_sentences(node.rawsource):
                     pairs.append((sentence, repl.sendone(sentence)))
+                if opt_fail:
+                    repl.sendone("Set Coqtop Exit On Error.")
 
                 dli = nodes.definition_list_item()
                 for sentence, output in pairs: