undo-tree-mode is disabled by default in Coq files

[kindaro]

Description

undo-tree-mode is disabled by default in Coq files.

Reproduction guide 🪲

• Make sure:
  • The Coq layer is available.
  • The undo-tree package is available.
• Start Emacs.
• Open a text file.
  • Run undo-tree-visualize (SPC a u).
  • Observe undo tree working normally.
• Open a Coq source file.
  • Run undo-tree-visualize (SPC a u).
  • Observe error: Undo-tree mode not enabled in buffer.

Observed behaviour: 👀 💔

Error: Undo-tree mode not enabled in buffer.

Expected behaviour: ❤️ 😄

Undo tree working normally.

System Info 💻

• OS: gnu/linux
• Emacs: 26.3
• Spacemacs: 0.300.0
• Spacemacs branch: develop (rev. c50d0a8)
• Graphic display: t
• Distribution: spacemacs
• Editing style: vim
• Completion: helm
• Layers:

(helm auto-completion emacs-lisp
      (keyboard-layout :variables kl-layout 'bepo)
      coq)

• System configuration features: XPM JPEG TIFF GIF PNG RSVG IMAGEMAGICK SOUND GPM DBUS GSETTINGS GLIB NOTIFY ACL GNUTLS LIBXML2 FREETYPE M17N_FLT LIBOTF XFT ZLIB TOOLKIT_SCROLL_BARS GTK3 X11 XDBE XIM MODULES THREADS LIBSYSTEMD LCMS2

[duianto]

Confirmed.

It seems to be on purpose, because: C-h l (l = lowercase L) shows that u calls:
u [pg-protected-undo]

The repository: https://github.com/ProofGeneral/PG
remaps undo to pg-protected-undo here:
https://github.com/ProofGeneral/PG/search?q=pg-protected-undo&unscoped_q=pg-protected-undo

Windows 1903

#### System Info :computer:
- OS: windows-nt
- Emacs: 26.3
- Spacemacs: 0.300.0
- Spacemacs branch: develop (rev. b5f0eb5f7)
- Graphic display: t
- Distribution: spacemacs
- Editing style: vim
- Completion: helm
- Layers:
```elisp
(autohotkey clojure command-log common-lisp coq emacs-lisp ess git helm imenu-list javascript
            (markdown :variables markdown-live-preview-engine 'vmd markdown-command "vmd")
            multiple-cursors
            (org :variables org-agenda-files
                 '("~/org/notes.org"))
            pdf python
            (shell :variables shell-default-shell 'shell shell-default-height 30 shell-default-position 'bottom)
            spell-checking syntax-checking treemacs version-control)
```
- System configuration features: XPM JPEG TIFF GIF PNG RSVG SOUND NOTIFY ACL GNUTLS LIBXML2 ZLIB TOOLKIT_SCROLL_BARS THREADS LCMS2

[kindaro]

Turns out there is an open issue in the Proof General repository that discusses this: ProofGeneral/PG#430

[github-actions]

This issue has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. Please let us know if this issue is still valid!

[kindaro]

This issue is still valid! And I still have not learned enough about Emacs's internals to fix it myself!

[github-actions]

This issue has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. Please let us know if this issue is still valid!

[github-actions]

This issue has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. Please let us know if this issue is still valid!