diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2011-01-18 19:30:44 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2011-01-18 19:30:44 +0000 |
| commit | 680d718e1e3ca280dfc35fc3f1807d0c373a1870 (patch) | |
| tree | de61698fa1d85609449ca0b2b882f417fe0702f6 /doc/PG-adapting.texi | |
| parent | aade2c8a764cfb9c82389e8275c2013bcdb0e6c7 (diff) | |
- implemented coq-lock-ancestors as described in the docs already
Diffstat (limited to 'doc/PG-adapting.texi')
| -rw-r--r-- | doc/PG-adapting.texi | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index c774200f..d97e32d7 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -2384,7 +2384,7 @@ can be achieved via two hook functions which are run before and after fontifying the output buffers. @c TEXI DOCSTRING MAGIC: proof-zap-commas -@defun proof-zap-commas limit +@defun proof-zap-commas Remove the face of all @samp{,} from point to @var{limit}.@* Meant to be used from @samp{@code{font-lock-keywords}} as a way to unfontify commas in declarations and definitions. @@ -2581,7 +2581,7 @@ To insert text into the current (usually script) buffer, the function @c TEXI DOCSTRING MAGIC: proof-insert -@defun proof-insert text +@defun proof-insert Insert @var{text} into the current buffer.@* @var{text} may include these special characters: @lisp @@ -2651,7 +2651,7 @@ Define command FN to prompt for string @var{cmdvar} to proof assistant.@* @end deffn @c TEXI DOCSTRING MAGIC: proof-format-filename -@defun proof-format-filename string filename +@defun proof-format-filename Format @var{string} by replacing quoted chars by escaped version of @var{filename}. %e uses the canonicalized expanded version of filename (including @@ -2900,14 +2900,14 @@ behaviour and appearance for boolean user options, as well as interfacing properly with the @code{customize} mechanism. @c TEXI DOCSTRING MAGIC: proof-set-value -@defun proof-set-value sym value +@defun proof-set-value Set a customize variable using @samp{@code{set-default}} and a function.@* -We first call @samp{@code{set-default}} to set @var{sym} to @var{value}. -Then if there is a function @var{sym} (i.e. with the same name as the -variable @var{sym}), it is called to take some dynamic action for the new +We first call @samp{@code{set-default}} to set SYM to @var{value}. +Then if there is a function SYM (i.e. with the same name as the +variable SYM), it is called to take some dynamic action for the new setting. -If there is no function @var{sym}, we try stripping +If there is no function SYM, we try stripping @samp{@code{proof-assistant-symbol}} and adding "proof-" instead to get a function name. This extends @code{proof-set-value} to work with generic individual settings. |