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

2 files changed, 53 insertions, 5 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 ``{+|``.