diff options
| -rw-r--r-- | coq/coq-indent.el | 76 | ||||
| -rw-r--r-- | coq/coq-smie.el | 18 |
2 files changed, 54 insertions, 40 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 93feebca..dee10cb6 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -14,6 +14,13 @@ (require 'coq-syntax) +;; debugging +;(defmacro measure-time (&rest body) +; "Measure the time it takes to evaluate BODY." +; `(let ((time (current-time))) +; ,@body +; (message "%.06f" (float-time (time-since time))))) + (eval-when-compile (defvar coq-script-indent nil)) @@ -112,18 +119,21 @@ detect if they start something or not." ;(defconst coq-bullet-end-command ; "\\(?2:\\s-\\|\\=\\)\\(?:\\(?1:-\\)\\|\\(?1:+\\)\\|\\(?1:\\*\\)\\)") ;; Allowing - -- --- and + ++ +++ ... -(defconst coq-bullet-end-command +(defconst coq-bullet-end-command-old "\\(?2:\\s-\\|\\=\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)") (defconst coq-bullet-regexp-nospace "\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)") +;TODO: add curly brackets +(defconst coq-bullet-end-command + "\\(?2:\\(?:[^.]\\|\\=\\|\\.\\.\\)\\(?:\\.\\)\\s-+\\(?:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)*\\)\\s-+\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)\\)") - +;; order matter here, since bullet regexp contains period regexp (defconst coq-end-command-regexp - (concat coq-period-end-command "\\|" - coq-curlybracket-end-command "\\|" - coq-bullet-end-command) + (concat coq-bullet-end-command "\\|" + coq-period-end-command "\\|" + coq-curlybracket-end-command) ; "\\(?2:[^.]\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)" "Regexp matching end of a command. There are 3 substrings: * number 1 is the real coq ending string, @@ -304,16 +314,15 @@ command end regexp." ;; Handle non-comments: assumed to be commands (if (< (coq-is-on-ending-context) 0) (ignore-errors (forward-char (coq-is-on-ending-context)))) - (let (foundend next-pos) + (let (foundend) ;; Find end of command (while (and (setq foundend (and - (re-search-forward proof-script-command-end-regexp limit t) + (re-search-forward coq-end-command-regexp limit t) (match-end 1))) - (setq next-pos (+ 1 (match-beginning 0))) (or - (if (not (or (string-equal (match-string 1) ".") - (string-equal (match-string 1) "..."))) + (and (not (or (string-equal (match-string 1) ".") + (string-equal (match-string 1) "..."))) ; command-end that are not a dot are + ++ - ; -- etc or { or } to ensure this is really ; a bullet (and not one of the numerous @@ -322,19 +331,17 @@ command end regexp." ; empty. example: ; destruct x. ; - (* - here ends an empty command*) - (save-excursion - (goto-char (match-beginning 1)) - (not (coq-empty-command-p))) - nil) - (and - (goto-char foundend) - (proof-buffer-syntactic-context)))) - ;; go back as far as possible before the start of the current - ;; matching string, this way we will match consecutive endings - ;; like ine "}." - (ignore-errors (goto-char next-pos)) -; (ignore-errors (forward-char -1)) - ) + (save-excursion + (goto-char (match-beginning 1)) + (not (coq-empty-command-p)))) + (and + (goto-char foundend) + (proof-buffer-syntactic-context)))) + ;; Given the form of coq-end-command-regexp + ;; match-end 1 is the right place to start again + ;; to search backward, next time we start from just + ;; there + (ignore-errors (goto-char foundend))) (if (and foundend (goto-char foundend) ; move to command end (not (proof-buffer-syntactic-context))) @@ -360,23 +367,26 @@ and return nil." ;; first shift if we are in the middle of a ending pattern (if (> (coq-is-on-ending-context) 0) (ignore-errors(forward-char (coq-is-on-ending-context)))) - (let (foundbeg next-pos) + (let (foundbeg) ;; Find end of command (while (and (setq foundbeg (and - (re-search-backward proof-script-command-end-regexp limit 'dummy) + (re-search-backward coq-end-command-regexp limit 'dummy) (match-beginning 1))) - (setq next-pos (- (match-end 0) 1)) - (or (if (not (or (string-equal (match-string 1) ".") - (string-equal (match-string 1) "..."))) - (save-excursion - (goto-char (match-beginning 1)) - (not (coq-empty-command-p))) - nil) + ;; Given the form of coq-end-command-regexp + ;; match-beginning 1 is the right place to start again + ;; to search backward, next time we start from just + ;; there + (goto-char foundbeg) + (or (and (not (or (string-equal (match-string 1) ".") + (string-equal (match-string 1) "..."))) + (save-excursion + (goto-char (match-beginning 1)) + (not (coq-empty-command-p)))) (and (goto-char foundbeg) (proof-buffer-syntactic-context)))) - (ignore-errors (goto-char next-pos))) + (ignore-errors (goto-char foundbeg))) (if (and foundbeg (goto-char foundbeg) ; move to command end (not (proof-buffer-syntactic-context))) diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 2dc5482c..939e0cc3 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -35,11 +35,12 @@ (require 'coq-indent) (require 'smie nil 'noerror) -(defmacro measure-time (&rest body) - "Measure the time it takes to evaluate BODY." - `(let ((time (current-time))) - ,@body - (message "%.06f" (float-time (time-since time))))) +; debugging +;(defmacro measure-time (&rest body) +; "Measure the time it takes to evaluate BODY." +; `(let ((time (current-time))) +; ,@body +; (message "%.06f" (float-time (time-since time))))) (defun coq-string-suffix-p (str1 str2 &optional ignore-case) @@ -209,7 +210,8 @@ command (and inside parenthesis)." (equal (char-syntax ?\)) (char-syntax (char-after))))) (throw 'found nil)) ((zerop (length next)) ;; capture other characters than closing parent - (let ((forward-sexp-function nil)) (forward-sexp -1))) + ;; don't use smmie-forward-sexp here + (let ((forward-sexp-function nil)) (forward-sexp 1))) ((member next tokens) (throw 'found next)))))))) (scan-error nil))) @@ -256,7 +258,9 @@ command (and inside parenthesis). " (or (equal (point) (point-min)) ; protecting char-before next line (equal (char-syntax ?\() (char-syntax (char-before))))) (throw 'found nil)) - ((zerop (length next)) (let ((forward-sexp-function nil)) (forward-sexp -1))) + ((zerop (length next)) + ;; don't use smmie-forward-sexp here + (let ((forward-sexp-function nil)) (forward-sexp -1))) ((member next tokens) (throw 'found next)))))))) (scan-error nil))) |