diff options
| -rw-r--r-- | coq/coq.el | 50 | ||||
| -rw-r--r-- | doc/PG-adapting.texi | 38 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 27 |
3 files changed, 63 insertions, 52 deletions
@@ -1504,30 +1504,24 @@ 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 '-R'). An element can be +The possible forms of elements of this list correspond to the 3 +forms of include options ('-I' and '-R'). An element can be - 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 '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 'path' ('-I dir -as path'). For convenience the symbol '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 directory (see `coq-load-path-include-current')." :type '(repeat (choice (string :tag "simple directory without path (-I)") - (list :tag "recursive directory without path (-R)" - (const rec) (string :tag "directory")) (list :tag "recursive directory with path (-R ... -as ...)" (const rec) @@ -1538,15 +1532,7 @@ directory (see `coq-load-path-include-current')." (const nonrec) (string :tag "directory") (string :tag "log path")))) - :safe '(lambda (v) (every - '(lambda (entry) - (or (stringp entry) - (and (eq (car entry) 'rec) - (every 'stringp (cdr entry))) - (and (eq (car entry) 'nonrec) - (every 'stringp (cdr entry))) - (every 'stringp entry))) - v)) + :safe 'coq-load-path-safep :group 'coq-auto-compile) (defcustom coq-compile-auto-save 'ask-coq @@ -1700,6 +1686,28 @@ DEP-MOD-TIMES is empty it returns nil." max)) +;; safety predicate for coq-load-path + +(defun coq-load-path-safep (path) + "Check if PATH is a safe value for `coq-load-path'." + (and + (listp path) + (every + '(lambda (entry) + (or (stringp entry) + (and (listp entry) + (eq (car entry) 'rec) + (every 'stringp (cdr entry)) + (equal (length entry) 3)) + (and (listp entry) + (eq (car entry) 'nonrec) + (every 'stringp (cdr entry)) + (equal (length entry) 3)) + (and (listp entry) + (every 'stringp entry) + (equal (length entry) 2)))) + path))) + ;; Compute command line for starting coqtop (defun coq-prog-args () @@ -1782,9 +1790,7 @@ options they are translated." (t (if (eq (car entry) 'rec) (setq entry (cdr entry))) - (if (nth 1 entry) - (list "-R" (expand-file-name (car entry)) "-as" (nth 1 entry)) - (list "-R" (expand-file-name (car entry))))))) + (list "-R" (expand-file-name (car entry)) "-as" (nth 1 entry))))) (defun coq-include-options (file) "Build the list of include options for coqc, coqdep and coqtop. @@ -1797,6 +1803,8 @@ append more arguments with `nconc'. FILE should be an absolute file name. It can be nil if `coq-load-path-include-current' is nil." (let ((result nil)) + (unless (coq-load-path-safep coq-load-path) + (error "Invalid value in coq-load-path")) (when coq-load-path (setq result (coq-option-of-load-path-entry (car coq-load-path))) (dolist (entry (cdr coq-load-path)) 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 |