max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(lean-mode): embed for the time being

Browse source
This commit is contained in:
Sebastian Ullrich 2018-09-07 09:55:57 -07:00
parent b3c44ec56e
commit 7d5a52299e
17 changed files with 3112 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lean-mode/.gitignore vendored Normal file
View file

@ -0,0 +1,2 @@
.cask
*.elc

201
lean-mode/LICENSE Normal file
View file

@ -0,0 +1,201 @@
Apache License
Version 2.0, January 2004
http://www.apache.org/licenses/
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
1. Definitions.
"License" shall mean the terms and conditions for use, reproduction,
and distribution as defined by Sections 1 through 9 of this document.
"Licensor" shall mean the copyright owner or entity authorized by
the copyright owner that is granting the License.
"Legal Entity" shall mean the union of the acting entity and all
other entities that control, are controlled by, or are under common
control with that entity. For the purposes of this definition,
"control" means (i) the power, direct or indirect, to cause the
direction or management of such entity, whether by contract or
otherwise, or (ii) ownership of fifty percent (50%) or more of the
outstanding shares, or (iii) beneficial ownership of such entity.
"You" (or "Your") shall mean an individual or Legal Entity
exercising permissions granted by this License.
"Source" form shall mean the preferred form for making modifications,
including but not limited to software source code, documentation
source, and configuration files.
"Object" form shall mean any form resulting from mechanical
transformation or translation of a Source form, including but
not limited to compiled object code, generated documentation,
and conversions to other media types.
"Work" shall mean the work of authorship, whether in Source or
Object form, made available under the License, as indicated by a
copyright notice that is included in or attached to the work
(an example is provided in the Appendix below).
"Derivative Works" shall mean any work, whether in Source or Object
form, that is based on (or derived from) the Work and for which the
editorial revisions, annotations, elaborations, or other modifications
represent, as a whole, an original work of authorship. For the purposes
of this License, Derivative Works shall not include works that remain
separable from, or merely link (or bind by name) to the interfaces of,
the Work and Derivative Works thereof.
"Contribution" shall mean any work of authorship, including
the original version of the Work and any modifications or additions
to that Work or Derivative Works thereof, that is intentionally
submitted to Licensor for inclusion in the Work by the copyright owner
or by an individual or Legal Entity authorized to submit on behalf of
the copyright owner. For the purposes of this definition, "submitted"
means any form of electronic, verbal, or written communication sent
to the Licensor or its representatives, including but not limited to
communication on electronic mailing lists, source code control systems,
and issue tracking systems that are managed by, or on behalf of, the
Licensor for the purpose of discussing and improving the Work, but
excluding communication that is conspicuously marked or otherwise
designated in writing by the copyright owner as "Not a Contribution."
"Contributor" shall mean Licensor and any individual or Legal Entity
on behalf of whom a Contribution has been received by Licensor and
subsequently incorporated within the Work.
2. Grant of Copyright License. Subject to the terms and conditions of
this License, each Contributor hereby grants to You a perpetual,
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
copyright license to reproduce, prepare Derivative Works of,
publicly display, publicly perform, sublicense, and distribute the
Work and such Derivative Works in Source or Object form.
3. Grant of Patent License. Subject to the terms and conditions of
this License, each Contributor hereby grants to You a perpetual,
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
(except as stated in this section) patent license to make, have made,
use, offer to sell, sell, import, and otherwise transfer the Work,
where such license applies only to those patent claims licensable
by such Contributor that are necessarily infringed by their
Contribution(s) alone or by combination of their Contribution(s)
with the Work to which such Contribution(s) was submitted. If You
institute patent litigation against any entity (including a
cross-claim or counterclaim in a lawsuit) alleging that the Work
or a Contribution incorporated within the Work constitutes direct
or contributory patent infringement, then any patent licenses
granted to You under this License for that Work shall terminate
as of the date such litigation is filed.
4. Redistribution. You may reproduce and distribute copies of the
Work or Derivative Works thereof in any medium, with or without
modifications, and in Source or Object form, provided that You
meet the following conditions:
(a) You must give any other recipients of the Work or
Derivative Works a copy of this License; and
(b) You must cause any modified files to carry prominent notices
stating that You changed the files; and
(c) You must retain, in the Source form of any Derivative Works
that You distribute, all copyright, patent, trademark, and
attribution notices from the Source form of the Work,
excluding those notices that do not pertain to any part of
the Derivative Works; and
(d) If the Work includes a "NOTICE" text file as part of its
distribution, then any Derivative Works that You distribute must
include a readable copy of the attribution notices contained
within such NOTICE file, excluding those notices that do not
pertain to any part of the Derivative Works, in at least one
of the following places: within a NOTICE text file distributed
as part of the Derivative Works; within the Source form or
documentation, if provided along with the Derivative Works; or,
within a display generated by the Derivative Works, if and
wherever such third-party notices normally appear. The contents
of the NOTICE file are for informational purposes only and
do not modify the License. You may add Your own attribution
notices within Derivative Works that You distribute, alongside
or as an addendum to the NOTICE text from the Work, provided
that such additional attribution notices cannot be construed
as modifying the License.
You may add Your own copyright statement to Your modifications and
may provide additional or different license terms and conditions
for use, reproduction, or distribution of Your modifications, or
for any such Derivative Works as a whole, provided Your use,
reproduction, and distribution of the Work otherwise complies with
the conditions stated in this License.
5. Submission of Contributions. Unless You explicitly state otherwise,
any Contribution intentionally submitted for inclusion in the Work
by You to the Licensor shall be under the terms and conditions of
this License, without any additional terms or conditions.
Notwithstanding the above, nothing herein shall supersede or modify
the terms of any separate license agreement you may have executed
with Licensor regarding such Contributions.
6. Trademarks. This License does not grant permission to use the trade
names, trademarks, service marks, or product names of the Licensor,
except as required for reasonable and customary use in describing the
origin of the Work and reproducing the content of the NOTICE file.
7. Disclaimer of Warranty. Unless required by applicable law or
agreed to in writing, Licensor provides the Work (and each
Contributor provides its Contributions) on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
implied, including, without limitation, any warranties or conditions
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
PARTICULAR PURPOSE. You are solely responsible for determining the
appropriateness of using or redistributing the Work and assume any
risks associated with Your exercise of permissions under this License.
8. Limitation of Liability. In no event and under no legal theory,
whether in tort (including negligence), contract, or otherwise,
unless required by applicable law (such as deliberate and grossly
negligent acts) or agreed to in writing, shall any Contributor be
liable to You for damages, including any direct, indirect, special,
incidental, or consequential damages of any character arising as a
result of this License or out of the use or inability to use the
Work (including but not limited to damages for loss of goodwill,
work stoppage, computer failure or malfunction, or any and all
other commercial damages or losses), even if such Contributor
has been advised of the possibility of such damages.
9. Accepting Warranty or Additional Liability. While redistributing
the Work or Derivative Works thereof, You may choose to offer,
and charge a fee for, acceptance of support, warranty, indemnity,
or other liability obligations and/or rights consistent with this
License. However, in accepting such obligations, You may act only
on Your own behalf and on Your sole responsibility, not on behalf
of any other Contributor, and only if You agree to indemnify,
defend, and hold each Contributor harmless for any liability
incurred by, or claims asserted against, such Contributor by reason
of your accepting any such warranty or additional liability.
END OF TERMS AND CONDITIONS
APPENDIX: How to apply the Apache License to your work.
To apply the Apache License to your work, attach the following
boilerplate notice, with the fields enclosed by brackets "{}"
replaced with your own identifying information. (Don't include
the brackets!) The text should be enclosed in the appropriate
comment syntax for the file format. We also recommend that a
file or class name and description of purpose be included on the
same "printed page" as the copyright notice for easier
identification within third-party archives.
Copyright {yyyy} {name of copyright owner}
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.

120
lean-mode/README.md Normal file
View file

