New chapter on Hints and Tips. Credit to Pierre.

1 files changed, 77 insertions, 59 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 736a9d58..f7594505 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -160,11 +160,11 @@ Isabelle.
 * Proof by Pointing::
 * Advanced Script Management::  
 * Support for other Packages::  
+* Hints and tips::
 * Customizing Proof General::   
 * LEGO Proof General::          
 * Coq Proof General::           
 * Isabelle Proof General::    
-* Using File Variables::
 * Adapting Proof General to Other Provers::  
 * Internals of Proof General::  
 * Obtaining and Installing::  
@@ -393,7 +393,8 @@ This manual was written by David Aspinall and Thomas Kleymann.  Some
 words found their way here from the user documentation of LEGO mode,
 prepared by Dilip Sequeira.  Healfdene Goguen supplied some text for Coq
 Proof General.  Since Proof General 2.0, this manual has been maintained
-and improved by David Aspinall.
+and improved by David Aspinall.  Pierre Courtieu wrote the section on
+file variables.
 
 The Proof General project has benefited from funding by EPSRC
 (Applications of a Type Theory Based Proof Assistant), the EC (Types for
@@ -1755,11 +1756,6 @@ The packages currently supported are
 @code{outline-mode},
 and @code{etags}.
 
-Apart from these designated packages, many other packages in Emacs will
-be useful when using Proof General, even though they need no specific
-configuration for Proof General.  It is worth taking time to explore the
-Emacs manual to find out about them.  One that we highlight in
-particular is @code{abbrev-mode}.
 
 @menu
 * Syntax highlighting::         
@@ -1767,7 +1763,6 @@ particular is @code{abbrev-mode}.
 * Support for function menus::  
 * Support for outline mode::    
 * Support for tags::            
-* Using abbreviations::
 @end menu
 
 @node Syntax highlighting
@@ -1911,6 +1906,78 @@ already have customized, Proof General doesn't do this automatically.
 
 For more information on how to use tags, @inforef{Tags, ,(xemacs)}.
 
+
+
+@node Hints and Tips
+@chapter Hints and Tips
+
+Apart from the packages officially supported in Proof General, many
+other features of Emacs are useful when using Proof General, even though
+they need no specific configuration for Proof General.  It is worth
+taking time to explore the Emacs manual to find out about them.
+
+Here we provide some hints and tips for a couple of Emacs features which
+users have found valuable with Proof General.  Further contributions to
+this chapter are welcomed!
+
+@menu
+* Using file variables::
+* Using abbreviations::
+@end menu
+
+
+@node Using file variables
+@section Using file variables
+@cindex file variables
+
+A very convenient way to customize file-specific variables is to use the
+File Variables (@inforef{File Variables, ,xemacs}). This feature of
+Emacs allows to specify the values to use for certain Emacs variables
+when a file is loaded. Those values are written as a list at the end of
+the file.
+
+For example, in projects involving multiple directories, it is often
+useful to set the variables @code{proof-prog-name} and
+@code{compile-command} for each file. Here is an example for Coq users:
+for the file @file{.../dir/bar/foo.v}, if you want Coq to be started
+with the path @code{.../dir/theories/} added in the libraries path
+(@code{"-I"} option), you can put at the end of @file{foo.v}:
+@lisp
+
+(* 
+ Local Variables: 
+ coq-prog-name: "coqtop -emacs -full -I ../theories"
+ End:
+*)
+@end lisp
+
+That way the good command is called when the scripting starts in
+@file{foo.v}. Notice that the command argument @code{"-I ../theories"}
+is specific to the file @file{foo.v}, and thus if you set it via the
+configuration tool, you will need to do it each time you load this
+file. On the contrary with this method, Emacs will do this operation
+automatically.
+
+Extending the previous example, if the makefile for @file{foo.v} is
+located in directory @file{.../dir/}, you can add the good compile
+command:
+
+@lisp
+(* 
+ Local Variables: 
+ coq-prog-name: "coqtop -emacs -full -I ../theories"
+ compile-command: "make -C .. -k bar/foo.vo" 
+ End:
+*)
+@end lisp
+
+And then the good call to makefile will be done if you use the @kbd{M-x
+compile} command. Notice that the lines are commented in order to be
+ignored by the proof assistant. It is possible to use this mechanism for
+any other buffer local variable. Read (@inforef{File Variables, ,xemacs}.
+
+
+
 @node Using abbreviations
 @section Using abbreviations
 
@@ -1964,6 +2031,8 @@ abbrev-mode RET}.  See the Emacs manual for more details.
 
 
 
+
+
 @node Customizing Proof General
 @chapter Customizing Proof General
 @cindex Customization
@@ -2990,57 +3059,6 @@ You can use the following format characters:
 @c   @code{%p}  -- replaced by names of parents, separated by @code{+}'s
 @c @end defopt
 
-@node Using File Variables
-@chapter Using File Variables
-@cindex Using File Variables
-
-
-A very convenient way to customize file-specific variables is to use the
-File Variables (@inforef{File Variables, ,xemacs}). This feature of
-Emacs allows to specify the values to use for certain Emacs variables
-when a file is loaded. Those values are written as a list at the end of
-the file.
-
-For example, in projects involving multiple directories, it is often
-useful to set the variables @code{proof-prog-name} and
-@code{compile-command} for each file. Here is an example for Coq users:
-for the file @file{.../dir/bar/foo.v}, if you want Coq to be started
-with the path @code{.../dir/theories/} added in the libraries path
-(@code{"-I"} option), you can put at the end of @file{foo.v}:
-@lisp
-
-(* 
- Local Variables: 
- coq-prog-name: "coqtop -emacs -full -I ../theories"
- End:
-*)
-@end lisp
-
-That way the good command is called when the scripting starts in
-@file{foo.v}. Notice that the command argument @code{"-I ../theories"}
-is specific to the file @file{foo.v}, and thus if you set it via the
-configuration tool, you will need to do it each time you load this
-file. On the contrary with this method, Emacs will do this operation
-automatically.
-
-Extending the previous example, if the makefile for @file{foo.v} is
-located in directory @file{.../dir/}, you can add the good compile
-command:
-
-@lisp
-(* 
- Local Variables: 
- coq-prog-name: "coqtop -emacs -full -I ../theories"
- compile-command: "make -C .. -k bar/foo.vo" 
- End:
-*)
-@end lisp
-
-And then the good call to makefile will be done if you use the @kbd{M-x
-compile} command. Notice that the lines are commented in order to be
-ignored by the proof assistant. It is possible to use this mechanism for
-any other buffer local variable. Read (@inforef{File Variables, ,xemacs}.
-
 
 @node Adapting Proof General to Other Provers
 @chapter Adapting Proof General to Other Provers