Added note about no specific doc for Coq PG

1 files changed, 86 insertions, 41 deletions

diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi
index f81d11e7..89e5024d 100644
--- a/doc/NewDoc.texi
+++ b/doc/NewDoc.texi
@@ -989,7 +989,7 @@ Print help message giving syntax.
 
 @c TEXI DOCSTRING MAGIC: proof-interrupt-process
 @deffn Command proof-interrupt-process 
-Interrupt the proof assistant.  WARNING! This may confuse Proof General.
+Interrupt the proof assistant.  @var{warning}! This may confuse Proof General.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-execute-minibuffer-cmd
@@ -1687,14 +1687,14 @@ generic level, for LEGO you can also customize:
 
 @c TEXI DOCSTRING MAGIC: lego-tags
 @defopt lego-tags 
-The directory of the TAGS table for the LEGO library
+The directory of the @var{tags} table for the @var{lego} library
 
 The default value is @code{"/usr/lib/lego/lib_Type/"}.
 @end defopt
 
 @c TEXI DOCSTRING MAGIC: lego-help-menu-list
 @defvar lego-help-menu-list 
-List of menu items, as defined in @samp{@code{easy-menu-define}} for LEGO
+List of menu items, as defined in @samp{@code{easy-menu-define}} for @var{lego}
 @lisp
   specific help.
 @end lisp
@@ -1725,6 +1725,16 @@ in your @file{~/.emacs} file.
 @node Coq Proof General
 @chapter Coq Proof General
 
+Sorry, there is no specific documentation written yet for Coq Proof
+General.
+
+If any Coq user would like to contribute, please send a message to
+@code{proofgen@@dcs.ed.ac.uk}.
+
+Type @kbd{C-h C-m} to get a list of Coq specific commands and
+browse the customize menus to find out what customization
+options there are for Coq.
+
 @menu
 * Coq specific commands::       
 * Coq customizations::          
@@ -1973,15 +1983,15 @@ Proof General's table of supported proof assistants.
 Extend this table to add a new proof assistant.
 Each entry is a list of the form
 @lisp
-    (SYMBOL NAME AUTOMODE-REGEXP)
+    (@var{symbol} @var{name} @var{automode-regexp})
 @end lisp
-The NAME is a string, naming the proof assistant.
-The SYMBOL is used to form the name of the mode for the
-assistant, @samp{SYMBOL-mode}, run when files with AUTOMODE-REGEXP
-are visited.  SYMBOL is also used to form the name of the
+The @var{name} is a string, naming the proof assistant.
+The @var{symbol} is used to form the name of the mode for the
+assistant, @samp{SYMBOL-mode}, run when files with @var{automode-regexp}
+are visited.  @var{symbol} is also used to form the name of the
 directory and elisp file for the mode, which will be
 @lisp
-    <proof-home-directory>/SYMBOL/SYMBOL.el
+    <proof-home-directory>/SYMBOL/@var{symbol}.el
 @end lisp
 where @samp{<proof-home-directory>/} is the value of the
 variable @code{proof-home-directory}.
@@ -2101,30 +2111,30 @@ func-menu configuration in proof-script-find-next-goalsave.
 Regular expressions to control finding definitions in script.
 This is the list of the form
 @lisp
-   (ANYENTITY-REGEXP
-    DISCRIMINATOR-REGEXP  ... DISCRIMINATOR-REGEXP)
+   (@var{anyentity-regexp}
+    @var{discriminator-regexp}  ... @var{discriminator-regexp})
 @end lisp
-The idea is that ANYENTITY-REGEXP matches any named entity in the
+The idea is that @var{anyentity-regexp} matches any named entity in the
 proof script, on a line where the name appears.  This is assumed to be
 the start or the end of the entity.  The discriminators then test
 which kind of entity has been found, to get its name.  A
-DISCRIMINATOR-REGEXP has one of the forms
+@var{discriminator-regexp} has one of the forms
 @lisp
-  (REGEXP MATCHNO) 
-  (REGEXP MATCHNO @code{backward} BACKREGEXP) 
-  (REGEXP MATCHNO @code{forward} FORWARDREGEXP)
+  (@var{regexp} @var{matchno}) 
+  (@var{regexp} @var{matchno} @code{backward} @var{backregexp}) 
+  (@var{regexp} @var{matchno} @code{forward} @var{forwardregexp})
 @end lisp
