Define a new customization variable <PA>-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.
@@ -185,12 +185,12 @@
Set default for the proof assistant specific variable <PA>-sym to value.
This should be used in prover-specific code to alter the default values
for prover specific settings.
Usage: (defpgdefault sym value) +
Usage: (defpgdefault SYM value)
All new instantiation variables are best declared using the @@ -204,18 +204,18 @@
Return the value for sym for the current prover.
+
Return the value for SYM for the current prover.
This macro should only be invoked once a specific prover is engaged.
Return the symbol for sym for the current prover. sym not evaluated.
+
Return the symbol for SYM for the current prover. SYM not evaluated.
This macro should only be called once a specific prover is known.
Return the symbol for sym for the current prover. sym evaluated.
+
Return the symbol for SYM for the current prover. SYM evaluated.
This macro should only be invoked once a specific prover is engaged.
Define a function VAR-toggle for toggling a boolean customize setting var.
+
Define a function VAR-toggle for toggling a boolean customize setting VAR.
The toggle function uses ‘customize-set-variable’ to change the variable.
othername gives an alternative name than the default <VAR>-toggle.
The name of the defined function is returned.
diff --git a/doc/master/adaptingman/Writing-More-Lisp-Code.html b/doc/master/adaptingman/Writing-More-Lisp-Code.html
index 62f872c..c40843f 100644
--- a/doc/master/adaptingman/Writing-More-Lisp-Code.html
+++ b/doc/master/adaptingman/Writing-More-Lisp-Code.html
@@ -50,12 +50,12 @@
defpgdefault macro:
Set default for the proof assistant specific variable <PA>-sym to value.
This should be used in prover-specific code to alter the default values
for prover specific settings.
Usage: (defpgdefault sym value) +
Usage: (defpgdefault SYM value)
In your prover-specific code you can simply use the setting @@ -151,11 +151,11 @@
Define shortcut function fn to insert string, optional keydef key.
+
Define shortcut function FN to insert string, optional keydef KEY.
This is intended for defining proof assistant specific functions.
string is inserted using ‘proof-insert’, which see.
-key is added onto proof assistant map.
+KEY is added onto proof assistant map.
The function proof-shell-invisible-command is a useful utility
for sending a single command to the process. You should use this to
@@ -190,23 +190,23 @@
proof-shell-invisible-command.
Define function fn to send string to proof assistant, optional keydef key.
+
Define function FN to send string to proof assistant, optional keydef KEY.
This is intended for defining proof assistant specific functions.
string is sent using ‘proof-shell-invisible-command’, which see.
string may be a string or a function which returns a string.
-key is added onto proof assistant map.
+KEY is added onto proof assistant map.
Define fn (docstring doc): check if cmdvar is set, then send body to prover.
+
Define FN (docstring DOC): check if cmdvar is set, then send body to prover.
body defaults to cmdvar, a variable.
Define fn (arg) with doc: check cmdvar is set, prompt a string and eval body.
+
Define FN (arg) with DOC: check cmdvar is set, prompt a string and eval body.
The body can contain occurrences of arg.
cmdvar is a variable holding a function or string. Automatically has history.