[nongnu] elpa/proof-general a78543cba7 3/5: Merge pull request #820 from hendriktews/fix-magic

[ELPA Syncer]

branch: elpa/proof-general
commit a78543cba785a7b0b0d1a8d4fe343305c6264d15
Merge: 1f93bf273d e237a3bb62
Author: hendriktews <hendrik@askra.de>
Commit: GitHub <noreply@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)