diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-07-12 14:00:46 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-07-12 14:00:46 +0000 |
| commit | 86d6f7053bba5cba50525f18e218a6784780b9e9 (patch) | |
| tree | 286fc11b54f563ce63eeccfb32833f03fd328187 /doc | |
| parent | 8b65a54fdeb50bc346fcf8d25315e54e28c4cca6 (diff) | |
Update docstrings
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/PG-adapting.texi | 2 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 32 |
2 files changed, 30 insertions, 4 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index c12a95c2..d7dc6fef 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -1529,7 +1529,7 @@ input, then newlines can be retained in the input. @c TEXI DOCSTRING MAGIC: proof-shell-insert-hook @defvar proof-shell-insert-hook -Hooks run by @code{proof-shell-insert} before inserting a command.@* +Hooks run by @samp{@code{proof-shell-insert}} before inserting a command.@* Can be used to configure the proof assistant to the interface in various ways -- for example, to observe or alter the commands sent to the prover, or to sneak in extra commands to configure the prover. diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index d080f027..5573ac41 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3820,14 +3820,40 @@ logic name are still appended. @c TEXI DOCSTRING MAGIC: isabelle-program-name-override +@defopt isabelle-program-name-override +Name of executable program to run Isabelle. -@c TEXI DOCSTRING MAGIC: isabelle-chosen-logic - -@c TEXI DOCSTRING MAGIC: isabelle-choose-logic +You can set customize this in case the automatic settings +mechanism (based on isatool) does not work for you. One reason +to do this is if you are running Isabelle remotely, or using +windows and avoiding isatool. +A possible value when running under Windows looks like this: +@lisp + C:\sml\bin\.run\run.x86-win32.exe @@SMLload=C:\Isabelle\ +@end lisp +This expects SML/NJ in C:\sml and Isabelle images in C:Isabelle. +The logic image name is tagged onto the end. +The default value is @code{nil}. +@end defopt +@c TEXI DOCSTRING MAGIC: isabelle-chosen-logic +@defopt isabelle-chosen-logic +Choice of logic to use with Isabelle.@* +If non-nil, added onto the Isabelle command line for invoking Isabelle. +You can set this as a file local variable, using a special comment +at the top of your theory file, like this: +@lisp + (* -*- @code{isabelle-chosen-logic}: "ZF" -*- *) +@end lisp +The default value is @code{nil}. +@end defopt +@c TEXI DOCSTRING MAGIC: isabelle-choose-logic +@deffn Command isabelle-choose-logic logic +Adjust @code{isabelle-prog-name} and @code{proof-prog-name} for running @var{logic}. +@end deffn @node Isabelle commands @section Isabelle commands @cindex Isabelle commands |