[nongnu] elpa/proof-general dc70d03 1/2: Fix #625 Indentation very slow.

[ELPA Syncer]

branch: elpa/proof-general
commit dc70d038469ef01d25f7f347f99b9ba3c0f6080c
Author: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Commit: Pierre Courtieu <Pierre.Courtieu@cnam.fr>

    Fix #625 Indentation very slow.
    
    Had to change the associativity from `left` to `assoc` for token
    `"."`. This speeds up things by limiting smie token lookups.
    
    I had to change a few indentation rules to restore the correct
    behaviour with the new grammar. I had to:
    
    - use `smie-indent-virtual`
    
    And as side effects:
    
    - fix a wrong tests.
    - fix bugs in find-real-start with sequences of "{ subproof" and comments.
    
    Left for another PR: cleaning up dead code in coq-indent.el.
---
 ci/test-indent/indent-tac.v |  2 +-
 coq/coq-indent.el           | 45 ++++++++++++++++++++++++++++++++++++++-------
 coq/coq-smie.el             | 39 ++++++++++-----------------------------
 3 files changed, 49 insertions(+), 37 deletions(-)

diff --git a/ci/test-indent/indent-tac.v b/ci/test-indent/indent-tac.v
index 7e474d4..19aede3 100644
--- a/ci/test-indent/indent-tac.v
+++ b/ci/test-indent/indent-tac.v
@@ -184,7 +184,7 @@ Module foo.
           simpl;
           intros...
         ]
-      ]
+      ].
   Qed.
 
 
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 715c1e2..e4f72c0 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -78,7 +78,7 @@ No context checking.")
 (defconst coq-bullet-prefix-regexp-backward
   (concat "\\(?:\\(?:" coq-simple-cmd-ender-prefix-regexp-backward 
"\\)\\(?:\\.\\s-+\\)"
           "\\(?:\\(?:" coq-goal-selector-regexp "\\)?"
-          "{\\|}\\|-\\|+\\|\\*\\s-\\)*\\)"))
+          "{\\|}\\|-\\|+\\|\\*\\)+\\s-*\\)"))
 
 ;; matches regular command end (. and ... followed by a space or "}" or buffer 
end)
 ;; ". " and "... " are command endings, ".. " is not, same as in
@@ -124,7 +124,7 @@ There are 2 substrings:
      "\\(?2:"
        "\\(?:" coq-bullet-prefix-regexp-forward"\\)\\)"
       "\\(?1:\\(?:" coq-goal-selector-regexp "\\)?{\\)"
-      "\\(?3:[^|]\\)"
+      "\\(?3:\\s-*[^|{]\\)"
      "\\|"
      ;; [^|]}
      "\\(?2:[^|.]\\|\\=\\)\\(?1:}\\)\\)")
@@ -175,7 +175,7 @@ precise regexp (but only when searching backward).")
 
 ; Order here is significant, when two pattern match with the same
 ; starting position, the first regexp is preferred. period-command is
