Commit graph

103 commits

Author SHA1 Message Date
Soonho Kong
87c236613a feat(emacs/lean-mode.el): add configuration menu-item for flycheck
close #451
2015-03-05 14:42:59 -05:00
Soonho Kong
b7c852a5c8 feat(src/lean-mode.el): add 'configuration' menu and add toggle option for 'Show type at point'
close #456
2015-03-05 14:37:44 -05:00
Soonho Kong
46d99c8077 chore(emacs): move lean-choose-minor-mode-based-on-extension to lean-util.el 2015-02-13 19:41:41 -05:00
Soonho Kong
dcee8ddb1f feat(emacs/lean-mode): add Standard/HoTT minor modes for lean-mode 2015-02-13 19:41:41 -05:00
Leonardo de Moura
a57251913a feat(emacs): assume lua-mode and mmm-mode are available 2015-01-30 13:05:30 -08:00
Leonardo de Moura
71e1555eb4 feat(emacs): use lean-mode for .hlean 2014-12-05 14:33:22 -08:00
Leonardo de Moura
0f854f592c fix(emacs): disable abbreviation mode that was expanding "def" into "definition" 2014-12-03 17:24:29 -08:00
Leonardo de Moura
4bee7554a3 chore(lean-mode): remove 'annoying' abbreviations 2014-11-26 14:50:26 -08:00
Soonho Kong
d25e74b921 fix(emacs/lean-mode): remove whitespace-cleanup-mode dependency
- When customization variable 'lean-delete-trailing-whitespace' is
   non-nil, trailing-whitespaces are removed before save.

 - It doesn't change TABs.

Close #226
2014-11-09 00:21:43 -05:00
Soonho Kong
18a41eb962 feat(emacs/lean-mode): bind "C-c C-k" to quail-show-key
- Use this to see how to type a unicode character
2014-11-07 17:28:21 -05:00
Soonho Kong
e71db7109d fix(emacs/lean-mode.el): remove quotation marks in lean-execute
Close #294
2014-11-05 09:20:14 -05:00
Leonardo de Moura
c6c090eda6 feat(src/emacs/lean-mode): add shortcut for restarting lean server 2014-11-04 18:01:20 -08:00
Soonho Kong
2273f75e9b fix(emacs/lean-mode): handle when there is spaces in filenames 2014-11-04 19:22:35 -05:00
Soonho Kong
cae543e665 chore(emacs): remove unnecessary requires 2014-10-31 16:01:10 -07:00
Soonho Kong
b7d805a145 feat(emacs/lean-settings): add 'lean-follow-changes' option 2014-10-29 23:58:50 -07:00
Soonho Kong
17455d191b feat(emacs/lean-mode): add lean-info-mode for "*lean-info*" buffer 2014-10-29 14:33:05 -07:00
Soonho Kong
343a9a690e feat(emacs/lean-type): add lean-show-type-add-to-kill-ring option
If a customization option 'lean-show-type-add-to-kill-ring' is non-nil
and a user runs 'lean-show-type' by explicitly typing 'C-c C-t',
lean-mode saves the displayed type information message into kill-ring
, which can be pasted by yank (C-y) command.

