fix(src/emacs): remove lua

src/emacs/lean-mmm-lua.el

@@ -1,27 +0,0 @@
-;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved.
-;; Released under Apache 2.0 license as described in the file LICENSE.
-;;
-;; Author: Soonho Kong
-;;
-
-(require 'mmm-mode)
-(require 'mmm-auto)
-(require 'lua-mode)
-(setq mmm-global-mode 'maybe)
-(setq mmm-submode-decoration-level 0)
-(eval-after-load 'mmm-vars
-  '(progn
-     (mmm-add-group
-      'lean-lua
-      '((lua-inline
-         :submode lua-mode
-         :face mmm-code-submode-face
-         :insert ((?l lean-tag nil @ "(*\n" @ " " _ "" @ "\n*)" @))
-         :front "[(][*]"
-         :back "[*][)]")))
-     (mmm-add-mode-ext-class 'lean-mode "\\.lean" 'lean-lua)))
-(defun lean-mmm-lua-hook ()
-  (setq-local mmm-parse-when-idle t)
-  (setq-local mmm-idle-timer-delay 0.5))
-
-(provide 'lean-mmm-lua)

src/emacs/lean-mode.el

@@ -25,7 +25,6 @@
 (require 'lean-tags)
 (require 'lean-option)
 (require 'lean-syntax)
-(require 'lean-mmm-lua)
 (require 'lean-company)
 (require 'lean-changes)
 (require 'lean-server)
@@ -312,7 +311,7 @@ enabled and disabled respectively.")
   ;; Flycheck
   (when lean-flycheck-use
     (lean-flycheck-turn-on)
-    (setq-local flycheck-disabled-checkers '(lua))
+    (setq-local flycheck-disabled-checkers '())
     (add-hook 'flycheck-after-syntax-check-hook 'lean-flycheck-delete-temporaries nil t))
   ;; Draw a vertical line for rule-column
   (when (and lean-rule-column
@@ -330,8 +329,6 @@ enabled and disabled respectively.")
   ;; company-mode
   (when lean-company-use
     (company-lean-hook))
-  ;; mmm-lua-mode
-  (lean-mmm-lua-hook)
   ;; choose minor mode -- Standard / HoTT
   (let ((minor-mode (lean-choose-minor-mode-based-on-extension)))
     (cond