[refman] Raise an error when a notation doesn't parse

2 files changed, 44 insertions, 15 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 0ade9fdbf5..1784519f5f 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -39,14 +39,29 @@ from sphinx.ext import mathbase
 from . import coqdoc
 from .repl import ansicolors
 from .repl.coqtop import CoqTop, CoqTopError
+from .notations.parsing import ParseError
 from .notations.sphinx import sphinxify
 from .notations.plain import stringify_with_ellipses
 
-def parse_notation(notation, source, line, rawtext=None):
+PARSE_ERROR = """Parse error in notation!
+Offending notation: {}
+Error message: {}"""
+
+def notation_to_sphinx(notation, source, line, rawtext=None):
     """Parse notation and wrap it in an inline node"""
-    node = nodes.inline(rawtext or notation, '', *sphinxify(notation), classes=['notation'])
-    node.source, node.line = source, line
-    return node
+    try:
+        node = nodes.inline(rawtext or notation, '', *sphinxify(notation), classes=['notation'])
+        node.source, node.line = source, line
+        return node
+    except ParseError as e:
+        raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e
+
+def notation_to_string(notation):
+    """Parse notation and format it as a string with ellipses."""
+    try:
+        return stringify_with_ellipses(notation)
+    except ParseError as e:
+        raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e
 
 def highlight_using_coqdoc(sentence):
     """Lex sentence using coqdoc, and yield inline nodes for each token"""
@@ -136,7 +151,7 @@ class CoqObject(ObjectDescription):
         self._render_signature(signature, signode)
         name = self._names.get(signature)
         if name is None:
-            name = self._name_from_signature(signature)
+            name = self._name_from_signature(signature) # pylint: disable=assignment-from-none
             # remove trailing ‘.’ found in commands, but not ‘...’ (ellipsis)
             if name is not None and name.endswith(".") and not name.endswith("..."):
                 name = name[:-1]
@@ -241,7 +256,7 @@ class NotationObject(DocumentableObject):
     """
     def _render_signature(self, signature, signode):
         position = self.state_machine.get_source_and_line(self.lineno)
-        tacn_node = parse_notation(signature, *position)
+        tacn_node = notation_to_sphinx(signature, *position)
         signode += addnodes.desc_name(signature, '', tacn_node)
 
 class GallinaObject(PlainObject):
@@ -346,7 +361,7 @@ class OptionObject(NotationObject):
     annotation = "Option"
 
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 
 class FlagObject(NotationObject):
@@ -365,7 +380,7 @@ class FlagObject(NotationObject):
     annotation = "Flag"
 
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 
 class TableObject(NotationObject):
@@ -383,7 +398,7 @@ class TableObject(NotationObject):
     annotation = "Table"
 
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 class ProductionObject(CoqObject):
     r"""A grammar production.
@@ -432,7 +447,7 @@ class ProductionObject(CoqObject):
         lhs_node = nodes.literal(lhs_op, lhs_op)
 
         position = self.state_machine.get_source_and_line(self.lineno)
-        rhs_node = parse_notation(rhs, *position)
+        rhs_node = notation_to_sphinx(rhs, *position)
         signode += addnodes.desc_name(signature, '', lhs_node, rhs_node)
 
         return ('token', lhs) if op == '::=' else None
@@ -475,7 +490,7 @@ class ExceptionObject(NotationObject):
 
     # Generate names automatically
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 class WarningObject(NotationObject):
     """An warning raised by a Coq command or tactic..
@@ -497,7 +512,7 @@ class WarningObject(NotationObject):
 
     # Generate names automatically
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
     #pylint: disable=unused-argument, dangerous-default-value
@@ -516,7 +531,7 @@ def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
     """
     notation = utils.unescape(text, 1)
     position = inliner.reporter.get_source_and_line(lineno)
-    return [nodes.literal(rawtext, '', parse_notation(notation, *position, rawtext=rawtext))], []
+    return [nodes.literal(rawtext, '', notation_to_sphinx(notation, *position, rawtext=rawtext))], []
 
 def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]):
     #pylint: disable=dangerous-default-value
diff --git a/doc/tools/coqrst/notations/parsing.py b/doc/tools/coqrst/notations/parsing.py
index 506240d907..2312e09090 100644
--- a/doc/tools/coqrst/notations/parsing.py
+++ b/doc/tools/coqrst/notations/parsing.py
@@ -11,10 +11,22 @@ from .TacticNotationsLexer import TacticNotationsLexer
 from .TacticNotationsParser import TacticNotationsParser
 
 from antlr4 import CommonTokenStream, InputStream
+from antlr4.error.ErrorListener import ErrorListener
 
 SUBSTITUTIONS = [#("@bindings_list", "{+ (@id := @val) }"),
                  ("@qualid_or_string", "@id|@string")]
 
+class ParseError(Exception):
+    def __init__(self, msg):
+        super().__init__()
+        self.msg = msg
+
+class ExceptionRaisingErrorListener(ErrorListener):
+    def syntaxError(self, recognizer, offendingSymbol, line, column, msg, e):
+        raise ParseError("{}:{}: {}".format(line, column, msg))
+
+ERROR_LISTENER = ExceptionRaisingErrorListener()
+
 def substitute(notation):
     """Perform common substitutions in the notation string.
 
@@ -27,11 +39,13 @@ def substitute(notation):
     return notation
 
 def parse(notation):
-    """Parse a notation string.
+    """Parse a notation string, optionally reporting errors to `error_listener`.
 
     :return: An ANTLR AST. Use one of the supplied visitors (or write your own)
              to turn it into useful output.
     """
     substituted = substitute(notation)
     lexer = TacticNotationsLexer(InputStream(substituted))
-    return TacticNotationsParser(CommonTokenStream(lexer)).top()
+    parser = TacticNotationsParser(CommonTokenStream(lexer))
+    parser.addErrorListener(ERROR_LISTENER)
+    return parser.top()