0001-doc-Add-position-information-to-messages-printed-whe.patch

From 1815f38d4b41257b02c08fa73d50f64712a801a0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= <[email protected]>
Date: Thu, 7 Feb 2019 15:39:35 -0500
Subject: [PATCH] [doc] Add position information to messages printed when
 coqtop fails

---
 doc/tools/coqrst/coqdomain.py   | 69 +++++++++++++++++++++++++----------------
 doc/tools/coqrst/repl/coqtop.py | 22 ++++++++-----
 2 files changed, 56 insertions(+), 35 deletions(-)

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 067af95..e9392af 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -30,15 +30,14 @@ from sphinx import addnodes
 from sphinx.roles import XRefRole
 from sphinx.errors import ExtensionError
 from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode
-from sphinx.util.logging import getLogger
+from sphinx.util.logging import getLogger, get_node_location
 from sphinx.directives import ObjectDescription
 from sphinx.domains import Domain, ObjType, Index
-from sphinx.domains.std import token_xrefs
 from sphinx.ext import mathbase
 
 from . import coqdoc
 from .repl import ansicolors
-from .repl.coqtop import CoqTop
+from .repl.coqtop import CoqTop, CoqTopError
 from .notations.sphinx import sphinxify
 from .notations.plain import stringify_with_ellipses
 
@@ -867,36 +866,52 @@ class CoqtopBlocksTransform(Transform):
                 blocks.append(re.sub("^", "    ", output, flags=re.MULTILINE) + "\n")
         return '\n'.join(blocks)
 
+    def add_coq_output_1(self, repl, node):
+        options = node['coqtop_options']
+        opt_undo, opt_reset, opt_input, opt_output = self.parse_options(options)
+
+        pairs = []
+
+        if opt_reset:
+            repl.sendone("Reset Initial.")
+        for sentence in self.split_sentences(node.rawsource):
+            pairs.append((sentence, repl.sendone(sentence)))
+        if opt_undo:
+            repl.sendone("Undo {}.".format(len(pairs)))
+
+        dli = nodes.definition_list_item()
+        for sentence, output in pairs:
+            # Use Coqdoq to highlight input
+            in_chunks = highlight_using_coqdoc(sentence)
+            dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(opt_input))
+            # Parse ANSI sequences to highlight output
+            out_chunks = AnsiColorsParser().colorize_str(output)
+            dli += nodes.definition(output, *out_chunks, classes=self.block_classes(opt_output, output))
+        node.clear()
+        node.rawsource = self.make_rawsource(pairs, opt_input, opt_output)
+        node['classes'].extend(self.block_classes(opt_input or opt_output))
+        node += nodes.inline('', '', classes=['coqtop-reset'] * opt_reset)
+        node += nodes.definition_list(node.rawsource, dli)
+
     def add_coqtop_output(self):
         """Add coqtop's responses to a Sphinx AST
 
         Finds nodes to process using is_coqtop_block."""
         with CoqTop(color=True) as repl:
             for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block):
-                options = node['coqtop_options']
-                opt_undo, opt_reset, opt_input, opt_output = self.parse_options(options)
-
-                if opt_reset:
-                    repl.sendone("Reset Initial.")
-                pairs = []
-                for sentence in self.split_sentences(node.rawsource):
-                    pairs.append((sentence, repl.sendone(sentence)))
-                if opt_undo:
-                    repl.sendone("Undo {}.".format(len(pairs)))
-
-                dli = nodes.definition_list_item()
-                for sentence, output in pairs:
-                    # Use Coqdoq to highlight input
-                    in_chunks = highlight_using_coqdoc(sentence)
-                    dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(opt_input))
-                    # Parse ANSI sequences to highlight output
-                    out_chunks = AnsiColorsParser().colorize_str(output)
-                    dli += nodes.definition(output, *out_chunks, classes=self.block_classes(opt_output, output))
-                node.clear()
-                node.rawsource = self.make_rawsource(pairs, opt_input, opt_output)
-                node['classes'].extend(self.block_classes(opt_input or opt_output))
-                node += nodes.inline('', '', classes=['coqtop-reset'] * opt_reset)
-                node += nodes.definition_list(node.rawsource, dli)
+                try:
+                    self.add_coq_output_1(repl, node)
+                except CoqTopError as err:
+                    import textwrap
+                    MSG = ("{}: Error while sending the following to coqtop:\n{}" +
+                           "\n  Last output was:\n{}" +
+                           "\n  Full error text:\n{}")
+                    indent = "    "
+                    loc = get_node_location(node)
+                    le = textwrap.indent(str(err.last_sentence), indent)
+                    lo = textwrap.indent(str(err.last_output), indent)
+                    fe = textwrap.indent(str(err.err), indent)
+                    raise ExtensionError(MSG.format(loc, le, lo, fe))
 
     @staticmethod
     def merge_coqtop_classes(kept_node, discarded_node):
diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py
index 3ff00ea..d51c613 100644
--- a/doc/tools/coqrst/repl/coqtop.py
+++ b/doc/tools/coqrst/repl/coqtop.py
@@ -20,6 +20,13 @@ import re
 
 import pexpect
 
+class CoqTopError(Exception):
+    def __init__(self, err, last_sentence, last_output):
+        super().__init__()
+        self.err = err
+        self.last_sentence = last_sentence
+        self.last_output = last_output
+
 class CoqTop:
     """Create an instance of coqtop.
 
@@ -49,6 +56,7 @@ class CoqTop:
             raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin))
         self.args = (args or []) + ["-boot"] * BOOT + ["-color", "on"] * color
         self.coqtop = None
+        self.last_output = None # Used for debugging
 
     def __enter__(self):
         if self.coqtop:
@@ -63,7 +71,7 @@ class CoqTop:
         self.coqtop.kill(9)
 
     def next_prompt(self):
-        "Wait for the next coqtop prompt, and return the output preceeding it."
+        """Wait for the next coqtop prompt, and return the output preceeding it."""
         self.coqtop.expect(CoqTop.COQTOP_PROMPT, timeout = 10)
         return self.coqtop.before
 
@@ -75,14 +83,12 @@ class CoqTop:
         """
         # Suppress newlines, but not spaces: they are significant in notations
         sentence = re.sub(r"[\r\n]+", " ", sentence).strip()
-        self.coqtop.sendline(sentence)
         try:
-            output = self.next_prompt()
-        except:
-            print("Error while sending the following sentence to coqtop: {}".format(sentence))
-            raise
-        # print("Got {}".format(repr(output)))
-        return output
+            self.coqtop.sendline(sentence)
+            self.last_output = self.next_prompt()
+        except Exception as err:
+            raise CoqTopError(err, sentence, self.last_output)
+        return self.last_output
 
 def sendmany(*sentences):
     """A small demo: send each sentence in sentences and print the output"""
-- 
2.7.4