Opened 10 years ago
Closed 9 years ago
#493 closed defect (wontfix)
ProofGeneral stalls/loops on ...
Reported by: | coquser | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | PG-Emacs-4.3 |
Component: | 2:pg-emacs | Keywords: | coq ltac |
Cc: | jasongross9@… |
Description
Goal True.
...
Evaluating this script (the "..." is literal) will cause PG to loop forever/stall while it waits for Coq to respond.
Change History (3)
comment:1 Changed 10 years ago by
comment:2 Changed 9 years ago by
The following patch fixes it for me. It's not too pretty, though.
--- coq-indent.el.~11.24.~ 2015-01-27 04:27:09.000000000 -0500 +++ coq-indent.el 2015-04-27 15:04:47.537983825 -0400 @@ -326,6 +326,13 @@ (goto-char (match-beginning 1)) (not (coq-empty-command-p))) nil) + (and (string-equal (match-string 1) ".") + (save-excursion + (goto-char (match-beginning 1)) + (skip-chars-backward ".") + (skip-chars-backward " \t\n") + (left-char) + (looking-at-p "[^a-zA-Z_][ \t\n]*\\.\\.\\."))) (and (goto-char foundend) (proof-buffer-syntactic-context))))
The real problem is in the definition of coq-period-end-command, which considers ... to be a sentence terminator in all cases (it is only when preceded by at least on alphabetic character (and possibly whitespace):
(defconst coq-period-end-command "\\(?2:[^.]\\|\\=\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)")
This could be a coq error though. Are there examples of ... as a command starter?
comment:3 Changed 9 years ago by
Resolution: | → wontfix |
---|---|
Status: | new → closed |
Hi,
Indeed this is a strang coq-8.4 behavior that seems fixed in v8.5.
v8.4 seem to be waiting for more input, and only after seeing a "." does he detect that ... is misplaced.
Maybe not worth fixing? Feel free to reopen if you feel the need. P.
Similarly with
However,
correctly goes through and solves the goal.