From 621a78bb1efd87a29efcfd109ed6713f7eb612d8 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 18 Jun 1999 10:48:29 +0000 Subject: New front page image. Updated magic. --- doc/ProofGeneral.texi | 34 ++++++++++++++++++++++++++-------- 1 file changed, 26 insertions(+), 8 deletions(-) diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 44692af8..c6bb6ebb 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -80,6 +80,9 @@ END-INFO-DIR-ENTRY @subtitle Proof General @value{version} @subtitle @value{last-update} @iftex +@vskip 1cm +@c This .eps file takes 8.4M! A pity texi can't seem +@c to deal with gzipped files? (goes down to 1.7M). @image{ProofGeneral} @end iftex @author D. Aspinall, H. Goguen, T. Kleymann and D. Sequeira @@ -1589,10 +1592,9 @@ The default value is @code{nil}. @end defopt @c TEXI DOCSTRING MAGIC: proof-prog-name-guess -@defopt proof-prog-name-guess -If non-nil, ProofGeneral tries to run `make -n' to guess -the command line arguments for the proof assistant -(Currently implemented for Coq only) +@defopt proof-prog-name-guess +If non-nil, use @samp{@code{proof-guess-command-line}} to guess @code{proof-prog-name}.@* +This option is compatible with @code{proof-prog-name-ask}. The default value is @code{nil}. @end defopt @@ -1656,10 +1658,26 @@ If non-nil, an error is given when an attempt is made to edit the read-only region. If nil, Proof General is more relaxed (but may give you a reprimand!) +The default value for @code{proof-strict-read-only} depends on which +version of Emacs you are using. In FSF Emacs, strict read only is buggy +when it used in conjunction with font-lock, so it is disabled by default. + The default value is @code{strict}. @end defopt @c TEXI DOCSTRING MAGIC: proof-strict-read-only +@defopt proof-strict-read-only +Whether Proof General is strict about the read-only region in buffers.@* +If non-nil, an error is given when an attempt is made to edit the +read-only region. If nil, Proof General is more relaxed (but may give +you a reprimand!) + +The default value for @code{proof-strict-read-only} depends on which +version of Emacs you are using. In FSF Emacs, strict read only is buggy +when it used in conjunction with font-lock, so it is disabled by default. + +The default value is @code{strict}. +@end defopt @c TEXI DOCSTRING MAGIC: proof-script-indent @defopt proof-script-indent @@ -2303,7 +2321,7 @@ directory and elisp file for the mode, which will be where @samp{PROOF-HOME-DIRECTORY} is the value of the variable @code{proof-home-directory}. -The default value is @code{((isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$"))}. +The default value is @code{((isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$") (plastic "Plastic" "\\.lf$"))}. @end defopt @node Major modes used by Proof General @@ -2976,7 +2994,7 @@ Where Proof General image files are installed. Ends with slash. @c TEXI DOCSTRING MAGIC: proof-info-directory @defvar proof-info-directory -Where Proof General Info files are installed. +Where Proof General Info files are installed. Ends with slash. @end defvar @@ -2991,7 +3009,7 @@ in the @code{proof-assistants} setting. @c TEXI DOCSTRING MAGIC: proof-assistants @defopt proof-assistants Choice of proof assistants to use with Proof General.@* -A list of symbols chosen from: @code{'isa} @code{'lego} @code{'coq}. +A list of symbols chosen from: @code{'isa} @code{'lego} @code{'coq} @code{'plastic}. Each proof assistant defines its own instance of Proof General, providing session control, script management, etc. Proof General will be started automatically for the assistants chosen here. @@ -3006,7 +3024,7 @@ edit the file @samp{proof-site.el} itself. Note: to change proof assistant, you must start a new Emacs session. -The default value is @code{(isa lego coq)}. +The default value is @code{(isa lego coq plastic)}. @end defopt The file @file{proof-site.el} also defines a version variable. -- cgit v1.2.3