diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-12-07 15:31:41 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-12-07 15:31:41 +0100 |
| commit | 295386b34a0c973dd9f5e4974fb4dd03402c3867 (patch) | |
| tree | 8e5e31acc254ed557e2fc7588c1ff7bd032313a2 /coq/coq-indent.el | |
| parent | a4410595a448c9b5b44cfd75e2c2f48e664d5aea (diff) | |
Speeding up indentation (regexp optim).
Diffstat (limited to 'coq/coq-indent.el')
| -rw-r--r-- | coq/coq-indent.el | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el index cdbd9efe..406fc673 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -100,13 +100,13 @@ detect if they start something or not." ;; ". " and "... " are command endings, ".. " is not, same as in ;; proof-script-command-end-regexp in coq.el (defconst coq-period-end-command - "\\(?2:[^.]\\|\\=\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)") + "\\(?:\\(?2:[^.]\\|\\=\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\)") ;; matches curly bracket but not {| and |} WARNING this matches more ;; than the script parenthesizing '{' and '}' as curly bracket may ;; match this when used in regular expressions (defconst coq-curlybracket-end-command - "\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)") + "\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)") @@ -119,24 +119,23 @@ detect if they start something or not." ;(defconst coq-bullet-end-command ; "\\(?2:\\s-\\|\\=\\)\\(?:\\(?1:-\\)\\|\\(?1:+\\)\\|\\(?1:\\*\\)\\)") ;; Allowing - -- --- and + ++ +++ ... -(defconst coq-bullet-end-command-old - "\\(?2:\\s-\\|\\=\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)") - -(defconst coq-bullet-regexp-nospace - "\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)") ;; captures a lot of false bullets, need to check that the commaand is ;; empty. When searching forward (typically when splitting the buffer ;; into commands commands) we can't do better than that. ;; For backward searching see `coq-bullet-end-command-backward' below. (defconst coq-bullet-end-command - "\\(?2:\\s-\\|\\=\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)") + "\\(?:\\(?2:\\s-\\|\\=\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)") + +(defconst coq-bullet-regexp-nospace + "\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)") ;; Trying to capture precisely bullets when search backward (forward ;; is harder since we need to look backward if a dot is eventually ;; there) (defconst coq-bullet-end-command-backward - "\\(?2:\\(?:[^.]\\|\\=\\|\\.\\.\\)\\(?:\\.\\)\\(?:\\s-\\)\\(?:\\s-+\\|{\\|}\\|\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)*\\)\\(?:\\s-\\)+\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)") +"\\(?:\\(?2:\\(?:[^.]\\|\\=\\|\\.\\.\\)\\(?:\\.\\)\\(?:\\s-\\)\\(?:\\s-\\|{\\|}\\|-\\|+\\|\\*\\)*\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)" +) ;; order matter here, since bullet regexp contains period regexp (defconst coq-end-command-regexp |