diff --git a/lean-mode/.gitignore b/lean-mode/.gitignore
new file mode 100644
index 0000000000..433da842b5
--- /dev/null
+++ b/lean-mode/.gitignore
@@ -0,0 +1,2 @@
+.cask
+*.elc
diff --git a/lean-mode/LICENSE b/lean-mode/LICENSE
new file mode 100644
index 0000000000..8dada3edaf
--- /dev/null
+++ b/lean-mode/LICENSE
@@ -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.
diff --git a/lean-mode/README.md b/lean-mode/README.md
new file mode 100644
index 0000000000..829c1382e9
--- /dev/null
+++ b/lean-mode/README.md
@@ -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 |
+|--------------------|---------------------------------------------------------------------------------|
+| M-. | jump to definition in source file (`lean-find-definition`) |
+| M-, | jump back to position before M-. (`xref-pop-marker-stack`) |
+| C-c C-k | shows the keystroke needed to input the symbol under the cursor |
+| C-c C-x | execute lean in stand-alone mode (`lean-std-exe`) |
+| C-c SPC | run a command on the hole at point (`lean-hole`) |
+| C-c C-d | show a searchable list of definitions (`helm-lean-definitions`) |
+| C-c C-g | toggle showing current tactic proof goal (`lean-toggle-show-goal`) |
+| C-c C-n | toggle showing next error in dedicated buffer (`lean-toggle-next-error`) |
+| C-c C-b | toggle showing output in inline boxes (`lean-message-boxes-toggle`) |
+| C-c C-r | restart the lean server (`lean-server-restart`) |
+| C-c C-s | switch to a different Lean version via [elan](https://github.com/Kha/elan) (`lean-server-switch-version`) |
+| C-c ! n | flycheck: go to next error |
+| C-c ! p | flycheck: go to previous error |
+| C-c ! l | 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 C-c C-b.
+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`.
diff --git a/lean-mode/lean-debug.el b/lean-mode/lean-debug.el
new file mode 100644
index 0000000000..196fed44c9
--- /dev/null
+++ b/lean-mode/lean-debug.el
@@ -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)
diff --git a/lean-mode/lean-dev.el b/lean-mode/lean-dev.el
new file mode 100644
index 0000000000..4d3c2b39d1
--- /dev/null
+++ b/lean-mode/lean-dev.el
@@ -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)
diff --git a/lean-mode/lean-eri.el b/lean-mode/lean-eri.el
new file mode 100644
index 0000000000..72b9d23c06
--- /dev/null
+++ b/lean-mode/lean-eri.el
@@ -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
diff --git a/lean-mode/lean-flycheck.el b/lean-mode/lean-flycheck.el
new file mode 100644
index 0000000000..ab30bae320
--- /dev/null
+++ b/lean-mode/lean-flycheck.el
@@ -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)
diff --git a/lean-mode/lean-hole.el b/lean-mode/lean-hole.el
new file mode 100644
index 0000000000..864dfd241b
--- /dev/null
+++ b/lean-mode/lean-hole.el
@@ -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
diff --git a/lean-mode/lean-info.el b/lean-mode/lean-info.el
new file mode 100644
index 0000000000..75fbbc192c
--- /dev/null
+++ b/lean-mode/lean-info.el
@@ -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
+;; Maintainer: Gabriel Ebner
+;; 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)
diff --git a/lean-mode/lean-input.el b/lean-mode/lean-input.el
new file mode 100644
index 0000000000..dcbfdddf76
--- /dev/null
+++ b/lean-mode/lean-input.el
@@ -0,0 +1,1167 @@
+;;; lean-input.el --- The Lean input method (based/copied from Agda)
+;;;
+;;; DISCLAIMER: This file is based on agda-input.el provided with the Agda language.
+;;; We did minor modifications
+;;
+;;; Commentary:
+;;
+;;;; A highly customisable input method which can inherit from other
+;; Quail input methods. By default the input method is geared towards
+;; the input of mathematical and other symbols in Lean programs.
+;;
+;; Use M-x customize-group lean-input to customise this input method.
+;; Note that the functions defined under "Functions used to tweak
+;; translation pairs" below can be used to tweak both the key
+;; translations inherited from other input methods as well as the
+;; ones added specifically for this one.
+;;
+;; Use lean-input-show-translations to see all the characters which
+;; can be typed using this input method (except for those
+;; corresponding to ASCII characters).
+
+;;; Code:
+
+(require 'quail)
+
+(eval-when-compile
+ (require 'cl))
+;; Quail is quite stateful, so be careful when editing this code. Note
+;; that with-temp-buffer is used below whenever buffer-local state is
+;; modified.
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Utility functions
+
+(defun lean-input-concat-map (f xs)
+ "Concat (map F XS)."
+ (apply 'append (mapcar f xs)))
+
+(defun lean-input-to-string-list (s)
+ "Convert a string S to a list of one-character strings, after
+removing all space and newline characters."
+ (lean-input-concat-map
+ (lambda (c) (if (member c (string-to-list " \n"))
+ nil
+ (list (string c))))
+ (string-to-list s)))
+
+(defun lean-input-character-range (from to)
+ "A string consisting of the characters from FROM to TO."
+ (let (seq)
+ (dotimes (i (1+ (- to from)))
+ (setq seq (cons (+ from i) seq)))
+ (concat (nreverse seq))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Functions used to tweak translation pairs
+
+;; lexical-let is used since Elisp lacks lexical scoping.
+
+(defun lean-input-compose (f g)
+ "\x -> concatMap F (G x)"
+ (lexical-let ((f1 f) (g1 g))
+ (lambda (x) (lean-input-concat-map f1 (funcall g1 x)))))
+
+(defun lean-input-or (f g)
+ "\x -> F x ++ G x"
+ (lexical-let ((f1 f) (g1 g))
+ (lambda (x) (append (funcall f1 x) (funcall g1 x)))))
+
+(defun lean-input-nonempty ()
+ "Only keep pairs with a non-empty first component."
+ (lambda (x) (if (> (length (car x)) 0) (list x))))
+
+(defun lean-input-prepend (prefix)
+ "Prepend PREFIX to all key sequences."
+ (lexical-let ((prefix1 prefix))
+ (lambda (x) `((,(concat prefix1 (car x)) . ,(cdr x))))))
+
+(defun lean-input-prefix (prefix)
+ "Only keep pairs whose key sequence starts with PREFIX."
+ (lexical-let ((prefix1 prefix))
+ (lambda (x)
+ (if (equal (substring (car x) 0 (length prefix1)) prefix1)
+ (list x)))))
+
+(defun lean-input-suffix (suffix)
+ "Only keep pairs whose key sequence ends with SUFFIX."
+ (lexical-let ((suffix1 suffix))
+ (lambda (x)
+ (if (equal (substring (car x)
+ (- (length (car x)) (length suffix1)))
+ suffix1)
+ (list x)))))
+
+(defun lean-input-drop (ss)
+ "Drop pairs matching one of the given key sequences.
+SS should be a list of strings."
+ (lexical-let ((ss1 ss))
+ (lambda (x) (unless (member (car x) ss1) (list x)))))
+
+(defun lean-input-drop-beginning (n)
+ "Drop N characters from the beginning of each key sequence."
+ (lexical-let ((n1 n))
+ (lambda (x) `((,(substring (car x) n1) . ,(cdr x))))))
+
+(defun lean-input-drop-end (n)
+ "Drop N characters from the end of each key sequence."
+ (lexical-let ((n1 n))
+ (lambda (x)
+ `((,(substring (car x) 0 (- (length (car x)) n1)) .
+ ,(cdr x))))))
+
+(defun lean-input-drop-prefix (prefix)
+ "Only keep pairs whose key sequence starts with PREFIX.
+This prefix is dropped."
+ (lean-input-compose
+ (lean-input-drop-beginning (length prefix))
+ (lean-input-prefix prefix)))
+
+(defun lean-input-drop-suffix (suffix)
+ "Only keep pairs whose key sequence ends with SUFFIX.
+This suffix is dropped."
+ (lexical-let ((suffix1 suffix))
+ (lean-input-compose
+ (lean-input-drop-end (length suffix1))
+ (lean-input-suffix suffix1))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Customization
+
+;; The :set keyword is set to 'lean-input-incorporate-changed-setting
+;; so that the input method gets updated immediately when users
+;; customize it. However, the setup functions cannot be run before all
+;; variables have been defined. Hence the :initialize keyword is set to
+;; 'custom-initialize-default to ensure that the setup is not performed
+;; until lean-input-setup is called at the end of this file.
+
+(defgroup lean-input nil
+ "The Lean input method.
+After tweaking these settings you may want to inspect the resulting
+translations using `lean-input-show-translations'."
+ :group 'lean
+ :group 'leim)
+
+(defcustom lean-input-tweak-all
+ '(lean-input-compose
+ (lean-input-prepend "\\")
+ (lean-input-nonempty))
+ "An expression yielding a function which can be used to tweak
+all translations before they are included in the input method.
+The resulting function (if non-nil) is applied to every
+\(KEY-SEQUENCE . TRANSLATION) pair and should return a list of such
+pairs. (Note that the translations can be anything accepted by
+`quail-defrule'.)
+
+If you change this setting manually (without using the
+customization buffer) you need to call `lean-input-setup' in
+order for the change to take effect."
+ :group 'lean-input
+ :set 'lean-input-incorporate-changed-setting
+ :initialize 'custom-initialize-default
+ :type 'sexp)
+
+(defcustom lean-input-inherit
+ `(("TeX" . (lean-input-compose
+ (lean-input-drop '("geq" "leq" "bullet" "qed" "par"))
+ (lean-input-or
+ (lean-input-drop-prefix "\\")
+ (lean-input-or
+ (lean-input-compose
+ (lean-input-drop '("^o"))
+ (lean-input-prefix "^"))
+ (lean-input-prefix "_")))))
+ )
+ "A list of Quail input methods whose translations should be
+inherited by the Lean input method (with the exception of
+translations corresponding to ASCII characters).
+
+The list consists of pairs (qp . tweak), where qp is the name of
+a Quail package, and tweak is an expression of the same kind as
+`lean-input-tweak-all' which is used to tweak the translation
+pairs of the input method.
+
+The inherited translation pairs are added last, after
+`lean-input-user-translations' and `lean-input-translations'.
+
+If you change this setting manually (without using the
+customization buffer) you need to call `lean-input-setup' in
+order for the change to take effect."
+ :group 'lean-input
+ :set 'lean-input-incorporate-changed-setting
+ :initialize 'custom-initialize-default
+ :type '(repeat (cons (string :tag "Quail package")
+ (sexp :tag "Tweaking function"))))
+
+(defcustom lean-input-translations
+ (let ((max-lisp-eval-depth 2800)) `(
+
+ ;; Negation
+
+ ("not" . ("¬"))
+
+ ;; Equality and similar symbols.
+
+ ("eq" . ,(lean-input-to-string-list "=∼∽≈≋∻∾∿≀≃⋍≂≅ ≌≊≡≣≐≑≒≓≔≕≖≗≘≙≚≛≜≝≞≟≍≎≏≬⋕"))
+ ("eqn" . ,(lean-input-to-string-list "≠≁ ≉ ≄ ≇≆ ≢ ≭ "))
+ ("equiv" . ,(lean-input-to-string-list "≃⋍"))
+ ("iso" . ,(lean-input-to-string-list "≅≌"))
+
+ ("=n" . ("≠"))
+ ("~" . ("∼")) ("~n" . ("≁")) ("homotopy" . ("∼"))
+ ("~~" . ("≈")) ("~~n" . ("≉"))
+ ("~~~" . ("≋"))
+ (":~" . ("∻"))
+ ("~-" . ("≃")) ("~-n" . ("≄"))
+ ("-~" . ("≂"))
+ ("~=" . ("≅")) ("~=n" . ("≇"))
+ ("~~-" . ("≊"))
+ ("==" . ("≡")) ("==n" . ("≢"))
+ ("===" . ("≣"))
+ (".=" . ("≐")) (".=." . ("≑"))
+ (":=" . ("≔")) ("=:" . ("≕"))
+ ("=o" . ("≗"))
+ ("(=" . ("≘"))
+ ("and=" . ("≙")) ("or=" . ("≚"))
+ ("*=" . ("≛"))
+ ("t=" . ("≜"))
+ ("def=" . ("≝"))
+ ("m=" . ("≞"))
+ ("?=" . ("≟"))
+
+ ("pr" . ("↣"))
+
+ ("1" . ("₁"))
+ ("2" . ("₂"))
+ ("3" . ("₃"))
+ ("4" . ("₄"))
+ ("5" . ("₅"))
+ ("6" . ("₆"))
+ ("7" . ("₇"))
+ ("8" . ("₈"))
+ ("9" . ("₉"))
+ ("0" . ("₀"))
+
+ ;; Inequality and similar symbols.
+
+ ("leq" . ,(lean-input-to-string-list "≤≦≲<≪⋘ ≶≺≼≾⊂⊆ ⋐⊏⊑ ⊰⊲⊴⋖⋚⋜⋞"))
+ ("leqn" . ,(lean-input-to-string-list "≰≨≮≴⋦ ≸⊀ ⋨⊄⊈⊊ ⋢⋤ ⋪⋬ ⋠"))
+ ("geq" . ,(lean-input-to-string-list "≥≧≳>≫⋙ ≷≻≽≿⊃⊇ ⋑⊐⊒ ⊱⊳⊵⋗⋛⋝⋟"))
+ ("geqn" . ,(lean-input-to-string-list "≱≩≯≵⋧ ≹ ⊁ ⋩⊅⊉⊋ ⋣⋥ ⋫⋭ ⋡"))
+
+ ("<=" . ("≤")) (">=" . ("≥"))
+ ("<=n" . ("≰")) (">=n" . ("≱"))
+ ("len" . ("≰")) ("gen" . ("≱"))
+ ("n" . ("≯"))
+ ("<~" . ("≲")) (">~" . ("≳"))
+ ("<~n" . ("⋦")) (">~n" . ("⋧"))
+ ("<~nn" . ("≴")) (">~nn" . ("≵"))
+
+ ("ssub" . ("⊂")) ("ssup" . ("⊃"))
+ ("ssubn" . ("⊄")) ("ssupn" . ("⊅"))
+ ("sub" . ("⊆")) ("sup" . ("⊇"))
+ ("subn" . ("⊈")) ("supn" . ("⊉"))
+ ("ssqub" . ("⊏")) ("ssqup" . ("⊐"))
+ ("squb" . ("⊑")) ("squp" . ("⊒"))
+ ("squbn" . ("⋢")) ("squpn" . ("⋣"))
+
+ ;; Set membership etc.
+
+ ("member" . ,(lean-input-to-string-list "∈∉∊∋∌∍⋲⋳⋴⋵⋶⋷⋸⋹⋺⋻⋼⋽⋾⋿"))
+ ("mem" . ("∈"))
+
+ ("inn" . ("∉"))
+ ("nin" . ("∌"))
+
+ ;; Types
+
+ ("T1" . ("Type₁"))
+ ("T2" . ("Type₂"))
+ ("T+" . ("Type₊"))
+
+ ;; Intersections, unions etc.
+
+ ("intersection" . ,(lean-input-to-string-list "∩⋂∧⋀⋏⨇⊓⨅⋒∏ ⊼ ⨉"))
+ ("union" . ,(lean-input-to-string-list "∪⋃∨⋁⋎⨈⊔⨆⋓∐⨿⊽⊻⊍⨃⊎⨄⊌∑⅀"))
+
+ ("and" . ("∧")) ("or" . ("∨"))
+ ("And" . ("⋀")) ("Or" . ("⋁"))
+ ("i" . ("∩")) ("un" . ("∪")) ("u+" . ("⊎")) ("u." . ("⊍"))
+ ("I" . ("⋂")) ("Un" . ("⋃")) ("U+" . ("⨄")) ("U." . ("⨃"))
+ ("glb" . ("⊓")) ("lub" . ("⊔"))
+ ("Glb" . ("⨅")) ("Lub" . ("⨆"))
+
+ ;; Entailment etc.
+
+ ("entails" . ,(lean-input-to-string-list "⊢⊣⊤⊥⊦⊧⊨⊩⊪⊫⊬⊭⊮⊯"))
+
+ ("|-" . ("⊢")) ("|-n" . ("⊬"))
+ ("-|" . ("⊣"))
+ ("|=" . ("⊨")) ("|=n" . ("⊭"))
+ ("||-" . ("⊩")) ("||-n" . ("⊮"))
+ ("||=" . ("⊫")) ("||=n" . ("⊯"))
+ ("|||-" . ("⊪"))
+
+ ;; Divisibility, parallelity.
+
+ ("|" . ("∣")) ("|n" . ("∤"))
+ ("||" . ("∥")) ("||n" . ("∦"))
+
+ ;; Some symbols from logic and set theory.
+
+ ("all" . ("∀"))
+ ("ex" . ("∃"))
+ ("exn" . ("∄"))
+ ("0" . ("∅"))
+ ("empty" . ("∅"))
+ ("C" . ("∁"))
+ ("powerset" . ("𝒫"))
+
+ ;; Corners, ceilings and floors.
+
+ ("c" . ,(lean-input-to-string-list "⌜⌝⌞⌟⌈⌉⌊⌋"))
+ ("cu" . ,(lean-input-to-string-list "⌜⌝ ⌈⌉ "))
+ ("cl" . ,(lean-input-to-string-list " ⌞⌟ ⌊⌋"))
+
+ ("cul" . ("⌜")) ("cuL" . ("⌈"))
+ ("cur" . ("⌝")) ("cuR" . ("⌉"))
+ ("cll" . ("⌞")) ("clL" . ("⌊"))
+ ("clr" . ("⌟")) ("clR" . ("⌋"))
+
+ ;; Various operators/symbols.
+ ("tr" . ,(lean-input-to-string-list "⬝▹"))
+ ("trans" . ,(lean-input-to-string-list "▹⬝"))
+ ("transport" . ("▹"))
+ ("con" . ("⬝"))
+ ("cdot" . ("⬝"))
+ ("dot" . ("⬝"))
+ ("sy" . ("⁻¹"))
+ ("inv" . ("⁻¹"))
+ ("-1" . ("⁻¹" "₋₁"))
+ ("-1e" . ("⁻¹ᵉ"))
+ ("-1f" . ("⁻¹ᶠ"))
+ ("-1g" . ("⁻¹ᵍ"))
+ ("-1h" . ("⁻¹ʰ"))
+ ("-1i" . ("⁻¹ⁱ"))
+ ("-1m" . ("⁻¹ᵐ"))
+ ("-1o" . ("⁻¹ᵒ"))
+ ("-1r" . ("⁻¹ʳ"))
+ ("-1p" . ("⁻¹ᵖ"))
+ ("-1s" . ("⁻¹ˢ"))
+ ("-1v" . ("⁻¹ᵛ"))
+ ("-1E" . ("⁻¹ᴱ"))
+ ("-2" . ("⁻²" "₋₂"))
+ ("-2o" . ("⁻²ᵒ"))
+ ("-3" . ("⁻³"))
+ ("qed" . ("∎"))
+ ("x" . ("×"))
+ ("o" . ("∘"))
+ ("comp" . ("∘"))
+ ("." . ("∙"))
+ ("*" . ("⋆"))
+ (".+" . ("∔"))
+ (".-" . ("∸"))
+ (":" . ("∶"))
+ ("::" . ("∷"))
+ ("::-" . ("∺"))
+ ("-:" . ("∹"))
+ ("+ " . ("⊹"))
+ ("surd3" . ("∛"))
+ ("surd4" . ("∜"))
+ ("increment" . ("∆"))
+ ("inf" . ("∞"))
+ ("&" . ("⅋"))
+ ("op" . ("ᵒᵖ"))
+ ("opf" . ("ᵒᵖᶠ"))
+
+ ;; Circled operators.
+
+ ("o+" . ("⊕"))
+ ("o--" . ("⊖"))
+ ("ox" . ("⊗"))
+ ("o/" . ("⊘"))
+ ("o." . ("⊙"))
+ ("oo" . ("⊚"))
+ ("o*" . ("∘*" "⊛"))
+ ("o=" . ("⊜"))
+ ("o-" . ("⊝"))
+
+ ("O+" . ("⨁"))
+ ("Ox" . ("⨂"))
+ ("O." . ("⨀"))
+ ("O*" . ("⍟"))
+
+ ;; Boxed operators.
+
+ ("b+" . ("⊞"))
+ ("b-" . ("⊟"))
+ ("bx" . ("⊠"))
+ ("b." . ("⊡"))
+
+ ;; Various symbols.
+
+ ("integral" . ,(lean-input-to-string-list "∫∬∭∮∯∰∱∲∳"))
+ ("angle" . ,(lean-input-to-string-list "∟∡∢⊾⊿"))
+ ("join" . ,(lean-input-to-string-list "⋈⋉⋊⋋⋌⨝⟕⟖⟗"))
+
+ ;; Arrows.
+ ("iff" . ("↔")) ("imp" . ("→"))
+ ("l" . ,(lean-input-to-string-list "←⇐⇚⇇⇆↤⇦↞↼↽⇠⇺↜⇽⟵⟸↚⇍⇷ ↹ ↢↩↫⇋⇜⇤⟻⟽⤆↶↺⟲ "))
+ ("r" . ,(lean-input-to-string-list "→⇒⇛⇉⇄↦⇨↠⇀⇁⇢⇻↝⇾⟶⟹↛⇏⇸⇶ ↴ ↣↪↬⇌⇝⇥⟼⟾⤇↷↻⟳⇰⇴⟴⟿ ➵➸➙➔➛➜➝➞➟➠➡➢➣➤➧➨➩➪➫➬➭➮➯➱➲➳➺➻➼➽➾⊸"))
+ ("u" . ,(lean-input-to-string-list "↑⇑⟰⇈⇅↥⇧↟↿↾⇡⇞ ↰↱➦ ⇪⇫⇬⇭⇮⇯ "))
+ ("d" . ,(lean-input-to-string-list "↓⇓⟱⇊⇵↧⇩↡⇃⇂⇣⇟ ↵↲↳➥ ↯ "))
+ ("ud" . ,(lean-input-to-string-list "↕⇕ ↨⇳ "))
+ ("lr" . ,(lean-input-to-string-list "↔⇔ ⇼↭⇿⟷⟺↮⇎⇹ "))
+ ("ul" . ,(lean-input-to-string-list "↖⇖ ⇱↸ "))
+ ("ur" . ,(lean-input-to-string-list "↗⇗ ➶➹➚ "))
+ ("dr" . ,(lean-input-to-string-list "↘⇘ ⇲ ➴➷➘ "))
+ ("dl" . ,(lean-input-to-string-list "↙⇙ "))
+ ("==>" . ("⟹")) ("nattrans" . ("⟹")) ("nat_trans" . ("⟹"))
+
+ ("l-" . ("←")) ("<-" . ("←")) ("l=" . ("⇐"))
+ ("r-" . ("→")) ("->" . ("→")) ("r=" . ("⇒")) ("=>" . ("⇒")) ("functor" . ("⇒"))
+ ("u-" . ("↑")) ("u=" . ("⇑"))
+ ("d-" . ("↓")) ("d=" . ("⇓"))
+ ("ud-" . ("↕")) ("ud=" . ("⇕"))
+ ("lr-" . ("↔")) ("<->" . ("↔")) ("lr=" . ("⇔")) ("<=>" . ("⇔"))
+ ("ul-" . ("↖")) ("ul=" . ("⇖"))
+ ("ur-" . ("↗")) ("ur=" . ("⇗"))
+ ("dr-" . ("↘")) ("dr=" . ("⇘"))
+ ("dl-" . ("↙")) ("dl=" . ("⇙"))
+
+ ("l==" . ("⇚")) ("l-2" . ("⇇")) ("l-r-" . ("⇆"))
+ ("r==" . ("⇛")) ("r-2" . ("⇉")) ("r-3" . ("⇶")) ("r-l-" . ("⇄"))
+ ("u==" . ("⟰")) ("u-2" . ("⇈")) ("u-d-" . ("⇅"))
+ ("d==" . ("⟱")) ("d-2" . ("⇊")) ("d-u-" . ("⇵"))
+
+ ("l--" . ("⟵")) ("<--" . ("⟵")) ("l~" . ("↜" "⇜"))
+ ("r--" . ("⟶")) ("-->" . ("⟶")) ("r~" . ("↝" "⇝" "⟿")) ("hom" . ("⟶"))
+ ("lr--" . ("⟷")) ("<-->" . ("⟷")) ("lr~" . ("↭"))
+
+ ("l-n" . ("↚")) ("<-n" . ("↚")) ("l=n" . ("⇍"))
+ ("r-n" . ("↛")) ("->n" . ("↛")) ("r=n" . ("⇏")) ("=>n" . ("⇏"))
+ ("lr-n" . ("↮")) ("<->n" . ("↮")) ("lr=n" . ("⇎")) ("<=>n" . ("⇎"))
+
+ ("l-|" . ("↤")) ("ll-" . ("↞"))
+ ("r-|" . ("↦")) ("rr-" . ("↠"))
+ ("u-|" . ("↥")) ("uu-" . ("↟"))
+ ("d-|" . ("↧")) ("dd-" . ("↡"))
+ ("ud-|" . ("↨"))
+
+ ("l->" . ("↢"))
+ ("r->" . ("↣"))
+
+ ("r-o" . ("⊸")) ("-o" . ("⊸"))
+
+ ("dz" . ("↯"))
+
+ ;; Ellipsis.
+
+ ("..." . ,(lean-input-to-string-list "⋯⋮⋰⋱"))
+
+ ;; Box-drawing characters.
+
+ ("---" . ,(lean-input-to-string-list "─│┌┐└┘├┤┬┼┴╴╵╶╷╭╮╯╰╱╲╳"))
+ ("--=" . ,(lean-input-to-string-list "═║╔╗╚╝╠╣╦╬╩ ╒╕╘╛╞╡╤╪╧ ╓╖╙╜╟╢╥╫╨"))
+ ("--_" . ,(lean-input-to-string-list "━┃┏┓┗┛┣┫┳╋┻╸╹╺╻
+ ┍┯┑┕┷┙┝┿┥┎┰┒┖┸┚┠╂┨┞╀┦┟╁┧┢╈┪┡╇┩
+ ┮┭┶┵┾┽┲┱┺┹╊╉╆╅╄╃ ╿╽╼╾"))
+ ("--." . ,(lean-input-to-string-list "╌╎┄┆┈┊
+ ╍╏┅┇┉┋"))
+
+ ;; Triangles.
+
+ ;; Big/small, black/white.
+
+ ("t" . ,(lean-input-to-string-list "▸▹►▻◂◃◄◅▴▵▾▿◢◿◣◺◤◸◥◹"))
+ ("Tr" . ,(lean-input-to-string-list "◀◁▶▷▲△▼▽◬◭◮"))
+
+ ("tb" . ,(lean-input-to-string-list "◂▸▴▾◄►◢◣◤◥"))
+ ("tw" . ,(lean-input-to-string-list "◃▹▵▿◅▻◿◺◸◹"))
+
+ ("Tb" . ,(lean-input-to-string-list "◀▶▲▼"))
+ ("Tw" . ,(lean-input-to-string-list "◁▷△▽"))
+
+ ;; Squares.
+
+ ("sq" . ,(lean-input-to-string-list "◾◽■□◼◻▣▢▤▥▦▧▨▩◧◨◩◪◫◰◱◲◳"))
+ ("sqb" . ,(lean-input-to-string-list "■◼◾"))
+ ("sqw" . ,(lean-input-to-string-list "□◻◽"))
+ ("sq." . ("▣"))
+ ("sqo" . ("▢"))
+
+ ;; Rectangles.
+
+ ("re" . ,(lean-input-to-string-list "▬▭▮▯"))
+ ("reb" . ,(lean-input-to-string-list "▬▮"))
+ ("rew" . ,(lean-input-to-string-list "▭▯"))
+
+ ;; Parallelograms.
+
+ ("pa" . ,(lean-input-to-string-list "▰▱"))
+ ("pab" . ("▰"))
+ ("paw" . ("▱"))
+
+ ;; Diamonds.
+
+ ("di" . ,(lean-input-to-string-list "◆◇◈"))
+ ("dib" . ("◆"))
+ ("diw" . ("◇"))
+ ("di." . ("◈"))
+
+ ;; Circles.
+
+ ("ci" . ,(lean-input-to-string-list "●○◎◌◯◍◐◑◒◓◔◕◖◗◠◡◴◵◶◷⚆⚇⚈⚉"))
+ ("cib" . ("●"))
+ ("ciw" . ("○"))
+ ("ci." . ("◎"))
+ ("ci.." . ("◌"))
+ ("ciO" . ("◯"))
+
+ ;; Stars.
+
+ ("st" . ,(lean-input-to-string-list "⋆✦✧✶✴✹ ★☆✪✫✯✰✵✷✸"))
+ ("st4" . ,(lean-input-to-string-list "✦✧"))
+ ("st6" . ("✶"))
+ ("st8" . ("✴"))
+ ("st12" . ("✹"))
+
+ ;; Blackboard bold letters.
+
+ ("bn" . ("ℕ"))
+ ("bz" . ("ℤ"))
+ ("bq" . ("ℚ"))
+ ("br" . ("ℝ"))
+ ("bc" . ("ℂ"))
+ ("bp" . ("ℙ"))
+ ("bb" . ("𝔹"))
+ ("bsum" . ("⅀"))
+
+ ;; Blackboard bold numbers.
+
+ ("b0" . ("𝟘"))
+ ("b1" . ("𝟙"))
+ ("b2" . ("𝟚"))
+ ("b3" . ("𝟛"))
+ ("b4" . ("𝟜"))
+ ("b5" . ("𝟝"))
+ ("b6" . ("𝟞"))
+ ("b7" . ("𝟟"))
+ ("b8" . ("𝟠"))
+ ("b9" . ("𝟡"))
+
+ ;; Parentheses.
+
+ ("(" . ,(lean-input-to-string-list "([{⁅⁽₍〈⎴⟅⟦⟨⟪⦃〈《‹«「『【〔〖〚︵︷︹︻︽︿﹁﹃﹙﹛﹝（［｛｢"))
+ (")" . ,(lean-input-to-string-list ")]}⁆⁾₎〉⎵⟆⟧⟩⟫⦄〉》›»」』】〕〗〛︶︸︺︼︾﹀﹂﹄﹚﹜﹞）］｝｣"))
+
+ ("[[" . ("⟦"))
+ ("]]" . ("⟧"))
+ ("<" . ("⟨"))
+ (">" . ("⟩"))
+ ("<<" . ("⟪"))
+ (">>" . ("⟫"))
+ ("f<" . ("‹"))
+ ("f>" . ("›"))
+ ("f<<" . ("«"))
+ ("f>>" . ("»"))
+ ("{{" . ("⦃"))
+ ("}}" . ("⦄"))
+
+ ("(b" . ("⟅"))
+ (")b" . ("⟆"))
+
+ ("lbag" . ("⟅"))
+ ("rbag" . ("⟆"))
+
+ ;; lambda
+
+ ("fun" . ("λ"))
+ ("lam" . ("λ"))
+
+ ("X" . ("⨯"))
+
+ ;; Primes.
+
+ ("'" . ,(lean-input-to-string-list "′″‴⁗"))
+ ("`" . ,(lean-input-to-string-list "‵‶‷"))
+
+ ;; Fractions.
+
+ ("frac" . ,(lean-input-to-string-list "¼½¾⅓⅔⅕⅖⅗⅘⅙⅚⅛⅜⅝⅞⅟"))
+
+ ;; Bullets.
+
+ ("bu" . ,(lean-input-to-string-list "•◦‣⁌⁍"))
+ ("bub" . ("•"))
+ ("buw" . ("◦"))
+ ("but" . ("‣"))
+
+ ;; Types
+ ("nat" . ("ℕ"))
+ ("Nat" . ("ℕ"))
+ ("N" . ("ℕ"))
+ ("N-2" . ("ℕ₋₂"))
+ ("N-1" . ("ℕ₋₁"))
+ ("int" . ("ℤ"))
+ ("Int" . ("ℤ"))
+ ("Z" . ("ℤ"))
+ ("rat" . ("ℚ"))
+ ("Rat" . ("ℚ"))
+ ("Q" . ("ℚ"))
+ ("real" . ("ℝ"))
+ ("Real" . ("ℝ"))
+ ("R" . ("ℝ"))
+ ("Com" . ("ℂ"))
+ ("com" . ("ℂ"))
+ ("C" . ("ℂ"))
+ ("A" . ("𝔸"))
+ ("F" . ("𝔽"))
+ ("H" . ("ℍ"))
+ ("K" . ("𝕂"))
+
+ ("a" . ("α"))
+ ("b" . ("β"))
+ ("g" . ("γ"))
+
+ ;; Musical symbols.
+
+ ("note" . ,(lean-input-to-string-list "♩♪♫♬"))
+ ("flat" . ("♭"))
+ ("#" . ("♯"))
+
+ ;; Other punctuation and symbols.
+
+ ("\\" . ("\\"))
+ ("en" . ("–"))
+ ("em" . ("—"))
+ ("^i" . ("ⁱ"))
+ ("^o" . ("ᵒ"))
+ ("!!" . ("‼"))
+ ("??" . ("⁇"))
+ ("?!" . ("‽" "⁈"))
+ ("!?" . ("⁉"))
+ ("die" . ,(lean-input-to-string-list "⚀⚁⚂⚃⚄⚅"))
+ ("asterisk" . ,(lean-input-to-string-list "⁎⁑⁂✢✣✤✥✱✲✳✺✻✼✽❃❉❊❋"))
+ ("8<" . ("✂" "✄"))
+ ("tie" . ("⁀"))
+ ("undertie" . ("‿"))
+ ("apl" . ,(lean-input-to-string-list "⌶⌷⌸⌹⌺⌻⌼⌽⌾⌿⍀⍁⍂⍃⍄⍅⍆⍇⍈
+ ⍉⍊⍋⍌⍍⍎⍏⍐⍑⍒⍓⍔⍕⍖⍗⍘⍙⍚⍛
+ ⍜⍝⍞⍟⍠⍡⍢⍣⍤⍥⍦⍧⍨⍩⍪⍫⍬⍭⍮
+ ⍯⍰⍱⍲⍳⍴⍵⍶⍷⍸⍹⍺⎕"))
+
+ ;; Some combining characters.
+ ;;
+ ;; The following combining characters also have (other)
+ ;; translations:
+ ;; ̀ ́ ̂ ̃ ̄ ̆ ̇ ̈ ̋ ̌ ̣ ̧ ̱
+
+ ("^--" . ,(lean-input-to-string-list"̅̿"))
+ ("_--" . ,(lean-input-to-string-list"̲̳"))
+ ("^~" . ,(lean-input-to-string-list"̃͌"))
+ ("_~" . ( "̰"))
+ ("^." . ,(lean-input-to-string-list"̇̈⃛⃜"))
+ ("_." . ,(lean-input-to-string-list"̣̤"))
+ ("^l" . ,(lean-input-to-string-list"⃖⃐⃔"))
+ ("^l-" . ( "⃖"))
+ ("^r" . ,(lean-input-to-string-list"⃗⃑⃕"))
+ ("^r-" . ( "⃗"))
+ ("^lr" . ( "⃡"))
+ ("_lr" . ( "͍"))
+ ("^^" . ,(lean-input-to-string-list"̂̑͆"))
+ ("_^" . ,(lean-input-to-string-list"̭̯̪"))
+ ("^v" . ,(lean-input-to-string-list"̌̆"))
+ ("_v" . ,(lean-input-to-string-list"̬̮̺"))
+
+ ;; Shorter forms of many greek letters plus ƛ.
+
+ ("Ga" . ("α")) ("GA" . ("Α"))
+ ("Gb" . ("β")) ("GB" . ("Β"))
+ ("Gg" . ("γ")) ("GG" . ("Γ"))
+ ("Gd" . ("δ")) ("GD" . ("Δ"))
+ ("Ge" . ("ε")) ("GE" . ("Ε")) ("eps" . ("ε"))
+ ("Gz" . ("ζ")) ("GZ" . ("Ζ"))
+ ;; \eta \Eta
+ ("Gth" . ("θ")) ("GTH" . ("Θ")) ("th" . ("θ"))
+ ("Gi" . ("ι")) ("GI" . ("Ι"))
+ ("Gk" . ("κ")) ("GK" . ("Κ"))
+ ("Gl" . ("λ")) ("GL" . ("Λ")) ("Gl-" . ("ƛ"))
+ ("Gm" . ("μ")) ("GM" . ("Μ"))
+ ("Gn" . ("ν")) ("GN" . ("Ν"))
+ ("Gx" . ("ξ")) ("GX" . ("Ξ"))
+ ;; \omicron \Omicron
+ ;; \pi \Pi
+ ("Gr" . ("ρ")) ("GR" . ("Ρ"))
+ ("Gs" . ("σ")) ("GS" . ("Σ"))
+ ("Gt" . ("τ")) ("GT" . ("Τ"))
+ ("Gu" . ("υ")) ("GU" . ("Υ"))
+ ("Gf" . ("φ")) ("GF" . ("Φ"))
+ ("Gc" . ("χ")) ("GC" . ("Χ"))
+ ("Gp" . ("ψ")) ("GP" . ("Ψ"))
+ ("Go" . ("ω")) ("GO" . ("Ω"))
+ ;; even shorter versions for central type constructors
+ ("S" . ("Σ")) ("P" . ("Π"))
+
+ ;; Mathematical characters
+
+ ("MiA" . ("𝐴"))
+ ("MiB" . ("𝐵"))
+ ("MiC" . ("𝐶"))
+ ("MiD" . ("𝐷"))
+ ("MiE" . ("𝐸"))
+ ("MiF" . ("𝐹"))
+ ("MiG" . ("𝐺"))
+ ("MiH" . ("𝐻"))
+ ("MiI" . ("𝐼"))
+ ("MiJ" . ("𝐽"))
+ ("MiK" . ("𝐾"))
+ ("MiL" . ("𝐿"))
+ ("MiM" . ("𝑀"))
+ ("MiN" . ("𝑁"))
+ ("MiO" . ("𝑂"))
+ ("MiP" . ("𝑃"))
+ ("MiQ" . ("𝑄"))
+ ("MiR" . ("𝑅"))
+ ("MiS" . ("𝑆"))
+ ("MiT" . ("𝑇"))
+ ("MiU" . ("𝑈"))
+ ("MiV" . ("𝑉"))
+ ("MiW" . ("𝑊"))
+ ("MiX" . ("𝑋"))
+ ("MiY" . ("𝑌"))
+ ("MiZ" . ("𝑍"))
+ ("Mia" . ("𝑎"))
+ ("Mib" . ("𝑏"))
+ ("Mic" . ("𝑐"))
+ ("Mid" . ("𝑑"))
+ ("Mie" . ("𝑒"))
+ ("Mif" . ("𝑓"))
+ ("Mig" . ("𝑔"))
+ ("Mii" . ("𝑖"))
+ ("Mij" . ("𝑗"))
+ ("Mik" . ("𝑘"))
+ ("Mil" . ("𝑙"))
+ ("Mim" . ("𝑚"))
+ ("Min" . ("𝑛"))
+ ("Mio" . ("𝑜"))
+ ("Mip" . ("𝑝"))
+ ("Miq" . ("𝑞"))
+ ("Mir" . ("𝑟"))
+ ("Mis" . ("𝑠"))
+ ("Mit" . ("𝑡"))
+ ("Miu" . ("𝑢"))
+ ("Miv" . ("𝑣"))
+ ("Miw" . ("𝑤"))
+ ("Mix" . ("𝑥"))
+ ("Miy" . ("𝑦"))
+ ("Miz" . ("𝑧"))
+ ("MIA" . ("𝑨"))
+ ("MIB" . ("𝑩"))
+ ("MIC" . ("𝑪"))
+ ("MID" . ("𝑫"))
+ ("MIE" . ("𝑬"))
+ ("MIF" . ("𝑭"))
+ ("MIG" . ("𝑮"))
+ ("MIH" . ("𝑯"))
+ ("MII" . ("𝑰"))
+ ("MIJ" . ("𝑱"))
+ ("MIK" . ("𝑲"))
+ ("MIL" . ("𝑳"))
+ ("MIM" . ("𝑴"))
+ ("MIN" . ("𝑵"))
+ ("MIO" . ("𝑶"))
+ ("MIP" . ("𝑷"))
+ ("MIQ" . ("𝑸"))
+ ("MIR" . ("𝑹"))
+ ("MIS" . ("𝑺"))
+ ("MIT" . ("𝑻"))
+ ("MIU" . ("𝑼"))
+ ("MIV" . ("𝑽"))
+ ("MIW" . ("𝑾"))
+ ("MIX" . ("𝑿"))
+ ("MIY" . ("𝒀"))
+ ("MIZ" . ("𝒁"))
+ ("MIa" . ("𝒂"))
+ ("MIb" . ("𝒃"))
+ ("MIc" . ("𝒄"))
+ ("MId" . ("𝒅"))
+ ("MIe" . ("𝒆"))
+ ("MIf" . ("𝒇"))
+ ("MIg" . ("𝒈"))
+ ("MIh" . ("𝒉"))
+ ("MIi" . ("𝒊"))
+ ("MIj" . ("𝒋"))
+ ("MIk" . ("𝒌"))
+ ("MIl" . ("𝒍"))
+ ("MIm" . ("𝒎"))
+ ("MIn" . ("𝒏"))
+ ("MIo" . ("𝒐"))
+ ("MIp" . ("𝒑"))
+ ("MIq" . ("𝒒"))
+ ("MIr" . ("𝒓"))
+ ("MIs" . ("𝒔"))
+ ("MIt" . ("𝒕"))
+ ("MIu" . ("𝒖"))
+ ("MIv" . ("𝒗"))
+ ("MIw" . ("𝒘"))
+ ("MIx" . ("𝒙"))
+ ("MIy" . ("𝒚"))
+ ("MIz" . ("𝒛"))
+ ("McA" . ("𝒜"))
+ ("McC" . ("𝒞"))
+ ("McD" . ("𝒟"))
+ ("McG" . ("𝒢"))
+ ("McJ" . ("𝒥"))
+ ("McK" . ("𝒦"))
+ ("McN" . ("𝒩"))
+ ("McO" . ("𝒪"))
+ ("McP" . ("𝒫"))
+ ("McQ" . ("𝒬"))
+ ("McS" . ("𝒮"))
+ ("McT" . ("𝒯"))
+ ("McU" . ("𝒰"))
+ ("McV" . ("𝒱"))
+ ("McW" . ("𝒲"))
+ ("McX" . ("𝒳"))
+ ("McY" . ("𝒴"))
+ ("McZ" . ("𝒵"))
+ ("Mca" . ("𝒶"))
+ ("Mcb" . ("𝒷"))
+ ("Mcc" . ("𝒸"))
+ ("Mcd" . ("𝒹"))
+ ("Mcf" . ("𝒻"))
+ ("Mch" . ("𝒽"))
+ ("Mci" . ("𝒾"))
+ ("Mcj" . ("𝒿"))
+ ("Mck" . ("𝓀"))
+ ("Mcl" . ("𝓁"))
+ ("Mcm" . ("𝓂"))
+ ("Mcn" . ("𝓃"))
+ ("Mcp" . ("𝓅"))
+ ("Mcq" . ("𝓆"))
+ ("Mcr" . ("𝓇"))
+ ("Mcs" . ("𝓈"))
+ ("Mct" . ("𝓉"))
+ ("Mcu" . ("𝓊"))
+ ("Mcv" . ("𝓋"))
+ ("Mcw" . ("𝓌"))
+ ("Mcx" . ("𝓍"))
+ ("Mcy" . ("𝓎"))
+ ("Mcz" . ("𝓏"))
+ ("MCA" . ("𝓐"))
+ ("MCB" . ("𝓑"))
+ ("MCC" . ("𝓒"))
+ ("MCD" . ("𝓓"))
+ ("MCE" . ("𝓔"))
+ ("MCF" . ("𝓕"))
+ ("MCG" . ("𝓖"))
+ ("MCH" . ("𝓗"))
+ ("MCI" . ("𝓘"))
+ ("MCJ" . ("𝓙"))
+ ("MCK" . ("𝓚"))
+ ("MCL" . ("𝓛"))
+ ("MCM" . ("𝓜"))
+ ("MCN" . ("𝓝"))
+ ("MCO" . ("𝓞"))
+ ("MCP" . ("𝓟"))
+ ("MCQ" . ("𝓠"))
+ ("MCR" . ("𝓡"))
+ ("MCS" . ("𝓢"))
+ ("MCT" . ("𝓣"))
+ ("MCU" . ("𝓤"))
+ ("MCV" . ("𝓥"))
+ ("MCW" . ("𝓦"))
+ ("MCX" . ("𝓧"))
+ ("MCY" . ("𝓨"))
+ ("MCZ" . ("𝓩"))
+ ("MCa" . ("𝓪"))
+ ("MCb" . ("𝓫"))
+ ("MCc" . ("𝓬"))
+ ("MCd" . ("𝓭"))
+ ("MCe" . ("𝓮"))
+ ("MCf" . ("𝓯"))
+ ("MCg" . ("𝓰"))
+ ("MCh" . ("𝓱"))
+ ("MCi" . ("𝓲"))
+ ("MCj" . ("𝓳"))
+ ("MCk" . ("𝓴"))
+ ("MCl" . ("𝓵"))
+ ("MCm" . ("𝓶"))
+ ("MCn" . ("𝓷"))
+ ("MCo" . ("𝓸"))
+ ("MCp" . ("𝓹"))
+ ("MCq" . ("𝓺"))
+ ("MCr" . ("𝓻"))
+ ("MCs" . ("𝓼"))
+ ("MCt" . ("𝓽"))
+ ("MCu" . ("𝓾"))
+ ("MCv" . ("𝓿"))
+ ("MCw" . ("𝔀"))
+ ("MCx" . ("𝔁"))
+ ("MCy" . ("𝔂"))
+ ("MCz" . ("𝔃"))
+ ("MfA" . ("𝔄"))
+ ("MfB" . ("𝔅"))
+ ("MfD" . ("𝔇"))
+ ("MfE" . ("𝔈"))
+ ("MfF" . ("𝔉"))
+ ("MfG" . ("𝔊"))
+ ("MfJ" . ("𝔍"))
+ ("MfK" . ("𝔎"))
+ ("MfL" . ("𝔏"))
+ ("MfM" . ("𝔐"))
+ ("MfN" . ("𝔑"))
+ ("MfO" . ("𝔒"))
+ ("MfP" . ("𝔓"))
+ ("MfQ" . ("𝔔"))
+ ("MfS" . ("𝔖"))
+ ("MfT" . ("𝔗"))
+ ("MfU" . ("𝔘"))
+ ("MfV" . ("𝔙"))
+ ("MfW" . ("𝔚"))
+ ("MfX" . ("𝔛"))
+ ("MfY" . ("𝔜"))
+ ("Mfa" . ("𝔞"))
+ ("Mfb" . ("𝔟"))
+ ("Mfc" . ("𝔠"))
+ ("Mfd" . ("𝔡"))
+ ("Mfe" . ("𝔢"))
+ ("Mff" . ("𝔣"))
+ ("Mfg" . ("𝔤"))
+ ("Mfh" . ("𝔥"))
+ ("Mfi" . ("𝔦"))
+ ("Mfj" . ("𝔧"))
+ ("Mfk" . ("𝔨"))
+ ("Mfl" . ("𝔩"))
+ ("Mfm" . ("𝔪"))
+ ("Mfn" . ("𝔫"))
+ ("Mfo" . ("𝔬"))
+ ("Mfp" . ("𝔭"))
+ ("Mfq" . ("𝔮"))
+ ("Mfr" . ("𝔯"))
+ ("Mfs" . ("𝔰"))
+ ("Mft" . ("𝔱"))
+ ("Mfu" . ("𝔲"))
+ ("Mfv" . ("𝔳"))
+ ("Mfw" . ("𝔴"))
+ ("Mfx" . ("𝔵"))
+ ("Mfy" . ("𝔶"))
+ ("Mfz" . ("𝔷"))
+
+ ;; Some ISO8859-1 characters.
+
+ (" " . (" "))
+ ("!" . ("¡"))
+ ("cent" . ("¢"))
+ ("brokenbar" . ("¦"))
+ ("degree" . ("°"))
+ ("?" . ("¿"))
+ ("^a_" . ("ª"))
+ ("^o_" . ("º"))
+
+ ;; Circled, parenthesised etc. numbers and letters.
+
+ ( "(0)" . ,(lean-input-to-string-list " ⓪"))
+ ( "(1)" . ,(lean-input-to-string-list "⑴①⒈❶➀➊"))
+ ( "(2)" . ,(lean-input-to-string-list "⑵②⒉❷➁➋"))
+ ( "(3)" . ,(lean-input-to-string-list "⑶③⒊❸➂➌"))
+ ( "(4)" . ,(lean-input-to-string-list "⑷④⒋❹➃➍"))
+ ( "(5)" . ,(lean-input-to-string-list "⑸⑤⒌❺➄➎"))
+ ( "(6)" . ,(lean-input-to-string-list "⑹⑥⒍❻➅➏"))
+ ( "(7)" . ,(lean-input-to-string-list "⑺⑦⒎❼➆➐"))
+ ( "(8)" . ,(lean-input-to-string-list "⑻⑧⒏❽➇➑"))
+ ( "(9)" . ,(lean-input-to-string-list "⑼⑨⒐❾➈➒"))
+ ("(10)" . ,(lean-input-to-string-list "⑽⑩⒑❿➉➓"))
+ ("(11)" . ,(lean-input-to-string-list "⑾⑪⒒"))
+ ("(12)" . ,(lean-input-to-string-list "⑿⑫⒓"))
+ ("(13)" . ,(lean-input-to-string-list "⒀⑬⒔"))
+ ("(14)" . ,(lean-input-to-string-list "⒁⑭⒕"))
+ ("(15)" . ,(lean-input-to-string-list "⒂⑮⒖"))
+ ("(16)" . ,(lean-input-to-string-list "⒃⑯⒗"))
+ ("(17)" . ,(lean-input-to-string-list "⒄⑰⒘"))
+ ("(18)" . ,(lean-input-to-string-list "⒅⑱⒙"))
+ ("(19)" . ,(lean-input-to-string-list "⒆⑲⒚"))
+ ("(20)" . ,(lean-input-to-string-list "⒇⑳⒛"))
+
+ ("(a)" . ,(lean-input-to-string-list "⒜Ⓐⓐ"))
+ ("(b)" . ,(lean-input-to-string-list "⒝Ⓑⓑ"))
+ ("(c)" . ,(lean-input-to-string-list "⒞Ⓒⓒ"))
+ ("(d)" . ,(lean-input-to-string-list "⒟Ⓓⓓ"))
+ ("(e)" . ,(lean-input-to-string-list "⒠Ⓔⓔ"))
+ ("(f)" . ,(lean-input-to-string-list "⒡Ⓕⓕ"))
+ ("(g)" . ,(lean-input-to-string-list "⒢Ⓖⓖ"))
+ ("(h)" . ,(lean-input-to-string-list "⒣Ⓗⓗ"))
+ ("(i)" . ,(lean-input-to-string-list "⒤Ⓘⓘ"))
+ ("(j)" . ,(lean-input-to-string-list "⒥Ⓙⓙ"))
+ ("(k)" . ,(lean-input-to-string-list "⒦Ⓚⓚ"))
+ ("(l)" . ,(lean-input-to-string-list "⒧Ⓛⓛ"))
+ ("(m)" . ,(lean-input-to-string-list "⒨Ⓜⓜ"))
+ ("(n)" . ,(lean-input-to-string-list "⒩Ⓝⓝ"))
+ ("(o)" . ,(lean-input-to-string-list "⒪Ⓞⓞ"))
+ ("(p)" . ,(lean-input-to-string-list "⒫Ⓟⓟ"))
+ ("(q)" . ,(lean-input-to-string-list "⒬Ⓠⓠ"))
+ ("(r)" . ,(lean-input-to-string-list "⒭Ⓡⓡ"))
+ ("(s)" . ,(lean-input-to-string-list "⒮Ⓢⓢ"))
+ ("(t)" . ,(lean-input-to-string-list "⒯Ⓣⓣ"))
+ ("(u)" . ,(lean-input-to-string-list "⒰Ⓤⓤ"))
+ ("(v)" . ,(lean-input-to-string-list "⒱Ⓥⓥ"))
+ ("(w)" . ,(lean-input-to-string-list "⒲Ⓦⓦ"))
+ ("(x)" . ,(lean-input-to-string-list "⒳Ⓧⓧ"))
+ ("(y)" . ,(lean-input-to-string-list "⒴Ⓨⓨ"))
+ ("(z)" . ,(lean-input-to-string-list "⒵Ⓩⓩ"))
+ ("y" . ("ɏ"))
+
+
+ ))
+ "A list of translations specific to the Lean input method.
+Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS).
+All the translation strings are possible translations
+of the given key sequence; if there is more than one you can choose
+between them using the arrow keys.
+
+Note that if you customize this setting you will not
+automatically benefit (or suffer) from modifications to its
+default value when the library is updated. If you just want to
+add some bindings it is probably a better idea to customize
+`lean-input-user-translations'.
+
+These translation pairs are included after those in
+`lean-input-user-translations', but before the ones inherited
+from other input methods (see `lean-input-inherit').
+
+If you change this setting manually (without using the
+customization buffer) you need to call `lean-input-setup' in
+order for the change to take effect."
+ :group 'lean-input
+ :set 'lean-input-incorporate-changed-setting
+ :initialize 'custom-initialize-default
+ :type '(repeat (cons (string :tag "Key sequence")
+ (repeat :tag "Translations" string))))
+
+(defcustom lean-input-user-translations nil
+ "Like `lean-input-translations', but more suitable for user
+customizations since by default it is empty.
+
+These translation pairs are included first, before those in
+`lean-input-translations' and the ones inherited from other input
+methods."
+ :group 'lean-input
+ :set 'lean-input-incorporate-changed-setting
+ :initialize 'custom-initialize-default
+ :type '(repeat (cons (string :tag "Key sequence")
+ (repeat :tag "Translations" string))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Inspecting and modifying translation maps
+
+(defun lean-input-get-translations (qp)
+ "Return a list containing all translations from the Quail
+package QP (except for those corresponding to ASCII).
+Each pair in the list has the form (KEY-SEQUENCE . TRANSLATION)."
+ (with-temp-buffer
+ (activate-input-method qp) ; To make sure that the package is loaded.
+ (unless (quail-package qp)
+ (error "%s is not a Quail package." qp))
+ (let ((decode-map (list 'decode-map)))
+ (quail-build-decode-map (list (quail-map)) "" decode-map 0)
+ (cdr decode-map))))
+
+(defun lean-input-show-translations (qp)
+ "Display all translations used by the Quail package QP (a string).
+\(Except for those corresponding to ASCII)."
+ (interactive (list (read-input-method-name
+ "Quail input method (default %s): " "Lean")))
+ (let ((buf (concat "*" qp " input method translations*")))
+ (with-output-to-temp-buffer buf
+ (with-current-buffer buf
+ (quail-insert-decode-map
+ (cons 'decode-map (lean-input-get-translations qp)))))))
+
+(defun lean-input-add-translations (trans)
+ "Add the given translations TRANS to the Lean input method.
+TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION). The
+translations are appended to the current translations."
+ (with-temp-buffer
+ (dolist (tr (lean-input-concat-map (eval lean-input-tweak-all) trans))
+ (quail-defrule (car tr) (cdr tr) "Lean" t))))
+
+(defun lean-input-inherit-package (qp &optional fun)
+ "Let the Lean input method inherit the translations from the
+Quail package QP (except for those corresponding to ASCII).
+
+The optional function FUN can be used to modify the translations.
+It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return
+a list of such pairs."
+ (let ((trans (lean-input-get-translations qp)))
+ (lean-input-add-translations
+ (if fun (lean-input-concat-map fun trans)
+ trans))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Setting up the input method
+
+(defun lean-input-setup ()
+ "Set up the Lean input method based on the customisable
+variables and underlying input methods."
+
+ ;; Create (or reset) the input method.
+ (with-temp-buffer
+ (quail-define-package "Lean" "UTF-8" "∏" t ; guidance
+ "Lean input method.
+The purpose of this input method is to edit Lean programs, but
+since it is highly customisable it can be made useful for other
+tasks as well."
+ nil nil nil nil nil nil t ; maximum-shortest
+ ))
+
+ (lean-input-add-translations
+ (mapcar (lambda (tr) (cons (car tr) (vconcat (cdr tr))))
+ (append lean-input-user-translations
+ lean-input-translations)))
+ (dolist (def lean-input-inherit)
+ (lean-input-inherit-package (car def)
+ (eval (cdr def)))))
+
+(defun lean-input-incorporate-changed-setting (sym val)
+ "Update the Lean input method based on the customisable
+variables and underlying input methods.
+Suitable for use in the :set field of `defcustom'."
+ (set-default sym val)
+ (lean-input-setup))
+
+;; Set up the input method.
+
+(lean-input-setup)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Administrative details
+
+(provide 'lean-input)
+;;; lean-input.el ends here
+
+(defun lean-input-export-translations ()
+ "Export the current translation, (input, output) pairs for
+input-method, in a javascript format. It can be copy-pasted to
+leanprover.github.io/tutorial/js/input-method.js"
+ (interactive)
+ (with-current-buffer
+ (get-buffer-create "*lean-translations*")
+ (let ((exclude-list '("\\newline")))
+ (insert "var corrections = {")
+ (--each
+ (--filter (not (member (car it) exclude-list))
+ (lean-input-get-translations "Lean"))
+ (let* ((input (substring (car it) 1))
+ (outputs (cdr it)))
+ (insert (format "%s:\"" (prin1-to-string input)))
+ (cond ((vectorp outputs)
+ (insert (elt outputs 0)))
+ (t (insert-char outputs)))
+ (insert (format "\",\n" input))))
+ (insert "};"))))
+
+(defun lean-input-export-translations-to-stdout ()
+ (lean-input-export-translations)
+ (with-current-buffer "*lean-translations*"
+ (princ (buffer-string))))
diff --git a/lean-mode/lean-leanpkg.el b/lean-mode/lean-leanpkg.el
new file mode 100644
index 0000000000..a959ae0490
--- /dev/null
+++ b/lean-mode/lean-leanpkg.el
@@ -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)
diff --git a/lean-mode/lean-mode.el b/lean-mode/lean-mode.el
new file mode 100644
index 0000000000..1d6267adb3
--- /dev/null
+++ b/lean-mode/lean-mode.el
@@ -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
+;; Soonho Kong
+;; Gabriel Ebner
+;; Sebastian Ullrich
+;; Maintainer: Sebastian Ullrich
+;; 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 "") #'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
diff --git a/lean-mode/lean-right-click.el b/lean-mode/lean-right-click.el
new file mode 100644
index 0000000000..7ef76192e3
--- /dev/null
+++ b/lean-mode/lean-right-click.el
@@ -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
diff --git a/lean-mode/lean-settings.el b/lean-mode/lean-settings.el
new file mode 100644
index 0000000000..07d025b3c1
--- /dev/null
+++ b/lean-mode/lean-settings.el
@@ -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)
diff --git a/lean-mode/lean-syntax.el b/lean-mode/lean-syntax.el
new file mode 100644
index 0000000000..a04c21fd22
--- /dev/null
+++ b/lean-mode/lean-syntax.el
@@ -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)
diff --git a/lean-mode/lean-type.el b/lean-mode/lean-type.el
new file mode 100644
index 0000000000..92688f965b
--- /dev/null
+++ b/lean-mode/lean-type.el
@@ -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)
diff --git a/lean-mode/lean-util.el b/lean-mode/lean-util.el
new file mode 100644
index 0000000000..a6b79ca8aa
--- /dev/null
+++ b/lean-mode/lean-util.el
@@ -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)