branch: elpa/proof-general
commit a78543cba785a7b0b0d1a8d4fe343305c6264d15
Merge: 1f93bf273d e237a3bb62
Author: hendriktews <hend...@askra.de>
Commit: GitHub <nore...@github.com>
Merge pull request #820 from hendriktews/fix-magic
Fix make magic
---
doc/PG-adapting.texi | 46 ++++++++++++++++++++++-----------------------
lib/texi-docstring-magic.el | 25 +++++++-----------------
2 files changed, 30 insertions(+), 41 deletions(-)
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 865a3083df..5e9a888e11 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -3090,12 +3090,12 @@ To set the default value for these settings in
prover-specific cases,
you should use the special @code{defpgdefault} macro:
@c TEXI DOCSTRING MAGIC: defpgdefault
-@deffn Macro defpgdefault
+@deffn Macro defpgdefault sym value
Set default for the proof assistant specific variable <PA>@var{-sym} to
@var{value}.@*
This should be used in prover-specific code to alter the default values
for prover specific settings.
-Usage: (defpgdefault SYM @var{value})
+Usage: (defpgdefault @var{sym} @var{value})
@end deffn
In your prover-specific code you can simply use the setting
@@ -3189,11 +3189,11 @@ Any other %-prefixed character inserts itself.
@end defun
@c TEXI DOCSTRING MAGIC: proof-defshortcut
-@deffn Macro proof-defshortcut
-Define shortcut function FN to insert @var{string}, optional keydef KEY.@*
+@deffn Macro proof-defshortcut fn string &optional key
+Define shortcut function @var{fn} to insert @var{string}, optional keydef
@var{key}.@*
This is intended for defining proof assistant specific functions.
@var{string} is inserted using @samp{@code{proof-insert}}, which see.
-KEY is added onto proof assistant map.
+@var{key} is added onto proof assistant map.
@end deffn
The function @code{proof-shell-invisible-command} is a useful utility
for sending a single command to the process. You should use this to
@@ -3228,23 +3228,23 @@ There are several handy macros to help you define
functions
which invoke @code{proof-shell-invisible-command}.
@c TEXI DOCSTRING MAGIC: proof-definvisible
-@deffn Macro proof-definvisible
-Define function FN to send @var{string} to proof assistant, optional keydef
KEY.@*
+@deffn Macro proof-definvisible fn string &optional key
+Define function @var{fn} to send @var{string} to proof assistant, optional
keydef @var{key}.@*
This is intended for defining proof assistant specific functions.
@var{string} is sent using @samp{@code{proof-shell-invisible-command}}, which
see.
@var{string} may be a string or a function which returns a string.
-KEY is added onto proof assistant map.
+@var{key} is added onto proof assistant map.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-define-assistant-command
-@deffn Macro proof-define-assistant-command
-Define FN (docstring DOC): check if @var{cmdvar} is set, then send @var{body}
to prover.@*
+@deffn Macro proof-define-assistant-command fn doc cmdvar &optional body
+Define @var{fn} (docstring @var{doc}): check if @var{cmdvar} is set, then send
@var{body} to prover.@*
@var{body} defaults to @var{cmdvar}, a variable.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-define-assistant-command-witharg
-@deffn Macro proof-define-assistant-command-witharg
-Define FN (arg) with DOC: check @var{cmdvar} is set, @var{prompt} a string and
eval @var{body}.@*
+@deffn Macro proof-define-assistant-command-witharg fn doc cmdvar prompt &rest
body
+Define @var{fn} (arg) with @var{doc}: check @var{cmdvar} is set, @var{prompt}
a string and eval @var{body}.@*
The @var{body} can contain occurrences of arg.
@var{cmdvar} is a variable holding a function or string. Automatically has
history.
@end deffn
@@ -3424,7 +3424,7 @@ same way as @code{defcustom}, except that the symbol
declared will
automatically be prefixed by the current proof assistant symbol.
@c TEXI DOCSTRING MAGIC: defpgcustom
-@deffn Macro defpgcustom
+@deffn Macro defpgcustom sym &rest args
Define a new customization variable <PA>@var{-sym} for the current proof
assistant.@*
This is intended for defining settings which are useful for any prover,
but which the user may require different values of across provers.
@@ -3441,12 +3441,12 @@ In specific instances of Proof General, the macro
@code{defpgdefault}
can be used to give a default value for a generic setting.
@c TEXI DOCSTRING MAGIC: defpgdefault
-@deffn Macro defpgdefault
+@deffn Macro defpgdefault sym value
Set default for the proof assistant specific variable <PA>@var{-sym} to
@var{value}.@*
This should be used in prover-specific code to alter the default values
for prover specific settings.
-Usage: (defpgdefault SYM @var{value})
+Usage: (defpgdefault @var{sym} @var{value})
@end deffn
All new instantiation variables are best declared using the
@@ -3460,18 +3460,18 @@ To access the generic settings, the following four
functions and
macros are useful.
@c TEXI DOCSTRING MAGIC: proof-ass
-@deffn Macro proof-ass
-Return the value for SYM for the current prover.@*
+@deffn Macro proof-ass sym
+Return the value for @var{sym} for the current prover.@*
This macro should only be invoked once a specific prover is engaged.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-ass-sym
-@deffn Macro proof-ass-sym
-Return the symbol for SYM for the current prover. SYM not evaluated.@*
+@deffn Macro proof-ass-sym sym
+Return the symbol for @var{sym} for the current prover. @var{sym} not
evaluated.@*
This macro should only be called once a specific prover is known.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-ass-symv
-@deffn Macro proof-ass-symv
-Return the symbol for SYM for the current prover. SYM evaluated.@*
+@deffn Macro proof-ass-symv sym
+Return the symbol for @var{sym} for the current prover. @var{sym} evaluated.@*
This macro should only be invoked once a specific prover is engaged.
@end deffn
@@ -3518,8 +3518,8 @@ approximation we test whether proof-config is
fully-loaded yet.
@end defun
@c TEXI DOCSTRING MAGIC: proof-deftoggle
-@deffn Macro proof-deftoggle
-Define a function VAR-toggle for toggling a boolean customize setting VAR.@*
+@deffn Macro proof-deftoggle var &optional othername
+Define a function VAR-toggle for toggling a boolean customize setting
@var{var}.@*
The toggle function uses @samp{@code{customize-set-variable}} to change the
variable.
@var{othername} gives an alternative name than the default <VAR>-toggle.
The name of the defined function is returned.
diff --git a/lib/texi-docstring-magic.el b/lib/texi-docstring-magic.el
index 91a3a5d1b9..11f055f727 100644
--- a/lib/texi-docstring-magic.el
+++ b/lib/texi-docstring-magic.el
@@ -3,7 +3,7 @@
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2021 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2024 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
@@ -100,16 +100,6 @@ Compatibility between FSF Emacs and XEmacs."
(or (facep face)
(and (fboundp 'find-face) (find-face face))))
-(defun texi-docstring-magic-splice-sep (strings sep)
- "Return concatenation of STRINGS spliced together with separator SEP."
- (let (str)
- (while strings
- (setq str (concat str (car strings)))
- (if (cdr strings)
- (setq str (concat str sep)))
- (setq strings (cdr strings)))
- str))
-
(defvar texi-docstring--args)
(defvar texi-docstring--in-quoted-region)
@@ -269,7 +259,7 @@ including any whitespace included to delimit matches.")
"Make a texi def environment ENV for entity NAME with DOCSTRING."
(concat "@def" env (if grp (concat " " grp) "") " " name
" "
- (texi-docstring-magic-splice-sep args " ")
+ (mapconcat #'identity args " ")
;; " "
;; (texi-docstring-magic-splice-sep extras " ")
"\n"
@@ -301,7 +291,7 @@ Markup as @code{stuff} or @lisp stuff @end Lisp."
(let*
((face symbol)
(name (symbol-name face))
- (docstring (or (face-doc-string face)
+ (docstring (or (face-documentation face)
"Not documented."))
(useropt (eq ?* (string-to-char docstring))))
;; Chop off user option setting
@@ -334,12 +324,11 @@ Markup as @code{stuff} or @lisp stuff @end Lisp."
(name (symbol-name function))
(docstring (or (documentation function)
"Not documented."))
- (def (symbol-function function))
+ (def (indirect-function function))
+ (def (if (not (autoloadp def)) def
+ (autoload-do-load def function)))
(macrop (eq 'macro (car-safe def)))
- (argsyms (cond ((eq (car-safe def) 'lambda)
- (nth 1 def))
- ((eq (car-safe def) 'closure)
- (nth 2 def))))
+ (argsyms (help-function-arglist def 'preserve-names))
(args (mapcar #'symbol-name argsyms)))
(cond
((commandp function)