Close #245
2014-10-14 09:27:25 -07:00
Leonardo de Moura
dc0e6861b7 fix(emacs/lean-mode): wrong pp highlighting, fixes #225 2014-10-07 02:32:59 -07:00
Soonho Kong
b78043ae24 feat(emacs/lean-mode): add 'clean-cache' to the menu
Related issue: #75
2014-10-03 10:11:21 -07:00
Soonho Kong
6c2e576dff fix(emacs/lean-mode): trigger eri-indent only at the beginning of line 2014-09-29 12:53:22 -07:00
Soonho Kong
11ff7b5d33 feat(lean-mode): enable mmm-parse-when-idle
Related issue: #74
2014-09-15 10:23:38 -07:00
Soonho Kong
f94e28ce39 fix(emacs/lean-mode): disable flycheck-lua inside of lean-mode
Related issue: #74
2014-09-15 10:23:31 -07:00
Soonho Kong
4bbfe4ec79 feat(emacs/lean-tags): add lean-global-search
close #170
2014-09-15 09:48:33 -07:00
Soonho Kong
ff6862f587 fix(emacs/lean-mode): pass lean-options to lean-execute
Related issue: #196
2014-09-15 09:48:26 -07:00
Soonho Kong
1527efb108 fix(emacs/lean-mode): run company-lean--check-prefix before auto-complete
fix #191
2014-09-14 23:15:24 -07:00
Soonho Kong
2d29d6d319 feat(emacs/lean-company): auto-completion for import
Close #126
2014-09-14 00:00:25 -07:00
Soonho Kong
563cfa73ec feat(emacs/lean-changes): handle before/after-revert 2014-09-12 14:25:08 -07:00
Soonho Kong
1c5497e632 feat(emacs/lean-project): add lean-project-create to imenu
Related with #170
2014-09-10 15:19:11 -07:00
Soonho Kong
b05ca1db0f fix(emacs/lean-tags): handle exceptions from find-tag 2014-09-10 14:14:42 -07:00
Soonho Kong
7c4debd1d1 feat(emacs/lean-server): handle modified buffer when send VISIT cmd
Close #159
2014-09-10 14:14:42 -07:00
Soonho Kong
60d14b50ab feat(emacs/lean-require): check lean-mode dependencies in initialization
Close #91
2014-09-09 15:11:57 -07:00
Soonho Kong
961dccf279 feat(emacs/Cask): add Cask file
Close #92
2014-09-09 15:11:57 -07:00
Soonho Kong
b460c02017 feat(emacs/lean-mode): add imenu support
Close #97
2014-09-09 09:04:31 -07:00
Soonho Kong
3682ca32d2 feat(emacs/lean-company): call FINDG if cursor is at "_" 2014-09-08 16:04:20 -07:00
Soonho Kong
50f16ad591 feat(emacs/lean-flycheck): delete flycheck temporaries after check
Close #140
2014-09-05 16:09:45 -07:00
Soonho Kong
cc89cd051a feat(emacs/lean-company): add lean-company 2014-09-04 16:32:07 -07:00
Soonho Kong
53390faebc chore(emacs/lean-mode): remove lean-tab function 2014-09-03 00:50:31 -07:00
Soonho Kong
b05aeb112b fix(emacs/lean-mode): Bind TAB with lean-tab-indent-or-compliete 2014-09-02 17:02:35 -04:00
Soonho Kong
cec2f8e466 feat(emacs/lean-mmm-lua.el): add mmm-mode to syntax-highlight lua code
in lean-mode

Close #74
2014-09-02 10:37:03 -07:00
Soonho Kong
50465a2d06 feat(emacs/lean-option): provide candidates and validation for lean-set-option
Close #106
2014-09-01 18:31:12 -07:00
Soonho Kong
fc2cbbe216 chore(emacs/lean-mode): add package info 2014-09-01 18:28:15 -07:00
Soonho Kong
26d548a069 feat(emacs/lean-mode): add lean-tab-indent-or-complete
Close #105
2014-08-30 14:57:34 -07:00
Soonho Kong
543fdf840e fix(emacs/lean-mode): add comment-start "--"
fix #113
2014-08-29 20:12:22 -07:00
Soonho Kong
1de515f693 feat(emacs/lean-mode): clean up old generic-mode 2014-08-26 17:16:16 -07:00
Soonho Kong
682b13a906 feat(emacs/lean-mode): run eldoc-documentation-function at openning 2014-08-26 16:22:32 -07:00
Soonho Kong
1f0bfb67b0 feat(emacs/lean-tags): use full-name to look up tags 2014-08-26 16:22:32 -07:00
Soonho Kong
3d3669e45e feat(emacs/lean-mode): add key-bindings, deps 2014-08-26 16:22:32 -07:00
Soonho Kong
679a034277 feat(emacs/lean-mode): use define-derived-mode 2014-08-26 16:22:31 -07:00
Leonardo de Moura
2f699fa53a feat(*): make sections 'permanent', and add 'transient' contexts, closes #88
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 15:45:15 -07:00
Soonho Kong
f4dfec548d fix(emacs/lean-mode): add missing flycheck-init 2014-08-21 10:05:14 -07:00