Update magic, tweak Makefile to make sure magic uses source .els

3 files changed, 34 insertions, 47 deletions

diff --git a/doc/Makefile.doc b/doc/Makefile.doc
index ff673b0c..937e0b97 100644
--- a/doc/Makefile.doc
+++ b/doc/Makefile.doc
@@ -150,11 +150,12 @@ distclean:   clean
 ##
 ## texi: update magic comments in texi from docstrings in code.
 ##	  (developer use only!)
+##       Must be run from source .els otherwise function arguments lost
 ##
-## remove this for now: no magic during dist ../*/*.el 
 $(DOCNAME).texi: 
 	$(MAKE) magic
 magic:
+	(cd ..; make clean)
 	$(EMACS) $(EMACSFLAGS) -batch -l ./docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer
 
 debugmagic:
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index d122cad1..c526d2df 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -1540,13 +1540,15 @@ Before sending @samp{string}, it will be stripped of carriage returns.
 Additionally, the hook can examine the variable @samp{action}.  It will be
 a symbol, set to the callback command which is executed in the proof
 shell filter once @samp{string} has been processed.  The @samp{action} variable
-suggests what class of command is about to be inserted:
+suggests what class of command is about to be inserted, the first two
+are normally the ones of interest:
 @lisp
- @code{'proof-done-invisible}       A non-scripting command
  @code{'proof-done-advancing}       A "forward" scripting command
  @code{'proof-done-retracting}      A "backward" scripting command
- @code{'init-cmd}                   Initialization command sent to prover
- @code{'interactive-input}          Special interactive input direct to prover
+ @code{'proof-done-invisible}       A non-scripting command
+ @code{'proof-shell-set-silent}     Indicates prover output has been surpressed
+ @code{'proof-shell-clear-silent}   Indicates prover output has been restored
+ @code{'init-cmd}                   Early initialization command sent to prover
 @end lisp
 Caveats: You should be very careful about setting this hook.  Proof
 General relies on a careful synchronization with the process between
@@ -3373,7 +3375,9 @@ is a space.
 @var{action} is the callback to be invoked when this item has been
 processed by the prover. For normal scripting items it is
 @samp{@code{proof-done-advancing}}, for retract items
-@samp{@code{proof-done-retracting}}, but there are more possibilities.
+@samp{@code{proof-done-retracting}}, but there are more possibilities (e.g.
+@samp{@code{proof-done-invisible}}, @samp{@code{proof-shell-set-silent}} and
+@samp{@code{proof-shell-clear-silent}}).
 
 The @var{displayflags} are set
 for non-scripting commands or for when scripting should not
@@ -3709,7 +3713,7 @@ This is useful even with empty delayed output as it can
 clear the buffers.
 
 The delayed output is in the region
-[proof-shell-last-output-start,proof-shell-last-output-end].
+[@code{proof-shell-delayed-output-start},@code{proof-shell-delayed-output-end}].
 
 If goals output is found, the last matching instance, possibly
 bounded by @samp{@code{proof-shell-end-goals-regexp}}, will be displayed.
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 0eef35b8..cce6788f 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4199,21 +4199,19 @@ Coq Auto Compile -> Coq Auto Compile}.
 
 
 @c TEXI DOCSTRING MAGIC: coq-compile-before-require
-@defopt coq-compile-before-require 
-If @samp{t} check dependencies of required modules and compile if necessary.@*
-If @samp{t} ProofGeneral intercepts "Require" commands and checks if the
+@defvar coq-compile-before-require 
+If non-nil, check dependencies of required modules and compile if necessary.@*
+If non-nil ProofGeneral intercepts "Require" commands and checks if the
 required library module and its dependencies are up-to-date. If not, they
 are compiled from the sources before the "Require" command is processed.
 
 This option can be set/reset via menu
 @samp{Coq -> Settings -> Compile Before Require}.
-
-The default value is @code{nil}.
-@end defopt
+@end defvar
 
 
 @c TEXI DOCSTRING MAGIC: coq-compile-command
-@defopt coq-compile-command 
+@defvar coq-compile-command 
 External compilation command. If empty ProofGeneral compiles itself.@*
 If unset (the empty string) ProofGeneral computes the dependencies of
 required modules with coqdep and compiles as necessary. This internal
@@ -4237,25 +4235,21 @@ when module "foo" from directory "bar" is required.
 
 After the substitution the command can be changed in the
 minibuffer if @samp{@code{coq-confirm-external-compilation}} is t.
-
-The default value is @code{""}.
-@end defopt
+@end defvar
 
 
 @c TEXI DOCSTRING MAGIC: coq-confirm-external-compilation
-@defopt coq-confirm-external-compilation 
+@defvar coq-confirm-external-compilation 
 If set let user change and confirm the compilation command.@*
 Otherwise start the external compilation without confirmation.
 
 This option can be set/reset via menu
 @samp{Coq -> Settings -> Confirm External Compilation}.
-
-The default value is @code{t}.
-@end defopt
+@end defvar
 
 
 @c TEXI DOCSTRING MAGIC: coq-compile-auto-save
-@defopt coq-compile-auto-save 
+@defvar coq-compile-auto-save 
 Buffers to save before checking dependencies for compilation.@*
 There are two orthogonal choices: Firstly one can save all or only the coq
 buffers, where coq buffers means all buffers in coq mode except the current
@@ -4267,20 +4261,16 @@ modified Coq buffers, @code{'ask-all} to confirm saving all modified
 buffers, @code{'save-coq} to save all modified Coq buffers without
 confirmation and @code{'save-all} to save all modified buffers without
 confirmation.
-
-The default value is @code{ask-coq}.
-@end defopt
+@end defvar
 
 
 @c TEXI DOCSTRING MAGIC: coq-lock-ancestors
-@defopt coq-lock-ancestors 
-If t lock ancestor module files.@*
+@defvar coq-lock-ancestors 
+If non-nil, lock ancestor module files.@*
 If external compilation is used (via @samp{@code{coq-compile-command}}) then
 only the direct ancestors are locked. Otherwise all ancestors are
 locked when the "Require" command is processed.
-
-The default value is @code{t}.
-@end defopt
+@end defvar
 
 
 The following two options deal with the load path. Proof General
@@ -4294,7 +4284,7 @@ determines whether the current directory is put into the load
 path of @code{coqdep}.
 
 @c TEXI DOCSTRING MAGIC: coq-load-path
-@defopt coq-load-path 
+@defvar coq-load-path 
 Non-standard coq library load path.@*
 List of directories to be added to the LoadPath of coqdep, coqc
 and coqtop. Under normal circumstances this list does not need to
@@ -4305,20 +4295,16 @@ library.
 For coqdep and coqc these directories are passed via "-I"
 options over the command line. For interactive scripting an
 "Add LoadPath" command is used.
-
-The default value is @code{nil}.
-@end defopt
+@end defvar
 
 
 @c TEXI DOCSTRING MAGIC: coq-load-path-include-current
-@defopt coq-load-path-include-current 
+@defvar coq-load-path-include-current 
 If @samp{t} let coqdep search the current directory too.@*
 Should be @samp{t} for normal users. If @samp{t} pass "-I dir" to coqdep when
 processing files in directory "dir" in addition to any entries
 in @samp{@code{coq-load-path}}.
-
-The default value is @code{t}.
-@end defopt
+@end defvar
 
 
 The following two options do only influence the behaviour if
@@ -4327,7 +4313,7 @@ These options determine whether Proof General should descend into
 other Coq libraries and into the Coq standard library. 
 
 @c TEXI DOCSTRING MAGIC: coq-compile-ignored-directories
-@defopt coq-compile-ignored-directories 
+@defvar coq-compile-ignored-directories 
 Directories in which ProofGeneral should not compile modules.@*
 List of regular expressions for directories in which ProofGeneral
 should not compile modules. If a library file name matches one
@@ -4336,23 +4322,19 @@ neither compile this file nor check its dependencies for
 compilation. It makes sense to include non-standard coq library
 directories here if they are not changed and if they are so big
 that dependency checking takes noticeable time.
-
-The default value is @code{nil}.
-@end defopt
+@end defvar
 
 
 @c TEXI DOCSTRING MAGIC: coq-compile-ignore-library-directory
-@defopt coq-compile-ignore-library-directory 
-If @samp{t} ProofGeneral does not compile modules from the coq library.@*
+@defvar coq-compile-ignore-library-directory 
+If non-nil, ProofGeneral does not compile modules from the coq library.@*
 Should be @samp{t} for normal coq users. If @samp{nil} library modules are
 compiled if their sources are newer.
 
 This option has currently no effect, because Proof General uses
 coqdep to translate qualified identifiers into library file names
 and coqdep does not output dependencies in the standard library.
-
-The default value is @code{t}.
-@end defopt
+@end defvar
 
 
 The last three Emacs constants are internal parameters. They only