diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 3e5e72e39..86bec7041 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -3022,12 +3022,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 @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 @@ -3121,11 +3121,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 @@ -3160,23 +3160,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 @@ -3356,7 +3356,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 @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. @@ -3373,12 +3373,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 @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 @@ -3392,18 +3392,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 @@ -3450,8 +3450,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 -toggle. The name of the defined function is returned. diff --git a/lib/texi-docstring-magic.el b/lib/texi-docstring-magic.el index d4abce3f7..11f055f72 100644 --- a/lib/texi-docstring-magic.el +++ b/lib/texi-docstring-magic.el @@ -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,7 +324,9 @@ 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 (help-function-arglist def 'preserve-names)) (args (mapcar #'symbol-name argsyms)))