2014-08-07 15:00:22 +00:00
|
|
|
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
|
|
;; Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
;;
|
|
|
|
;; Author: Soonho Kong
|
|
|
|
;;
|
|
|
|
|
2014-08-07 17:40:20 +00:00
|
|
|
(require 'cl-lib)
|
|
|
|
|
2014-08-07 15:00:22 +00:00
|
|
|
(defgroup lean nil "Lean mode" :prefix 'lean :group 'languages)
|
|
|
|
|
2014-08-14 00:02:49 +00:00
|
|
|
(defvar-local lean-default-executable-name
|
2014-08-07 17:40:20 +00:00
|
|
|
(cl-case system-type
|
2014-08-07 15:00:22 +00:00
|
|
|
('gnu "lean")
|
|
|
|
('gnu/linux "lean")
|
|
|
|
('gnu/kfreebsd "lean")
|
|
|
|
('darwin "lean")
|
|
|
|
('ms-dos "lean")
|
|
|
|
('windows-nt "lean.exe")
|
|
|
|
('cygwin "lean.exe") ;; TODO(soonhok): check this
|
|
|
|
)
|
2014-08-07 17:40:20 +00:00
|
|
|
"Default executable name of Lean")
|
2014-08-07 15:00:22 +00:00
|
|
|
|
|
|
|
(defcustom lean-rootdir nil
|
|
|
|
"Full pathname of lean root directory. It should be defined by user."
|
|
|
|
:group 'lean
|
2014-08-07 17:40:20 +00:00
|
|
|
:type 'string)
|
2014-08-07 15:00:22 +00:00
|
|
|
|
|
|
|
(defcustom lean-executable-name lean-default-executable-name
|
|
|
|
"Name of lean executable"
|
|
|
|
:group 'lean
|
2014-08-07 17:40:20 +00:00
|
|
|
:type 'string)
|
2014-08-07 15:00:22 +00:00
|
|
|
|
2014-08-07 20:48:08 +00:00
|
|
|
(defcustom lean-flycheck-use t
|
2014-08-07 18:59:03 +00:00
|
|
|
"Use flycheck for lean."
|
|
|
|
:group 'lean
|
|
|
|
:type 'boolean)
|
|
|
|
|
2014-08-18 23:10:07 +00:00
|
|
|
(defcustom lean-company-use t
|
|
|
|
"Use company mode for lean."
|
|
|
|
:group 'lean
|
|
|
|
:type 'boolean)
|
|
|
|
|
2014-08-13 22:06:22 +00:00
|
|
|
(defcustom lean-flycheck-checker-name "lmake"
|
|
|
|
"lean-flychecker checker name"
|
|
|
|
:group 'lean
|
|
|
|
:type 'string)
|
|
|
|
|
2014-08-14 22:04:50 +00:00
|
|
|
(defcustom lean-flycheck-checker-options '("--jobs" "--keep-going" "--permissive" "--flycheck")
|
2014-08-13 22:06:22 +00:00
|
|
|
"lean-flychecker checker option"
|
|
|
|
:group 'lean)
|
|
|
|
|
2014-08-07 15:00:22 +00:00
|
|
|
(defcustom lean-delete-trailing-whitespace nil
|
|
|
|
"Set this variable to true to automatically delete trailing
|
|
|
|
whitespace when a buffer is loaded from a file or when it is
|
|
|
|
written."
|
|
|
|
:group 'lean
|
|
|
|
:type 'boolean)
|
|
|
|
|
|
|
|
(defcustom lean-rule-column 100
|
|
|
|
"Specify rule-column."
|
|
|
|
:group 'lean
|
|
|
|
:type '(choice (integer :tag "Columns")
|
|
|
|
(const :tag "Unlimited" nil))
|
|
|
|
:type 'int)
|
|
|
|
|
2014-08-07 18:57:46 +00:00
|
|
|
(defcustom lean-rule-color "#cccccc"
|
|
|
|
"Color used to draw the fill-column rule"
|
|
|
|
:group 'fill-column-indicator
|
|
|
|
:tag "Fill-column rule color"
|
|
|
|
:type 'color)
|
|
|
|
|
2014-08-07 15:00:22 +00:00
|
|
|
(defcustom lean-show-rule-column-method nil
|
|
|
|
"If enabled, it highlights column"
|
|
|
|
:group 'lean
|
|
|
|
:type '(choice (const :tag "Disabled" nil)
|
|
|
|
(const :tag "Vertical Line" vline)
|
|
|
|
;;(const :tag "Whole Lines" lines)
|
|
|
|
;;(const :tag "Only Beyond lean-rule-column" lines-tail)
|
|
|
|
))
|
|
|
|
|
|
|
|
(provide 'lean-settings)
|