Skip to content

Commit ed6adac

Browse files
committed
[info] EXPERIMENT: Remove local settings in lean4-info-mockup-mode
1 parent 14573f3 commit ed6adac

File tree

1 file changed

+1
-6
lines changed

1 file changed

+1
-6
lines changed

lean4-info.el

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -44,12 +44,7 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean."
4444
(define-derived-mode lean4-info-mockup-mode prog-mode "Lean-Info"
4545
"Major mode used internally to syntax highlight Lean4."
4646
:syntax-table lean4-syntax-table
47-
:group 'lean4
48-
(set (make-local-variable 'font-lock-defaults) lean4-info-font-lock-defaults)
49-
(set (make-local-variable 'indent-tabs-mode) nil)
50-
(set 'compilation-mode-font-lock-keywords '())
51-
(set (make-local-variable 'lisp-indent-function)
52-
'common-lisp-indent-function))
47+
:group 'lean4)
5348

5449
(defun lean4-info-ensure-buffer (buffer)
5550
"Create BUFFER if it does not exist.

0 commit comments

Comments
 (0)