diff options
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq-smie-lexer.el | 44 | ||||
-rw-r--r-- | coq/coq-syntax.el | 2 |
2 files changed, 25 insertions, 21 deletions
diff --git a/coq/coq-smie-lexer.el b/coq/coq-smie-lexer.el index a87beb82..c40adda8 100644 --- a/coq/coq-smie-lexer.el +++ b/coq/coq-smie-lexer.el @@ -14,20 +14,23 @@ ;; - We identify the different types of bullets (First approximation). ;; - We distinguish "with match" from other "with". -(setq coq-smie-dot-friends '("*." "-*." "|-*." "*|-*.")) +(require 'coq-indent) +(require 'smie) + +(defconst coq-smie-dot-friends '("*." "-*." "|-*." "*|-*.")) ; for debuging (defun coq-time-indent () (interactive) - (let ((deb (time-to-seconds))) + (let ((deb (float-time))) (smie-indent-line) - (message "time: %S"(- (time-to-seconds) deb)))) + (message "time: %S"(- (float-time) deb)))) (defun coq-time-indent-region (beg end) (interactive "r") - (let ((deb (time-to-seconds))) + (let ((deb (float-time))) (indent-region beg end nil) - (message "time: %S"(- (time-to-seconds) deb)))) + (message "time: %S"(- (float-time) deb)))) @@ -131,9 +134,9 @@ command (and inside parenthesis)." (coq-smie-search-token-forward (append parops (cons "." nil)) end ignore-between) - (cons "." nil))) ;coq-smie-dot-friends + (cons "." nil)) ;coq-smie-dot-friends (goto-char (point)) - next) + next)) ;; Do not consider "." when not followed by a space (when (or (not (equal next ".")) (looking-at "[[:space:]]")) @@ -656,18 +659,19 @@ Lemma foo: forall n, ; To show the bug. Comment this and then try to indent the following: ; Module X. ; Module Y. <-- here --> Error: (wrong-type-argument integer-or-marker-p nil) -(defun smie-indent--parent () - (or smie--parent - (save-excursion - (let* ((pos (point)) - (tok (funcall smie-forward-token-function))) - (unless (numberp (cadr (assoc tok smie-grammar))) - (goto-char pos)) - (setq smie--parent - (or (smie-backward-sexp 'halfsexp) - (let (res) - (while (null (setq res (smie-backward-sexp)))) - (list nil (point) (nth 2 res))))))))) +; No need anymore? +;; (defun smie-indent--parent () +;; (or smie--parent +;; (save-excursion +;; (let* ((pos (point)) +;; (tok (funcall smie-forward-token-function))) +;; (unless (numberp (cadr (assoc tok smie-grammar))) +;; (goto-char pos)) +;; (setq smie--parent +;; (or (smie-backward-sexp 'halfsexp) +;; (let (res) +;; (while (null (setq res (smie-backward-sexp)))) +;; (list nil (point) (nth 2 res))))))))) (defun coq-smie-rules (kind token) "Indentation rules for Coq. See `smie-rules-function'. @@ -775,4 +779,4 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." -(provide 'coq-smie-lexer)
\ No newline at end of file +(provide 'coq-smie-lexer) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 2030d141..5d80c114 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -328,7 +328,7 @@ "Coq tactic(al)s that solve a subgoal." ) -(setq develock-coq-font-lock-keywords +(defvar develock-coq-font-lock-keywords '((develock-find-long-lines (1 'develock-long-line-1 t) (2 'develock-long-line-2 t)) |