-If REGEXP matches the string captured by ANYENTITY-REGEXP, then
-MATCHNO is the match number for the substring which names the entity.
+If @var{regexp} matches the string captured by @var{anyentity-regexp}, then
+@var{matchno} is the match number for the substring which names the entity.
 
-If @code{backward} BACKREGEXP is present, then the start of the entity
-is found by searching backwards for BACKREGEXP.
+If @code{backward} @var{backregexp} is present, then the start of the entity
+is found by searching backwards for @var{backregexp}.
 
-Conversely, if @code{forward} FORWARDREGEXP is found, then the end of
-the entity is found by searching forwards for FORWARDREGEXP.
+Conversely, if @code{forward} @var{forwardregexp} is found, then the end of
+the entity is found by searching forwards for @var{forwardregexp}.
 
 Otherwise, the start and end of the entity will be the region matched
-by ANYENTITY-REGEXP.
+by @var{anyentity-regexp}.
 
 This mechanism allows fairly complex parsing of the buffer, in
 particular, it allows for goal..save regions which are named
@@ -2344,27 +2354,27 @@ variables.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-handle-error-hook
 @defvar proof-shell-handle-error-hook 
-Hooks run after an error has been reported in the RESPONSE buffer.
+Hooks run after an error has been reported in the @var{response} buffer.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-process-file
 @defvar proof-shell-process-file 
 A tuple of the form (regexp . function) to match a processed file name.
 
-If REGEXP matches output, then the function FUNCTION is invoked on the
+If @var{regexp} matches output, then the function @var{function} is invoked on the
 output string chunk. It must return a script file name (with complete
-path) the system is currently processing. In practice, FUNCTION is
+path) the system is currently processing. In practice, @var{function} is
 likely to inspect the match data.  If it returns the empty string,
 the file name of the scripting buffer is used instead.  If it
 returns nil, no action is taken.
 
 Care has to be taken in case the prover only reports on compiled
-versions of files it is processing. In this case, FUNCTION needs to
+versions of files it is processing. In this case, @var{function} needs to
 reconstruct the corresponding script file name. The new (true) file
 name is added to the front of @samp{@code{proof-included-files-list}}.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-retract-files-regexp
 @defvar proof-shell-retract-files-regexp 
-A REGEXP to match that the prover has retracted across file boundaries.
+A @var{regexp} to match that the prover has retracted across file boundaries.
 
 At this stage, Proof General's view of the processed files is out of
 date and needs to be updated with the help of the function
@@ -2387,7 +2397,7 @@ Set this variable to handle system specific output.
 Errors, start of proofs, abortions of proofs and completions of
 proofs are recognised in the function @samp{@code{proof-shell-process-output}}.
 All other output from the proof engine is simply reported to the
-user in the RESPONSE buffer.
+user in the @var{response} buffer.
 
 To catch further special cases, set this variable to a pair of
 functions '(condf . actf). Both are given (cmd string) as arguments.
@@ -2618,7 +2628,7 @@ is located in, or to the variable of the environment variable
 @c TEXI DOCSTRING MAGIC: proof-home-directory
 @defvar proof-home-directory 
 Directory where Proof General is installed. Ends with slash.
-Default value taken from environment variable PROOFGENERAL_HOME if set, 
+Default value taken from environment variable PROOFGENERAL_@var{home} if set, 
 otherwise based on where the file proof-site was loaded from.
 You can use customize to set this variable.
 @end defvar
@@ -2659,7 +2669,7 @@ providing session control, script management, etc.  Proof General
 will be started automatically for the assistants chosen here.
 To avoid accidently invoking a proof assistant you don't have,
 only select the proof assistants you (or your site) may need.
-NOTE: to change proof assistant, you must start a new Emacs session.
+@var{note}: to change proof assistant, you must start a new Emacs session.
 
 The default value is @code{(isa lego coq)}.
 @end defopt
@@ -2901,6 +2911,11 @@ shell mode is defined to inherit from @code{comint-mode} using
 code in the file is concerned with sending code to and from the shell,
 and processing output for the associated buffers (goals and response).
 
