diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 0aab77fe7..4e5b09d22 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -10,18 +10,10 @@ ;; Version: 0.1 ;; URL: https://github.com/leanprover/lean/blob/master/src/emacs ;; -;; ;; Released under Apache 2.0 license as described in the file LICENSE. ;; -;; - -(require 'cl-lib) +(require 'lean-require) (require 'eri) -(require 'generic-x) -(require 'compile) -(require 'flymake) -(require 'dash) -(require 'dash-functional) (require 'lean-variable) (require 'lean-util) (require 'lean-settings) diff --git a/src/emacs/lean-require.el b/src/emacs/lean-require.el new file mode 100644 index 000000000..72bd45e68 --- /dev/null +++ b/src/emacs/lean-require.el @@ -0,0 +1,33 @@ +;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. +;; Released under Apache 2.0 license as described in the file LICENSE. +;; +;; Author: Soonho Kong +;; +(defun lean-mode-require-package (pkg) + "Check whether pkg is available or not." + (unless (featurep pkg) + (if (not (require pkg (symbol-name pkg) t)) + (error "lean-mode: required package '%s' is not found." (symbol-name pkg)) + (message "lean-mode: package %S loaded." pkg)))) + +(defun lean-mode-check-package (pkg) + "Check whether pkg is available or not." + (unless (featurep pkg) + (if (not (require pkg (symbol-name pkg) t)) + (message "lean-mode: optional package '%s' is not found." (symbol-name pkg)) + (message "lean-mode: optional package %S loaded." pkg)))) + +(defun lean-mode-check-requirements () + "Check lean-mode requirements" + (if (not (>= emacs-major-version 24)) + (error "Emacs version >= 24 is required to use lean-mode")) + (lean-mode-check-package 'package) + (lean-mode-check-package 'dash) + (let ((required-packages '(cl-lib dash dash-functional flymake compile s)) + (optional-packages '(flycheck whitespace-cleanup-mode fill-column-indicator + lua-mode mmm-mode))) + (-each required-packages 'lean-mode-require-package) + (-each optional-packages 'lean-mode-check-package))) + +(lean-mode-check-requirements) +(provide 'lean-require)