From 9fa30e3f7d8334c1cbd0a327506a4e9f8f7bc749 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 11 May 2016 13:50:45 -0400
Subject: [PATCH] chore(emacs): remove Lua support

---
 src/emacs/Cask            |  2 --
 src/emacs/README.md       | 16 +---------------
 src/emacs/lean-mmm-lua.el | 27 ---------------------------
 src/emacs/lean-mode.el    |  4 ----
 src/emacs/lean-require.el |  2 +-
 src/emacs/load-lean.el    |  2 +-
 6 files changed, 3 insertions(+), 50 deletions(-)
 delete mode 100644 src/emacs/lean-mmm-lua.el

diff --git a/src/emacs/Cask b/src/emacs/Cask
index 1df55fff1..38e704c00 100644
--- a/src/emacs/Cask
+++ b/src/emacs/Cask
@@ -11,6 +11,4 @@
  (depends-on "flycheck")
  (depends-on "flymake")
  (depends-on "fill-column-indicator")
- (depends-on "lua-mode")
- (depends-on "mmm-mode")
  (depends-on "s"))
diff --git a/src/emacs/README.md b/src/emacs/README.md
index 6a9fcb602..ee7ffccd1 100644
--- a/src/emacs/README.md
+++ b/src/emacs/README.md
@@ -25,8 +25,6 @@ to use full features of ``lean-mode``.
  - [company][company]
  - [flycheck][flycheck]
  - [fill-column-indicator][fci]
- - [lua-mode][lua-mode]
- - [mmm-mode][mmm-mode]
 
 Both the optional and required packages will be installed for you
 automatically the first time you use ``lean-mode``, if you follow the
@@ -35,8 +33,6 @@ installation instructions below.
 [company]: http://company-mode.github.io/
 [flycheck]: http://www.flycheck.org/manual/latest/index.html
 [fci]: https://github.com/alpaker/Fill-Column-Indicator
-[lua-mode]: http://immerrr.github.io/lua-mode/
-[mmm-mode]: https://github.com/purcell/mmm-mode
 
 
 Installation
@@ -75,7 +71,7 @@ Put the following code in your Emacs init file:
 ;; Install required/optional packages for lean-mode
 (defvar lean-mode-required-packages
   '(company dash dash-functional flycheck f
-            fill-column-indicator s lua-mode mmm-mode))
+            fill-column-indicator s))
 (let ((need-to-refresh t))
   (dolist (p lean-mode-required-packages)
     (when (not (package-installed-p p))
@@ -216,16 +212,6 @@ You may also need to install [emacs-unicode-fonts](https://github.com/rolandwalk
 (unicode-fonts-setup)
    ```
 
-"Variable binding depth exceeds max-specpdl-size" Error
----------------------------------------------------------
-
-See [Issue 906](https://github.com/leanprover/lean/issues/906) for details.
-[Moritz Kiefer](https://github.com/cocreature) reported that `proofgeneral` 
-comes with an old version of `mmm-mode` (0.4.8, released in 2004) on ArchLinux
-and it caused this problem. Either removing `proofgeneral` or upgrading
-`mmm-mode` to the latest version (0.5.1 as of 2015 Dec) resolves this issue.
-
-
 Contributions
 =============
 
diff --git a/src/emacs/lean-mmm-lua.el b/src/emacs/lean-mmm-lua.el
deleted file mode 100644
index f2e41253a..000000000
--- a/src/emacs/lean-mmm-lua.el
+++ /dev/null
@@ -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)
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 81f5017d8..950eda73c 100644
--- a/src/emacs/lean-mode.el
+++ b/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)
@@ -313,7 +312,6 @@ enabled and disabled respectively.")
   ;; Flycheck
   (when lean-flycheck-use
     (lean-flycheck-turn-on)
-    (setq-local flycheck-disabled-checkers '(lua))
     (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
@@ -331,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
diff --git a/src/emacs/lean-require.el b/src/emacs/lean-require.el
index 506a96dcf..df0c4f4ad 100644
--- a/src/emacs/lean-require.el
+++ b/src/emacs/lean-require.el
@@ -24,7 +24,7 @@
   (lean-mode-check-package 'package)
   (lean-mode-check-package 'dash)
   (let ((required-packages '(cl-lib compile dash dash-functional f flymake s))
-        (optional-packages '(flycheck fill-column-indicator lua-mode mmm-mode)))
+        (optional-packages '(flycheck fill-column-indicator)))
     (-each required-packages 'lean-mode-require-package)
     (-each optional-packages 'lean-mode-check-package)))
 
diff --git a/src/emacs/load-lean.el b/src/emacs/load-lean.el
index 095156ce7..2c0c738dc 100644
--- a/src/emacs/load-lean.el
+++ b/src/emacs/load-lean.el
@@ -14,7 +14,7 @@
       (condition-case nil
 	  (create-image (format "%s/lean.pgm" lean-emacs-path))
 	(error nil)))
-(setq lean-required-packages '(company dash dash-functional f fill-column-indicator flycheck let-alist lua-mode mmm-mode s seq))
+(setq lean-required-packages '(company dash dash-functional f fill-column-indicator flycheck let-alist s seq))
 
 (setq load-path
       (append