diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-indent.el | 144 |
1 files changed, 71 insertions, 73 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 9ca75457..a069ab07 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -47,10 +47,10 @@ ;; "using" "after")))) ; "ALL" "True" "False" "EX" "end" "in" "of" "with" -;; (defconst coq-comment-start-regexp "(\\*") -;; (defconst coq-comment-end-regexp "\\*)") -;; (defconst coq-comment-start-or-end-regexp -;; (concat coq-comment-start-regexp "\\|" coq-comment-end-regexp)) +(defconst coq-comment-start-regexp "(\\*") +(defconst coq-comment-end-regexp "\\*)") +(defconst coq-comment-start-or-end-regexp + (concat coq-comment-start-regexp "\\|" coq-comment-end-regexp)) ;; (defconst coq-indent-open-regexp ;; (proof-regexp-alt ;(proof-regexp-alt-list coq-keywords-goal) goal-command-p instead ;; (proof-ids-to-regexp '("Cases" "match" "BeginSubproof")) @@ -234,75 +234,73 @@ Remqrk: This regexp is much more precise than `coq-end-command-regexp' but only works when searching backward.") -;; (defun coq-search-comment-delimiter-forward () -;; "Search forward for a comment start (return 1) or end (return -1). -;; Return nil if not found." -;; (when (re-search-forward coq-comment-start-or-end-regexp nil 'dummy) -;; (save-excursion -;; (goto-char (match-beginning 0)) -;; (if (looking-at coq-comment-start-regexp) 1 -1)))) - - -;; (defun coq-search-comment-delimiter-backward () -;; "Search backward for a comment start (return 1) or end (return -1). -;; Return nil if not found." -;; (when (re-search-backward coq-comment-start-or-end-regexp nil 'dummy) -;; (if (looking-at coq-comment-start-regexp) 1 -1))) - - -;; (defun coq-skip-until-one-comment-backward () -;; "Skips comments and normal text until finding an unclosed comment start. -;; Return nil if not found. Point is moved to the the unclosed comment start -;; if found, to (point-max) otherwise. Return t if found, nil otherwise." -;; (if (= (point) (point-min)) nil -;; (ignore-errors (backward-char 1)) ; if point is between '(' and '*' -;; (if (looking-at coq-comment-start-regexp) t -;; (forward-char 1) -;; (let ((nbopen 1) (kind nil)) -;; (while (and (> nbopen 0) (setq kind (coq-search-comment-delimiter-backward))) -;; (if (< kind 0) -;; (setq nbopen (+ 1 nbopen)) -;; (setq nbopen (- nbopen 1)))) -;; (= nbopen 0))))) - -;; (defun coq-skip-until-one-comment-forward () -;; "Skips comments and normal text until finding an unopened comment end." -;; (ignore-errors (backward-char 1)) ; if point is between '*' and ')' -;; (if (looking-at coq-comment-end-regexp) (progn (forward-char 2) t) -;; (forward-char 1) -;; (let ((nbopen 1) (kind nil)) -;; (while (and (> nbopen 0) (setq kind (coq-search-comment-delimiter-forward))) -;; (if (> kind 0) (setq nbopen (+ 1 nbopen)) -;; (setq nbopen (- nbopen 1)))) -;; (= nbopen 0)))) - -;; (defun coq-looking-at-comment () -;; "Return non-nil if point is inside a comment." -;; (or (proof-inside-comment (point)) -;; (proof-inside-comment (+ 1 (point))))) - -;; (defun coq-find-comment-start () -;; "Go to the current comment start. -;; If inside nested comments, go to the start of the outer most comment. -;; Return the position of the comment start. If not inside a comment, -;; return nil and does not move the point." -;; (when (coq-looking-at-comment) -;; (let ((prevpos (point)) (init (point))) -;; (while (coq-skip-until-one-comment-backward) -;; (setq prevpos (point))) -;; (goto-char prevpos) -;; (if (= prevpos init) nil prevpos)))) - -;; (defun coq-find-comment-end () -;; "Go to the current comment end. -;; If inside nested comments, go to the end of the outer most -;; comment. Return the position of the end of comment end. If not inside -;; a comment, return nil and does not move the point." -;; (let ((prevpos (point)) (init (point))) -;; (while (coq-skip-until-one-comment-forward) -;; (setq prevpos (point))) -;; (goto-char prevpos) -;; (if (= prevpos init) nil prevpos))) +(defun coq-search-comment-delimiter-forward () + "Search forward for a comment start (return 1) or end (return -1). +Return nil if not found." + (when (re-search-forward coq-comment-start-or-end-regexp nil 'dummy) + (save-excursion + (goto-char (match-beginning 0)) + (if (looking-at coq-comment-start-regexp) 1 -1)))) + +(defun coq-search-comment-delimiter-backward () + "Search backward for a comment start (return 1) or end (return -1). + Return nil if not found." + (when (re-search-backward coq-comment-start-or-end-regexp nil 'dummy) + (if (looking-at coq-comment-start-regexp) 1 -1))) + +(defun coq-skip-until-one-comment-backward () + "Skips comments and normal text until finding an unclosed comment start. + Return nil if not found. Point is moved to the the unclosed comment start +if found, to (point-max) otherwise. Return t if found, nil otherwise." + (if (= (point) (point-min)) nil + (ignore-errors (backward-char 1)) ; if point is between '(' and '*' + (if (looking-at coq-comment-start-regexp) t + (forward-char 1) + (let ((nbopen 1) (kind nil)) + (while (and (> nbopen 0) (setq kind (coq-search-comment-delimiter-backward))) + (if (< kind 0) + (setq nbopen (+ 1 nbopen)) + (setq nbopen (- nbopen 1)))) + (= nbopen 0))))) + +(defun coq-skip-until-one-comment-forward () + "Skips comments and normal text until finding an unopened comment end." + (ignore-errors (backward-char 1)) ; if point is between '*' and ')' + (if (looking-at coq-comment-end-regexp) (progn (forward-char 2) t) + (forward-char 1) + (let ((nbopen 1) (kind nil)) + (while (and (> nbopen 0) (setq kind (coq-search-comment-delimiter-forward))) + (if (> kind 0) (setq nbopen (+ 1 nbopen)) + (setq nbopen (- nbopen 1)))) + (= nbopen 0)))) + +(defun coq-looking-at-comment () + "Return non-nil if point is inside a comment." + (or (proof-inside-comment (point)) + (proof-inside-comment (+ 1 (point))))) + +(defun coq-find-comment-start () + "Go to the current comment start. +If inside nested comments, go to the start of the outer most comment. +Return the position of the comment start. If not inside a comment, +return nil and does not move the point." + (when (coq-looking-at-comment) + (let ((prevpos (point)) (init (point))) + (while (coq-skip-until-one-comment-backward) + (setq prevpos (point))) + (goto-char prevpos) + (if (= prevpos init) nil prevpos)))) + +(defun coq-find-comment-end () + "Go to the current comment end. +If inside nested comments, go to the end of the outer most +comment. Return the position of the end of comment end. If not inside +a comment, return nil and does not move the point." + (let ((prevpos (point)) (init (point))) + (while (coq-skip-until-one-comment-forward) + (setq prevpos (point))) + (goto-char prevpos) + (if (= prevpos init) nil prevpos))) ; generic function is wrong when the point in between ( and * ;; (defun coq-looking-at-syntactic-context () |