diff options
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 14 |
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: |