[doc] Add an ELisp snippet to insert Sphinx roles and quotes

3 files changed, 52 insertions, 1 deletions

diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index 9dd12087a..70a9756e5 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -23,7 +23,7 @@
 
 ;; If you load this file from a git repository, checking out an old
 ;; commit will make it disappear and cause errors for your Emacs
-;; startup. To ignore those errors use (require 'coqdev nil t). If you
+;; startup.  To ignore those errors use (require 'coqdev nil t).  If you
 ;; check out a malicious commit Emacs startup would allow it to run
 ;; arbitrary code, to avoid this you can copy coqdev.el to any
 ;; location and adjust the load path accordingly (of course if you run
@@ -115,5 +115,36 @@ This does not enable `bug-reference-mode'."
       (setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s"))))
 (add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode)
 
+(defun coqdev-sphinx-quote-coq-refman-region (left right &optional offset beg end)
+  "Add LEFT and RIGHT around the BEG..END.
+Leave the point after RIGHT.  BEG and END default to the bounds
+of the current region.  Leave point OFFSET characters after the
+left quote (if OFFSET is nil, leave the point after the right
+quote)."
+  (unless beg
+    (if (region-active-p)
+        (setq beg (region-beginning) end (region-end))
+      (setq beg (point) end nil)))
+  (save-excursion
+    (goto-char (or end beg))
+    (insert right))
+  (save-excursion
+    (goto-char beg)
+    (insert left))
+  (if (and end (not offset)) ;; Second test handles the ::`` case
+      (goto-char (+ end (length left) (length right)))
+    (goto-char (+ beg (or offset (length left))))))
+
+(defun coqdev-sphinx-rst-coq-action ()
+  "Insert a Sphinx role template or quote the current region."
+  (interactive)
+  (pcase (read-char "Command [gntm:`]?")
+    (?g (coqdev-sphinx-quote-coq-refman-region ":g:`" "`"))
+    (?n (coqdev-sphinx-quote-coq-refman-region ":n:`" "`"))
+    (?t (coqdev-sphinx-quote-coq-refman-region ":token:`" "`"))
+    (?m (coqdev-sphinx-quote-coq-refman-region ":math:`" "`"))
+    (?: (coqdev-sphinx-quote-coq-refman-region "::`" "`" 1))
+    (?` (coqdev-sphinx-quote-coq-refman-region "``" "``"))))
+
 (provide 'coqdev)
 ;;; coqdev ends here
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 5dcefda4f..b22c5086c 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -286,3 +286,13 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
     `production list
     <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_
     and reference its tokens using ``:token:`…```.
+
+Tips and tricks
+===============
+
+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``::
+
+   (with-eval-after-load 'rst
+     (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action))
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index a387247e5..2f7ba028a 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -81,3 +81,13 @@ Coq roles
 In addition to the objects and directives above, the ``coqrst`` Sphinx plugin defines the following roles:
 
 [ROLES]
+
+Tips and tricks
+===============
+
+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``::
+
+   (with-eval-after-load 'rst
+     (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action))