diff options
| -rw-r--r-- | coq/coq-abbrev.el | 9 | ||||
| -rw-r--r-- | coq/coq-db.el | 8 | ||||
| -rw-r--r-- | coq/coq.el | 72 |
3 files changed, 73 insertions, 16 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 3c926639..538ad5ec 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -61,12 +61,9 @@ ;; da: this test will always fail. Assume bound-->non-empty ;; (not (equal coq-mode-abbrev-table (make-abbrev-table)))) (message "Coq abbrevs already exists, default not loaded") - (let - ;; prevent query to immediately save these abbrevs - ((save-abbrevs nil)) - (define-abbrev-table 'coq-mode-abbrev-table - (append coq-tactics-abbrev-table coq-tacticals-abbrev-table - coq-commands-abbrev-table coq-terms-abbrev-table))) + (define-abbrev-table 'coq-mode-abbrev-table + (append coq-tactics-abbrev-table coq-tacticals-abbrev-table + coq-commands-abbrev-table coq-terms-abbrev-table)) ;; if we use default coq abbrev, never ask to save it ;; PC: fix trac #382 I comment this. But how to disable abbrev ;; saving for coq mode only? diff --git a/coq/coq-db.el b/coq/coq-db.el index 7fa7d1f4..10c6c25d 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -227,11 +227,11 @@ See `coq-syntax-db' for DB structure." ) ;; careful: nconc destructive! (when e2 - (if coq-holes-minor-mode - (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete)))) - (setq res (nconc res (list `(,e2 ,e3)))))) + (push `(,e2 ,e3 ,(if coq-holes-minor-mode #'holes-abbrev-complete) + :system t) + res)) (setq l tl))) - res)) + (nreverse res))) (defun filter-state-preserving (l) @@ -240,6 +240,7 @@ SMIE is a navigation and indentation framework available in Emacs ≥ 23.3." ("if" exp "then" exp "else" exp) ("forall" exp "," exp) ("(" exps ")") + ("{|" exps "|}") (exp ":" exp) (exp "->" exp)) ;; Having "return" here rather than as a separate rule in `exp' @@ -250,22 +251,37 @@ SMIE is a navigation and indentation framework available in Emacs ≥ 23.3." (exps (exp) (exps "," exps)) (decls ("Lemma" exp ":=" exp) ("Definition" exp ":=" exp) + ("Let" exp ":=" exp) ("Function" exp ":=" exp) ("Fixpoint" exp ":=" exp) ("Inductive" exp ":=" branches) ("Notation" exp ":=" exp) + ("Record" exp ":=" exp) ;; The above elements are far from the only ones terminated by "." ;; (think of all the tactics). So we won't list them all, instead ;; we'll use "." as separator rather than terminator. ;; This has the downside that smie-forward-sexp on a "Definition" ;; stops right before the "." rather than right after. - (decls "." decls))) + (decls "." decls) + ("BeginSubproof" decls "EndSubproof") + ("Module" decls "End") + ("Section" decls "End"))) ;; Resolve the "trailing expression ambiguity" as in "else x -> b". '((nonassoc "else" "in" "=>" ",") (left ":") (assoc "->")) ;; Declare that we don't care about associativity of separators. '((assoc "|")) '((assoc ",")) '((assoc ";")) '((assoc "."))))) "Parsing table for Coq. See `smie-grammar'.") +(defun coq-smie-search-token (tokens &optional end) + "Search for one of TOKENS between point and END." + (unless end (setq end (point-max))) + (catch 'found + (while (< (point) end) + (let ((next (funcall smie-forward-token-function))) + (cond + ((zerop (length next)) (forward-sexp 1)) + ((member next tokens) (throw 'found next))))))) + (defun coq-smie-forward-token () (let ((tok (smie-default-forward-token))) (cond @@ -285,6 +301,16 @@ SMIE is a navigation and indentation framework available in Emacs ≥ 23.3." next (goto-char pos) tok))) + ((equal tok "Module") + (let ((pos (point)) + (next (smie-default-forward-token))) + (unless (equal next "Type") (goto-char pos)) + (save-excursion + (if (equal (coq-smie-search-token '(":=" ".")) ":=") + "Module def" tok)))) + ((and (equal tok "") (looking-at "{|")) (goto-char (match-end 0)) "{|") + ((and (equal tok "|") (eq (char-after) ?\})) + (goto-char (1+ (point))) "|}") (tok)))) (defun coq-smie-backward-token () @@ -303,27 +329,61 @@ SMIE is a navigation and indentation framework available in Emacs ≥ 23.3." (prev (smie-default-backward-token))) (unless (equal prev "Program") (goto-char pos)) tok)) + ((equal tok "Type") + (let ((pos (point)) + (prev (smie-default-backward-token))) + (if (equal prev "Module") + pref + (goto-char pos) + tok))) + ((equal tok "Module") + (save-excursion + (if (equal (coq-smie-search-token '(":=" ".")) ":=") + "Module def" tok))) + ((and (equal tok "|") (eq (char-before) ?\{)) + (goto-char (1- (point))) "{|") + ((and (equal tok "") (looking-back "|}" (- (point) 2))) + (goto-char (match-beginning 0)) "|}") (tok)))) (defun coq-smie-rules (kind token) - "Indentation rules for Coq. See `smie-rules-function'." + "Indentation rules for Coq. See `smie-rules-function'. +KIND is the situation and TOKEN is the thing w.r.t which the rule applies." (case kind (:elem (case token (basic proof-indent))) - (:list-intro (member token '("fun" "forall"))) + (:list-intro + (or (member token '("fun" "forall")) + ;; We include "." in list-intro for the ". { .. } \n { .. }" so the + ;; second {..} is aligned with the first rather than being indented as + ;; if it were an argument to the first. + (when (equal token ".") + (smie-default-forward-token) + (forward-comment (point-max)) + (looking-at "{")))) (:after (cond ;; Override the default indent step added because of their presence ;; in smie-closer-alist. + ((equal token "with") 4) ((member token '("," ":=")) 0))) (:before (cond ((equal token "return") (if (smie-rule-parent-p "match") 3)) - ((equal token "|") (if (smie-rule-parent-p "with") 3)) + ((equal token "|") + (if (smie-rule-parent-p "with") + (- (funcall smie-rules-function :after "with") 2))) ((equal token ":=") (if (smie-rule-parent-p "Definition" "Lemma" "Fixpoint" "Inductive" - "Function") - (or proof-indent smie-indent-basic))))))) + "Function" "Let" "Record") + (or proof-indent smie-indent-basic))) + ((equal token ".") + (if (smie-rule-parent-p "BeginSubproof" "Module" "Section" "Proof") 2)) + ((and (equal token "{") (smie-rule-prev-p ":=")) + (smie-rule-parent)) + ((and (equal token ",") (smie-rule-parent-p "forall")) 2) + ((and (equal token ":") (smie-rule-parent-p "Lemma")) 2) + )))) ;; ;; Auxiliary code for Coq modes |