diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-06-06 15:03:19 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-06-06 15:03:19 +0200 |
| commit | 8b0a89887d175866c3c47594ce24508076500110 (patch) | |
| tree | 80c16d01118b00d0118facd818e0d6c3384d2477 | |
| parent | 1725748691514dcb819df36da92b774c4f827dad (diff) | |
Small fix in a regexp.
| -rw-r--r-- | coq/coq-syntax.el | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index c24b63f9..5219afa7 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1354,11 +1354,18 @@ It is used: (proof-zap-commas)))) -;; ", " is for multiple hypothesis displayed in v8.5. If more than -;; 1 space this is a hypothesis displayed in the middle of a line (> v8.5) -;; "^ " is for goals in debug mode. +;; ", " is for multiple hypothesis displayed in v8.5. +;; exactly no space after start of line = hyps names in +;; Search results (and when we get a more compact display of hyps) +;; exactly 2 spaces at start of line = is for normal goal display at +;; start of line +;; exactly 3 spaces at start of line = hyps on the same line (Set +;; Printing Compact Goals". +;; If more than 3 spaces: not a hyp. +;; we used to have: "^ " for goals in debug mode but it does not seem +;; necessary anymore. (defvar coq-hyp-name-in-goal-or-response-regexp - "\\(?:\\(?1:\n\\)\\|\\(?1:\n \\)\\|\\(?1:\n \\)\\|\\(?:[^ ]\\)\\(?1: \\)\\)\\(?2:\\(?:[^\n :(),=]\\|, \\)+\\) *\\(?::=?[ \n]\\|,$\\)" + "\\(?:\\(?1:^\\)\\|\\(?1:^ \\)\\|\\(?:[^ ]\\)\\(?1: \\)\\)\\(?2:\\(?:[^\n :(),=]\\|, \\)+\\) *\\(?::=?[ \n]\\|,$\\)" "regexp matching hypothesis names in goal or response buffer. Subexpr 2 contains the real name of the function. Subexpr 1 contains the prefix context (spaces mainly) that is not |