# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1336338915 14400
# Node ID d62ed7381a0b251659c1ba83ecbc9f507b1114ca
# Parent  def1a6b35ccd7b154477c4e959186c3d6815b40a
Instructions on directory-local Coq parameter specification, thanks to a tip from Thomas Braibant

diff -r def1a6b35ccd -r d62ed7381a0b src/Intro.v
--- a/src/Intro.v	Sun Apr 22 16:27:46 2012 -0400
+++ b/src/Intro.v	Sun May 06 17:15:15 2012 -0400
@@ -200,13 +200,17 @@
 
 %\item %#<li>#Run %\texttt{%#<tt>#make#</tt>#%}% in %\texttt{%#<tt>#DIR#</tt>#%}%.#</li>#
 
-%\item %#<li>#There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the %\texttt{%#<tt>#coqtop#</tt>#%}% program, which provides the interactive Coq toplevel.  The best way to add settings that will be shared by many source files is to add a custom variable setting to your %\index{.emacs file@\texttt{.emacs} file}\texttt{%#<tt>#.emacs#</tt>#%}% file, like this:
+%\item %#<li>#There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the %\texttt{%#<tt>#coqtop#</tt>#%}% program, which provides the interactive Coq toplevel.  One way to add settings that will be shared by many source files is to add a custom variable setting to your %\index{.emacs file@\texttt{.emacs} file}\texttt{%#<tt>#.emacs#</tt>#%}% file, like this:
 %\begin{verbatim}%#<pre>#(custom-set-variables
   ...
   '(coq-prog-args '("-I" "DIR/src"))
   ...
 )#</pre>#%\end{verbatim}%
-The extra arguments demonstrated here are the proper choices for working with the code for this book.  The ellipses stand for other Emacs customization settings you may already have.  It can be helpful to save several alternate sets of flags in your %\texttt{%#<tt>#.emacs#</tt>#%}% file, with all but one commented out within the %\texttt{%#<tt>#custom-set-variables#</tt>#%}% block at any given time.#</li>#
+The extra arguments demonstrated here are the proper choices for working with the code for this book.  The ellipses stand for other Emacs customization settings you may already have.  It can be helpful to save several alternate sets of flags in your %\texttt{%#<tt>#.emacs#</tt>#%}% file, with all but one commented out within the %\texttt{%#<tt>#custom-set-variables#</tt>#%}% block at any given time.
+
+Alternatively, Proof General configuration can be set on a per-directory basis, using a %\index{.dir-locals.el file@\texttt{.dir-locals.el} file}\texttt{%#<i>#.dir-locals.el#</i>#%}% file in the directory of the source files for which you want the settings to apply.  Here is an example that could be written in such a file to enable use of the book source.  Note the need to include an argument that starts Coq in Emacs support mode.
+%\begin{verbatim}%#<pre>#((coq-mode . ((coq-prog-args . ("-emacs-U" "-I" "DIR/src")))))#</pre>#%\end{verbatim}%
+ #</li>#
 
 #</ol>#%\end{enumerate}%
 
diff -r def1a6b35ccd -r d62ed7381a0b src/Large.v
--- a/src/Large.v	Sun Apr 22 16:27:46 2012 -0400
+++ b/src/Large.v	Sun May 06 17:15:15 2012 -0400
@@ -852,4 +852,12 @@
 )
 >>
 
-   When working on multiple projects, it is useful to leave multiple versions of this setting in your %\texttt{%#<tt>#.emacs#</tt>#%}% file, commenting out all but one of them at any moment in time.  To switch between projects, change the commenting structure and restart Emacs. *)
+   When working on multiple projects, it is useful to leave multiple versions of this setting in your %\texttt{%#<tt>#.emacs#</tt>#%}% file, commenting out all but one of them at any moment in time.  To switch between projects, change the commenting structure and restart Emacs.
+
+   Alternatively, we can revisit the directory-local settings approach and write the following into a file %\texttt{%#<tt>#.dir-locals.el#</tt>#%}% in %\texttt{%#<i>#CLIENT#</i>#%}%:
+
+<<
+((coq-mode . ((coq-prog-args .
+  ("-emacs-U" "-R" "LIB" "Lib" "-R" "CLIENT" "Client")))))
+>>
+*)