max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: lean4-mode: inaccessibles highlighting

Browse source
This commit is contained in:
Sebastian Ullrich 2021-03-28 17:53:19 +02:00
parent 9e3b8caa4b
commit 0dfefb7b78
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
lean4-mode/lean4-info.el
View file

@ -44,7 +44,8 @@
(unless (get-buffer buffer)
(with-current-buffer (get-buffer-create buffer)
(buffer-disable-undo)
(magit-section-mode))))
(magit-section-mode)
(set-syntax-table lean4-syntax-table))))
(defun lean4-toggle-info-buffer (buffer)
(-if-let (window (get-buffer-window buffer))