diff options
| author | David Aspinall | 1999-02-22 14:54:02 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-02-22 14:54:02 +0000 |
| commit | 6acfaf0683cc83e1ff047d1a834ebb707c1e3269 (patch) | |
| tree | e49d7ec7d9da8a73a0836165102cd2b0d9202e0b | |
| parent | 93f33c9240d3adab95ab6f75e884fa37f00e0063 (diff) | |
Comments from Healf explaining need for coq-goal-command-p
| -rw-r--r-- | coq/coq-syntax.el | 5 | ||||
| -rw-r--r-- | coq/coq.el | 7 |
2 files changed, 5 insertions, 7 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index a696cf32..16f2a15f 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -28,11 +28,6 @@ "Scheme" )) -;; FIXME da: I'm not sure why this variable includes more than -;; just the Goal-type commands. Perhaps it was so that func-menu -;; worked neatly, but it leads to the nasty use of proof-goal-command-p -;; instead of a proof-goal-regexp. Func menu configuration has since -;; been overhauled, so this could maybe be improved now. (defvar coq-keywords-goal '( "Definition" @@ -145,8 +145,11 @@ (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-defn)) "Declaration and definition regexp.") -;; FIXME da: this one function breaks the nice configuration of Proof General: -;; should have proof-goal-regexp instead. +;; da: this one function breaks the nice configuration of Proof General: +;; would be nice to have proof-goal-regexp instead. +;; Unfortunately Coq allows Goals beginning with "Definition" and the +;; like, so it is difficult to have just a proof-goal-regexp setting. + (defun coq-goal-command-p (str) "Decide whether argument is a goal or not" (and (proof-string-match coq-goal-command-regexp str) |