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

feat(emacs): define lean-mode as a derived-mode of prog-mode

Browse source 
Fix #52
This commit is contained in:
Soonho Kong 2014-08-18 13:32:58 -07:00
parent 5fa2b9c057
commit 46013b6ad2
2 changed files with 132 additions and 55 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -15,6 +15,7 @@
(require 'lean-input)
(require 'lean-type)
(require 'lean-tags)
(require 'lean-syntax)
(defun lean-compile-string (exe-name args file-name)
"Concatenate exe-name, args, and file-name"
@ -53,63 +54,51 @@
(local-set-key "\M-." 'lean-find-tag)
(local-set-key [tab] 'lean-complete-tag))
(define-abbrev-table 'lean-mode-abbrev-table '(
("var" "variable")
(define-abbrev-table 'lean-abbrev-table
'(("var" "variable")
("vars" "variables")
("def" "definition")
("th" "theorem")))
(define-generic-mode
'lean-mode ;; name of the mode to create
'("--") ;; comments start with
'("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "renaming" "inline" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "private" "using" "namespace" "builtin" "including" "instance" "section" "set_option" "add_rewrite" "extends") ;; some keywords
'(("\\_<\\(bool\\|int\\|nat\\|real\\|Prop\\|Type\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face)
("\\_<\\(calc\\|have\\|obtains\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
("\"[^\"]*\"" . 'font-lock-string-face)
("\\(->\\|↔\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-]\\)" . 'font-lock-constant-face)
("\\(λ\\|→\\|∃\\|∀\\|:\\|:=\\)" . font-lock-constant-face)
("\\_<\\(\\b.*_tac\\|Cond\\|or_else\\|t\\(?:hen\\|ry\\)\\|when\\|assumption\\|apply\\|b\\(?:ack\\|eta\\)\\|done\\|exact\\)\\_>" . 'font-lock-constant-face)
("\\_<\\(universe\\|inductive\\|theorem\\|axiom\\|lemma\\|hypothesis\\|abbreviation\\|definition\\|variable\\|parameter\\)\\_>[ \t\{\[]*\\([^ \t\n]*\\)" (2 'font-lock-function-name-face))
("\\_<\\(variables\\|parameters\\)\\_>[ \t\(\{\[]*\\([^:]*\\)" (2 'font-lock-function-name-face))
("\\(set_opaque\\|set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face))
("\\_<_\\_>" . 'font-lock-preprocessor-face)
("\\_<sorry\\_>" . 'font-lock-warning-face)
;;
)
'("\\.lean$") ;; files for which to activate this mode
'((lambda()
(set-input-method "Lean")
(set (make-local-variable 'lisp-indent-function)
'common-lisp-indent-function)
(lean-set-keys)
(setq local-abbrev-table lean-mode-abbrev-table)
(abbrev-mode 1)
(add-hook 'before-change-functions '
lean-before-change-function nil t)
(add-hook 'after-change-functions '
lean-after-change-function nil t)
;; Draw a vertical line for rule-column
(when (and lean-rule-column
lean-show-rule-column-method)
(cl-case lean-show-rule-column-method
('vline (require 'fill-column-indicator)
(setq fci-rule-column lean-rule-column)
(setq fci-rule-color lean-rule-color)
(add-hook 'lean-mode-hook 'fci-mode nil t))))
;; Delete Trailing Whitespace
(if lean-delete-trailing-whitespace
(progn (require 'whitespace-cleanup-mode)
(add-hook 'lean-mode-hook 'whitespace-cleanup-mode nil t))
(remove-hook 'lean-mode-hook 'whitespace-cleanup-mode))
;; eldoc
(set (make-local-variable 'eldoc-documentation-function)
'lean-eldoc-documentation-function)
(eldoc-mode +1)
))
"A mode for Lean files" ;; doc string for this mode
)
;; Automode List
;;;###autoload
(define-derived-mode lean-mode prog-mode "Lean"
"Major mode for Lean"
:syntax-table lean-syntax-table
:abbrev-table lean-abbrev-table
:group 'lean
(set (make-local-variable 'comment-start) "--")
(set (make-local-variable 'font-lock-defaults) lean-font-lock-defaults)
(set (make-local-variable 'indent-tabs-mode) nil)
(set-input-method "Lean")
(set (make-local-variable 'lisp-indent-function)
'common-lisp-indent-function)
(lean-set-keys)
(abbrev-mode 1)
(add-hook 'before-change-functions 'lean-before-change-function nil t)
(add-hook 'after-change-functions 'lean-after-change-function nil t)
;; Draw a vertical line for rule-column
(when (and lean-rule-column
lean-show-rule-column-method)
(cl-case lean-show-rule-column-method
('vline (require 'fill-column-indicator)
(setq fci-rule-column lean-rule-column)
(setq fci-rule-color lean-rule-color)
(add-hook 'lean-mode-hook 'fci-mode nil t))))
;; Delete Trailing Whitespace
(if lean-delete-trailing-whitespace
(progn (require 'whitespace-cleanup-mode)
(add-hook 'lean-mode-hook 'whitespace-cleanup-mode nil t))
(remove-hook 'lean-mode-hook 'whitespace-cleanup-mode))
;; eldoc
(set (make-local-variable 'eldoc-documentation-function)
'lean-eldoc-documentation-function))
;; Automatically use lean-mode for .lean files.
;;;###autoload
(push '("\\.lean$" . lean-mode) auto-mode-alist)
;; Use utf-8 encoding
;;;###autoload
(modify-coding-system-alist 'file "\\.lean\\'" 'utf-8)
(provide 'lean-mode)
; (regexp-opt '("Int" "Bool" "Nat" "Type" "Real") t)
; (regexp-opt '("let" "in" "have" "calc" "forall" "exists") t)
; (regexp-opt '("=" "->" "≠" "∨" "∧" "¬" "/\\" "\\/" "+" "-" "*" "/" "<" ">" "≤" "≥" "==" "∀" "∃" "→" "λ" ":") t)
; (regexp-opt '("apply" "exact" "trivial" "absurd" "beta" "apply" "unfold" "done" "back" "Try" "Then" "OrElse" "OrElse" "Cond" "When" "unfold_all" ) t)

88
src/emacs/lean-syntax.el Normal file
View file

@ -0,0 +1,88 @@
;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Leonardo de Moura
;; Soonho Kong
;;
(require 'rx)
(defconst lean-keywords
'("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "renaming"
"inline" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture"
"hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem"
"axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
"options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl"
"infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
"private" "using" "namespace" "builtin" "including" "instance" "section"
"set_option" "add_rewrite" "extends")
"lean keywords")
(defconst lean-syntax-table
(let ((st (make-syntax-table (standard-syntax-table))))
;; Matching parens
(modify-syntax-entry ?\( "()" st)
(modify-syntax-entry ?\) ")(" st)
(modify-syntax-entry ?\[ "(]" st)
(modify-syntax-entry ?\] ")[" st)
;; Matching {}, but with nested comments
(modify-syntax-entry ?\{ "(} 1bn" st)
(modify-syntax-entry ?\} "){ 4bn" st)
(modify-syntax-entry ?\- "_ 123" st)
(modify-syntax-entry ?\n ">" st)
;; ' and _ can be names
(modify-syntax-entry ?' "w" st)
(modify-syntax-entry ?_ "w" st)
;; Lean operator chars
(mapc #'(lambda (ch) (modify-syntax-entry ch "_" st))
"!#$%&*+./<=>@^|~:")
;; Whitespace is whitespace
(modify-syntax-entry ?\ " " st)
(modify-syntax-entry ?\t " " st)
;; ;; Strings
(modify-syntax-entry ?\" "\"" st)
(modify-syntax-entry ?\\ "/" st)
st))
(defconst lean-font-lock-defaults
`((;; Comments
(,(rx (group "--") (group (0+ ".")))
(1 font-lock-comment-delimiter-face)
(2 font-lock-comment-face))
;; Types
(,(rx symbol-start (or "bool" "int" "nat" "real" "Prop" "Type" "ℕ" "ℤ") symbol-end) . 'font-lock-type-face)
;; Keywords
(,(rx symbol-start (or "calc" "have" "obtains" "show" "by" "in" "let" "forall" "fun"
"exists" "if" "then" "else" "assume" "take" "obtain" "from") symbol-end)
. font-lock-keyword-face)
;; String
("\"[^\"]*\"" . 'font-lock-string-face)
;; Constants
(,(rx (or "->" "↔" "/" "==" "\/" "[*+/<=>¬∧∨≠≤≥-]")) . 'font-lock-constant-face)
(,(rx (or "λ" "→" "∃" "∀" ":" ":=")) . 'font-lock-constant-face )
(,(rx symbol-start
(or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact")
symbol-end)
. 'font-lock-constant-face)
;; universe/inductive/theorem... "names"
(,(rx symbol-start
(group (or "universe" "inductive" "theorem" "axiom" "lemma" "hypothesis"
"abbreviation" "definition" "variable" "parameter"))
symbol-end
(zero-or-more (or whitespace "{" "["))
(group (zero-or-more (not whitespace))))
(2 'font-lock-function-name-face))
("\\(set_opaque\\|set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face))
;; place holder
(,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
;; sorry
(,(rx symbol-start "sorry" symbol-end) . 'font-lock-warning-face)
;; lean-keywords
(, (concat "\\(" (regexp-opt lean-keywords 'words) "\\)")
(1 'font-lock-keyword-face)))))
(provide 'lean-syntax)