+Clever process handling is a tricky issue.  Proof General attempts to
+manage the process strictly, by mainting a queue of commands to send to
+the process.  Once a command has been processed, another one is popped
+off the queue and sent.
+
 There are several important internal variables which control
 interaction with the process.
 
@@ -2918,11 +2933,12 @@ Marker in proof shell buffer pointing to previous command input.
 
 @c TEXI DOCSTRING MAGIC: proof-action-list
 @defvar proof-action-list 
-A list of
+A list of lists of the form:
 @lisp
-  (span,command,action)
+  (@var{span} @var{command} @var{action})
 @end lisp
-triples, which is a queue of things to do.
+which is a queue of things to do.
+See the functions @code{proof-start-queue} and proof-exec-loop.
 @end defvar
 
 The function @code{proof-shell-start} is used to initialise a shell
@@ -2971,7 +2987,7 @@ and clearing all script buffers.
 
 Input to the proof shell via the queue region is dealt with by
 the functions @code{proof-start-queue} and
-@code{proof-shell-exec-loop}.
+@code{proof-shell-exec-loop}.    
 
 @c TEXI DOCSTRING MAGIC: proof-start-queue
 @defun proof-start-queue start end alist
@@ -2983,7 +2999,7 @@ active scripting buffer for the queue region.
 @c TEXI DOCSTRING MAGIC: proof-shell-exec-loop
 @defun proof-shell-exec-loop 
 Process the @code{proof-action-list}.
-@code{proof-action-list} contains a list of (span,command,action) triples.
+@code{proof-action-list} contains a list of (SPAN COMMAND ACTION) triples.
 This function is called with a non-empty @code{proof-action-list}, where the
 head of the list is the previously executed command which succeeded.
 We execute (action span) on the first item, then (action span) on
@@ -2993,6 +3009,11 @@ and removes the queue region.  Otherwise send the next command to the
 proof process.
 @end defun
 
+A useful utility function for sending a single command to the process is
+@code{proof-shell-invisible-command}.  This should be used to implement
+user-level functions rather than attempting to manipulate the proof
+action list directly.
+
 @c
 @c OUTPUT
 @c
@@ -3016,7 +3037,7 @@ This function deals with errors, start of proofs, abortions of
 proofs and completions of proofs. All other output from the proof
 engine is simply reported to the user in the response buffer
 by setting @code{proof-shell-delayed-output} to a cons cell of
-(insert . txt) where TXT is the text to be inserted.
+(@var{insert} . @var{text}) where @var{text} is the text to be inserted.
 
 To extend this function, set
 @code{proof-shell-process-output-system-specific}.
@@ -3045,10 +3066,34 @@ The main processing point which triggers other actions is
 @c TEXI DOCSTRING MAGIC: proof-shell-filter
 @defun proof-shell-filter str
 Filter for the proof assistant shell-process.
-We process urgent messages first.  Then wait until we get a
-@code{proof-shell-wakeup-char} in the input, then run
-@code{proof-shell-process-output}, and set @code{proof-marker} to keep track of
-how far we've got.
+
+Process urgent messages first.  As many as possible are processed,
+using the function @samp{@code{proof-shell-process-urgent-messages}}.
+
+Otherwise wait until an annotated prompt appears in the input, then
+run @code{proof-shell-process-output} on the output between the new prompt
+and the last input (position of @code{proof-marker}) or the last
+urgent message (position of @code{proof-shell-urgent-message-marker}),
+whichever is later.  For example, in this case:
+@lisp
+ PROMPT> @var{input}
+ @var{output-1}
+ @var{urgent-message}
+ @var{output-2}
+ PROMPT>
+@end lisp
+@code{proof-marker} is set after @var{input} by @code{proof-shell-insert} and
+@code{proof-shell-urgent-message-marker} is set after @var{urgent-message}.
+Only @var{output-2} will be processed.  For this reason, error
+messages and interrupt messages should @strong{not} be considered
+urgent messages.
+
+Appropriate action is taken depending on the what
+@code{proof-shell-process-output} returns: maybe handle an interrupt, an
+error, or deal with ordinary output which is a candidate
+for the goal or response buffer.
+Ordinary output is only displayed when the proof action list
+becomes empty, to avoid a confusing rapidly changing output.
 @end defun