From 0dfefb7b78452fe9c3af21a57ebf0cca96f4b7e8 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 28 Mar 2021 17:53:19 +0200 Subject: [PATCH] fix: lean4-mode: inaccessibles highlighting --- lean4-mode/lean4-info.el | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lean4-mode/lean4-info.el b/lean4-mode/lean4-info.el index f5f00b26c3..494628409c 100644 --- a/lean4-mode/lean4-info.el +++ b/lean4-mode/lean4-info.el @@ -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))