- erase invalid coq-load-path entry format '("dir")

- check if coq-load-path is well-formed
- update documentation

2 files changed, 34 insertions, 31 deletions

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index d5264412..bd80d47e 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -364,7 +364,7 @@ file for the mode, which will be
 where @var{proof-home-directory} is the value of the
 variable @samp{@code{proof-home-directory}}.
 
-The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (phox "PhoX" "phx") (lego "LEGO" "l") (hol-light "HOL Light" "ml"))}.
+The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (phox "PhoX" "phx") (hol-light "HOL Light" "ml") (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci"))}.
 @end defopt
 
 
@@ -3216,7 +3216,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{'isar} @code{'coq} @code{'phox} @code{'lego} @code{'hol-light}.
+A list of symbols chosen from: @code{'isar} @code{'coq} @code{'phox} @code{'hol-light} @code{'pgshell} @code{'pgocaml} @code{'pghaskell}.
 If nil, the default will be ALL available proof assistants.
 
 Each proof assistant defines its own instance of Proof General,
@@ -4132,44 +4132,50 @@ after a completed proof.
 
 @c TEXI DOCSTRING MAGIC: proof-shell-handle-delayed-output
 @defun proof-shell-handle-delayed-output 
-Display delayed outputs, when queue is stopped or completed.@*
+Display delayed goals/responses, when queue is stopped or completed.@*
 This function handles the cases of @samp{proof-shell-output-kind} which
 are not dealt with eagerly during script processing, namely
 @code{'response} and @code{'goals} types.
 
-This is useful even with empty delayed output as it can
-clear the buffers.
+This is useful even with empty delayed output as it will empty
+the buffers.
 
 The delayed output is in the region
 [@code{proof-shell-delayed-output-start},@code{proof-shell-delayed-output-end}].
 
+If no goals classified output is found, the whole output is
+displayed in the response buffer.
+
 If goals output is found, the last matching instance, possibly
-bounded by @samp{@code{proof-shell-end-goals-regexp}}, will be displayed.
-Any output that appears @strong{before} the first goals output (but
+bounded by @samp{@code{proof-shell-end-goals-regexp}}, will be displayed
+in the goals buffer (and may be further analysed by Proof General).
+
+Any output that appears @strong{before} the last goals output (but
 after messages classified as urgent, see @samp{@code{proof-shell-filter}})
-will also be displayed in the response buffer.  For example,
-if @var{output} has this form:
+will also be displayed in the response buffer.
+
+For example, if @var{output} has this form:
 @lisp
   @var{messsage-1}
   @var{goals-1}
   @var{message-2}
   @var{goals-2}
+  @var{junk}
 @end lisp
 then @var{goals-2} will be displayed in the goals buffer, and @var{message-2}
-in the response buffer.  Notice that the above alternation can
+in the response buffer.  @var{junk} will be ignored.
+
+Notice that the above alternation (and separation of @var{junk}) can
 only be distinguished if both @samp{@code{proof-shell-start-goals-regexp}}
-and @samp{@code{proof-shell-end-goals-regexp}} are set.  With just the
-former, @var{message-1} @var{goals-1} @var{message-2} would all appear in
-the response buffer.
+and @samp{@code{proof-shell-end-goals-regexp}} are set.  With just the start
+goals regexp set, @var{goals-2} @var{junk} will appear in the goals buffer
+and no response output would occur.
 @lisp
 @end lisp
 The goals and response outputs are copied into
 @samp{@code{proof-shell-last-goals-output}} and
 @samp{@code{proof-shell-last-response-output}} respectively.
 
-If no other kind of classified output is found, the default
-is to display the output in the response buffer.
-
 The value returned is the value for @samp{@code{proof-shell-last-output-kind}},
 i.e., @code{'goals} or @code{'response}.
 @end defun
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 177601ff..b998b70c 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4435,23 +4435,19 @@ This list specifies the LoadPath extension for coqdep, coqc and
 coqtop. Usually, the elements of this list are strings (for
 "-I") or lists of two strings (for "-R" dir "-as" path).
 
-The possible forms of elements of this list correspond to the 4
-possible forms of the Add LoadPath command and the 4 forms of the
-include options ('-I' and @code{'-R'}). An element can be
+The possible forms of elements of this list correspond to the 3
+forms of include options ('-I' and @code{'-R'}). An element can be
 @lisp
   - A string, specifying a directory to be mapped to the empty
     logical path ('-I').
   - A list of the form '(rec dir path)' (where dir and path are
     strings) specifying a directory to be recursively mapped to the
     logical path @code{'path'} ('-R dir -as path').
-  - A list of the form '(rec dir)', specifying a directory to be
-    recursively mapped to the empty logical path ('-R dir').
   - A list of the form '(norec dir path)', specifying a directory
     to be mapped to the logical path @code{'path'} ('-I dir -as path').
 @end lisp
 For convenience the symbol @code{'rec'} can be omitted and entries of
-the form '(dir)' and '(dir path)' are interpreted as '(rec dir)
-and '(rec dir path)', respectively.
+the form '(dir path)' are interpreted as '(rec dir path)'.
 
 Under normal circumstances this list does not need to
 contain the coq standard library or "." for the current
@@ -4527,14 +4523,15 @@ are treated as errors.
 @c TEXI DOCSTRING MAGIC: coq-coqdep-error-regexp
 @defvar coq-coqdep-error-regexp 
 Regexp to match errors in the output of coqdep.@*
-coqdep indicates errors not via a non-zero exit status, but only
-via printing warnings. This regular expression is used for
-recognizing error conditions in the output of coqdep. Its
-default value matches the warning that some required library
-cannot be found on the load path and ignores the warning for
-finding a library at multiple places in the load path. If you
-want to turn the latter condition into an error, then set this
-variable to "^\*\*\* Warning".
+coqdep indicates errors not always via a non-zero exit status,
+but sometimes only via printing warnings. This regular expression
+is used for recognizing error conditions in the output of
+coqdep (when coqdep terminates with exit status 0). Its default
+value matches the warning that some required library cannot be
+found on the load path and ignores the warning for finding a
+library at multiple places in the load path. If you want to turn
+the latter condition into an error, then set this variable to
+"^\*\*\* Warning".
 @end defvar