diff options
| -rw-r--r-- | doc/sphinx/README.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/README.template.rst | 28 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 21 |
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 |