-; the shorter one so let us have it at the end, but what about cury vs
+; the shorter one so let us have it at the end, but what about curly vs
 ; bullets?
 (defconst coq-end-command-regexp-backward
   (concat coq-bullet-end-command-backward "\\|"
@@ -191,6 +191,38 @@ There are 3 substrings (2 and 3 may be nil):
 Remark: This regexp is much more precise than `coq-end-command-regexp-forward'
 but only works when searching backward.")
 
+(defconst coq-cmd-end-backward-matcher (concat "\\(?2:" 
coq-simple-cmd-ender-prefix-regexp-backward "\\)\\.\\s-"))
+
+(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-previous-endcmd ()
+  "Internal use, look backward for a \".\" that is an end of command.
+
+Go backward and put point exactly after the first \".\" that is
+an end of command, or at point-min if none found. Return the new
+position."
+  (re-search-backward (concat "\\(?2:" 
coq-simple-cmd-ender-prefix-regexp-backward "\\)\\.\\s-") (point-min) 'dummy)
+  (while (coq-looking-at-comment) ;; we are looking for ". " so this is enough
+    (re-search-backward (concat "\\(?2:" 
coq-simple-cmd-ender-prefix-regexp-backward "\\)\\.\\s-") (point-min) 'dummy))
+  ;; unless we reached point-min, jump over the "."
+  (when (match-end 2) (goto-char (match-end 2)) (forward-char 1))
+  (point))
+
+(defun coq-find-start-of-cmd ()
+  (let ((p (point)) (something-found))
+    (coq-find-previous-endcmd)
+    (while (not something-found)
+      (forward-comment (point-max))
+      (if (and (looking-at "\\({\\|}\\|\\++\\|\\*+\\|-+\\)")
+               (< (point) p) ;; if we are after the starting point then 
anything is the start of the current command, even "#" or ".".
+               )
+          (forward-char 1)
+        (setq something-found t))))
+  (point))
+
 
 (defun coq-search-comment-delimiter-forward ()
   "Search forward for a comment start (return 1) or end (return -1).
@@ -417,6 +449,7 @@ regexp."
 
 ;; This is not used by generic pg, just by a few functions in here.
 ;; It is less trustable that itsforward version above.
+;; FIXME: rely on coq-find-previous-endcmd
 (defun coq-script-parse-cmdend-backward (&optional limit)
   "Move to the first end of command (not commented) found looking up.
 Point is put exactly before the last ending token (before the last
@@ -430,7 +463,7 @@ and return nil."
     (if (> (coq-is-on-ending-context) 0)
         (ignore-errors(forward-char (coq-is-on-ending-context))))
     (let (foundbeg)
-      ;; Find end of command
+      ;; Find end of previous command
       (while (and (setq foundbeg
                         (and
                          (re-search-backward coq-end-command-regexp-backward 
limit 'dummy)
@@ -477,9 +510,7 @@ the (point-min) if there is no previous command."
 (defun coq-find-real-start ()
   "Move to the start of command at point.
 The point is put exactly before first non comment letter of the command."
-  (coq-find-current-start)
-  (forward-comment (point-max))
-  (point))
+  (coq-find-start-of-cmd))
 
 ;; (defun same-line (pt pt2)
 ;;  (or (= (line-number-at-pos pt) (line-number-at-pos pt2))))
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index b3357d0..708c793 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -1142,6 +1142,7 @@ Typical values are 2 or 4."
            (exp))
 
       (commands (commands "." commands)
+                ;(commands ". sameline" commands)
                (commands "- bullet" commands)
                (commands "+ bullet" commands)
                (commands "* bullet" commands)
@@ -1171,7 +1172,7 @@ Typical values are 2 or 4."
       (assoc "-- bullet") (assoc "++ bullet") (assoc "** bullet")
       (assoc "--- bullet") (assoc "+++ bullet") (assoc "*** bullet")
       (assoc "---- bullet") (assoc "++++ bullet") (assoc "**** bullet")
-      (left ".")
+      (assoc ".")
       (assoc "with inductive" "with fixpoint" "where"))
     '((nonassoc "Com start") (assoc ":= equations")
       (assoc ":= def" ":= inductive")
@@ -1368,7 +1369,7 @@ KIND is the situation and TOKEN is the thing w.r.t which 
the rule applies."
       (pcase (cons kind token)
         (`(,_ . (or "; record")) (smie-rule-separator kind)) ;; see also the 
"before" rule
         (`(:elem . basic) (or coq-indent-basic (bound-and-true-p proof-indent) 
2))
-        (`(:elem . arg) nil)
+        (`(:elem . arg)  (if (smie-rule-prev-p "} subproof") 0 nil)) ;; hack: 
"{} {}"" not an application
         (`(:close-all . ,_) t)
         (`(:list-intro . ,_) (member token '("fun" "forall" "quantif exists"
                                              "with" "Com start")))
@@ -1409,34 +1410,14 @@ KIND is the situation and TOKEN is the thing w.r.t 
which the rule applies."
              ;; rather querying its virtual indentation to compute indentation 
of another
              ;; (child) token. unbox ==> indent relative to parent.
              ;; unboxed indent for "{" not at bol:
-             ((and (or "{ subproof" "[" "{") (guard (not (smie-rule-bolp))))
-              (cond 
-               ((smie-rule-prev-p "} subproof" "]" "}") (parent 0))
-               (t (parent 2))))
-             ;; unboxed indent for quantifiers (if coq-indent-box-style non 
nil)
-             ((and (or "forall" "quantif exists") (guard (not boxed))
-                   (guard (not (smie-rule-bolp))) )
+             ((and (or "forall" "quantif exists") (guard (and (not 
(smie-rule-bolp)) (not boxed))))
               (parent coq-smie-after-bolp-indentation))
-             ;;((guard (and (message "DEFAULTING") nil)) nil)
-             )))))))
-
-
-
-;; No need of this hack anymore?
-;;       ((and (equal token "Proof End")
-;;             (parent-p "Module" "Section" "goalcmd"))
-;;        ;; ¡¡Major gross hack!!
-;;        ;; This typically happens when a Lemma had no "Proof" keyword.
-;;        ;; We should ideally find some other way to handle it (e.g. matching 
Qed
-;;        ;; not with Proof but with any of the keywords like Lemma that can
-;;        ;; start a new proof), but we can workaround the problem here, 
because
-;;        ;; SMIE happened to decide arbitrarily that Qed will stop before 
Module
-;;        ;; when parsing backward.
-;;        ;; FIXME: This is fundamentally very wrong, but it seems to work
-;;        ;; OK in practice.
-;;        (parent 2))
-
-
+             ((and (or "[" "{") (guard (not (smie-rule-bolp)))) (parent 2))
+             ((guard (and (smie-rule-prev-p "} subproof" "{ subproof" ".") 
(not (smie-rule-bolp))))
+              (cond
+               ((smie-rule-prev-p "} subproof") (parent))
+               ((smie-rule-prev-p "{ subproof") (coq-smie-backward-token) (+ 2 
(smie-indent-virtual)))
+               ((smie-rule-prev-p ".") (smie-backward-sexp 'half) 
(smie-indent-virtual)))))))))))
 
 
 (provide 'coq-smie)