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

feat(emacs/lean): add multi-line comments

Browse source 
This is related with issue #63.

There are two known issues:

 - Emacs behaves as if the multi-line comment start/end symols are "(-"
   and "-)" instead of "(--" and "--)". As a result, it shows all the
   correct lean comments as it is. However, it will show some examples
   such as "(-5)" as a part of comment even if Lean doesn't interpret it
   as it is. Technically, it's because we are using a syntax-table based
   method to define comments. For more information read a documentation
   of 'modify-syntax-entry' function.

 - Somehow, the matching parens are broken. When we type "--)" to close
   a multi-line comment. Emacs warns "Mismatched Parentheses".
This commit is contained in:
Soonho Kong 2014-08-19 10:24:19 -07:00
parent c27a379f28
commit 51b86b219b
2 changed files with 17 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -68,6 +68,9 @@
:abbrev-table lean-abbrev-table
:group 'lean
(set (make-local-variable 'comment-start) "--")
(set (make-local-variable 'comment-end) "")
(set (make-local-variable 'comment-padding) 1)
(set (make-local-variable 'comment-use-syntax) t)
(set (make-local-variable 'font-lock-defaults) lean-font-lock-defaults)
(set (make-local-variable 'indent-tabs-mode) nil)
(set-input-method "Lean")

33
src/emacs/lean-syntax.el
View file

@ -19,17 +19,16 @@
"lean keywords")
(defconst lean-syntax-table
(let ((st (make-syntax-table (standard-syntax-table))))
(let ((st (make-syntax-table)))
;; Matching parens
(modify-syntax-entry ?\( "()" st)
(modify-syntax-entry ?\) ")(" st)
(modify-syntax-entry ?\[ "(]" st)
(modify-syntax-entry ?\] ")[" st)
(modify-syntax-entry ?\{ "(}" st)
(modify-syntax-entry ?\} "){" st)
(modify-syntax-entry ?\( "() 1nb" st)
(modify-syntax-entry ?\) ")( 4nb" st)
;; Matching {}, but with nested comments
(modify-syntax-entry ?\{ "(} 1bn" st)
(modify-syntax-entry ?\} "){ 4bn" st)
(modify-syntax-entry ?\- "_ 123" st)
(modify-syntax-entry ?- "_ 123" st)
(modify-syntax-entry ?\n ">" st)
;; ' and _ can be names
@ -44,17 +43,13 @@
(modify-syntax-entry ?\ " " st)
(modify-syntax-entry ?\t " " st)
;; ;; Strings
;; 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
`((;; 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"
@ -71,12 +66,12 @@
. '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))
(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)