diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2015-03-04 14:34:09 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2015-03-04 14:34:09 +0000 |
commit | 69198d98ee274af7ab60e26d93a4078c540c9e59 (patch) | |
tree | fd5d663c01f8e739870f0f8c81f6a707d5549389 /coq | |
parent | 4e0cdecdc3fa43dc07585ac05334bb6c9a3e622a (diff) |
Fixed Proof end/start detection on Proof using ...
Was making scripting confused.
P.
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq-smie.el | 2 | ||||
-rw-r--r-- | coq/coq-syntax.el | 9 |
2 files changed, 5 insertions, 6 deletions
diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 993674b6..9a7df711 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -106,7 +106,7 @@ the token of \".\" is simply \".\"." ((looking-at "Proof\\>") (forward-char 5) (coq-find-not-in-comment-forward "[^[:space:]]") ;; skip spaces and comments - (if (looking-at "\\.\\|with") ". proofstart" ".")) + (if (looking-at "\\.\\|with\\|using") ". proofstart" ".")) ((or (looking-at "Next\\s-+Obligation\\>") (coq-smie-detect-goal-command)) (save-excursion diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index a4e11ba1..9075c1e1 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -741,7 +741,7 @@ Used by `coq-goal-command-p'" (defun coq-section-command-p (str) (proof-string-match "\\`\\(Section\\|Chapter\\)\\>" str)) - +;; unused anymore (for good) (defun coq-goal-command-str-p (str) "Decide syntactically whether STR is a goal start or not. Use `coq-goal-command-p' on a span instead if possible." @@ -776,7 +776,8 @@ Used by `coq-goal-command-p'" (or (coq-section-command-p str) (coq-module-opening-p str))))) -;; TODO: rely on coq response nistead for span grouping +;; TODO: rely on coq response nistead for span grouping Or better have +;; coq change its syntax for something better. (defvar coq-keywords-save-strict '("Defined" "Save" "Qed" "End" "Admitted" "Abort" ) "This regexp must match *exactly* commands that close a goal/Module. @@ -793,9 +794,7 @@ It is used: "Decide whether argument is a Save command or not" (or (proof-string-match coq-save-command-regexp-strict str) (and (proof-string-match "\\`Proof\\>" str) - (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\)" str))) - ) - ) + (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\|using\\)" str))))) ;; ----- keywords for font-lock. |