From ece7af6fc988d835de9b16fc1bb67f5762bb6aad Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 14 Jan 2016 16:04:50 +0100 Subject: Fix #29 + indentation glitch + regexp refactoring. --- coq/coq-indent.el | 119 ++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 79 insertions(+), 40 deletions(-) (limited to 'coq/coq-indent.el') diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 406fc673..fddfc373 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -96,77 +96,116 @@ detect if they start something or not." (not (proof-string-match "{\\s-*\\(wf\\|measure\\)" str))))))) +(defconst coq-simple-cmd-ender-regexp "[^.]\\|\\=\\|\\.\\." + "Used internally. Matches the allow prefix of the coq \".\" command ending.") + +(defconst coq-bullet-regexp-nospace "\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+" + "Matches single bullet, WARNING: Lots of false positive. + +No context checking.") + +;; We can detect precisely bullets (and curlies) by looking at there +;; prefix: the prefix should be a real "." then spaces then only +;; bullets and curlys and spaces). This is used when search backward. +;; This variable is the regexp of possible prefixes +(defconst coq-bullet-prefix-regexp + (concat "\\(?:\\(?:" coq-simple-cmd-ender-regexp "\\)" + "\\(?:\\.\\)\\(?:\\s-\\)\\(?:\\s-\\|{\\|}\\|-\\|+\\|\\*\\)*\\)")) + ;; matches regular command end (. and ... followed by a space or buffer end) ;; ". " 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-\\|\\'\\)\\)") + (concat "\\(?:\\(?2:" coq-simple-cmd-ender-regexp "\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\)") + "Matches coq regular syntax for ending a command (except bullets and curlies). -;; 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:}\\)\\)") +This should match EXACTLY command ending syntax. No false +positive should be accepted. \"...\" is matched as \".\" with a +left context \"..\". - - -;; bullets must be preceded by a space but since we usually -;; search for this expression from the first non white char of the -;; command, so we give two versions of this regexp - -;; matches bullets. WARNING this matches more than real bullets as - + -;; and * may match this when used in regular expressions -;(defconst coq-bullet-end-command -; "\\(?2:\\s-\\|\\=\\)\\(?:\\(?1:-\\)\\|\\(?1:+\\)\\|\\(?1:\\*\\)\\)") -;; Allowing - -- --- and + ++ +++ ... +There are 3 substrings (2 and 3 may be nil): +* number 1 is the real bullet string, +* number 2 is the left context matched that is not part of the bullet +* number 3 is the right context matched that is not part of the bullet +") ;; 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:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)") + (concat "\\(?:\\(?2:\\s-\\|\\=\\)" "\\(?1:" coq-bullet-regexp-nospace "\\)\\)") + "Matches ltac bullets. WARNING: lots of false positive. -(defconst coq-bullet-regexp-nospace - "\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)") +This matches more than real bullets as - + and * may match this +when used in regular expressions. See +`coq-bullet-end-command-backward' for a more precise regexp (but +only when searching backward).") -;; Trying to capture precisely bullets when search backward (forward -;; is harder since we need to look backward if a dot is eventually -;; there) +;; Context aware detecting regexp, usefull when search backward. (defconst coq-bullet-end-command-backward -"\\(?:\\(?2:\\(?:[^.]\\|\\=\\|\\.\\.\\)\\(?:\\.\\)\\(?:\\s-\\)\\(?:\\s-\\|{\\|}\\|-\\|+\\|\\*\\)*\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)" -) + (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)") + "Matches ltac bullets when searching backward. + +This should match EXACTLY bullets. No false positive should be accepted. +There are 2 substrings: +* number 1 is the real bullet string, +* number 2 is the left context matched that is not part of the bullet" ) + +(defconst coq-curlybracket-end-command + "\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)" + "Matches ltac curlies when searching backward. Warning: False positive. + +There are 3 substrings (2 and 3 may be nil): +* number 1 is the real bullet string, +* number 2 is the left context matched that is not part of the bullet +* number 3 is the right context matched that is not part of the bullet + +This matches more than real ltac curlies. See +`coq-bullet-end-command-backward' for a more precise regexp (but +only when searching backward).") + +(defconst coq-curlybracket-end-command-backward + (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)\\(?:\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\)\\|\\(?1:}\\)\\)\\)") + "Matches ltac curly brackets when searching backward. + +This should match EXACTLY script structuring curlies. No false +positive should be accepted. +There are 3 substrings (2 and 3 may be nil): +* number 1 is the real bullet string, +* number 2 is the left context matched that is not part of the bullet +* number 3 is the right context matched that is not part of the bullet") -;; order matter here, since bullet regexp contains period regexp (defconst coq-end-command-regexp (concat coq-period-end-command "\\|" coq-bullet-end-command "\\|" coq-curlybracket-end-command) -; "\\(?2:[^.]\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)" - "Regexp matching end of a command. There are 3 substrings: + "Matches end of commands (and ltac bullets and curlies). WARNING: False positive. + +There are 3 substrings: * number 1 is the real coq ending string, * number 2 is the left context matched that is not part of the ending string * number 3 is the right context matched that is not part of the ending string -WARNING: this regexp accepts curly brackets (if not preceded by -'|') and bullets (+ - *) (if preceded by a space or at cursor). -This is of course not correct and some more check is needed to -distinguish between the different uses of this characters. -Currently bullets are always ending an empty command, so we just -need to check that the command ended by the bullet-like regexp is empty. -This is done below and also in coq-smie.el.") +WARNING: this regexp accepts some curly brackets and bullets (+ - +*) with no sufficient context verification. Lots of false +positive are matched. Currently bullets and curlies are always +ending an empty command, so we just need to check that the +command ended by the bullet-like regexp is empty. This is done in +coq-smie.el, and see `coq-end-command-regexp-backward' for a more +precise regexp (but only when searching backward).") (defconst coq-end-command-regexp-backward (concat coq-bullet-end-command-backward "\\|" coq-period-end-command "\\|" - coq-curlybracket-end-command) -; "\\(?2:[^.]\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)" - "Regexp matching end of a command. There are 3 substrings: + coq-curlybracket-end-command-backward) + "Matches end of commands, including bullets and curlies. + +There are 3 substrings (2 and 3 may be nil): * number 1 is the real coq ending string, * number 2 is the left context matched that is not part of the ending string * number 3 is the right context matched that is not part of the ending string -This regexp is much more precise than `coq-end-command-regexp' but only +Remqrk: This regexp is much more precise than `coq-end-command-regexp' but only works when searching backward.") -- cgit v1.2.3