branch: elpa/proof-general
commit 3d361fa6915df412c3ecf707f219316ccb894e62
Author: Stefan Monnier <monn...@iro.umontreal.ca>
Commit: Stefan Monnier <monn...@iro.umontreal.ca>
* doc/PG-adapting.texi: Refresh with `make -C doc magic`
* lib/texi-docstring-magic.el: Use lexical-binding.
Fix regexps to avoid ineffective backslashes.
(texi-docstring--args, texi-docstring--in-quoted-region):
Rename dynamically scoped vars.
(texi-docstring-magic-munge-table): Use functions rather than
quoted expressions.
(texi-docstring--funcall): New function.
(texi-docstring-magic-munge-docstring): Use it instead of `eval`.
---
doc/PG-adapting.texi | 16 +++----
lib/texi-docstring-magic.el | 110 ++++++++++++++++++++++++++------------------
2 files changed, 70 insertions(+), 56 deletions(-)
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 86b7eab..4e0ec65 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -335,7 +335,7 @@ more details.
@c Internals.
@c TEXI DOCSTRING MAGIC: proof-assistant-table
-@defopt proof-assistant-table
+@defvar proof-assistant-table
Proof General's table of supported proof assistants.@*
This is copied from @samp{@code{proof-assistant-table-default}} at load time,
removing any entries that do not have a corresponding directory
@@ -360,9 +360,7 @@ file for the mode, which will be
@end lisp
where @var{proof-home-directory} is the value of the
variable @samp{@code{proof-home-directory}}.
-
-The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo"
".glob")) (easycrypt "EasyCrypt" "ec" "\\.eca?\\'") (phox "PhoX" "phx" nil
(".phi" ".pho")) (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml")
(pghaskell "PG-Haskell" "pghci"))}.
-@end defopt
+@end defvar
The final step of the description above is where the work lies. There
@@ -2914,7 +2912,7 @@ assistant is already busy with the next item from
@code{proof-action-list}.
@c TEXI DOCSTRING MAGIC: proof-tree-handle-delayed-output
-@defun proof-tree-handle-delayed-output old-proof-marker cmd flags span
+@defun proof-tree-handle-delayed-output old-proof-marker cmd flags _span
Process delayed output for prooftree.@*
This function is the main entry point of the Proof General
prooftree support. It examines the delayed output in order to
@@ -3307,9 +3305,9 @@ extension. The proof assistants enabled are the ones
listed
in the @code{proof-assistants} setting.
@c TEXI DOCSTRING MAGIC: proof-assistants
-@defopt proof-assistants
+@defvar proof-assistants
Choice of proof assistants to use with Proof General.@*
-A list of symbols chosen from: @code{'isar} @code{'coq} @code{'easycrypt}
@code{'phox} @code{'pgshell} @code{'pgocaml} @code{'pghaskell}.
+A list of symbols chosen from: @samp{isar} @samp{coq} @samp{easycrypt}
@samp{phox} @samp{pgshell} @samp{pgocaml} @samp{pghaskell}.
If nil, the default will be ALL available proof assistants.
Each proof assistant defines its own instance of Proof General,
@@ -3325,9 +3323,7 @@ symbols you want, for example "lego isa". Or you can
edit the file @samp{proof-site.el} itself.
Note: to change proof assistant, you must start a new Emacs session.
-
-The default value is @code{nil}.
-@end defopt
+@end defvar
The file @file{proof-site.el} also defines a version variable.
diff --git a/lib/texi-docstring-magic.el b/lib/texi-docstring-magic.el
index a028f56..b6ef604 100644
--- a/lib/texi-docstring-magic.el
+++ b/lib/texi-docstring-magic.el
@@ -1,9 +1,9 @@
-;;; texi-docstring-magic.el --- munge internal docstrings into texi
+;;; texi-docstring-magic.el --- munge internal docstrings into texi -*-
lexical-binding: t; -*-
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
@@ -110,28 +110,32 @@ Compatibility between FSF Emacs and XEmacs."
(setq strings (cdr strings)))
str))
+(defvar texi-docstring--args)
+(defvar texi-docstring--in-quoted-region)
+
(defconst texi-docstring-magic-munge-table
- '(;; 0. Escape @, { and } characters
+ `(;; 0. Escape @, { and } characters
("\\(@\\)" t "@@")
("\\({\\)" t "@{")
("\\(}\\)" t "@}")
;; 1. Indented lines are gathered into @lisp environment.
("^\\(\n\\|.+\\)$"
t
- (let
- ((line (match-string 0 docstring)))
- (if (save-match-data (string-match "^[ \t]" line))
- ;; whitespace
- (if in-quoted-region
- line
- (setq in-quoted-region t)
- (concat "@lisp\n" line))
- ;; non-white space/carriage return
- (if (and in-quoted-region (not (equal line "\n")))
- (progn
- (setq in-quoted-region nil)
- (concat "@end lisp\n" line))
- line))))
+ ,(lambda (docstring)
+ (let
+ ((line (match-string 0 docstring)))
+ (if (save-match-data (string-match "^[ \t]" line))
+ ;; whitespace
+ (if texi-docstring--in-quoted-region
+ line
+ (setq texi-docstring--in-quoted-region t)
+ (concat "@lisp\n" line))
+ ;; non-white space/carriage return
+ (if (and texi-docstring--in-quoted-region (not (equal line "\n")))
+ (progn
+ (setq texi-docstring--in-quoted-region nil)
+ (concat "@end lisp\n" line))
+ line)))))
;; 2. Pieces of text `stuff' or surrounded in quotes
;; are marked up with @samp. NB: Must be backquote
;; followed by forward quote for this to work.
@@ -142,21 +146,25 @@ Compatibility between FSF Emacs and XEmacs."
;; and symbols put inside quotes.
("\\(`\\([^']+\\)'\\)"
t
- (concat "@samp{" (match-string 2 docstring) "}"))
+ ,(lambda (docstring)
+ (concat "@samp{" (match-string 2 docstring) "}")))
;; 3. Words *emphasized* are made @strong{emphasized}
("\\(\\*\\(\\w+\\)\\*\\)"
t
- (concat "@strong{" (match-string 2 docstring) "}"))
+ ,(lambda (docstring)
+ (concat "@strong{" (match-string 2 docstring) "}")))
;; 4. Words sym-bol which are symbols become @code{sym-bol}.
;; Must have at least one hyphen to be recognized,
;; terminated in whitespace, end of line, or punctuation.
;; Only consider symbols made from word constituents
;; and hyphen.
- ("\\(\\(\\w+\\-\\(\\w\\|\\-\\)+\\)\\)\\(\\s\)\\|\\s-\\|\\s.\\|$\\)"
- (or (boundp (intern (match-string 2 docstring)))
- (fboundp (intern (match-string 2 docstring))))
- (concat "@code{" (match-string 2 docstring) "}"
- (match-string 4 docstring)))
+ ("\\(\\(\\w+-\\(\\w\\|-\\)+\\)\\)\\(\\s)\\|\\s-\\|\\s.\\|$\\)"
+ ,(lambda (docstring)
+ (or (boundp (intern (match-string 2 docstring)))
+ (fboundp (intern (match-string 2 docstring)))))
+ ,(lambda (docstring)
+ (concat "@code{" (match-string 2 docstring) "}"
+ (match-string 4 docstring))))
;; 5. Upper cased words ARG corresponding to arguments become
;; @var{arg}
;; In fact, include any word so long as it is more than 3 characters
@@ -165,19 +173,23 @@ Compatibility between FSF Emacs and XEmacs."
;; FIXME: maybe we don't want to downcase stuff already
;; inside @samp
;; FIXME: should - terminate? should _ be included?
- ("\\([A-Z0-9_\\-]+\\)\\(/\\|\)\\|}\\|\\s-\\|\\s.\\|$\\)"
- (or (> (length (match-string 1 docstring)) 3)
- (member (downcase (match-string 1 docstring)) args))
- (concat "@var{" (downcase (match-string 1 docstring)) "}"
- (match-string 2 docstring)))
+ ("\\([A-Z0-9_\\-]+\\)\\(/\\|)\\|}\\|\\s-\\|\\s.\\|$\\)"
+ ,(lambda (docstring)
+ (or (> (length (match-string 1 docstring)) 3)
+ (member (downcase (match-string 1 docstring))
+ texi-docstring--args)))
+ ,(lambda (docstring)
+ (concat "@var{" (downcase (match-string 1 docstring)) "}"
+ (match-string 2 docstring))))
;; 6. Words 'sym which are lisp quoted are
;; marked with @code.
- ("\\(\\(\\s-\\|^\\)'\\(\\(\\w\\|\\-\\)+\\)\\)\\(\\s\)\\|\\s-\\|\\s.\\|$\\)"
+ ("\\(\\(\\s-\\|^\\)'\\(\\(\\w\\|-\\)+\\)\\)\\(\\s)\\|\\s-\\|\\s.\\|$\\)"
t
- (concat (match-string 2 docstring)
- "@code{'" (match-string 3 docstring) "}"
- (match-string 5 docstring)))
+ ,(lambda (docstring)
+ (concat (match-string 2 docstring)
+ "@code{'" (match-string 3 docstring) "}"
+ (match-string 5 docstring))))
;; 7,8. Clean up for @lisp environments left with spurious newlines
;; after 1.
("\\(\\(^\\s-*$\\)\n@lisp\\)" t "@lisp")
@@ -186,14 +198,16 @@ Compatibility between FSF Emacs and XEmacs."
;; Changed to just @samp of uppercase.
("\\(@samp{@var{\\([^}]+\\)}}\\)"
t
- (concat "@samp{" (upcase (match-string 2 docstring)) "}")))
+ ,(lambda (docstring)
+ (concat "@samp{" (upcase (match-string 2 docstring)) "}"))))
"Table of regexp matches and replacements used to markup docstrings.
Format of table is a list of elements of the form
- (regexp predicate replacement-form)
-If regexp matches and predicate holds, then replacement-form is
-evaluated to get the replacement for the match.
-predicate and replacement-form can use variables arg,
-and forms such as (match-string 1 docstring)
+ (REGEXP PREDICATE REPLACEMENT)
+If REGEXP matches and PREDICATE holds, then REPLACEMENT is
+used to replace the match.
+PREDICATE and REPLACEMENT can be functions taking
+the docstring as argument and they can use the dynamically scoped
+variables `texi-docstring--args' and `texi-docstring--in-quoted-region'.
Match string 1 is assumed to determine the
length of the matched item, hence where parsing restarts from.
The replacement must cover the whole match (match string 0),
@@ -207,30 +221,34 @@ including any whitespace included to delimit matches.")
(untabify (point-min) (point-max))
(buffer-string)))
+(defun texi-docstring--funcall (f arg)
+ (if (functionp f) (funcall f arg) f))
+
(defun texi-docstring-magic-munge-docstring (docstring args)
"Markup DOCSTRING for texi according to regexp matches."
;; FIXME(EMD): seems buggy as ARGS is not used
- (let ((case-fold-search nil))
+ (let ((case-fold-search nil)
+ (texi-docstring--args args))
(setq docstring (texi-docstring-magic-untabify docstring))
(dolist (test texi-docstring-magic-munge-table)
(let ((regexp (nth 0 test))
(predicate (nth 1 test))
(replace (nth 2 test))
(i 0)
- in-quoted-region)
+ texi-docstring--in-quoted-region)
(while (and
(< i (length docstring))
(string-match regexp docstring i))
(setq i (match-end 1))
- (if (eval predicate)
+ (if (texi-docstring--funcall predicate docstring)
(let* ((origlength (- (match-end 0) (match-beginning 0)))
- (replacement (eval replace))
+ (replacement (texi-docstring--funcall replace docstring))
(newlength (length replacement)))
(setq docstring
(replace-match replacement t t docstring))
(setq i (+ i (- newlength origlength))))))
- (if in-quoted-region
+ (if texi-docstring--in-quoted-region
(setq docstring (concat docstring "\n@end lisp"))))))
;; Force a new line after (what should be) the first sentence,
;; if not already a new paragraph.
@@ -322,7 +340,7 @@ Markup as @code{stuff} or @lisp stuff @end Lisp."
(nth 1 def))
((eq (car-safe def) 'closure)
(nth 2 def))))
- (args (mapcar 'symbol-name argsyms)))
+ (args (mapcar #'symbol-name argsyms)))
(cond
((commandp function)
(texi-docstring-magic-texi "fn" "Command" name docstring args))
@@ -361,7 +379,7 @@ With prefix arg, no errors on unknown symbols. (This
results in
(let ((text-quoting-style 'grave)
(magic (concat "^"
(regexp-quote texi-docstring-magic-comment)
- "\\s-*\\(\\(\\w\\|\\-\\)+\\)[ \t]*$"))
+ "\\s-*\\(\\(\\w\\|-\\)+\\)[ \t]*$"))
p
symbol
deleted)
