michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(emacs/lean-mode): wrong pp highlighting, fixes #225

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-07 02:27:52 -07:00
parent 39645390ff
commit dc0e6861b7
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/emacs/lean-mode.el
View file

@ -200,6 +200,7 @@ Invokes `lean-mode-hook'.
(set (make-local-variable 'comment-use-syntax) t)
(set (make-local-variable 'font-lock-defaults) lean-font-lock-defaults)
(set (make-local-variable 'indent-tabs-mode) nil)
(set 'compilation-mode-font-lock-keywords '())
(set-input-method "Lean")
(set (make-local-variable 'lisp-indent-function)
'common-lisp-indent-function)