Enhancement: quick way to adjust bullet levels

[andersk]

I often find that I want to refactor a giant bulleted proof tree by inserting or deleting a level of bullets, say to turn

  eexists.
  simpl.
  split.
  - destruct H.
    + destruct H1.
      econstructor.
    + econstructor.
      * econstructor.
        eassumption.
      * reflexivity.
  - eassumption.

into

  edestruct IHa.
  - reflexivity.
  - eexists.
    simpl.
    split.
    + destruct H.
      * destruct H1.
        econstructor.
      * econstructor.
        -- econstructor.
           eassumption.
        -- reflexivity.
    + eassumption.

I would find it useful to have a quick way to adjust all of the bullets automatically when doing so. This could perhaps take the form of keyboard shortcuts to increase/decrease all bullet levels within the selected region.

[cpitclaudel]

Thanks, this is a cool idea.

Can you try pasting the following into *scratch* and running eval-buffer after opening a Coq file?

(defun company-coq-features/code-folding--cycle-bullet (bullet delta)
  (let* ((bullets '(?- ?+ ?*))
         (bullet-char (aref bullet 0))
         (char-idx (-elem-index bullet-char bullets))
         (new-idx (mod (+ char-idx delta) (length bullets)))
         (new-char (nth new-idx bullets))
         (new-length (+ (length bullet)
                        (if (eq (+ char-idx delta) new-idx) 0 delta))))
    (make-string (max 1 new-length) new-char)))

(defvar company-coq--features/code-folding--increment-bullets-map
  (let ((map (make-sparse-keymap)))
    (define-key map (kbd ">") #'company-coq-features/code-folding-increment)
    (define-key map (kbd "<") #'company-coq-features/code-folding-decrement)
    (define-key map (kbd "<right>") #'company-coq-features/code-folding-increment)
    (define-key map (kbd "<left>") #'company-coq-features/code-folding-decrement)
    map))

(defun company-coq-features/code-folding--increment-bullets (delta)
  (save-excursion
    (let ((beg (region-beginning))
          (end (region-end)))
      (goto-char beg)
      (set-transient-map company-coq--features/code-folding--increment-bullets-map t)
      (while (re-search-forward company-coq-features/code-folding--bullet-regexp end t)
        (goto-char (match-beginning 1))
        (when (company-coq-features/code-folding--really-on-bullet-p (point))
          (let ((bullet (and (looking-at "[-+*]+") (match-string 0))))
            (replace-match (company-coq-features/code-folding--cycle-bullet bullet delta) t t))))
      (indent-rigidly beg end (* 2 delta))
      (setq deactivate-mark nil))))

(defun company-coq-features/code-folding-increment ()
  (interactive)
  (company-coq-features/code-folding--increment-bullets 1))

(defun company-coq-features/code-folding-decrement ()
  (interactive)
  (company-coq-features/code-folding--increment-bullets -1))

(define-key coq-mode-map (kbd "C-c >"))
(define-key coq-mode-map (kbd "C-c <"))

With these definitions you should be able to press C-c > after selecting a block of lines to increment all bullets. Repeating > and < (no need for C-c for repeats) should indent (resp. dedent) further.

Let me know if that works for you; if it does I'll merge it :)

[andersk]

Cool, that was fast! It almost works.

• The last two define-keys are missing their third argument.
• The <right> and <left> bindings surprised me; I just wanted to move the cursor.
• You maybe want to disable the decrement command if there’s a - bullet, since the current behavior there is not reversible.
• Sometimes the decrement command also causes the line following the region to be dedented by two spaces. I think end needs to be adjusted after the replace-match operations.

[cpitclaudel]

Thanks!

The last two define-keys are missing their third argument.

Uh, you're right; I wonder where that argument went :/

The and bindings surprised me; I just wanted to move the cursor.

I'll remove them :) (I modeled them after C-x TAB)

You maybe want to disable the decrement command if there’s a - bullet, since the current behavior there is not reversible.

An alternative could be to drop the bullets once they pass '-'. The would allow you to remove a top-level bullet.

Sometimes the decrement command also causes the line following the region to be dedented by two spaces. I think end needs to be adjusted after the replace-match operations.

That's right.

Here's a new version:

(defun company-coq--cycle-bullet (bullet delta)
  (let* ((bullets '(?- ?+ ?*))
         (bullet-char (aref bullet 0))
         (char-idx (-elem-index bullet-char bullets))
         (new-idx (mod (+ char-idx delta) (length bullets)))
         (new-char (nth new-idx bullets))
         (new-length (+ (length bullet)
                        (if (eq (+ char-idx delta) new-idx) 0 delta))))
    (if (= new-length 0) " "
      (make-string new-length new-char))))

(defvar company-coq--increment-bullets-map
  (let ((map (make-sparse-keymap)))
    (define-key map (kbd ">") #'company-coq-increment-bullets)
    (define-key map (kbd "<") #'company-coq-decrement-bullets)
    map))

(defun company-coq--increment-bullets-1 (beg end delta)
  (save-excursion
    (goto-char beg)
    (setq beg (goto-char (point-at-bol)))
    (setq end (move-marker (make-marker) end))
    (while (re-search-forward company-coq-features/code-folding--bullet-regexp end t)
      (goto-char (match-beginning 1))
      (when (company-coq-features/code-folding--really-on-bullet-p (point))
        (let ((bullet (and (looking-at "[-+*]+") (match-string 0))))
          (replace-match (company-coq--cycle-bullet bullet delta) t t)))))
  (indent-rigidly beg end (* 2 delta))
  (setq deactivate-mark nil)
  (move-marker end nil))

(defun company-coq--increment-bullets (delta)
  (set-transient-map company-coq--increment-bullets-map t)
  (company-coq--increment-bullets-1 (region-beginning) (region-end) delta))

(defun company-coq-increment-bullets ()
  (interactive)
  (company-coq--increment-bullets 1))

(defun company-coq-decrement-bullets ()
  (interactive)
  (company-coq--increment-bullets -1))

(define-key coq-mode-map (kbd "C-c >") #'company-coq-increment-bullets)
(define-key coq-mode-map (kbd "C-c <") #'company-coq-decrement-bullets)

Thanks for your help!

[andersk]

Thank you—this looks great!