Update doc for % escapes in Sphinx doc, improve error messages

3 files changed, 65 insertions, 14 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index b20669c7f1..549598b187 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -64,7 +64,14 @@ The signatures of most objects can be written using a succinct DSL for Coq notat
   an alternative, indicating than one of multiple constructs can be used
 
 ``%{``, ``%}``, ``%|``
-  an escaped character (rendered without the leading ``%``).  In most cases, escaping is not necessary.  In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``.  But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``.  (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.)
+  an escaped character (rendered without the leading ``%``).  In most cases,
+  escaping is not necessary.  In particular, the following expressions are
+  all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``.
+  But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``.
+  (We use ``%`` instead of the usual ``\`` because you'd have to type ``\``
+  twice in your reStructuredText file.)
+
+  For more details and corner cases, see `Advanced uses of notations`_ below.
 
 ..
    FIXME document the new subscript support
@@ -300,7 +307,7 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
           \WTEG{\forall~x:T,U}{\Prop}
 
 ``.. preamble::`` A reST directive to include a TeX file.
-    Mostly useful to let MathJax know about `\def`s and `\newcommand`s.  The
+    Mostly useful to let MathJax know about `\def`\s and `\newcommand`\s.  The
     contents of the TeX file are wrapped in a math environment, as MathJax
     doesn't process LaTeX definitions otherwise.
 
@@ -536,7 +543,24 @@ Emacs
 
 The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes.  It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes.  You can also select a region of text, and wrap it in single or double backticks using that function.
 
-Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``::
+Use the following snippet to bind it to `F12` in ``rst-mode``::
 
    (with-eval-after-load 'rst
      (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action))
+
+
+Advanced uses of notations
+--------------------------
+
+
+  - Use `%` to escape grammar literal strings that are the same as metasyntax,
+    such as ``{``, ``|``, ``}`` and ``{|``.  (While this is optional for
+    ``|`` and ``{ ... }`` outside of ``{| ... }``, always using the escape
+    requires less thought.)
+
+  - Literals such as ``|-`` and ``||`` don't need to be escaped.
+
+  - The literal ``%`` shouldn't be escaped.
+
+  - Don't use the escape for a ``|`` separator in ``{*`` and ``{+``.  These
+    should appear as ``{*|`` and ``{+|``.
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 2093765608..51d5174567 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -64,7 +64,14 @@ The signatures of most objects can be written using a succinct DSL for Coq notat
   an alternative, indicating than one of multiple constructs can be used
 
 ``%{``, ``%}``, ``%|``
-  an escaped character (rendered without the leading ``%``).  In most cases, escaping is not necessary.  In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``.  But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``.  (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.)
+  an escaped character (rendered without the leading ``%``).  In most cases,
+  escaping is not necessary.  In particular, the following expressions are
+  all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``.
+  But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``.
+  (We use ``%`` instead of the usual ``\`` because you'd have to type ``\``
+  twice in your reStructuredText file.)
+
+  For more details and corner cases, see `Advanced uses of notations`_ below.
 
 ..
    FIXME document the new subscript support
@@ -290,7 +297,24 @@ Emacs
 
 The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes.  It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes.  You can also select a region of text, and wrap it in single or double backticks using that function.
 
-Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``::
+Use the following snippet to bind it to `F12` in ``rst-mode``::
 
    (with-eval-after-load 'rst
      (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action))
+
+
+Advanced uses of notations
+--------------------------
+
+
+  - Use `%` to escape grammar literal strings that are the same as metasyntax,
+    such as ``{``, ``|``, ``}`` and ``{|``.  (While this is optional for
+    ``|`` and ``{ ... }`` outside of ``{| ... }``, always using the escape
+    requires less thought.)
+
+  - Literals such as ``|-`` and ``||`` don't need to be escaped.
+
+  - The literal ``%`` shouldn't be escaped.
+
+  - Don't use the escape for a ``|`` separator in ``{*`` and ``{+``.  These
+    should appear as ``{*|`` and ``{+|``.
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 6c32a4968c..eff70bdac5 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -15,6 +15,7 @@ could imagine extending it.
 
 # pylint: disable=too-few-public-methods
 
+import os
 import re
 from itertools import chain
 from collections import defaultdict
@@ -42,7 +43,7 @@ from .notations.parsing import ParseError
 from .notations.sphinx import sphinxify
 from .notations.plain import stringify_with_ellipses
 
-PARSE_ERROR = """Parse error in notation!
+PARSE_ERROR = """{}:{} Parse error in notation!
 Offending notation: {}
 Error message: {}"""
 
@@ -53,14 +54,14 @@ def notation_to_sphinx(notation, source, line, rawtext=None):
         node.source, node.line = source, line
         return node
     except ParseError as e:
-        raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e
+        raise ExtensionError(PARSE_ERROR.format(os.path.basename(source), line, 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
+        raise ExtensionError(PARSE_ERROR.format(os.path.basename(source), line, notation, e.msg)) from e
 
 def highlight_using_coqdoc(sentence):
     """Lex sentence using coqdoc, and yield inline nodes for each token"""
@@ -426,7 +427,7 @@ class ProductionObject(CoqObject):
     def _render_signature(self, signature, signode):
         raise NotImplementedError(self)
 
-    SIG_ERROR = ("Invalid syntax in ``.. prodn::`` directive"
+    SIG_ERROR = ("{}: Invalid syntax in ``.. prodn::`` directive"
                  + "\nExpected ``name ::= ...`` or ``name += ...``"
                  + " (e.g. ``pattern += constr:(@ident)``)")
 
@@ -434,11 +435,13 @@ class ProductionObject(CoqObject):
         nsplits = 2
         parts = signature.split(maxsplit=nsplits)
         if len(parts) != 3:
-            raise ExtensionError(ProductionObject.SIG_ERROR)
+            loc = os.path.basename(get_node_location(signode))
+            raise ExtensionError(ProductionObject.SIG_ERROR.format(loc))
 
         lhs, op, rhs = (part.strip() for part in parts)
         if op not in ["::=", "+="]:
-            raise ExtensionError(ProductionObject.SIG_ERROR)
+            loc = os.path.basename(get_node_location(signode))
+            raise ExtensionError(ProductionObject.SIG_ERROR.format(loc))
 
         self._render_annotation(signode)
 
@@ -681,7 +684,7 @@ class ExampleDirective(BaseAdmonition):
 class PreambleDirective(Directive):
     r"""A reST directive to include a TeX file.
 
-    Mostly useful to let MathJax know about `\def`s and `\newcommand`s.  The
+    Mostly useful to let MathJax know about `\def`\s and `\newcommand`\s.  The
     contents of the TeX file are wrapped in a math environment, as MathJax
     doesn't process LaTeX definitions otherwise.
 
@@ -850,12 +853,12 @@ class CoqtopBlocksTransform(Transform):
 
         unexpected_options = list(options - {'all', 'none', 'in', 'out'})
         if unexpected_options:
-            loc = get_node_location(node)
+            loc = os.path.basename(get_node_location(node))
             raise ExtensionError("{}: Unexpected options for .. coqtop:: {}".format(loc,unexpected_options))
 
         # Display options
         if len(options) != 1:
-            loc = get_node_location(node)
+            loc = os.path.basename(get_node_location(node))
             raise ExtensionError("{}: Exactly one display option must be passed to .. coqtop::".format(loc))
 
         opt_all = 'all' in options