@ -0,0 +1,120 @@
This is the Emacs mode for the [Lean theorem prover][lean].
[lean]: https://github.com/leanprover/lean
Installation
============
`lean-mode` requires GNU Emacs 24.3 or newer. The recommended way to install it is via [MELPA](https://melpa.org). If you have not already configured MELPA, put the following code in your Emacs init file (typically `~/.emacs.d/init.el`):
```elisp
(require 'package) ; You might already have this line
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/"))
(package-initialize) ; You might already have this line
```
See also [MELPA: Getting Started](https://melpa.org/#/getting-started).
With MELPA configured, you can `M-x package-install` the packages `lean-mode` and `company-lean`. The latter package gives you auto completion and is strongly recommended. There is a third package, `helm-lean`, which provides a searchable list of declarations on `C-c C-d` using the Helm interface. `helm-lean` requires Emacs 24.4 or newer.
For `company-lean`, you should also bind a key to trigger completion, if you have not already done so:
```elisp
;; Trigger completion on Shift-Space
(global-set-key (kbd "S-SPC") #'company-complete)
```
Updating
--------
For updating the Lean MELPA packages, use `package-list-packages`. See the section "Updating Packages" on [MELPA: Getting Started](https://melpa.org/#/getting-started) for details.
Trying It Out
=============
If things are working correctly, you should see the word ``Lean`` in the
Emacs mode line when you open a file with extension `.lean`. If you type
```lean
#check id
```
the word ``#check`` will be underlined, and hovering over it will show
you the type of ``id``. The mode line will show ``FlyC:0/1``, indicating
that there are no errors and one piece of information displayed.
Key Bindings and Commands
=========================
| Key | Function |
|--------------------|---------------------------------------------------------------------------------|
| <kbd>M-.</kbd> | jump to definition in source file (`lean-find-definition`) |
| <kbd>M-,</kbd> | jump back to position before <kbd>M-.</kbd> (`xref-pop-marker-stack`) |
| <kbd>C-c C-k</kbd> | shows the keystroke needed to input the symbol under the cursor |
| <kbd>C-c C-x</kbd> | execute lean in stand-alone mode (`lean-std-exe`) |
| <kbd>C-c SPC</kbd> | run a command on the hole at point (`lean-hole`) |
| <kbd>C-c C-d</kbd> | show a searchable list of definitions (`helm-lean-definitions`) |
| <kbd>C-c C-g</kbd> | toggle showing current tactic proof goal (`lean-toggle-show-goal`) |
| <kbd>C-c C-n</kbd> | toggle showing next error in dedicated buffer (`lean-toggle-next-error`) |
| <kbd>C-c C-b</kbd> | toggle showing output in inline boxes (`lean-message-boxes-toggle`) |
| <kbd>C-c C-r</kbd> | restart the lean server (`lean-server-restart`) |
| <kbd>C-c C-s</kbd> | switch to a different Lean version via [elan](https://github.com/Kha/elan) (`lean-server-switch-version`) |
| <kbd>C-c ! n</kbd> | flycheck: go to next error |
| <kbd>C-c ! p</kbd> | flycheck: go to previous error |
| <kbd>C-c ! l</kbd> | flycheck: show list of errors |
In the default configuration, the Flycheck annotation `FlyC:n/n` indicates the
number of errors / responses from Lean; clicking on `FlyC` opens the Flycheck menu.
Message Boxes
================
To view the output of commands such as `check` and `print` in boxes in the buffer, enable the feature using <kbd>C-c C-b</kbd>.
If you then type
```lean
#check id
```
a box appears after the line showing the type of `id`. Customize `lean-message-boxes-enabled-captions` to choose categories of boxes.
In particular, add `"trace output"` to the list to see proof states and other traces in the buffer.
Known Issues and Possible Solutions
===================================
Unicode
-------
If you experience a problem rendering unicode symbols on emacs,
please download the following fonts and install them on your machine:
- [Quivira.ttf](http://www.quivira-font.com/files/Quivira.ttf)
- [Dejavu Fonts](http://sourceforge.net/projects/dejavu/files/dejavu/2.35/dejavu-fonts-ttf-2.35.tar.bz2)
- [NotoSans](https://github.com/googlei18n/noto-fonts/blob/master/hinted/NotoSans-Regular.ttc?raw=true)
- [NotoSansSymbols](https://github.com/googlei18n/noto-fonts/blob/master/unhinted/NotoSansSymbols-Regular.ttf?raw=true)
Then, have the following lines in your emacs setup to use `DejaVu Sans Mono` font:
```elisp
(when (member "DejaVu Sans Mono" (font-family-list))
(set-face-attribute 'default nil :font "DejaVu Sans Mono-11"))
```
You may also need to install the [emacs-unicode-fonts](https://github.com/rolandwalker/unicode-fonts) package, after which you should add the following lines to your emacs setup:
```elisp
(require 'unicode-fonts)
(unicode-fonts-setup)
```
Contributions
=============
Contributions are welcome!
Building from Source
--------------------
When working on `lean-mode` itself, it is much easier to just `require` the sources than repeatedly building the MELPA packages:
```elisp
(add-to-load-path "~/path/to/lean-mode/")
(require 'company-lean)
(require 'helm-lean)
```
Make sure you have the packages' dependencies listed on MELPA installed -- the easiest way to do this may be to just install the official Lean MELPA packages and making sure the `require` commands above are execute before `package-initialize`.

47
lean-mode/lean-debug.el Normal file
View file

@ -0,0 +1,47 @@
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(require 'cl-lib)
(defvar lean-debug-mode nil)
(defvar lean-debug-buffer-name "*lean-debug*")
(defun lean-turn-on-debug-mode (&optional print-msg)
(interactive)
(when (or (called-interactively-p 'any) print-msg)
(message "lean: turn on debug mode"))
(get-buffer-create lean-debug-buffer-name)
(buffer-disable-undo lean-debug-buffer-name)
(display-buffer lean-debug-buffer-name 'display-buffer-reuse-window
'((reusable-frames . t)))
(setq lean-debug-mode t))
(defun lean-turn-off-debug-mode (&optional print-msg)
(interactive)
(when (eq major-mode 'lean-mode)
(when (or (called-interactively-p 'any) print-msg)
(message "lean: turn off debug mode"))
(setq lean-debug-mode nil)))
(defun lean-output-to-buffer (buffer-name format-string args)
(with-current-buffer
(get-buffer-create buffer-name)
(save-selected-window
(ignore-errors
(select-window (get-buffer-window buffer-name t)))
(goto-char (point-max))
(insert (apply 'format format-string args)))))
(defun lean-debug (format-string &rest args)
"Display a message at the bottom of the *lean-debug* buffer."
(when lean-debug-mode
(let ((time-str (format-time-string "%H:%M:%S.%3N" (current-time))))
(lean-output-to-buffer lean-debug-buffer-name
(concat "%s -- " format-string "\n")
(cons (propertize time-str 'face 'font-lock-keyword-face)
args)))))
(provide 'lean-debug)

19
lean-mode/lean-dev.el Normal file
View file

@ -0,0 +1,19 @@
;; -*- lexical-binding: t -*-
;;
;; Copyright (c) 2017 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Sebastian Ullrich
;;
(require 'f)
(require 'lean-util)
(defun lean-diff-test-file ()
"Use interactive ./test_input.sh on file of current buffer"
(interactive)
(message (shell-command-to-string (format "yes | ./test_single.sh \"%s\" \"%s\" yes"
(lean-get-executable "lean")
(f-filename (buffer-file-name))))))
(provide 'lean-dev)

208
lean-mode/lean-eri.el Normal file
View file

@ -0,0 +1,208 @@
;;; lean-eri.el --- Enhanced relative indentation (eri)
;;; Commentary:
;; Adapted from agda-mode (https://github.com/agda/agda/blob/master/src/data/emacs-mode/eri.el)
;;; Code:
(require 'cl)
(defun lean-eri-current-line-length nil
"Calculate length of current line."
(- (line-end-position) (line-beginning-position)))
(defun lean-eri-current-line-empty nil
"Return non-nil if the current line is empty (not counting white space)."
(equal (current-indentation)
(lean-eri-current-line-length)))
(defun lean-eri-maximum (xs)
"Calculate maximum element in XS.
Returns nil if the list is empty."
(if xs (apply 'max xs)))
(defun lean-eri-take (n xs)
"Return the first N elements of XS."
(butlast xs (- (length xs) n)))
(defun lean-eri-split (x xs)
"Return a pair of lists (XS1 . XS2).
If XS is sorted, then XS = (append XS1 XS2), and all elements in
XS1 are <= X, whereas all elements in XS2 are > X."
(let* ((pos (or (position-if (lambda (y) (> y x)) xs) (length xs)))
(xs1 (lean-eri-take pos xs))
(xs2 (nthcdr pos xs)))
(cons xs1 xs2)))
(defun lean-eri-calculate-indentation-points-on-line (max)
"Calculate indentation points on current line.
Only points left of column number MAX are included. If MAX is
nil, then all points are included. Points are returned in
ascending order.
Example (positions marked with ^ are returned):
f x y = g 3 (Just y) 5 4
^ ^ ^ ^ ^ ^ ^ ^ |
|
MAX"
(let ((result))
(save-excursion
(save-restriction
(beginning-of-line)
; To make \\` work in the regexp below:
(narrow-to-region (line-beginning-position) (line-end-position))
(while
(progn
(let ((pos (and (search-forward-regexp
"\\(?:\\s-\\|\\`\\)\\(\\S-\\)" nil t)
(match-beginning 1))))
(when (not (null pos))
(let ((pos1 (- pos (line-beginning-position))))
(when (or (null max) (< pos1 max))
(add-to-list 'result pos1))))
(and pos
(< (point) (line-end-position))
(or (null max) (< (current-column) max))))))
(nreverse result) ; Destructive operation.
))))
(defun lean-eri-new-indentation-points ()
"Calculate new indentation points.
Returns a singleton list containing the column number two steps
in from the indentation of the first non-empty line (white space
excluded) above the current line. If there is no such line,
then the empty list is returned."
(let ((start (line-beginning-position)))
(save-excursion
; Find a non-empty line above the current one, if any.
(while
(progn
(forward-line -1)
(not (or (bobp)
(not (lean-eri-current-line-empty))))))
(if (or (equal (point) start)
(lean-eri-current-line-empty))
nil
(list (+ 2 (current-indentation)))))))
(defun lean-eri-calculate-indentation-points (reverse)
"Calculate points used to indent the current line.
The points are given in reverse order if REVERSE is non-nil. See
`lean-eri-indent' for a description of how the indentation points are
calculated; note that the current indentation is not included in
the returned list."
;; First find a bunch of indentations used above the current line.
(let ((points)
(max)
(start (line-beginning-position)))
(save-excursion
(while
(progn
(forward-line -1)
; Skip the line we started from and lines with nothing but
; white space.
(unless (or (equal (point) start)
(lean-eri-current-line-empty))
(setq points
(append
(lean-eri-calculate-indentation-points-on-line max)
points))
(setq max (car points)))
;; Stop after hitting the beginning of the buffer or a
;; non-empty, non-indented line.
(not (or (bobp)
(and (equal (current-indentation) 0)
(> (lean-eri-current-line-length) 0)))))))
;; Add new indentation points, but remove the current indentation.
;; Sort the indentations. Rearrange the points so that the next
;; point is the one after the current one. Reverse if necessary.
;;
;; Note: sort and nreverse are destructive.
(let* ((ps0 (remove (current-indentation)
(append (lean-eri-new-indentation-points) points)))
(ps1 (lean-eri-split (current-indentation) (sort ps0 '<)))
(ps2 (append (cdr ps1) (car ps1))))
(if reverse
(nreverse ps2)
ps2))))
(defun lean-eri-indent (&optional reverse)
"Cycle between some possible indentation points.
With prefix argument REVERSE, cycle in reverse order.
Assume that a file contains the following lines of code, with
point on the line with three dots:
frob = loooooooooooooooooooooooooong identifier
foo = f a b
where
f (Foo x) y = let bar = x
baz = 3 + 5
...
^ ^ ^ ^ ^ ^ ^ ^ ^ * ^ ^ ^ ^
Then the ^'s and the * mark the indentation points that this
function cycles through. The indentation points are selected as
follows:
* All lines before the current one, up to and including the
first non-indented line (or the beginning of the buffer) are
considered.
foo = f a b
where
f (Foo x) y = let bar = x
baz = 3 + 5
* On these lines, erase all characters that stand to the right
of some non-white space character on a lower line.
foo
whe
f (Foo x) y = let b
baz = 3 + 5
* Also erase all characters not immediately preceded by white
space.
f
w
f ( x y = l b
b = 3 + 5
* The columns of all remaining characters are indentation
points.
f w f ( x y = l b = 3 + 5
^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^
* A new indentation point is also added, two steps in from the
indentation of the first non-empty line (white space
excluded) above the current line (if there is such a line).
f w f ( x y = l b = 3 + 5
^ ^ ^ ^ ^ ^ ^ ^ ^ * ^ ^ ^ ^"
(interactive "P")
(let* ((points (lean-eri-calculate-indentation-points reverse))
(remaining-points (cdr (member (current-indentation) points)))
(indentation (if remaining-points
(car remaining-points)
(car points))))
(when indentation
(save-excursion (indent-line-to indentation))
(if (< (current-column) indentation)
(indent-line-to indentation)))))
(defun lean-eri-indent-reverse nil
"Cycle between some possible indentation points (in reverse order).
See `lean-eri-indent' for a description of how the indentation points
are calculated."
(interactive)
(lean-eri-indent t))
(provide 'lean-eri)
;;; lean-eri.el ends here

122
lean-mode/lean-flycheck.el Normal file
View file

@ -0,0 +1,122 @@
;; -*- lexical-binding: t -*-
;;
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(require 'cl-lib)
(require 'flycheck)
(require 'lean-settings)
(require 'lean-server)
(require 'lean-info)
(defun lean-toggle-flycheck-mode ()
"Toggle flycheck-mode"
(interactive)
(cond
(flycheck-mode (flycheck-mode -1))
(t (flycheck-mode 1))))
(cl-defun lean-flycheck-parse-task (checker buffer cur-file-name
&key pos_line pos_col desc file_name &allow-other-keys)
(if (equal cur-file-name file_name)
(flycheck-error-new-at pos_line (1+ pos_col)
'info
(format "still running: %s" desc)
:filename file_name
:checker checker :buffer buffer)
(flycheck-error-new-at 1 1
'info
(format "still running: %s" desc)
:filename cur-file-name
:checker checker :buffer buffer)))
(defun lean-flycheck-mk-task-msgs (checker buffer sess)
(if (and sess (lean-server-session-tasks sess)
(plist-get (lean-server-session-tasks sess) :is_running))
(let* ((cur-fn (buffer-file-name))
(tasks (lean-server-session-tasks sess))
(cur-task (plist-get tasks :cur_task))
(tasks-for-cur-file (cl-remove-if-not (lambda (task) (equal cur-fn (plist-get task :file_name)))
(plist-get tasks :tasks)))
(display-tasks))
;; do not display tasks for current file when highlighting is enabled
(when (not lean-server-show-pending-tasks)
(setq display-tasks tasks-for-cur-file))
;; show current task when not in current file
(when (and cur-task
(not (equal cur-fn (plist-get cur-task :file_name))))
(setq display-tasks (cons cur-task display-tasks)))
(mapcar (lambda (task) (apply #'lean-flycheck-parse-task checker buffer cur-fn task))
display-tasks))))
(defun lean-info-fontify-string (str)
(lean-ensure-info-buffer "*lean-fontify*")
(with-current-buffer "*lean-fontify*"
(erase-buffer)
(insert str)
(font-lock-fontify-region (point-min) (point-max) nil)
(buffer-string)))
(cl-defun lean-flycheck-parse-error (checker buffer &key pos_line pos_col severity text file_name &allow-other-keys)
(flycheck-error-new-at pos_line (1+ pos_col)
(pcase severity
("error" 'error)
("warning" 'warning)
("information" 'info)
(_ 'info))
(lean-info-fontify-string text)
:filename file_name
:checker checker :buffer buffer))
(defun lean-flycheck-start (checker callback)
(let ((cur-fn (buffer-file-name))
(buffer (current-buffer)))
(funcall callback 'finished
(if lean-server-session
(append
(lean-flycheck-mk-task-msgs checker buffer lean-server-session)
(mapcar (lambda (msg) (apply #'lean-flycheck-parse-error checker buffer msg))
(cl-remove-if-not (lambda (msg) (equal cur-fn (plist-get msg :file_name)))
(lean-server-session-messages lean-server-session))))))))
(defun lean-flycheck-init ()
"Initialize lean-flychek checker"
(flycheck-define-generic-checker 'lean-checker
"A Lean syntax checker."
:start #'lean-flycheck-start
:modes '(lean-mode))
(add-to-list 'flycheck-checkers 'lean-checker))
(defun lean-flycheck-turn-on ()
(flycheck-mode t))
(defconst lean-next-error-buffer-name "*Lean Next Error*")
(defun lean-next-error--handler ()
(when (lean-info-buffer-active lean-next-error-buffer-name)
(let ((deactivate-mark) ; keep transient mark
(errors (or
;; prefer error of current position, if any
(flycheck-overlay-errors-at (point))
;; try errors in current line next
(sort (flycheck-overlay-errors-in (line-beginning-position) (line-end-position))
#'flycheck-error-<)
;; fall back to next error position
(-if-let* ((pos (flycheck-next-error-pos 1)))
(flycheck-overlay-errors-at pos)))))
(lean-with-info-output-to-buffer lean-next-error-buffer-name
(dolist (e errors)
(princ (format "%d:%d: " (flycheck-error-line e) (flycheck-error-column e)))
(princ (flycheck-error-message e))
(princ "\n\n"))
(when flycheck-current-errors
(princ (format "(%d more messages above...)" (length flycheck-current-errors))))))))
(defun lean-toggle-next-error ()
(interactive)
(lean-toggle-info-buffer lean-next-error-buffer-name)
(lean-next-error--handler))
(provide 'lean-flycheck)

151
lean-mode/lean-hole.el Normal file
View file

@ -0,0 +1,151 @@
;; -*- lexical-binding: t -*-
;;
;; Copyright (c) 2017 David Christiansen.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: David Christiansen
;;
;;; Commentary:
;; This is an interface to Lean's support for holes.
;;
;; The interface consists of two components: the hole command, which
;; collects the list of completions and the message, and a handler,
;; which selects a completion.
;;
;; For now, the only handler uses completing-read, but handlers using
;; helm or company's interface would be a good addition.
;;
;;; Code:
(require 'lean-server)
(defun lean-hole-handler-completing-read (alternatives)
"Pick a hole replacement from ALTERNATIVES with `completing-read'."
(let* ((choices (cl-loop for alt in alternatives
collect (cons (concat (plist-get alt :code)
" — "
(plist-get alt :description))
(plist-get alt :code))))
(selection (let ((this-command 'lean-hole))
(completing-read
"Response: "
choices
nil t nil nil nil t)))
(code (assoc selection choices)))
(if code
(cdr code)
(error "Didn't select a hole completion"))))
(defvar lean-hole-handler-function 'lean-hole-handler-completing-read)
(defun lean-hole--line-col->pos (line col)
"Compute the position corresponding to LINE and COL."
(save-restriction
(widen)
(save-excursion
(goto-char (point-min))
(forward-line (1- line))
(forward-char col)
(point))))
(defun lean-hole ()
"Ask Lean for a list of holes, then ask the user which to use."
(interactive)
(with-demoted-errors "lean hole: %s"
(lean-server-send-command
'hole_commands (list :file_name (buffer-file-name)
:line (line-number-at-pos)
:column (lean-line-offset))
(cl-function
(lambda (&key start end results)
(let ((start-pos (lean-hole--line-col->pos (plist-get start :line)
(plist-get start :column)))
(end-pos (lean-hole--line-col->pos (plist-get end :line)
(plist-get end :column))))
(let ((start-marker (make-marker))
(end-marker (make-marker)))
(set-marker start-marker start-pos (current-buffer))
(set-marker end-marker end-pos (current-buffer))
(let* ((choices
(cl-loop for res in results
collect (cons (concat (plist-get res :name)
" — "
(plist-get res :description))
(plist-get res :name))))
(selection (let ((this-command 'lean-hole))
(completing-read
"Hole command: "
choices
nil t nil nil nil t)))
(code (assoc selection choices)))
(if code
(lean-hole--command (cdr code) start-marker end-marker)
(error "Didn't select a hole completion"))))))))))
;; This uses markers to ensure that if the hole moves while the
;; command is running, it is still updated.
(defun lean-hole--command (command start-marker end-marker)
"Execute COMMAND in the hole between START-MARKER and END-MARKER."
(interactive)
(with-demoted-errors "lean hole: %s"
(lean-server-send-command
'hole (list :action command
:file_name (buffer-file-name)
:line (line-number-at-pos start-marker)
:column (lean-line-offset start-marker))
(cl-function
(lambda (&key message replacements)
(let ((replacement-count (length (plist-get replacements :alternatives))))
(let ((selected-code
(cond ((= replacement-count 0)
nil)
((= replacement-count 1)
(plist-get (car (plist-get replacements :alternatives)) :code))
(t
(lean-hole-handler-completing-read
(plist-get replacements :alternatives))))))
(when selected-code
(save-excursion
(goto-char start-marker)
(delete-region start-marker end-marker)
(insert selected-code)))))
(when message
(message "%s" (s-trim message)))
(set-marker start-marker nil)
(set-marker end-marker nil))))))
(defun lean-hole-right-click ()
"Ask Lean for a list of hole commands, then ask the user which to use."
(interactive)
(let ((buf (current-buffer)))
(ignore-errors
(list
'hole_commands
(list :file_name (buffer-file-name)
:line (line-number-at-pos)
:column (lean-line-offset))
(cl-function
(lambda (&key start end results)
(when (and start end)
(with-current-buffer buf
(let ((start-pos (lean-hole--line-col->pos (plist-get start :line)
(plist-get start :column)))
(end-pos (lean-hole--line-col->pos (plist-get end :line)
(plist-get end :column))))
(let ((start-marker (make-marker))
(end-marker (make-marker)))
(set-marker start-marker start-pos (current-buffer))
(set-marker end-marker (1+ end-pos) (current-buffer))
(mapcar (lambda (res)
(let ((item-name (plist-get res :name))
(item-desc (plist-get res :description)))
(list :name
(concat item-name " — " item-desc)
:action
(lambda ()
(lean-hole--command
item-name
start-marker end-marker)))))
results)))))))))))
(provide 'lean-hole)
;;; lean-hole.el ends here

114
lean-mode/lean-info.el Normal file
View file

@ -0,0 +1,114 @@
;; -*- lexical-binding: t -*-
;;
;;; lean-info.el --- Emacs mode for Lean theorem prover
;;
;; Copyright (c) 2016 Gabriel Ebner. All rights reserved.
;;
;; Author: Gabriel Ebner <gebner@gebner.org>
;; Maintainer: Gabriel Ebner <gebner@gebner.org>
;; Created: Oct 29, 2016
;; Keywords: languages
;; 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 'lean-syntax)
;; Lean Info Mode (for "*lean-info*" buffer)
;; Automode List
;;;###autoload
(define-derived-mode lean-info-mode prog-mode "Lean-Info"
"Major mode for Lean Info Buffer"
:syntax-table lean-syntax-table
:group 'lean
(set (make-local-variable 'font-lock-defaults) lean-info-font-lock-defaults)
(set (make-local-variable 'indent-tabs-mode) nil)
(set 'compilation-mode-font-lock-keywords '())
(set-input-method "Lean")
(set (make-local-variable 'lisp-indent-function)
'common-lisp-indent-function))
(defmacro lean-with-info-output-to-buffer (buffer &rest body)
`(let ((buf (get-buffer ,buffer)))
(with-current-buffer buf
(setq buffer-read-only nil)
(erase-buffer)
(setq standard-output buf)
. ,body)))
(defun lean-ensure-info-buffer (buffer)
(unless (get-buffer buffer)
(with-current-buffer (get-buffer-create buffer)
(buffer-disable-undo)
(lean-info-mode))))
(defun lean-toggle-info-buffer (buffer)
(-if-let (window (get-buffer-window buffer))
(quit-window nil window)
(lean-ensure-info-buffer buffer)
(display-buffer buffer)))
(defun lean-info-buffer-active (buffer)
"Checks whether the given info buffer should show info for the current buffer"
(and
;; info buffer visible
(get-buffer-window buffer)
;; current window of current buffer is selected (i.e., in focus)
(eq (current-buffer) (window-buffer))))
(defun lean-get-info-record-at-point (cont)
"Get info-record at the current point"
(with-demoted-errors "lean get info: %s"
(lean-server-send-command
'info (list :file_name (buffer-file-name)
:line (line-number-at-pos)
:column (lean-line-offset))
(cl-function
(lambda (&key record)
(funcall cont record))))))
(defun lean-info-right-click-find-definition ()
"Offer to jump to definition of right-click target."
(interactive)
(list 'info
(list :file_name (buffer-file-name)
:line (line-number-at-pos)
:column (lean-line-offset))
(cl-function
(lambda (&key record)
(let ((source-record (plist-get record :source)))
(if source-record
(let ((full-name (plist-get record :full-id)))
(list
(list :name (if full-name
(concat "Find definition of " full-name)
"Find definition")
:action (lambda ()
(apply #'lean-find-definition-cont source-record)))))
(list)))))))
(cl-defun lean-find-definition-cont (&key file line column)
(when (fboundp 'xref-push-marker-stack) (xref-push-marker-stack))
(when file
(find-file file))
(goto-char (point-min))
(forward-line (1- line))
(forward-char column))
(defun lean-find-definition ()
"Jump to definition of thing at point"
(interactive)
(setq lean-show-goal--handler-mask t) ; avoid the current request to the Lean server to by
; interrupted by requests made for `lean-show-goal`
(lean-get-info-record-at-point
(lambda (info-record)
(-if-let (source-record (plist-get info-record :source))
(apply #'lean-find-definition-cont source-record)
(-if-let (id (plist-get info-record :full-id))
(message "no source location available for %s" id)
(message "unknown thing at point"))))))
(provide 'lean-info)

1167
lean-mode/lean-input.el Normal file
View file

File diff suppressed because it is too large Load diff

96
lean-mode/lean-leanpkg.el Normal file
View file

@ -0,0 +1,96 @@
;; -*- lexical-binding: t -*-
;;
;; Copyright (c) 2017 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Gabriel Ebner
;;
(require 's)
(require 'json)
(require 'lean-util)
(defun lean-leanpkg-find-dir-in (dir)
(when dir
(or (lean-leanpkg-find-dir-in (f-parent dir))
(when (f-exists? (f-join dir "leanpkg.toml")) dir))))
(defun lean-leanpkg-find-dir ()
(and (buffer-file-name)
(lean-leanpkg-find-dir-in (f-dirname (buffer-file-name)))))
(defun lean-leanpkg-find-dir-safe ()
(or (lean-leanpkg-find-dir)
(error (format "cannot find leanpkg.toml for %s" (buffer-file-name)))))
(defun lean-leanpkg-executable ()
(lean-get-executable "leanpkg"))
(defvar lean-leanpkg-running nil)
(defvar-local lean-leanpkg-configure-prompt-shown nil)
(defun lean-leanpkg-run (cmd &optional restart-lean-server)
"Call `leanpkg $cmd`"
(let ((dir (file-name-as-directory (lean-leanpkg-find-dir-safe)))
(orig-buf (current-buffer)))
(with-current-buffer (get-buffer-create "*leanpkg*")
(let ((inhibit-read-only t)) (erase-buffer))
(switch-to-buffer-other-window (current-buffer))
(redisplay)
(insert (format "> leanpkg %s\n" cmd))
(setq lean-leanpkg-running t)
(let* ((default-directory dir)
(out-buf (current-buffer))
(proc (start-process "leanpkg" (current-buffer)
(lean-leanpkg-executable) cmd)))
(comint-mode)
(set-process-filter proc #'comint-output-filter)
(set-process-sentinel
proc (lambda (_p _e)
(setq lean-leanpkg-running nil)
(when restart-lean-server
(with-current-buffer out-buf
(insert "; restarting lean server\n"))
(with-current-buffer orig-buf
(lean-server-restart)))
(with-current-buffer out-buf
(insert "; done"))))))))
(defun lean-leanpkg-configure ()
"Call leanpkg configure"
(interactive)
(lean-leanpkg-run "configure" 't))
(defun lean-leanpkg-build ()
"Call leanpkg build"
(interactive)
(lean-leanpkg-run "build"))
(defun lean-leanpkg-test ()
"Call leanpkg test"
(interactive)
(lean-leanpkg-run "test"))
(defun lean-leanpkg-find-path-file ()
(let* ((json-object-type 'plist) (json-array-type 'list) (json-false nil)
(path-json (shell-command-to-string
(concat (shell-quote-argument (lean-get-executable lean-executable-name))
" -p")))
(path-out (json-read-from-string path-json)))
(when (and (eq major-mode 'lean-mode)
(plist-get path-out :is_user_leanpkg_path)
(not lean-leanpkg-running)
(not lean-leanpkg-configure-prompt-shown)
(setq lean-leanpkg-configure-prompt-shown t)
(lean-leanpkg-find-dir)
(y-or-n-p (format "Found leanpkg.toml in %s, call leanpkg configure?" (lean-leanpkg-find-dir))))
(save-match-data ; running in timer so that we don't mess up the window layout
(run-at-time nil nil
(lambda (buf)
(with-current-buffer buf
(lean-leanpkg-configure)))
(current-buffer))))
(setq lean-leanpkg-configure-prompt-shown t)
(plist-get path-out :leanpkg_path_file)))
(provide 'lean-leanpkg)

240
lean-mode/lean-mode.el Normal file
View file

@ -0,0 +1,240 @@
;;; lean-mode.el --- A major mode for the Lean language -*- lexical-binding: t -*-
;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved.
;; Copyright (c) 2014, 2015 Soonho Kong. All rights reserved.
;; Author: Leonardo de Moura <leonardo@microsoft.com>
;; Soonho Kong <soonhok@cs.cmu.edu>
;; Gabriel Ebner <gebner@gebner.org>
;; Sebastian Ullrich <sebasti@nullri.ch>
;; Maintainer: Sebastian Ullrich <sebasti@nullri.ch>
;; Created: Jan 09, 2014
;; Keywords: languages
;; Package-Requires: ((emacs "24.3") (dash "2.12.0") (dash-functional "1.2.0") (s "1.10.0") (f "0.19.0") (flycheck "30"))
;; URL: https://github.com/leanprover/lean-mode
;; Released under Apache 2.0 license as described in the file LICENSE.
;;; Commentary:
;; Provides a major mode for the Lean programming language.
;; Provides highlighting, diagnostics, goal visualization,
;; and many other useful features for Lean users.
;; See the README.md for more advanced features and the
;; associated keybindings.
;;; Code:
(require 'cl-lib)
(require 'dash)
(require 'pcase)
(require 'flycheck)
(require 'lean-eri)
(require 'lean-util)
(require 'lean-settings)
(require 'lean-input)
(require 'lean-syntax)
(require 'lean-leanpkg)
(require 'lean-server)
(require 'lean-flycheck)
(require 'lean-info)
(require 'lean-hole)
(require 'lean-type)
(require 'lean-message-boxes)
(require 'lean-right-click)
(require 'lean-dev)
(defun lean-compile-string (exe-name args file-name)
"Concatenate EXE-NAME, ARGS, and FILE-NAME."
(format "%s %s %s" exe-name args file-name))
(defun lean-create-temp-in-system-tempdir (file-name prefix)
"Create a temp lean file and return its name."
(make-temp-file (or prefix "flymake") nil (f-ext file-name)))
(defun lean-execute (&optional arg)
"Execute Lean in the current buffer."
(interactive)
(when (called-interactively-p 'any)
(setq arg (read-string "arg: " arg)))
(let ((cc compile-command)
(target-file-name
(or
(buffer-file-name)
(flymake-init-create-temp-buffer-copy 'lean-create-temp-in-system-tempdir))))
(compile (lean-compile-string
(shell-quote-argument (f-full (lean-get-executable lean-executable-name)))
(or arg "")
(shell-quote-argument (f-full target-file-name))))
;; restore old value
(setq compile-command cc)))
(defun lean-std-exe ()
(interactive)
(lean-execute))
(defun lean-check-expansion ()
(interactive)
(save-excursion
(if (looking-at (rx symbol-start "_")) t
(if (looking-at "\\_>") t
(backward-char 1)
(if (looking-at "\\.") t
(backward-char 1)
(if (looking-at "->") t nil))))))
(defun lean-tab-indent ()
(interactive)
(cond ((looking-back (rx line-start (* white)) nil)
(lean-eri-indent))
(t (indent-for-tab-command))))
(defun lean-set-keys ()
(local-set-key lean-keybinding-std-exe1 #'lean-std-exe)
(local-set-key lean-keybinding-std-exe2 #'lean-std-exe)
(local-set-key lean-keybinding-show-key #'quail-show-key)
(local-set-key lean-keybinding-server-restart #'lean-server-restart)
(local-set-key lean-keybinding-server-switch-version #'lean-server-switch-version)
(local-set-key lean-keybinding-find-definition #'lean-find-definition)
(local-set-key lean-keybinding-tab-indent #'lean-tab-indent)
(local-set-key lean-keybinding-hole #'lean-hole)
(local-set-key lean-keybinding-lean-toggle-show-goal #'lean-toggle-show-goal)
(local-set-key lean-keybinding-lean-toggle-next-error #'lean-toggle-next-error)
(local-set-key lean-keybinding-lean-message-boxes-toggle #'lean-message-boxes-toggle)
(local-set-key lean-keybinding-leanpkg-configure #'lean-leanpkg-configure)
(local-set-key lean-keybinding-leanpkg-build #'lean-leanpkg-build)
(local-set-key lean-keybinding-leanpkg-test #'lean-leanpkg-test)
;; This only works as a mouse binding due to the event, so it is not abstracted
;; to avoid user confusion.
(local-set-key (kbd "<mouse-3>") #'lean-right-click-show-menu)
)
(define-abbrev-table 'lean-abbrev-table
'())
(defvar lean-mode-map (make-sparse-keymap)
"Keymap used in Lean mode")
(defun lean-mk-check-menu-option (text sym)
`[,text (lean-set-check-mode ',sym)
:style radio :selected (eq lean-server-check-mode ',sym)])
(easy-menu-define lean-mode-menu lean-mode-map
"Menu for the Lean major mode"
`("Lean"
["Execute lean" lean-execute t]
;; ["Create a new project" (call-interactively 'lean-project-create) (not (lean-project-inside-p))]
"-----------------"
["Show type info" lean-show-type (and lean-eldoc-use eldoc-mode)]
["Toggle goal display" lean-toggle-show-goal t]
["Toggle next error display" lean-toggle-next-error t]
["Toggle message boxes" lean-message-boxes-toggle t]
["Highlight pending tasks" lean-server-toggle-show-pending-tasks
:active t :style toggle :selected lean-server-show-pending-tasks]
["Find definition at point" lean-find-definition t]
"-----------------"
["List of errors" flycheck-list-errors flycheck-mode]
"-----------------"
["Restart lean process" lean-server-restart t]
"-----------------"
,(lean-mk-check-menu-option "Check nothing" 'nothing)
,(lean-mk-check-menu-option "Check visible lines" 'visible-lines)
,(lean-mk-check-menu-option "Check visible lines and above" 'visible-lines-and-above)
,(lean-mk-check-menu-option "Check visible files" 'visible-files)
,(lean-mk-check-menu-option "Check open files" 'open-files)
"-----------------"
("Configuration"
["Show type at point"
lean-toggle-eldoc-mode :active t :style toggle :selected eldoc-mode])
"-----------------"
["Customize lean-mode" (customize-group 'lean) t]))
(defconst lean-hooks-alist
'(
;; server
;; (kill-buffer-hook . lean-server-stop)
(after-change-functions . lean-server-change-hook)
(focus-in-hook . lean-server-show-messages)
(window-scroll-functions . lean-server-window-scroll-function-hook)
;; Handle events that may start automatic syntax checks
(before-save-hook . lean-whitespace-cleanup)
;; info windows
(post-command-hook . lean-show-goal--handler)
(post-command-hook . lean-next-error--handler)
(flycheck-after-syntax-check-hook . lean-show-goal--handler)
(flycheck-after-syntax-check-hook . lean-next-error--handler)
)
"Hooks which lean-mode needs to hook in.
The `car' of each pair is a hook variable, the `cdr' a function
to be added or removed from the hook variable if Flycheck mode is
enabled and disabled respectively.")
(defun lean-mode-setup ()
"Default lean-mode setup"
;; server
(ignore-errors (lean-server-ensure-alive))
(setq mode-name '("Lean" (:eval (lean-server-status-string))))
;; Right click menu sources
(setq lean-right-click-item-functions '(lean-info-right-click-find-definition
lean-hole-right-click))
;; Flycheck
(lean-flycheck-turn-on)
(setq-local flycheck-disabled-checkers '())
;; info buffers
(lean-ensure-info-buffer lean-next-error-buffer-name)
(lean-ensure-info-buffer lean-show-goal-buffer-name)
;; eldoc
(when lean-eldoc-use
(set (make-local-variable 'eldoc-documentation-function)
'lean-eldoc-documentation-function)
(eldoc-mode t)))
;; Automode List
;;;###autoload
(define-derived-mode lean-mode prog-mode "Lean"
"Major mode for Lean
\\{lean-mode-map}
Invokes `lean-mode-hook'.
"
:syntax-table lean-syntax-table
:abbrev-table lean-abbrev-table
:group 'lean
(set (make-local-variable 'comment-start) "--")
(set (make-local-variable 'comment-start-skip) "[-/]-[ \t]*")
(set (make-local-variable 'comment-end) "")
(set (make-local-variable 'comment-end-skip) "[ \t]*\\(-/\\|\\s>\\)")
(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 'compilation-mode-font-lock-keywords '())
(set-input-method "Lean")
(set (make-local-variable 'lisp-indent-function)
'common-lisp-indent-function)
(lean-set-keys)
(if (fboundp 'electric-indent-local-mode)
(electric-indent-local-mode -1))
;; (abbrev-mode 1)
(pcase-dolist (`(,hook . ,fn) lean-hooks-alist)
(add-hook hook fn nil 'local))
(lean-mode-setup))
;; Automatically use lean-mode for .lean files.
;;;###autoload
(push '("\\.lean$" . lean-mode) auto-mode-alist)
(push '("\\.hlean$" . lean-mode) auto-mode-alist)
;; Use utf-8 encoding
;;;### autoload
(modify-coding-system-alist 'file "\\.lean\\'" 'utf-8)
(modify-coding-system-alist 'file "\\.hlean\\'" 'utf-8)
;; Flycheck init
(eval-after-load 'flycheck
'(lean-flycheck-init))
(provide 'lean-mode)
;;; lean-mode.el ends here

84
lean-mode/lean-right-click.el Normal file
View file

@ -0,0 +1,84 @@
;; -*- lexical-binding: t -*-
;;
;;; lean-right-click.el
;;
;; Copyright (c) 2017 David Christiansen. All rights reserved.
;;
;; Author: David Christiansen
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;;; Code:
(defvar lean-right-click-item-functions nil
"A list of functions to compute menu items from source locations.
The functions take no arguments. They will be run in a context
where `current-buffer' gives the buffer in which the click
occurred. The function should return a three-element list, where
the first is a Lean server command, the second is its parameter
list, and the third is a continuation that will compute a list of
menu items.
Each menu item is a plist that maps the key :name to the string
to show in the menu and the key :action to a zero-argument
function that implements the action.")
(make-variable-buffer-local 'lean-right-click-item-functions)
(defvar lean-right-click--unique-val-counter 0
"A global counter for unique values for lean-right-click.")
(defun lean-right-click--unique-val ()
"Get a unique value for internal tagging."
(cl-incf lean-right-click--unique-val-counter))
(defun lean-right-click--items-for-location ()
"Return the menu items for point in the current buffer."
(let ((commands (cl-loop for fun in lean-right-click-item-functions
collecting (funcall fun))))
(let ((timeout 0.15)
(items '())
(start-time (time-to-seconds))
(command-count (length commands))
(commands-returned 0))
(cl-loop for (cmd args cont) in commands
do (progn (lean-server-send-command
cmd args
(lambda (&rest result)
(setq items (append items (apply cont result)))
(cl-incf commands-returned))
(lambda (&rest _whatever)
(cl-incf commands-returned)))
;; This is necessary to ensure that async IO happens.
(sit-for 0.02)))
(while (and (< (time-to-seconds) (+ timeout start-time))
(< commands-returned command-count))
(sit-for 0.02))
items)))
(defun lean-right-click-show-menu (click)
"Show a menu based on the location of CLICK, computed from the `lean-right-click-functions'."
(interactive "e")
(let* ((window (posn-window (event-end click)))
(buffer (window-buffer window))
(where (posn-point (event-end click)))
(menu-items (with-current-buffer buffer
(save-excursion
(goto-char where)
(lean-right-click--items-for-location)))))
(when menu-items
(let* ((menu (make-sparse-keymap))
(todo (cl-loop for item in menu-items
collecting (let ((sym (lean-right-click--unique-val)))
(define-key-after menu `[,sym]
`(menu-item ,(plist-get item :name)
(lambda () (interactive)))
t)
(cons sym (plist-get item :action)))))
(selection (x-popup-menu click menu)))
(when selection
(funcall (cdr (assoc (car selection) todo))))))))
(provide 'lean-right-click)
;;; lean-right-click.el ends here

133
lean-mode/lean-settings.el Normal file
View file

@ -0,0 +1,133 @@
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(require 'cl-lib)
(defgroup lean nil
"Lean Theorem Prover"
:prefix "lean-"
:group 'languages
:link '(url-link :tag "Website" "http://leanprover.github.io")
:link '(url-link :tag "Github" "https://github.com/leanprover/lean"))
(defgroup lean-keybinding nil
"Keybindings for lean-mode."
:prefix "lean-"
:group 'lean)
(defvar-local lean-default-executable-name
(cl-case system-type
('windows-nt "lean.exe")
('cygwin "lean.exe")
(t "lean"))
"Default executable name of Lean")
(defcustom lean-rootdir nil
"Full pathname of lean root directory. It should be defined by user."
:group 'lean
:type 'string)
(defcustom lean-executable-name lean-default-executable-name
"Name of lean executable"
:group 'lean
:type 'string)
(defcustom lean-memory-limit 1024
"Memory limit for lean process in megabytes"
:group 'lean
:type 'number)
(defcustom lean-timeout-limit 100000
"Deterministic timeout limit (it is approximately the maximum number of memory allocations in thousands)"
:group 'lean
:type 'number)
(defcustom lean-extra-arguments nil
"Extra command-line arguments to the lean process"
:group 'lean
:type '(list string))
(defcustom lean-eldoc-use t
"Use eldoc mode for lean."
:group 'lean
:type 'boolean)
(defcustom lean-eldoc-nay-retry-time 0.3
"When eldoc-function had nay, try again after this amount of time."
:group 'lean
:type 'number)
(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-show-type-add-to-kill-ring nil
"If it is non-nil, add the type information to the kill-ring so
that user can yank(paste) it later. By default, it's
false (nil)."
:group 'lean
:type 'boolean)
(defcustom lean-server-show-pending-tasks t
"Highlights pending tasks in the current buffer."
:group 'lean
:type 'boolean)
(defcustom lean-server-check-mode 'visible-lines-and-above
"What parts of the open files the Lean server should check"
:group 'lean
:type 'symbol
:options '(nothing visible-lines visible-lines-and-above visible-files open-files))
(defcustom lean-keybinding-std-exe1 (kbd "C-c C-x")
"Lean Keybinding for std-exe #1"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-std-exe2 (kbd "C-c C-l")
"Lean Keybinding for std-exe #2"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-show-key (kbd "C-c C-k")
"Lean Keybinding for show-key"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-server-restart (kbd "C-c C-r")
"Lean Keybinding for server-restart"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-server-switch-version (kbd "C-c C-s")
"Lean Keybinding for lean-server-switch-version"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-find-definition (kbd "M-.")
"Lean Keybinding for find-definition"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-tab-indent (kbd "TAB")
"Lean Keybinding for tab-indent"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-auto-complete (kbd "S-SPC")
"Lean Keybinding for auto completion"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-hole (kbd "C-c SPC")
"Lean Keybinding for hole manipulation"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-lean-toggle-show-goal (kbd "C-c C-g")
"Lean Keybinding for show-goal-at-pos"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-lean-toggle-next-error (kbd "C-c C-n")
"Lean Keybinding for lean-toggle-next-error"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-lean-message-boxes-toggle (kbd "C-c C-b")
"Lean Keybinding for lean-message-boxes-toggle"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-leanpkg-configure (kbd "C-c C-p C-c")
"Lean Keybinding for lean-leanpkg-configure"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-leanpkg-build (kbd "C-c C-p C-b")
"Lean Keybinding for lean-leanpkg-build"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-leanpkg-test (kbd "C-c C-p C-t")
"Lean Keybinding for lean-leanpkg-test"
:group 'lean-keybinding :type 'key-sequence)
(provide 'lean-settings)

194
lean-mode/lean-syntax.el Normal file
View file

@ -0,0 +1,194 @@
;; 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-keywords1
'("import" "prelude" "protected" "private" "noncomputable" "definition" "meta" "renaming"
"hiding" "exposing" "parameter" "parameters" "begin" "constant" "constants"
"lemma" "variable" "variables" "theorem" "example" "abbreviation"
"open" "export" "axiom" "axioms" "inductive" "coinductive" "with" "without"
"structure" "universe" "universes" "hide"
"precedence" "reserve" "declare_trace" "add_key_equivalence"
"match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
"end" "this" "using" "using_well_founded" "namespace" "section"
"attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
"attributes" "raw" "replacing"
"calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "forall" "Pi" "fun"
"exists" "if" "then" "else" "assume" "from"
"mutual" "def" "run_cmd")
"lean keywords ending with 'word' (not symbol)")
(defconst lean-keywords1-regexp
(eval `(rx word-start (or ,@lean-keywords1) word-end)))
(defconst lean-constants
'("#" "@" "!" "$" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨"
"≠" "<" ">" "≤" "≥" "¬" "<=" ">=" "⁻¹" "⬝" "▸" "+" "*" "-" "/" "λ"
"→" "∃" "∀" "∘" "×" "Σ" "Π" "~" "||" "&&" "≃" "≡" "≅"
"ℕ" "ℤ" "ℚ" "ℝ" "ℂ" "𝔸"
"⬝e" "⬝i" "⬝o" "⬝op" "⬝po" "⬝h" "⬝v" "⬝hp" "⬝vp" "⬝ph" "⬝pv" "⬝r" "◾" "◾o"
"∘n" "∘f" "∘fi" "∘nf" "∘fn" "∘n1f" "∘1nf" "∘f1n" "∘fn1"
"^c" "≃c" "≅c" "×c" "×f" "×n" "+c" "+f" "+n" "ℕ₋₂")
"lean constants")
(defconst lean-constants-regexp (regexp-opt lean-constants))
(defconst lean-numerals-regexp
(eval `(rx word-start
(one-or-more digit) (optional (and "." (zero-or-more digit)))
word-end)))
(defconst lean-warnings '("sorry" "exit") "lean warnings")
(defconst lean-warnings-regexp
(eval `(rx word-start (or ,@lean-warnings) word-end)))
(defconst lean-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)
;; comment
(modify-syntax-entry ?/ ". 14nb" st)
(modify-syntax-entry ?- ". 123" st)
(modify-syntax-entry ?\n ">" st)
(modify-syntax-entry ?« "<" st)
(modify-syntax-entry ?» ">" st)
;; Word constituent
(--map (modify-syntax-entry it "w" st)
(list ?a ?b ?c ?d ?e ?f ?g ?h ?i ?j ?k ?l ?m
?n ?o ?p ?q ?r ?s ?t ?u ?v ?w ?x ?y ?z
?A ?B ?C ?D ?E ?F ?G ?H ?I ?J ?K ?L ?M
?N ?O ?P ?Q ?R ?S ?T ?U ?V ?W ?X ?Y ?Z))
(--map (modify-syntax-entry it "w" st)
(list ?0 ?1 ?2 ?3 ?4 ?5 ?6 ?7 ?8 ?9))
(--map (modify-syntax-entry it "w" st)
(list ?α ?β ?γ ?δ ?ε ?ζ ?η ?θ ?ι ?κ ;;?λ
?μ ?ν ?ξ ?ο ?π ?ρ ?ς ?σ ?τ ?υ
?φ ?χ ?ψ ?ω))
(--map (modify-syntax-entry it "w" st)
(list ?ϊ ?ϋ ?ό ?ύ ?ώ ?Ϗ ?ϐ ?ϑ ?ϒ ?ϓ ?ϔ ?ϕ ?ϖ
?ϗ ?Ϙ ?ϙ ?Ϛ ?ϛ ?Ϝ ?ϝ ?Ϟ ?ϟ ?Ϡ ?ϡ ?Ϣ ?ϣ
?Ϥ ?ϥ ?Ϧ ?ϧ ?Ϩ ?ϩ ?Ϫ ?ϫ ?Ϭ ?ϭ ?Ϯ ?ϯ ?ϰ
?ϱ ?ϲ ?ϳ ?ϴ ?ϵ ?϶ ?Ϸ ?ϸ ?Ϲ ?Ϻ ?ϻ))
(--map (modify-syntax-entry it "w" st)
(list ?ἀ ?ἁ ?ἂ ?ἃ ?ἄ ?ἅ ?ἆ ?ἇ ?Ἀ ?Ἁ ?Ἂ ?Ἃ ?Ἄ
?Ἅ ?Ἆ ?Ἇ ?ἐ ?ἑ ?ἒ ?ἓ ?ἔ ?ἕ ?἖ ?἗ ?Ἐ ?Ἑ
?Ἒ ?Ἓ ?Ἔ ?Ἕ ?἞ ?἟ ?ἠ ?ἡ ?ἢ ?ἣ ?ἤ ?ἥ
?ἦ ?ἧ ?Ἠ ?Ἡ ?Ἢ ?Ἣ ?Ἤ ?Ἥ ?Ἦ ?Ἧ ?ἰ ?ἱ
?ἲ ?ἳ ?ἴ ?ἵ ?ἶ ?ἷ ?Ἰ ?Ἱ ?Ἲ ?Ἳ ?Ἴ ?Ἵ ?Ἶ ?Ἷ
?ὀ ?ὁ ?ὂ ?ὃ ?ὄ ?ὅ ?὆ ?὇ ?Ὀ ?Ὁ ?Ὂ ?Ὃ
?Ὄ ?Ὅ ?὎ ?὏ ?ὐ ?ὑ ?ὒ ?ὓ ?ὔ ?ὕ ?ὖ ?ὗ
?὘ ?Ὑ ?὚ ?Ὓ ?὜ ?Ὕ ?὞ ?Ὗ ?ὠ ?ὡ ?ὢ
?ὣ ?ὤ ?ὥ ?ὦ ?ὧ ?Ὠ ?Ὡ ?Ὢ ?Ὣ ?Ὤ ?Ὥ ?Ὦ
?Ὧ ?ὰ ?ά ?ὲ ?έ ?ὴ ?ή ?ὶ ?ί ?ὸ ?ό ?ὺ ?ύ ?ὼ
?ώ ?὾ ?὿ ?ᾀ ?ᾁ ?ᾂ ?ᾃ ?ᾄ ?ᾅ ?ᾆ ?ᾇ ?ᾈ
?ᾉ ?ᾊ ?ᾋ ?ᾌ ?ᾍ ?ᾎ ?ᾏ ?ᾐ ?ᾑ ?ᾒ ?ᾓ ?ᾔ
?ᾕ ?ᾖ ?ᾗ ?ᾘ ?ᾙ ?ᾚ ?ᾛ ?ᾜ ?ᾝ ?ᾞ ?ᾟ ?ᾠ ?ᾡ ?ᾢ
?ᾣ ?ᾤ ?ᾥ ?ᾦ ?ᾧ ?ᾨ ?ᾩ ?ᾪ ?ᾫ ?ᾬ ?ᾭ ?ᾮ ?ᾯ ?ᾰ
?ᾱ ?ᾲ ?ᾳ ?ᾴ ?᾵ ?ᾶ ?ᾷ ?Ᾰ ?Ᾱ ?Ὰ ?Ά ?ᾼ ?᾽
?ι ?᾿ ?῀ ?῁ ?ῂ ?ῃ ?ῄ ?῅ ?ῆ ?ῇ ?Ὲ ?Έ ?Ὴ
?Ή ?ῌ ?῍ ?῎ ?῏ ?ῐ ?ῑ ?ῒ ?ΐ ?῔ ?῕ ?ῖ ?ῗ
?Ῐ ?Ῑ ?Ὶ ?Ί ?῜ ?῝ ?῞ ?῟ ?ῠ ?ῡ ?ῢ ?ΰ ?ῤ ?ῥ
?ῦ ?ῧ ?Ῠ ?Ῡ ?Ὺ ?Ύ ?Ῥ ?῭ ?΅ ?` ?῰ ?῱ ?ῲ ?ῳ
?ῴ ?῵ ?ῶ ?ῷ ?Ὸ ?Ό ?Ὼ ?Ώ ?ῼ ?´ ?῾))
(--map (modify-syntax-entry it "w" st)
(list ?℀ ?℁ ?ℂ ?℃ ?℄ ?℅ ?℆ ?ℇ ?℈ ?℉ ?ℊ ?ℋ ?ℌ ?ℍ ?ℎ
?ℏ ?ℐ ?ℑ ?ℒ ?ℓ ?℔ ?ℕ ?№ ?℗ ?℘ ?ℙ ?ℚ ?ℛ ?ℜ ?ℝ
?℞ ?℟ ?℠ ?℡ ?™ ?℣ ?ℤ ?℥ ?Ω ?℧ ?ℨ ?℩ ?K ?Å ?ℬ
?ℭ ?℮ ?ℯ ?ℰ ?ℱ ?Ⅎ ?ℳ ?ℴ ?ℵ ?ℶ ?ℷ ?ℸ ?ℹ ?℺ ?℻
?ℼ ?ℽ ?ℾ ?ℿ ?⅀ ?⅁ ?⅂ ?⅃ ?⅄ ?ⅅ ?ⅆ ?ⅇ ?ⅈ ?ⅉ ?⅊
?⅋ ?⅌ ?⅍ ?ⅎ ?⅏))
(modify-syntax-entry ?' "w" st)
(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
`((;; attributes
(,(rx word-start "attribute" word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace))))
(1 'font-lock-doc-face))
(,(rx (group "@[" (zero-or-more (not (any "]"))) "]"))
(1 'font-lock-doc-face))
(,(rx (group "#" (or "eval" "print" "reduce" "help" "check")))
(1 'font-lock-keyword-face))
;; mutual definitions "names"
(,(rx word-start
"mutual"
word-end
(zero-or-more whitespace)
word-start
(or "inductive" "definition" "def")
word-end
(group (zero-or-more (not (any " \t\n\r{([,"))) (zero-or-more (zero-or-more whitespace) "," (zero-or-more whitespace) (not (any " \t\n\r{([,")))))
(1 'font-lock-function-name-face))
;; declarations
(,(rx word-start
(group (or "inductive" (group "class" (zero-or-more whitespace) "inductive") "instance" "structure" "class" "theorem" "axiom" "axioms" "lemma" "definition" "def" "constant"))
word-end (zero-or-more whitespace)
(group (zero-or-more "{" (zero-or-more (not (any "}"))) "}" (zero-or-more whitespace)))
(zero-or-more whitespace)
(group (zero-or-more (not (any " \t\n\r{([")))))
(4 'font-lock-function-name-face))
;; Constants which have a keyword as subterm
(,(rx (or "∘if")) . 'font-lock-constant-face)
;; Keywords
("\\(set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face))
(,lean-keywords1-regexp . 'font-lock-keyword-face)
(,(rx word-start (group "example") ".") (1 'font-lock-keyword-face))
(,(rx (or "∎")) . 'font-lock-keyword-face)
;; Types
(,(rx word-start (or "Prop" "Type" "Type*" "Sort" "Sort*") symbol-end) . 'font-lock-type-face)
(,(rx word-start (group (or "Prop" "Type" "Sort")) ".") (1 'font-lock-type-face))
;; String
("\"[^\"]*\"" . 'font-lock-string-face)
;; ;; Constants
(,lean-constants-regexp . 'font-lock-constant-face)
(,lean-numerals-regexp . 'font-lock-constant-face)
;; place holder
(,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
;; warnings
(,lean-warnings-regexp . 'font-lock-warning-face)
;; escaped identifiers
(,(rx (and (group "«") (group (one-or-more (not (any "»")))) (group "»")))
(1 font-lock-comment-face t)
(2 nil t)
(3 font-lock-comment-face t))
)))
;; Syntax Highlighting for Lean Info Mode
(defconst lean-info-font-lock-defaults
(let ((new-entries
`(;; Please add more after this:
(,(rx (group (+ symbol-start (+ (or word (char ?₁ ?₂ ?₃ ?₄ ?₅ ?₆ ?₇ ?₈ ?₉ ?₀))) symbol-end (* white))) ":")
(1 'font-lock-variable-name-face))
(,(rx white ":" white)
. 'font-lock-keyword-face)
(,(rx "⊢" white)
. 'font-lock-keyword-face)
(,(rx "[" (group "stale") "]")
(1 'font-lock-warning-face))
(,(rx line-start "No Goal" line-end)
. 'font-lock-constant-face)))
(inherited-entries (car lean-font-lock-defaults)))
`(,(-concat new-entries inherited-entries))))
(provide 'lean-syntax)

110
lean-mode/lean-type.el Normal file
View file

@ -0,0 +1,110 @@
;; -*- lexical-binding: t; -*-
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Authors: Soonho Kong, Sebastian Ullrich
;;
(require 'cl-lib)
(require 'dash)
(require 'dash-functional)
(require 's)
(require 'lean-util)
(require 'lean-server)
(require 'lean-debug)
(require 'flymake)
(defun lean-fill-placeholder-cont (info-record)
"Continuation for lean-fill-placeholder"
(let ((synth (and info-record (plist-get info-record :synth))))
(when synth
(let ((synth-str
(replace-regexp-in-string "?M_[0-9]+" "_" synth)))
(when (cl-search " " synth-str)
(setq synth-str (concat "(" synth-str ")")))
(when (looking-at "_")
(delete-char 1)
(insert synth-str))))))
(defun lean-fill-placeholder ()
"Fill the placeholder with a synthesized expression by Lean."
(interactive)
(lean-get-info-record-at-point 'lean-fill-placeholder-cont))
(cl-defun lean-info-record-to-string (info-record)
"Given typeinfo, overload, and sym-name, compose information as a string."
(destructuring-bind (&key type tactic_params tactic_param_idx text doc full-id &allow-other-keys) info-record
(let ((name-str (or full-id text))
(type-str type)
str)
(when tactic_params
(setq tactic_params (-map-indexed (lambda (i param)
(if (eq i tactic_param_idx)
(propertize param 'face 'eldoc-highlight-function-argument)
param)) tactic_params))
(setq type-str (mapconcat 'identity tactic_params " ")))
(when (and name-str type-str)
(setq str (format (if tactic_params "%s %s" "%s : %s")
(propertize name-str 'face 'font-lock-variable-name-face)
type-str)))
(when doc
(let* ((lines (split-string doc "\n"))
(doc (if (cdr lines)
(concat (car lines) " ⋯")
(car lines))))
(setq str (concat str
(format "\n%s"
(propertize doc 'face 'font-lock-comment-face))))))
str)))
(defvar-local lean-eldoc-documentation-cache nil)
(defun lean-eldoc-documentation-function-cont (info-record &optional add-to-kill-ring)
"Continuation for lean-eldoc-documentation-function"
(let ((info-string (and info-record (lean-info-record-to-string info-record))))
(when info-string
(when add-to-kill-ring
(kill-new
(substring-no-properties info-string))))
(setq lean-eldoc-documentation-cache (and info-string (format "%s" info-string)))
(eldoc-message lean-eldoc-documentation-cache)))
(defun lean-eldoc-documentation-function (&optional add-to-kill-ring)
"Show information of lean expression at point if any"
(interactive)
(when (not (eq lean-server-check-mode 'nothing)) ; TODO(gabriel): revisit once info no longer reparses the file
(lean-get-info-record-at-point
(lambda (info-record)
(lean-eldoc-documentation-function-cont info-record add-to-kill-ring)))
lean-eldoc-documentation-cache))
(defun lean-show-type ()
"Show information of lean-expression at point if any."
(interactive)
(lean-eldoc-documentation-function lean-show-type-add-to-kill-ring))
(defconst lean-show-goal-buffer-name "*Lean Goal*")
(setq lean-show-goal--handler-mask nil)
(defun lean-show-goal--handler ()
(if lean-show-goal--handler-mask
(setq lean-show-goal--handler-mask nil)
(let ((deactivate-mark)) ; keep transient mark
(when (and (not (eq lean-server-check-mode 'nothing))
; TODO(gabriel): revisit ^^ once info no longer reparses the file
(lean-info-buffer-active lean-show-goal-buffer-name))
(lean-get-info-record-at-point
(lambda (info-record)
(let ((state (plist-get info-record :state)))
(unless (or (s-blank? state) (s-blank? (s-trim state)))
(lean-with-info-output-to-buffer lean-show-goal-buffer-name (princ state))))))))))
(defun lean-toggle-show-goal ()
"Show goal at the current point."
(interactive)
(lean-toggle-info-buffer lean-show-goal-buffer-name)
(lean-show-goal--handler))
(provide 'lean-type)

104
lean-mode/lean-util.el Normal file
View file

@ -0,0 +1,104 @@
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: Soonho Kong
;;
(require 'cl-lib)
(require 'f)
(require 's)
(require 'dash)
(require 'dash-functional)
(defun lean-setup-rootdir ()
(let ((root (executable-find lean-executable-name)))
(when root
(setq lean-rootdir (f-dirname (f-dirname root))))
root))
(defun lean-get-rootdir ()
(if lean-rootdir
(let ((lean-path (f-full (f-join lean-rootdir "bin" lean-executable-name))))
(unless (f-exists? lean-path)
(error "Incorrect 'lean-rootdir' value, path '%s' does not exist." lean-path))
lean-rootdir)
(or
(lean-setup-rootdir)
(error
(concat "Lean was not found in the 'exec-path' and 'lean-rootdir' is not defined. "
"Please set it via M-x customize-variable RET lean-rootdir RET.")))))
(defun lean-get-executable (exe-name)
"Return fullpath of lean executable"
(let ((lean-bin-dir-name "bin"))
(f-full (f-join (lean-get-rootdir) lean-bin-dir-name exe-name))))
(defun lean-line-offset (&optional pos)
"Return the byte-offset of `pos` or current position, counting from the
beginning of the line"
(interactive)
(let* ((pos (or pos (point)))
(bol-pos
(save-excursion
(goto-char pos)
(beginning-of-line)
(point))))
(- pos bol-pos)))
(defun lean-pos-at-line-col (l c)
"Return the point of the given line and column."
;; http://emacs.stackexchange.com/a/8083
(save-excursion
(goto-char (point-min))
(forward-line (- l 1))
(move-to-column c)
(point)))
(defun lean-whitespace-cleanup ()
(when lean-delete-trailing-whitespace
(delete-trailing-whitespace)))
(defun lean-in-comment-p ()
"t if a current point is inside of comment block
nil otherwise"
(nth 4 (syntax-ppss)))
;; The following function is a slightly modified version of
;; f--collect-entries written by Johan Andersson
;; The URL is at https://github.com/rejeep/f.el/blob/master/f.el#L416-L435
(defun lean--collect-entries (path recursive)
(let (result
(entries
(-reject
(lambda (file)
(or
(equal (f-filename file) ".")
(equal (f-filename file) "..")))
(directory-files path t))))
;; The following line is the only modification that I made
;; It waits 0.0001 second for an event. This wait allows
;; wait-timeout function to check the timer and kill the execution
;; of this function.
(sit-for 0.0001)
(cond (recursive
(-map
(lambda (entry)
(if (f-file? entry)
(setq result (cons entry result))
(when (f-directory? entry)
(setq result (cons entry result))
(setq result (append result (lean--collect-entries entry recursive))))))
entries))
(t (setq result entries)))
result))
;; The following function is a slightly modified version of
;; f-files function written by Johan Andersson The URL is at
;; https://github.com/rejeep/f.el/blob/master/f.el#L478-L481
(defun lean-find-files (path &optional fn recursive)
"Find all files in PATH."
;; It calls lean--collect-entries instead of f--collect-entries
(let ((files (-select 'f-file? (lean--collect-entries path recursive))))
(if fn (-select fn files) files)))
(provide 'lean-util)