chore(src/emacs): move lean-mode to https://github.com/leanprover/lean-mode
Closes #410
This commit is contained in:
Sebastian Ullrich
Leonardo de Moura
parent
bcad5309d9
commit
5efa1b829c
37 changed files with 3 additions and 3806 deletions
|
|
@ -18,7 +18,6 @@ About
|
|||
- [Homepage](http://leanprover.github.io)
|
||||
- [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean/index.html)
|
||||
- [Core library](library/library.md)
|
||||
- [Emacs Mode](src/emacs/README.md)
|
||||
- [Change Log](doc/changes.md)
|
||||
- For HoTT mode, please use [Lean2](https://github.com/leanprover/lean2).
|
||||
|
||||
|
|
|
|||
2
bin/.gitignore
vendored
2
bin/.gitignore
vendored
|
|
@ -1,4 +1,2 @@
|
|||
lean
|
||||
lean.exe
|
||||
leanemacs
|
||||
leanemacs.bat
|
||||
|
|
|
|||
|
|
@ -1,4 +0,0 @@
|
|||
SET MY_PATH=%~dp0
|
||||
SET LEAN_ROOTDIR=%MY_PATH%/..
|
||||
SET LEAN_EMACS_PATH=%MY_PATH%/../@EMACS_LISP_DIR@
|
||||
emacs -load %LEAN_EMACS_PATH%/load-lean.el
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
MY_PATH="`dirname \"$0\"`" # relative
|
||||
MY_PATH="`( cd \"$MY_PATH\" && pwd )`" # absolutized and normalized
|
||||
|
||||
export LEAN_ROOTDIR="$MY_PATH/.."
|
||||
export LEAN_EMACS_PATH="$MY_PATH/../@EMACS_LISP_DIR@"
|
||||
|
||||
emacs -load $LEAN_EMACS_PATH/load-lean.el $*
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
MY_PATH="`dirname \"$0\"`" # relative
|
||||
MY_PATH="`( cd \"$MY_PATH\" && pwd )`" # absolutized and normalized
|
||||
|
||||
export LEAN_ROOTDIR="$MY_PATH/.."
|
||||
export LEAN_EMACS_PATH="$LEAN_ROOTDIR/src/emacs"
|
||||
|
||||
emacs -load $LEAN_EMACS_PATH/load-lean.el $*
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
SET MY_PATH=%~dp0
|
||||
SET LEAN_ROOTDIR=%MY_PATH%/..
|
||||
SET LEAN_EMACS_PATH=%MY_PATH%/../src/emacs
|
||||
emacs -load %LEAN_EMACS_PATH%/load-lean.el
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
# Script for testing load-lean.el without installing Lean
|
||||
MY_PATH="`dirname \"$0\"`" # relative
|
||||
MY_PATH="`( cd \"$MY_PATH\" && pwd )`" # absolutized and normalized
|
||||
|
||||
export LEAN_ROOTDIR="$MY_PATH/.."
|
||||
export LEAN_EMACS_PATH="$MY_PATH/../src/emacs"
|
||||
|
||||
emacs -load $LEAN_EMACS_PATH/load-lean.el -debug-init $*
|
||||
|
|
@ -5,21 +5,10 @@ The binary distribution package contains:
|
|||
|
||||
- Lean executable (located in the sub-directory bin)
|
||||
- Standard library (located in the sub-directory lib/lean/library)
|
||||
- Emacs modes (located in the sub-directory share/emacs/site-list/lean)
|
||||
|
||||
Assuming you are in the same directory this file is located,
|
||||
the following command executes a simple set of examples
|
||||
|
||||
% bin/lean examples/ex.lean
|
||||
|
||||
The Emacs mode is the ideal way to use Lean. It requires at
|
||||
least Emacs version 24.3
|
||||
|
||||
Documentation
|
||||
-------------
|
||||
|
||||
The tutorial "Theorem Proving in Lean" describes Lean main features,
|
||||
and provides many examples. The tutorial is available in two different forms:
|
||||
|
||||
- Interactive HTML: http://leanprover.github.io/tutorial/index.html
|
||||
- PDF: http://leanprover.github.io/tutorial/tutorial.pdf
|
||||
For more information on Lean and supported editors, please see https://leanprover.github.io/documentation/.
|
||||
|
|
|
|||
|
|
@ -150,6 +150,8 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
|
|||
|
||||
* User attributes can no longer be set with `set_basic_attribute`. You need to use `user_attribute.set` now.
|
||||
|
||||
* The Emacs mode has been moved into its own repository and MELPA packages: https://github.com/leanprover/lean-mode
|
||||
|
||||
*API name changes*
|
||||
|
||||
* `list.dropn` => `list.drop`
|
||||
|
|
|
|||
|
|
@ -50,8 +50,6 @@ option(CUSTOM_ALLOCATORS "CUSTOM_ALLOCATORS" ON)
|
|||
option(SAVE_SNAPSHOT "SAVE_SNAPSHOT" ON)
|
||||
option(SAVE_INFO "SAVE_INFO" ON)
|
||||
|
||||
# emacs site-lisp dir
|
||||
set(EMACS_LISP_DIR "share/emacs/site-lisp/lean" CACHE STRING "emacs site-lisp dir")
|
||||
# library dir
|
||||
set(LIBRARY_DIR "lib/lean" CACHE STRING "library dir")
|
||||
set(LEAN_EXT_INCLUDE_DIR "include/lean_ext" CACHE STRING "include dir for building Lean extensions")
|
||||
|
|
@ -102,8 +100,6 @@ if (NOT("${SAVE_INFO}" MATCHES "ON"))
|
|||
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_NO_INFO")
|
||||
endif()
|
||||
|
||||
message(STATUS "Lean emacs-mode will be installed at "
|
||||
"${CMAKE_INSTALL_PREFIX}/${EMACS_LISP_DIR}")
|
||||
message(STATUS "Lean library will be installed at "
|
||||
"${CMAKE_INSTALL_PREFIX}/${LIBRARY_DIR}")
|
||||
|
||||
|
|
@ -192,7 +188,6 @@ set(CMAKE_CXX_FLAGS_GPROF "-O2 -g -pg")
|
|||
set(CPACK_DMG_BACKGROUND_IMAGE "${LEAN_SOURCE_DIR}/../images/lean.png")
|
||||
set(CPACK_DMG_VOLUME_NAME "Lean-${LEAN_VERSION_STRING}")
|
||||
set(CPACK_BUNDLE_NAME "Lean-${LEAN_VERSION_STRING}")
|
||||
set(CPACK_BUNDLE_STARTUP_COMMAND "bin/leanemacs")
|
||||
set(CPACK_PACKAGE_ICON "${LEAN_SOURCE_DIR}/../images/lean.png")
|
||||
##################
|
||||
|
||||
|
|
@ -352,10 +347,6 @@ configure_file("${LEAN_SOURCE_DIR}/githash.h.in" "${LEAN_BINARY_DIR}/githash.h")
|
|||
# Version
|
||||
configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h")
|
||||
|
||||
# leanemacs file
|
||||
configure_file("${LEAN_SOURCE_DIR}/../bin/leanemacs.in" "${LEAN_SOURCE_DIR}/../bin/leanemacs")
|
||||
configure_file("${LEAN_SOURCE_DIR}/../bin/leanemacs.bat.in" "${LEAN_SOURCE_DIR}/../bin/leanemacs.bat")
|
||||
|
||||
include_directories("${LEAN_BINARY_DIR}")
|
||||
add_subdirectory(util)
|
||||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:util>)
|
||||
|
|
@ -419,7 +410,6 @@ if (NOT("${CROSS_COMPILE}" MATCHES "ON"))
|
|||
endif()
|
||||
|
||||
add_subdirectory(shell)
|
||||
add_subdirectory(emacs)
|
||||
|
||||
function(add_exec_test name tgt)
|
||||
if(${EMSCRIPTEN})
|
||||
|
|
@ -494,16 +484,6 @@ install(FILES "${CMAKE_SOURCE_DIR}/../bin/leanpkg"
|
|||
DESTINATION bin
|
||||
PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
|
||||
|
||||
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
|
||||
install(FILES "${CMAKE_SOURCE_DIR}/../bin/leanemacs.bat" "${CMAKE_SOURCE_DIR}/../bin/leanemacs.bat"
|
||||
DESTINATION bin
|
||||
PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
|
||||
else()
|
||||
install(FILES "${CMAKE_SOURCE_DIR}/../bin/leanemacs" "${CMAKE_SOURCE_DIR}/../bin/leanemacs"
|
||||
DESTINATION bin
|
||||
PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
|
||||
endif()
|
||||
|
||||
install(DIRECTORY "${CMAKE_SOURCE_DIR}/../library" DESTINATION "${LIBRARY_DIR}"
|
||||
FILES_MATCHING
|
||||
PATTERN "*.lean"
|
||||
|
|
@ -522,9 +502,6 @@ install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION "${LEAN_EXT_INCLUDE_DIR}"
|
|||
FILES_MATCHING
|
||||
PATTERN "*.h")
|
||||
|
||||
install(FILES "${CMAKE_SOURCE_DIR}/../src/emacs/lean.pgm"
|
||||
DESTINATION "${EMACS_LISP_DIR}")
|
||||
|
||||
if("${INCLUDE_MSYS2_DLLS}" MATCHES "ON")
|
||||
# TODO(Leo): do not use hardlinks to required DLLs.
|
||||
# For example, we can try to use ldd to retrieve the list of required DLLs.
|
||||
|
|
|
|||
2
src/emacs/.gitignore
vendored
2
src/emacs/.gitignore
vendored
|
|
@ -1,2 +0,0 @@
|
|||
.cask
|
||||
*.elc
|
||||
|
|
@ -1,2 +0,0 @@
|
|||
FILE(GLOB LEAN_MODE_FILES *.el)
|
||||
install(FILES ${LEAN_MODE_FILES} DESTINATION "${EMACS_LISP_DIR}")
|
||||
|
|
@ -1,14 +0,0 @@
|
|||
(source gnu)
|
||||
(source melpa)
|
||||
(package-file "lean-mode.el")
|
||||
(development
|
||||
(depends-on "cl-lib")
|
||||
(depends-on "company")
|
||||
(depends-on "dash" 2.8.0)
|
||||
(depends-on "dash-functional" "1.1.0")
|
||||
(depends-on "ert-runner")
|
||||
(depends-on "ecukes")
|
||||
(depends-on "f")
|
||||
(depends-on "flycheck")
|
||||
(depends-on "flymake")
|
||||
(depends-on "s"))
|
||||
|
|
@ -1,17 +0,0 @@
|
|||
CASK ?= cask
|
||||
EMACS ?= emacs
|
||||
|
||||
all: test
|
||||
|
||||
test: unit ecukes
|
||||
|
||||
unit:
|
||||
${CASK} exec ert-runner
|
||||
|
||||
ecukes:
|
||||
${CASK} exec ecukes
|
||||
|
||||
install:
|
||||
${CASK} install
|
||||
|
||||
.PHONY: all test unit ecukes install
|
||||
|
|
@ -1,165 +0,0 @@
|
|||
This is the emacs mode for the [Lean theorem prover][lean].
|
||||
|
||||
[lean]: https://github.com/leanprover/lean
|
||||
|
||||
Quick-start
|
||||
===========
|
||||
|
||||
If you have built lean from source, all that is necessary is to call the
|
||||
`leanemacs_build` script which automatically installs all the dependencies and
|
||||
opens up emacs with lean-mode loaded:
|
||||
```
|
||||
~/projects/lean/bin/leanemacs_build
|
||||
```
|
||||
|
||||
If you have installed lean from a binary package, you can run `leanemacs`.
|
||||
|
||||
Trying It Out
|
||||
=============
|
||||
|
||||
If things are working correctly, you should see the word ``Lean`` in the
|
||||
Emacs mode line when you open a file with extension `.lean`. If you type
|
||||
```lean
|
||||
#check id
|
||||
```
|
||||
the word ``#check`` will be underlined, and hovering over it will show
|
||||
you the type of ``id``. The mode line will show ``FlyC:0/1``, indicating
|
||||
that there are no errors and one piece of information displayed.
|
||||
|
||||
Key Bindings and Commands
|
||||
=========================
|
||||
|
||||
| Key | Function |
|
||||
|--------------------|---------------------------------------------------------------------------------|
|
||||
| <kbd>M-.</kbd> | jump to definition in source file (`lean-find-definition`) |
|
||||
| <kbd>S-SPC</kbd> | auto complete identifiers, options, imports, etc. (`company-complete`) |
|
||||
| <kbd>C-c C-k</kbd> | shows the keystroke needed to input the symbol under the cursor |
|
||||
| <kbd>C-c C-x</kbd> | execute lean in stand-alone mode (`lean-std-exe`) |
|
||||
| <kbd>C-c SPC</kbd> | run a command on the hole at point (`lean-hole`)
|
||||
| <kbd>C-c C-g</kbd> | toggle showing current tactic proof goal (`lean-toggle-show-goal`) |
|
||||
| <kbd>C-c C-n</kbd> | toggle showing next error in dedicated buffer (`lean-toggle-next-error`) |
|
||||
| <kbd>C-c C-b</kbd> | toggle showing output in inline boxes (`lean-message-boxes-toggle`) |
|
||||
| <kbd>C-c C-r</kbd> | restart the lean server (`lean-server-restart`) |
|
||||
| <kbd>C-c ! n</kbd> | flycheck: go to next error |
|
||||
| <kbd>C-c ! p</kbd> | flycheck: go to previous error |
|
||||
| <kbd>C-c ! l</kbd> | flycheck: show list of errors |
|
||||
|
||||
In the default configuration, the Flycheck annotation `FlyC:n/n` indicates the
|
||||
number of errors / responses from Lean; clicking on `FlyC` opens the Flycheck menu.
|
||||
|
||||
|
||||
Message Boxes
|
||||
================
|
||||
To view the output of commands such as `check` and `print` in boxes in the buffer, enable the feature using <kbd>C-c C-b</kbd>.
|
||||
If you then type
|
||||
```lean
|
||||
#check id
|
||||
```
|
||||
a box appears after the line showing the type of `id`. Customize `lean-message-boxes-enabled-captions` to choose categories of boxes.
|
||||
In particular, add `"trace output"` to the list to see proof states and other traces in the buffer.
|
||||
|
||||
Requirements
|
||||
============
|
||||
|
||||
``lean-mode`` requires [Emacs 24][emacs24] or later and the following
|
||||
packages, which can be installed via <kbd>M-x package-install</kbd>:
|
||||
[dash][dash], [dash-functional][dash], [f][f], [s][s], [company][company],
|
||||
and [flycheck][flycheck]
|
||||
|
||||
[emacs24]: http://www.gnu.org/software/emacs
|
||||
[dash]: https://github.com/magnars/dash.el
|
||||
[f]: https://github.com/rejeep/f.el
|
||||
[s]: https://github.com/magnars/s.el
|
||||
[company]: http://company-mode.github.io/
|
||||
[flycheck]: http://www.flycheck.org/manual/latest/index.html
|
||||
|
||||
Installation
|
||||
============
|
||||
|
||||
You can also include lean-mode permanently in your emacs init file. In this
|
||||
case, just put the following code in your Emacs init file (typically `~/.emacs.d/init.el`):
|
||||
```elisp
|
||||
;; You need to modify the following two lines:
|
||||
(setq lean-rootdir "~/projects/lean")
|
||||
(setq lean-emacs-path "~/projects/lean/src/emacs")
|
||||
|
||||
(setq lean-mode-required-packages '(company dash dash-functional f
|
||||
flycheck let-alist s seq))
|
||||
|
||||
(require 'package)
|
||||
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/"))
|
||||
(package-initialize)
|
||||
(let ((need-to-refresh t))
|
||||
(dolist (p lean-mode-required-packages)
|
||||
(when (not (package-installed-p p))
|
||||
(when need-to-refresh
|
||||
(package-refresh-contents)
|
||||
(setq need-to-refresh nil))
|
||||
(package-install p))))
|
||||
|
||||
(setq load-path (cons lean-emacs-path load-path))
|
||||
|
||||
(require 'lean-mode)
|
||||
```
|
||||
|
||||
If you already have the dependencies installed, the following three lines suffice:
|
||||
```elisp
|
||||
;; You need to modify the following two lines:
|
||||
(setq lean-rootdir "~/projects/lean")
|
||||
(setq load-path (cons "~/projects/lean/src/emacs" load-path))
|
||||
(require 'lean-mode)
|
||||
```
|
||||
|
||||
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 [emacs-unicode-fonts](https://github.com/rolandwalker/unicode-fonts) package.
|
||||
|
||||
- Run `M-x package-refresh-contents`, `M-x package-install`, and type `unicode-fonts`.
|
||||
- Add the following lines in your emacs setup:
|
||||
|
||||
```lisp
|
||||
(require 'unicode-fonts)
|
||||
(unicode-fonts-setup)
|
||||
```
|
||||
|
||||
"Variable binding depth exceeds max-specpdl-size" Error
|
||||
---------------------------------------------------------
|
||||
|
||||
See [Issue 906](https://github.com/leanprover/lean/issues/906) for details.
|
||||
[Moritz Kiefer](https://github.com/cocreature) reported that `proofgeneral`
|
||||
comes with an old version of `mmm-mode` (0.4.8, released in 2004) on ArchLinux
|
||||
and it caused this problem. Either removing `proofgeneral` or upgrading
|
||||
`mmm-mode` to the latest version (0.5.1 as of 2015 Dec) resolves this issue.
|
||||
|
||||
Contributions
|
||||
=============
|
||||
|
||||
Contributions are welcome!
|
||||
|
||||
Install [Cask](https://github.com/cask/cask) if you haven't already, then:
|
||||
|
||||
$ cd /path/to/lean/src/emacs
|
||||
$ cask
|
||||
|
||||
Run all tests with:
|
||||
|
||||
$ make
|
||||
206
src/emacs/eri.el
206
src/emacs/eri.el
|
|
@ -1,206 +0,0 @@
|
|||
;;; eri.el --- Enhanced relative indentation (eri)
|
||||
|
||||
;;; Commentary:
|
||||
|
||||
;;; Code:
|
||||
|
||||
(require 'cl)
|
||||
|
||||
(defun eri-current-line-length nil
|
||||
"Calculate length of current line."
|
||||
(- (line-end-position) (line-beginning-position)))
|
||||
|
||||
(defun eri-current-line-empty nil
|
||||
"Return non-nil if the current line is empty (not counting white space)."
|
||||
(equal (current-indentation)
|
||||
(eri-current-line-length)))
|
||||
|
||||
(defun eri-maximum (xs)
|
||||
"Calculate maximum element in XS.
|
||||
Returns nil if the list is empty."
|
||||
(if xs (apply 'max xs)))
|
||||
|
||||
(defun eri-take (n xs)
|
||||
"Return the first N elements of XS."
|
||||
(butlast xs (- (length xs) n)))
|
||||
|
||||
(defun 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 (eri-take pos xs))
|
||||
(xs2 (nthcdr pos xs)))
|
||||
(cons xs1 xs2)))
|
||||
|
||||
(defun 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 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 (eri-current-line-empty))))))
|
||||
(if (or (equal (point) start)
|
||||
(eri-current-line-empty))
|
||||
nil
|
||||
(list (+ 2 (current-indentation)))))))
|
||||
|
||||
(defun 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
|
||||
`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)
|
||||
(eri-current-line-empty))
|
||||
(setq points
|
||||
(append
|
||||
(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)
|
||||
(> (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 (eri-new-indentation-points) points)))
|
||||
(ps1 (eri-split (current-indentation) (sort ps0 '<)))
|
||||
(ps2 (append (cdr ps1) (car ps1))))
|
||||
(if reverse
|
||||
(nreverse ps2)
|
||||
ps2))))
|
||||
|
||||
(defun 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 (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 eri-indent-reverse nil
|
||||
"Cycle between some possible indentation points (in reverse order).
|
||||
See `eri-indent' for a description of how the indentation points
|
||||
are calculated."
|
||||
(interactive)
|
||||
(eri-indent t))
|
||||
|
||||
(provide 'eri)
|
||||
;;; eri.el ends here
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
Feature: Do Some things
|
||||
In order to do something
|
||||
As a user
|
||||
I want to do something
|
||||
|
||||
Scenario: Do Something
|
||||
Given I have "something"
|
||||
When I have "something"
|
||||
Then I should have "something"
|
||||
And I should have "something"
|
||||
But I should not have "something"
|
||||
|
|
@ -1,28 +0,0 @@
|
|||
;; This file contains your project specific step definitions. All
|
||||
;; files in this directory whose names end with "-steps.el" will be
|
||||
;; loaded automatically by Ecukes.
|
||||
|
||||
(Given "^I have \"\\(.+\\)\"$"
|
||||
(lambda (something)
|
||||
;; ...
|
||||
))
|
||||
|
||||
(When "^I have \"\\(.+\\)\"$"
|
||||
(lambda (something)
|
||||
;; ...
|
||||
))
|
||||
|
||||
(Then "^I should have \"\\(.+\\)\"$"
|
||||
(lambda (something)
|
||||
;; ...
|
||||
))
|
||||
|
||||
(And "^I have \"\\(.+\\)\"$"
|
||||
(lambda (something)
|
||||
;; ...
|
||||
))
|
||||
|
||||
(But "^I should not have \"\\(.+\\)\"$"
|
||||
(lambda (something)
|
||||
;; ...
|
||||
))
|
||||
|
|
@ -1,32 +0,0 @@
|
|||
(require 'f)
|
||||
|
||||
(defvar emacs-support-path
|
||||
(f-dirname load-file-name))
|
||||
|
||||
(defvar emacs-features-path
|
||||
(f-parent emacs-support-path))
|
||||
|
||||
(defvar emacs-root-path
|
||||
(f-parent emacs-features-path))
|
||||
|
||||
(add-to-list 'load-path emacs-root-path)
|
||||
|
||||
(require 'emacs)
|
||||
(require 'espuds)
|
||||
(require 'ert)
|
||||
|
||||
(Setup
|
||||
;; Before anything has run
|
||||
)
|
||||
|
||||
(Before
|
||||
;; Before each scenario is run
|
||||
)
|
||||
|
||||
(After
|
||||
;; After each scenario is run
|
||||
)
|
||||
|
||||
(Teardown
|
||||
;; After when everything has been run
|
||||
)
|
||||
|
|
@ -1,187 +0,0 @@
|
|||
;; -*- 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 'company)
|
||||
(require 'company-etags)
|
||||
(require 'dash)
|
||||
(require 'dash-functional)
|
||||
(require 'f)
|
||||
(require 's)
|
||||
(require 'cl-lib)
|
||||
(require 'lean-util)
|
||||
(require 'lean-server)
|
||||
|
||||
(defun company-lean-hook ()
|
||||
(set (make-local-variable 'company-backends) '(company-lean))
|
||||
(setq-local company-tooltip-limit 20) ; bigger popup window
|
||||
(setq-local company-minimum-prefix-length 5)
|
||||
(setq-local company-idle-delay nil) ; decrease delay before autocompletion popup shows
|
||||
;(setq-local company-echo-delay 0) ; remove annoying blinking
|
||||
(setq-local company-begin-commands '(self-insert-command)) ; start autocompletion only after typing
|
||||
(company-mode t))
|
||||
|
||||
(cl-defun company-lean--make-candidate (prefix &key text type (tactic_params 'empty) doc source &allow-other-keys)
|
||||
(destructuring-bind (&key file line column) source
|
||||
(let ((source (cond
|
||||
(file (cons file line))
|
||||
(line (cons (current-buffer) (lean-pos-at-line-col line 0))))))
|
||||
(propertize text
|
||||
'type type
|
||||
'tactic_params tactic_params
|
||||
'doc doc
|
||||
'source source
|
||||
'prefix prefix))))
|
||||
|
||||
(defun company-lean--handle-singleton-candidate (prefix candidates)
|
||||
"Handle singleton candidate. If the candidate does not start
|
||||
with prefix, we add prefix itself as a candidate to prevent
|
||||
from auto-completion."
|
||||
(let ((candidate (car candidates)))
|
||||
(cond ((s-prefix? prefix candidate) candidates)
|
||||
(t `(,candidate ,prefix)))))
|
||||
|
||||
(cl-defun company-lean--exec (&key skip-completions)
|
||||
"Synchronously queries completions for the current point from server and returns a plist with keys :prefix and :candidates., or nil if no completion should be triggered."
|
||||
(lean-server-sync)
|
||||
(let* ((col (lean-line-offset))
|
||||
(response (lean-server-send-synchronous-command
|
||||
'complete (list :file_name (buffer-file-name)
|
||||
:line (line-number-at-pos)
|
||||
:column col
|
||||
:skip_completions (or skip-completions :json-false))))
|
||||
(candidates (plist-get response :completions))
|
||||
(prefix (plist-get response :prefix)))
|
||||
(when candidates
|
||||
(setq candidates
|
||||
(--map (apply 'company-lean--make-candidate prefix it)
|
||||
candidates))
|
||||
(when (= (length candidates) 1)
|
||||
(setq candidates
|
||||
(company-lean--handle-singleton-candidate prefix candidates))))
|
||||
(when (plist-member response :prefix)
|
||||
(list :prefix prefix :candidates candidates))))
|
||||
|
||||
(defun company-lean--annotation (candidate)
|
||||
(let ((type (get-text-property 0 'type candidate))
|
||||
(tactic_params (get-text-property 0 'tactic_params candidate)))
|
||||
(when type
|
||||
(let* ((annotation-str (if (not (eq tactic_params 'empty))
|
||||
(format " %s" (mapconcat 'identity tactic_params " "))
|
||||
(format " : %s" type)))
|
||||
(annotation-len (length annotation-str))
|
||||
(candidate-len (length candidate))
|
||||
(entry-width (+ candidate-len
|
||||
annotation-len))
|
||||
(allowed-width (truncate (* 0.90 (window-body-width)))))
|
||||
(when (> entry-width allowed-width)
|
||||
(setq annotation-str
|
||||
(concat
|
||||
(substring-no-properties annotation-str
|
||||
0
|
||||
(- allowed-width candidate-len 3))
|
||||
"...")))
|
||||
annotation-str))))
|
||||
|
||||
(defun company-lean--location (arg)
|
||||
(get-text-property 0 'source arg))
|
||||
|
||||
(defun company-lean--match (arg)
|
||||
"Return the end of matched region"
|
||||
(let ((prefix (get-text-property 0 'prefix arg)))
|
||||
(when (and prefix (eq (s-index-of prefix arg) 0))
|
||||
(length prefix))))
|
||||
|
||||
(defun company-lean--meta (arg)
|
||||
(get-text-property 0 'doc arg))
|
||||
|
||||
(defun company-lean (command &optional arg &rest ignored)
|
||||
(cl-case command
|
||||
(prefix (plist-get (company-lean--exec :skip-completions t) :prefix))
|
||||
(candidates (plist-get (company-lean--exec) :candidates))
|
||||
(annotation (company-lean--annotation arg))
|
||||
(location (company-lean--location arg))
|
||||
(match (company-lean--match arg))
|
||||
(meta (company-lean--meta arg))
|
||||
(no-cache t)
|
||||
(require-match 'never)
|
||||
(sorted t)))
|
||||
|
||||
;; ADVICES
|
||||
;; =======
|
||||
|
||||
(defadvice company--window-width
|
||||
(after lean-company--window-width activate)
|
||||
(when (eq major-mode 'lean-mode)
|
||||
(setq ad-return-value (truncate (* 0.95 (window-body-width))))))
|
||||
|
||||
(defun replace-regex-return-position (regex rep string &optional start)
|
||||
"Find regex and replace with rep on string.
|
||||
|
||||
Return replaced string and start and end positions of replacement."
|
||||
(let* ((start (or start 0))
|
||||
(len (length string))
|
||||
(m-start (string-match regex string start))
|
||||
(m-end (match-end 0))
|
||||
pre-string post-string matched-string replaced-string result)
|
||||
(cond (m-start
|
||||
(setq pre-string (substring string 0 m-start))
|
||||
(setq matched-string (substring string m-start m-end))
|
||||
(setq post-string (substring string m-end))
|
||||
(string-match regex matched-string)
|
||||
(setq replaced-string
|
||||
(replace-match rep nil nil matched-string))
|
||||
(setq result (concat pre-string
|
||||
replaced-string
|
||||
post-string))
|
||||
`(,result ,m-start ,(+ m-start (length replaced-string)))
|
||||
))))
|
||||
|
||||
(defun replace-regex-add-properties-all (regex rep string properties)
|
||||
"Find all occurrences of regex in string, and replace them with
|
||||
rep. Then, add text-properties on the replaced region."
|
||||
(let ((replace-result-items (replace-regex-return-position regex rep string))
|
||||
(result string))
|
||||
(while replace-result-items
|
||||
(pcase replace-result-items
|
||||
(`(,replaced-string ,m-start ,m-end)
|
||||
(setq result replaced-string)
|
||||
(add-text-properties m-start m-end properties result)
|
||||
(setq replace-result-items
|
||||
(replace-regex-return-position regex rep result m-end)))))
|
||||
result))
|
||||
|
||||
(eval-after-load 'company
|
||||
'(defadvice company-fill-propertize
|
||||
(after lean-company-fill-propertize activate)
|
||||
(when (eq major-mode 'lean-mode)
|
||||
(let* ((selected (ad-get-arg 3))
|
||||
(foreground-color lean-company-type-foreground)
|
||||
(background-color (if selected (face-background 'company-tooltip-selection)
|
||||
(face-background 'company-tooltip)))
|
||||
(face-attrs
|
||||
(cond (background-color `(:foreground ,foreground-color
|
||||
:background ,background-color))
|
||||
(t `(:foreground ,foreground-color))))
|
||||
(properties `(face ,face-attrs
|
||||
mouse-face company-tooltip))
|
||||
(old-return ad-return-value)
|
||||
(old-len (length old-return))
|
||||
new-return new-len)
|
||||
(setq new-return
|
||||
(replace-regex-add-properties-all
|
||||
(rx "?" word-start (group (+ (not white))) word-end)
|
||||
"\\1"
|
||||
ad-return-value
|
||||
properties))
|
||||
(setq new-len (length new-return))
|
||||
(while (< (length new-return) old-len)
|
||||
(setq new-return
|
||||
(concat new-return " ")))
|
||||
(when background-color
|
||||
(add-text-properties new-len old-len properties new-return))
|
||||
(setq ad-return-value new-return)))))
|
||||
|
||||
(provide 'lean-company)
|
||||
|
|
@ -1,47 +0,0 @@
|
|||
;; 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)
|
||||
|
|
@ -1,16 +0,0 @@
|
|||
;; -*- 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
|
||||
;;
|
||||
|
||||
(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)
|
||||
|
|
@ -1,151 +0,0 @@
|
|||
;; -*- 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
|
||||
|
|
@ -1,118 +0,0 @@
|
|||
;; -*- lexical-binding: t -*-
|
||||
;;
|
||||
;;; lean-info.el --- Emacs mode for Lean theorem prover
|
||||
;;
|
||||
;; Copyright (c) 2016 Gabriel Ebner. All rights reserved.
|
||||
;;
|
||||
;; Author: Gabriel Ebner <gebner@gebner.org>
|
||||
;; Maintainer: Gabriel Ebner <gebner@gebner.org>
|
||||
;; Created: Oct 29, 2016
|
||||
;; Keywords: languages
|
||||
;; Version: 0.1
|
||||
;; URL: https://github.com/leanprover/lean/blob/master/src/emacs
|
||||
;;
|
||||
;; Released under Apache 2.0 license as described in the file LICENSE.
|
||||
;;
|
||||
|
||||
;; 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-highlight-string (str)
|
||||
"Returns 'str' highlighted in lean-info-mode"
|
||||
(lean-ensure-info-buffer " Lean tmp buffer")
|
||||
(lean-with-info-output-to-buffer (get-buffer " Lean tmp buffer")
|
||||
(princ str)
|
||||
(font-lock-fontify-buffer)
|
||||
(buffer-string)))
|
||||
|
||||
(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)
|
||||
(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)
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -1,124 +0,0 @@
|
|||
;; -*- lexical-binding: t -*-
|
||||
;;
|
||||
;; Copyright (c) 2016 David Christiansen.
|
||||
;; Released under Apache 2.0 license as described in the file LICENSE.
|
||||
;;
|
||||
;; Author: David Christiansen
|
||||
;;
|
||||
;;; Code:
|
||||
|
||||
(require 's)
|
||||
(require 'lean-server)
|
||||
|
||||
(defface lean-message-boxes-content-face
|
||||
'((t :inherit font-lock-doc-face))
|
||||
"Face for Lean message box contents."
|
||||
:group 'lean)
|
||||
|
||||
(defcustom lean-message-boxes-enabled-captions '("check result" "print result")
|
||||
"Which captions should result in boxes?"
|
||||
:group 'lean
|
||||
:type '(repeat (choice (const "check result")
|
||||
(const "print result")
|
||||
(const "trace output"))))
|
||||
|
||||
(defvar lean-message-boxes-enabledp nil
|
||||
"Whether or not to display message boxes.")
|
||||
(make-variable-buffer-local 'lean-message-boxes-enabledp)
|
||||
|
||||
(defun lean-message-boxes--ask-for-messages ()
|
||||
"Get the current messages out of the Lean server session."
|
||||
(let ((buf (current-buffer)))
|
||||
(if lean-server-session
|
||||
(remove-if-not (lambda (msg)
|
||||
(equal (buffer-file-name buf)
|
||||
(plist-get msg :file_name)))
|
||||
(lean-server-session-messages lean-server-session))
|
||||
'())))
|
||||
|
||||
(defun lean-message-boxes--set-enabledp (enabledp)
|
||||
"Enable the boxes if ENABLEDP is non-nil."
|
||||
(setq lean-message-boxes-enabledp enabledp)
|
||||
(lean-message-boxes-display (lean-message-boxes--ask-for-messages)))
|
||||
|
||||
(defun lean-message-boxes-toggle ()
|
||||
"Toggle the display of message boxes."
|
||||
(interactive)
|
||||
(lean-message-boxes--set-enabledp (not lean-message-boxes-enabledp)))
|
||||
|
||||
(defun lean-message-boxes-enable ()
|
||||
"Enable the display of message boxes."
|
||||
(interactive)
|
||||
(setq lean-message-boxes--set-enabledp t))
|
||||
|
||||
(defun lean-message-boxes-disable ()
|
||||
"Disable the display of message boxes."
|
||||
(interactive)
|
||||
(setq lean-message-boxes--set-enabledp t))
|
||||
|
||||
(defvar lean-message-boxes--overlays '()
|
||||
"The overlays in the current buffer from Lean messages.")
|
||||
(make-variable-buffer-local 'lean-message-boxes--overlays)
|
||||
|
||||
(defun lean-message-boxes--kill-overlays ()
|
||||
"Delete all Lean message overlays in the current buffer."
|
||||
(dolist (o lean-message-boxes--overlays)
|
||||
(delete-overlay o))
|
||||
(setq lean-message-boxes--overlays '()))
|
||||
|
||||
(defun lean-message-boxes--pad-to (str width)
|
||||
"Pad the string STR to a particular WIDTH."
|
||||
(concat str (make-string (max 0 (- width (length str))) ?\ )))
|
||||
|
||||
(defun lean-message-boxes-display (msgs)
|
||||
"Show the messages MSGS in the Lean buffer as boxes when `lean-message-boxes-enabledp' is non-nil."
|
||||
(lean-message-boxes--kill-overlays)
|
||||
(when lean-message-boxes-enabledp
|
||||
(dolist (msg msgs)
|
||||
(let ((end-line (plist-get msg :end_pos_line))
|
||||
(end-col (plist-get msg :end_pos_col))
|
||||
(caption (plist-get msg :caption))
|
||||
(text (plist-get msg :text)))
|
||||
(when (member caption lean-message-boxes-enabled-captions)
|
||||
(let ((overlay (lean-message-boxes--make-overlay
|
||||
end-line end-col
|
||||
caption text)))
|
||||
(push overlay lean-message-boxes--overlays)))))))
|
||||
|
||||
(defun lean-message-boxes--as-string (caption str)
|
||||
"Construct a propertized string representing CAPTION and STR."
|
||||
(let* ((caption-copy (concat caption))
|
||||
(str-copy (s-trim str)))
|
||||
(put-text-property 0 (length str-copy)
|
||||
'face 'lean-message-boxes-content-face
|
||||
str-copy)
|
||||
(let* ((lines (s-lines str-copy))
|
||||
(w (apply #'max (mapcar #'length (cons caption lines)))))
|
||||
(apply #'concat
|
||||
(mapcar
|
||||
(lambda (l)
|
||||
(concat "│ "
|
||||
(lean-message-boxes--pad-to l w)
|
||||
"\n"))
|
||||
lines)))))
|
||||
|
||||
(defun lean-message-boxes--make-overlay (end-line end-col caption text)
|
||||
"Construct a message box overlay at LINE and COL with CAPTION and TEXT."
|
||||
(let* ((end-pos (save-excursion (goto-char (point-min))
|
||||
(forward-line (1- end-line))
|
||||
(forward-char (1- end-col))
|
||||
(while (looking-at-p "[\t\r\n ]")
|
||||
(forward-char -1))
|
||||
(end-of-line)
|
||||
(1+ (point))))
|
||||
(overlay (make-overlay end-pos (1+ end-pos)))
|
||||
(as-box (lean-message-boxes--as-string caption text)))
|
||||
(put-text-property 0 1 'cursor t as-box)
|
||||
(overlay-put overlay 'before-string as-box)
|
||||
(overlay-put overlay 'help-echo caption)
|
||||
(overlay-put overlay 'lean-is-output-overlay t)
|
||||
(overlay-put overlay 'evaporate t)
|
||||
overlay))
|
||||
|
||||
(add-hook 'lean-server-show-message-hook 'lean-message-boxes-display)
|
||||
(provide 'lean-message-boxes)
|
||||
|
|
@ -1,233 +0,0 @@
|
|||
;; -*- lexical-binding: t -*-
|
||||
;;
|
||||
;;; lean-mode.el --- Emacs mode for Lean theorem prover
|
||||
;;
|
||||
;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved.
|
||||
;; Copyright (c) 2014, 2015 Soonho Kong. All rights reserved.
|
||||
;;
|
||||
;; Author: Leonardo de Moura <leonardo@microsoft.com>
|
||||
;; Soonho Kong <soonhok@cs.cmu.edu>
|
||||
;; Maintainer: Soonho Kong <soonhok@cs.cmu.edu>
|
||||
;; Created: Jan 09, 2014
|
||||
;; 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 'cl-lib)
|
||||
(require 'pcase)
|
||||
(require 'lean-require)
|
||||
(require 'eri)
|
||||
(require 'flycheck)
|
||||
(require 'lean-util)
|
||||
(require 'lean-settings)
|
||||
(require 'lean-input)
|
||||
(require 'lean-syntax)
|
||||
(require 'lean-pkg)
|
||||
(require 'lean-company)
|
||||
(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)
|
||||
(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-find-definition 'lean-find-definition)
|
||||
(local-set-key lean-keybinding-tab-indent 'lean-tab-indent)
|
||||
(local-set-key lean-keybinding-auto-complete 'company-complete)
|
||||
(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 'leanpkg-configure)
|
||||
(local-set-key lean-keybinding-leanpkg-build 'leanpkg-build)
|
||||
(local-set-key lean-keybinding-leanpkg-test 'leanpkg-test)
|
||||
(local-set-key lean-keybinding-lean-helm-definitions 'lean-helm-definitions)
|
||||
;; This only works as a mouse binding due to the event, so it is not abstracted
|
||||
;; to avoid user confusion.
|
||||
(local-set-key (kbd "<mouse-3>") 'lean-right-click-show-menu)
|
||||
)
|
||||
|
||||
(define-abbrev-table 'lean-abbrev-table
|
||||
'())
|
||||
|
||||
(defvar lean-mode-map (make-sparse-keymap)
|
||||
"Keymap used in Lean mode")
|
||||
|
||||
(defun lean-mk-check-menu-option (text sym)
|
||||
`[,text (lean-set-check-mode ',sym)
|
||||
:style radio :selected (eq lean-server-check-mode ',sym)])
|
||||
|
||||
(easy-menu-define lean-mode-menu lean-mode-map
|
||||
"Menu for the Lean major mode"
|
||||
`("Lean"
|
||||
["Execute lean" lean-execute t]
|
||||
;; ["Create a new project" (call-interactively 'lean-project-create) (not (lean-project-inside-p))]
|
||||
"-----------------"
|
||||
["Show type info" lean-show-type (and lean-eldoc-use eldoc-mode)]
|
||||
["Toggle goal display" lean-toggle-show-goal t]
|
||||
["Toggle next error display" lean-toggle-next-error t]
|
||||
["Toggle message boxes" lean-message-boxes-toggle t]
|
||||
["Highlight pending tasks" lean-server-toggle-show-pending-tasks
|
||||
:active t :style toggle :selected lean-server-show-pending-tasks]
|
||||
["Find definition at point" lean-find-definition t]
|
||||
"-----------------"
|
||||
["List of errors" flycheck-list-errors flycheck-mode]
|
||||
"-----------------"
|
||||
["Restart lean process" lean-server-restart t]
|
||||
"-----------------"
|
||||
,(lean-mk-check-menu-option "Check nothing" 'nothing)
|
||||
,(lean-mk-check-menu-option "Check visible lines" 'visible-lines)
|
||||
,(lean-mk-check-menu-option "Check visible lines and above" 'visible-lines-and-above)
|
||||
,(lean-mk-check-menu-option "Check visible files" 'visible-files)
|
||||
,(lean-mk-check-menu-option "Check open files" 'open-files)
|
||||
"-----------------"
|
||||
("Configuration"
|
||||
["Show type at point"
|
||||
lean-toggle-eldoc-mode :active t :style toggle :selected eldoc-mode])
|
||||
"-----------------"
|
||||
["Customize lean-mode" (customize-group 'lean) t]))
|
||||
|
||||
(defconst lean-hooks-alist
|
||||
'(
|
||||
;; server
|
||||
;; (kill-buffer-hook . lean-server-stop)
|
||||
(after-change-functions . lean-server-change-hook)
|
||||
(focus-in-hook . lean-server-show-messages)
|
||||
(window-scroll-functions . lean-server-window-scroll-function-hook)
|
||||
;; Handle events that may start automatic syntax checks
|
||||
(before-save-hook . lean-whitespace-cleanup)
|
||||
;; info windows
|
||||
(post-command-hook . lean-show-goal--handler)
|
||||
(post-command-hook . lean-next-error--handler)
|
||||
(flycheck-after-syntax-check-hook . lean-show-goal--handler)
|
||||
(flycheck-after-syntax-check-hook . lean-next-error--handler)
|
||||
)
|
||||
"Hooks which lean-mode needs to hook in.
|
||||
|
||||
The `car' of each pair is a hook variable, the `cdr' a function
|
||||
to be added or removed from the hook variable if Flycheck mode is
|
||||
enabled and disabled respectively.")
|
||||
|
||||
(defun lean-mode-setup ()
|
||||
"Default lean-mode setup"
|
||||
;; server
|
||||
(ignore-errors (lean-server-ensure-alive))
|
||||
(setq mode-name '("Lean" (:eval (lean-server-status-string))))
|
||||
;; Right click menu sources
|
||||
(setq lean-right-click-item-functions '(lean-info-right-click-find-definition
|
||||
lean-hole-right-click))
|
||||
;; Flycheck
|
||||
(lean-flycheck-turn-on)
|
||||
(setq-local flycheck-disabled-checkers '())
|
||||
;; info buffers
|
||||
(lean-ensure-info-buffer lean-next-error-buffer-name)
|
||||
(lean-ensure-info-buffer lean-show-goal-buffer-name)
|
||||
;; company-mode
|
||||
(when lean-company-use
|
||||
(company-lean-hook))
|
||||
;; 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
|
||||
|
|
@ -1,93 +0,0 @@
|
|||
;; -*- 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 leanpkg-find-dir-in (dir)
|
||||
(when dir
|
||||
(or (leanpkg-find-dir-in (f-parent dir))
|
||||
(when (f-exists? (f-join dir "leanpkg.toml")) dir))))
|
||||
|
||||
(defun leanpkg-find-dir ()
|
||||
(and (buffer-file-name)
|
||||
(leanpkg-find-dir-in (f-dirname (buffer-file-name)))))
|
||||
|
||||
(defun leanpkg-find-dir-safe ()
|
||||
(or (leanpkg-find-dir)
|
||||
(error (format "cannot find leanpkg.toml for %s" (buffer-file-name)))))
|
||||
|
||||
(defun leanpkg-executable ()
|
||||
(lean-get-executable "leanpkg"))
|
||||
|
||||
(defvar leanpkg-running nil)
|
||||
(defvar-local leanpkg-configure-prompt-shown nil)
|
||||
|
||||
(defun leanpkg-run (cmd &optional restart-lean-server)
|
||||
"Call `leanpkg $cmd`"
|
||||
(let ((dir (file-name-as-directory (leanpkg-find-dir-safe)))
|
||||
(orig-buf (current-buffer)))
|
||||
(with-current-buffer (get-buffer-create "*leanpkg*")
|
||||
(setq buffer-read-only nil)
|
||||
(erase-buffer)
|
||||
(switch-to-buffer-other-window (current-buffer))
|
||||
(redisplay)
|
||||
(insert (format "> leanpkg %s\n" cmd))
|
||||
(setq leanpkg-running t)
|
||||
(let* ((default-directory dir)
|
||||
(out-buf (current-buffer))
|
||||
(proc (start-process "leanpkg" (current-buffer)
|
||||
(leanpkg-executable) cmd)))
|
||||
(set-process-sentinel
|
||||
proc (lambda (p e)
|
||||
(setq 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)))))))))
|
||||
|
||||
(defun leanpkg-configure ()
|
||||
"Call leanpkg configure"
|
||||
(interactive)
|
||||
(leanpkg-run "configure" 't))
|
||||
|
||||
(defun leanpkg-build ()
|
||||
"Call leanpkg build"
|
||||
(interactive)
|
||||
(leanpkg-run "build"))
|
||||
|
||||
(defun leanpkg-test ()
|
||||
"Call leanpkg test"
|
||||
(interactive)
|
||||
(leanpkg-run "test"))
|
||||
|
||||
(defun 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 leanpkg-running)
|
||||
(not leanpkg-configure-prompt-shown)
|
||||
(setq leanpkg-configure-prompt-shown t)
|
||||
(leanpkg-find-dir)
|
||||
(y-or-n-p (format "Found leanpkg.toml in %s, call leanpkg configure?" (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
|
||||
(leanpkg-configure)))
|
||||
(current-buffer))))
|
||||
(setq leanpkg-configure-prompt-shown t)
|
||||
(plist-get path-out :leanpkg_path_file)))
|
||||
|
||||
(provide 'lean-pkg)
|
||||
|
|
@ -1,32 +0,0 @@
|
|||
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
;; Released under Apache 2.0 license as described in the file LICENSE.
|
||||
;;
|
||||
;; Author: Soonho Kong
|
||||
;;
|
||||
(defun lean-mode-require-package (pkg)
|
||||
"Check whether pkg is available or not."
|
||||
(unless (featurep pkg)
|
||||
(if (not (require pkg (symbol-name pkg) t))
|
||||
(error "lean-mode: required package '%s' is not found." (symbol-name pkg))
|
||||
(message "lean-mode: package %S loaded." pkg))))
|
||||
|
||||
(defun lean-mode-check-package (pkg)
|
||||
"Check whether pkg is available or not."
|
||||
(unless (featurep pkg)
|
||||
(if (not (require pkg (symbol-name pkg) t))
|
||||
(message "lean-mode: optional package '%s' is not found." (symbol-name pkg))
|
||||
(message "lean-mode: optional package %S loaded." pkg))))
|
||||
|
||||
(defun lean-mode-check-requirements ()
|
||||
"Check lean-mode requirements"
|
||||
(if (not (>= emacs-major-version 24))
|
||||
(error "Emacs version >= 24 is required to use lean-mode"))
|
||||
(lean-mode-check-package 'package)
|
||||
(lean-mode-check-package 'dash)
|
||||
(let ((required-packages '(cl-lib compile dash dash-functional f flymake s))
|
||||
(optional-packages '(flycheck)))
|
||||
(-each required-packages 'lean-mode-require-package)
|
||||
(-each optional-packages 'lean-mode-check-package)))
|
||||
|
||||
(lean-mode-check-requirements)
|
||||
(provide 'lean-require)
|
||||
|
|
@ -1,84 +0,0 @@
|
|||
;; -*- 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
|
||||
|
|
@ -1,487 +0,0 @@
|
|||
;; -*- lexical-binding: t -*-
|
||||
;;
|
||||
;; Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
;; Released under Apache 2.0 license as described in the file LICENSE.
|
||||
;;
|
||||
;; Author: Gabriel Ebner
|
||||
;;
|
||||
|
||||
(require 'json)
|
||||
(require 'lean-debug)
|
||||
(require 'lean-pkg)
|
||||
(require 'dash)
|
||||
|
||||
(defcustom lean-server-show-message-hook '(lean-message-boxes-display)
|
||||
"Hook run on messages from Lean, allowing custom display.
|
||||
|
||||
Each hook is a function that receives a list of message objects
|
||||
for the current buffer. Each message object is a plist with at
|
||||
least the following keys:
|
||||
- :pos_line is the line number of the message, a number
|
||||
- :pos_col is the column of the start of the message, a number
|
||||
- :caption is a category of message, a string
|
||||
- :text is the text to display, a string."
|
||||
:group 'lean
|
||||
:type 'hook
|
||||
:options '(lean-message-boxes-display))
|
||||
|
||||
(defstruct lean-server-session
|
||||
path-file ; the leanpkg.path file of this lean server
|
||||
process ; process object of lean --server
|
||||
seq-num ; sequence number
|
||||
callbacks ; alist of (seq_num . (success_cb . error_cb))
|
||||
current-roi ; alist of (file_name (begin_line . end_line) ...)
|
||||
tasks ; last deserialized current_tasks message
|
||||
messages) ; list of messages in deserialized json
|
||||
|
||||
(defun lean-server-session-proc-buffer (sess)
|
||||
(process-buffer (lean-server-session-process sess)))
|
||||
|
||||
(defun lean-server-session-pop-callback (sess seq-num)
|
||||
(let ((cbp (assoc seq-num (lean-server-session-callbacks sess))))
|
||||
(setf (lean-server-session-callbacks sess)
|
||||
(delete cbp (lean-server-session-callbacks sess)))
|
||||
(if cbp (cdr cbp) (cons nil nil))))
|
||||
|
||||
(defun lean-server-process-response (sess res)
|
||||
(pcase (plist-get res :response)
|
||||
("additional_message"
|
||||
(setf (lean-server-session-messages sess)
|
||||
(cons (plist-get res :msg) (lean-server-session-messages sess)))
|
||||
(lean-server-notify-messages-changed sess))
|
||||
("all_messages"
|
||||
(setf (lean-server-session-messages sess)
|
||||
(plist-get res :msgs))
|
||||
(lean-server-notify-messages-changed sess))
|
||||
("current_tasks"
|
||||
(let ((old-tasks (lean-server-session-tasks sess)))
|
||||
(setf (lean-server-session-tasks sess) res)
|
||||
(lean-server-notify-tasks-changed sess old-tasks)))
|
||||
("error"
|
||||
(message "error: %s" (plist-get res :message))
|
||||
;; TODO(gabriel): maybe even add the error as a message
|
||||
(when (plist-get res :seq_num)
|
||||
(let ((cb (lean-server-session-pop-callback sess (plist-get res :seq_num))))
|
||||
(when (cdr cb) (funcall (cdr cb) res)))))
|
||||
("ok"
|
||||
(let ((cb (lean-server-session-pop-callback sess (plist-get res :seq_num))))
|
||||
(when (car cb) (funcall (car cb) res))))))
|
||||
|
||||
(defun lean-server-process-line (sess line)
|
||||
(condition-case-unless-debug err
|
||||
(progn
|
||||
(lean-debug "server=> %s" line)
|
||||
(let* ((json-array-type 'list)
|
||||
(json-object-type 'plist)
|
||||
(json-false nil)
|
||||
(response (json-read-from-string line)))
|
||||
(lean-server-process-response sess response)))
|
||||
(error (message "error in lean-server command handler: %s\nServer response was:\n%s" err (buffer-string)))))
|
||||
|
||||
(defun lean-server-process-buffer (sess)
|
||||
(goto-char (point-min))
|
||||
(when (search-forward "\n" nil t)
|
||||
(let ((line (buffer-substring (point-min) (point))))
|
||||
(delete-region (point-min) (point))
|
||||
(lean-server-process-line sess line)
|
||||
(lean-server-process-buffer sess))))
|
||||
|
||||
(defun lean-server-filter (sess string)
|
||||
(when (buffer-live-p (lean-server-session-proc-buffer sess))
|
||||
(with-current-buffer (lean-server-session-proc-buffer sess)
|
||||
(goto-char (point-max))
|
||||
(insert string)
|
||||
(lean-server-process-buffer sess))))
|
||||
|
||||
(defun lean-server-handle-signal (process event)
|
||||
"Handle signals for lean-server-process"
|
||||
(force-mode-line-update)
|
||||
(let ((event-string (s-trim event)))
|
||||
(lean-debug "lean-server-handle-signal: %s"
|
||||
(propertize event-string 'face '(:foreground "red")))
|
||||
(if (s-contains? "abnormally" event)
|
||||
(message (concat "Lean server died. See lean-server stderr buffer for details; "
|
||||
"use lean-server-restart to restart it")))))
|
||||
|
||||
(defun lean-server-session-create (path-file)
|
||||
"Creates a new server session"
|
||||
(let* ((default-directory (f--traverse-upwards (f-dir? it) path-file))
|
||||
; Setting process-connection-type is necessary, otherwise
|
||||
; emacs truncates lines with >4096 bytes:
|
||||
; https://debbugs.gnu.org/cgi/bugreport.cgi?bug=24531
|
||||
(process-connection-type nil)
|
||||
(cmd `(,(lean-get-executable lean-executable-name)
|
||||
"--server"
|
||||
,(format "-M%i" lean-memory-limit)
|
||||
,(format "-T%i" lean-timeout-limit)
|
||||
,@lean-extra-arguments
|
||||
,(format "*%s*" path-file)))
|
||||
(proc (if (fboundp 'make-process)
|
||||
(make-process ;; emacs >= 25 lets us redirect stderr
|
||||
:name "lean-server"
|
||||
:buffer (format " *lean-server (%s)*" path-file)
|
||||
:command cmd
|
||||
:coding 'utf-8
|
||||
:noquery t
|
||||
:sentinel #'lean-server-handle-signal
|
||||
:stderr (make-pipe-process
|
||||
:name "lean-server stderr"
|
||||
:buffer (format "*lean-server stderr (%s)*" path-file)
|
||||
:noquery t))
|
||||
(progn
|
||||
; emacs 24 loves directory separators, without it
|
||||
; the server gets started in the parent directory....
|
||||
(setq default-directory (format "%s/" default-directory))
|
||||
(apply #'start-process "lean-server"
|
||||
(format " *lean-server (%s)*" (buffer-name))
|
||||
cmd))))
|
||||
(sess (make-lean-server-session
|
||||
:path-file path-file
|
||||
:process proc
|
||||
:seq-num 0
|
||||
:current-roi 'not-yet-sent
|
||||
:callbacks nil
|
||||
:messages nil)))
|
||||
(set-process-filter proc (lambda (proc string) (lean-server-filter sess string)))
|
||||
(set-process-coding-system proc 'utf-8 'utf-8)
|
||||
(set-process-query-on-exit-flag proc nil)
|
||||
sess))
|
||||
|
||||
(defun lean-server-session-send-command (sess cmd-name params &optional cb error-cb)
|
||||
(let* ((seq-num (lean-server-session-seq-num sess))
|
||||
(req `(:seq_num ,seq-num :command ,cmd-name . ,params))
|
||||
(json-array-type 'list)
|
||||
(json-object-type 'plist)
|
||||
(json-false :json-false)
|
||||
(json-req (json-encode req))
|
||||
(cur-buf (current-buffer))
|
||||
(wrapped-cb (and cb
|
||||
(lambda (res)
|
||||
(and cur-buf
|
||||
(with-current-buffer cur-buf
|
||||
(apply cb :allow-other-keys t res))))))
|
||||
(wrapped-err-cb (and error-cb
|
||||
(lambda (res)
|
||||
(and cur-buf
|
||||
(with-current-buffer cur-buf
|
||||
(apply error-cb :allow-other-keys t res)))))))
|
||||
(setf (lean-server-session-seq-num sess) (1+ seq-num))
|
||||
(if (or cb error-cb)
|
||||
(setf (lean-server-session-callbacks sess)
|
||||
(cons (cons seq-num (cons wrapped-cb wrapped-err-cb)) (lean-server-session-callbacks sess))))
|
||||
(lean-debug "server<= %s" json-req)
|
||||
(process-send-string (lean-server-session-process sess)
|
||||
(concat json-req "\n"))))
|
||||
|
||||
(defvar lean-server-sessions nil
|
||||
"list of all running lean-server-sessions")
|
||||
|
||||
(defun lean-server-session-alive-p (sess)
|
||||
(and sess
|
||||
(lean-server-session-process sess)
|
||||
(equal 'run (process-status (lean-server-session-process sess)))))
|
||||
|
||||
(defun lean-server-session-kill (sess)
|
||||
(ignore-errors (delete-process (lean-server-session-process sess)))
|
||||
(ignore-errors (kill-buffer (lean-server-session-proc-buffer sess)))
|
||||
(setf (lean-server-session-process sess) nil)
|
||||
(setq lean-server-sessions (delete sess lean-server-sessions)))
|
||||
|
||||
(defun lean-server-session-get (path-file)
|
||||
(setq lean-server-sessions
|
||||
(remove-if-not #'lean-server-session-alive-p
|
||||
lean-server-sessions))
|
||||
(or (find path-file lean-server-sessions
|
||||
:test (lambda (d s) (equal d (lean-server-session-path-file s))))
|
||||
(let ((sess (lean-server-session-create path-file)))
|
||||
(setq lean-server-sessions (cons sess lean-server-sessions))
|
||||
sess)))
|
||||
|
||||
(defvar-local lean-server-session nil
|
||||
"Lean server session for the current buffer")
|
||||
|
||||
(defun lean-server-session-running-p (sess)
|
||||
(and sess (plist-get (lean-server-session-tasks sess) :is_running)))
|
||||
|
||||
(defun lean-server-status-string ()
|
||||
(if (not (lean-server-session-alive-p lean-server-session)) " ☠"
|
||||
(if (lean-server-session-running-p lean-server-session) " ⌛"
|
||||
" ✓")))
|
||||
|
||||
(defvar-local lean-server-flycheck-delay-timer nil)
|
||||
|
||||
(defvar-local lean-server-task-overlays nil)
|
||||
|
||||
(defun lean-server-task-region (task)
|
||||
(let ((bl (1- (plist-get task :pos_line)))
|
||||
(bc (plist-get task :pos_col))
|
||||
(el (1- (plist-get task :end_pos_line)))
|
||||
(ec (plist-get task :end_pos_col)))
|
||||
(save-excursion
|
||||
(widen)
|
||||
(goto-char (point-min))
|
||||
(forward-line bl)
|
||||
(if (equal (cons bl bc) (cons el ec))
|
||||
(progn
|
||||
(let ((beg (point)))
|
||||
(forward-line 1)
|
||||
(cons beg (point))))
|
||||
(ignore-errors (forward-char bc))
|
||||
(let ((beg (point)))
|
||||
(goto-char (point-min))
|
||||
(forward-line el)
|
||||
(ignore-errors (forward-char ec))
|
||||
(cons beg (point)))))))
|
||||
|
||||
(defface lean-server-task-face
|
||||
nil
|
||||
"Face to highlight pending Lean tasks."
|
||||
:group 'lean)
|
||||
|
||||
(if (fboundp 'define-fringe-bitmap)
|
||||
(define-fringe-bitmap 'lean-server-fringe-bitmap
|
||||
(vector) 16 8))
|
||||
|
||||
(defface lean-server-task-fringe-face
|
||||
'((((class color) (background light))
|
||||
:background "chocolate1")
|
||||
(((class color) (background dark))
|
||||
:background "navajo white")
|
||||
(t :inverse-video t))
|
||||
"Face to highlight the fringe of pending Lean tasks."
|
||||
:group 'lean)
|
||||
|
||||
(defun lean-server-update-task-overlays ()
|
||||
(dolist (ov lean-server-task-overlays) (delete-overlay ov))
|
||||
(setq lean-server-task-overlays nil)
|
||||
(when (and lean-server-show-pending-tasks lean-server-session)
|
||||
(let* ((tasks (lean-server-session-tasks lean-server-session))
|
||||
(cur-fn (buffer-file-name))
|
||||
(roi (cdr (assq cur-fn (lean-server-session-current-roi lean-server-session)))))
|
||||
(dolist (task (plist-get tasks :tasks))
|
||||
(if (and (equal (plist-get task :file_name) cur-fn)
|
||||
(--any? (<= (max (car it) (plist-get task :pos_line))
|
||||
(min (cdr it) (plist-get task :end_pos_line)))
|
||||
roi))
|
||||
(let* ((reg (lean-server-task-region task))
|
||||
(ov (make-overlay (car reg) (cdr reg))))
|
||||
(setq lean-server-task-overlays (cons ov lean-server-task-overlays))
|
||||
(overlay-put ov 'face 'lean-server-task-face)
|
||||
(overlay-put ov 'line-prefix
|
||||
(propertize " " 'display
|
||||
'(left-fringe lean-server-fringe-bitmap lean-server-task-fringe-face)))
|
||||
(overlay-put ov 'help-echo (format "%s..." (plist-get task :desc)))))))))
|
||||
|
||||
(defun lean-server-toggle-show-pending-tasks ()
|
||||
"Toggles highlighting of pending tasks"
|
||||
(interactive)
|
||||
(setq lean-server-show-pending-tasks (not lean-server-show-pending-tasks))
|
||||
(dolist (sess lean-server-sessions)
|
||||
(lean-server-notify-tasks-changed sess nil)))
|
||||
|
||||
(defvar-local lean-server-flycheck-delay-timer nil)
|
||||
(defvar-local lean-server-flycheck-delayed-update nil)
|
||||
|
||||
(defun lean-server-show-messages (&optional buf)
|
||||
(with-current-buffer (or buf (current-buffer))
|
||||
(save-match-data
|
||||
(when (and (eq buf flycheck-error-list-source-buffer)
|
||||
(get-buffer-window buf))
|
||||
(if (memq lean-server-flycheck-delay-timer timer-list)
|
||||
(setq lean-server-flycheck-delayed-update t) ; arm timer
|
||||
(flycheck-buffer)
|
||||
(setq lean-server-flycheck-delay-timer
|
||||
(run-at-time "100 milliseconds" nil
|
||||
(lambda (buf)
|
||||
(with-current-buffer buf
|
||||
(when lean-server-flycheck-delayed-update
|
||||
(setq lean-server-flycheck-delayed-update nil)
|
||||
(flycheck-buffer))))
|
||||
(current-buffer))))))
|
||||
(when lean-server-session
|
||||
(let ((relevant-msgs
|
||||
(remove-if-not (lambda (msg)
|
||||
(equal (buffer-file-name buf)
|
||||
(plist-get msg :file_name)))
|
||||
(lean-server-session-messages lean-server-session))))
|
||||
(dolist (hook lean-server-show-message-hook)
|
||||
(funcall hook relevant-msgs))))))
|
||||
|
||||
(defvar-local lean-server-show-tasks-delay-timer nil)
|
||||
|
||||
(defun lean-server-show-tasks (&optional buf)
|
||||
(with-current-buffer (or buf (current-buffer))
|
||||
(save-match-data
|
||||
(when (not (memq lean-server-show-tasks-delay-timer timer-list))
|
||||
(setq lean-server-show-tasks-delay-timer
|
||||
(run-at-time "300 milliseconds" nil
|
||||
(lambda (buf)
|
||||
(with-current-buffer buf
|
||||
(lean-server-update-task-overlays)))
|
||||
(current-buffer)))))))
|
||||
|
||||
(defun lean-server-notify-messages-changed (sess)
|
||||
(dolist (buf (buffer-list))
|
||||
(with-current-buffer buf
|
||||
(when (and lean-server-session
|
||||
(eq sess lean-server-session))
|
||||
(lean-server-show-messages)))))
|
||||
|
||||
(defun lean-server-notify-tasks-changed (sess old-tasks)
|
||||
(force-mode-line-update)
|
||||
(when (and (not lean-server-show-pending-tasks)
|
||||
(or (plist-get old-tasks :tasks)
|
||||
(plist-get (lean-server-session-tasks sess) :tasks)))
|
||||
; update task flycheck messages only if the task list is non-empty
|
||||
(lean-server-notify-messages-changed sess))
|
||||
(dolist (buf (buffer-list))
|
||||
(with-current-buffer buf
|
||||
(when (eq sess lean-server-session)
|
||||
(lean-server-show-tasks)))))
|
||||
|
||||
(defun lean-server-stop ()
|
||||
"Stops the lean server associated with the current buffer"
|
||||
(interactive)
|
||||
(when lean-server-session
|
||||
(lean-server-session-kill lean-server-session)))
|
||||
|
||||
(defun lean-server-ensure-alive ()
|
||||
"Ensures that the current buffer has a lean server"
|
||||
(when (not (lean-server-session-alive-p lean-server-session))
|
||||
(setq lean-server-session (lean-server-session-get (leanpkg-find-path-file)))
|
||||
(lean-server-show-tasks)
|
||||
(lean-server-show-messages)
|
||||
(lean-server-sync)))
|
||||
|
||||
(defun lean-server-restart ()
|
||||
"Restarts the lean server for the current buffer"
|
||||
(interactive)
|
||||
(lean-server-stop)
|
||||
(lean-server-ensure-alive)
|
||||
(flycheck-stop)
|
||||
(flycheck-buffer))
|
||||
|
||||
(defun lean-server-send-command (cmd params &optional cb error-cb)
|
||||
"Sends a command to the lean server for the current buffer, with a callback to be called upon completion"
|
||||
(lean-server-ensure-alive)
|
||||
(lean-server-session-send-command lean-server-session cmd params cb error-cb))
|
||||
|
||||
(defun lean-server-send-synchronous-command (cmd params)
|
||||
"Sends a command to the lean server for the current buffer, waiting for and returning the response"
|
||||
;; inspired by company--force-sync
|
||||
(let ((res 'trash)
|
||||
(ok t)
|
||||
(start (time-to-seconds)))
|
||||
(lean-server-send-command cmd params
|
||||
(lambda (&rest result) (setq res result))
|
||||
(cl-function
|
||||
(lambda (&key message)
|
||||
(setq ok nil)
|
||||
(setq res message))))
|
||||
(while (eq res 'trash)
|
||||
(if (> (- (time-to-seconds) start) company-async-timeout)
|
||||
(error "Lean server timed out")
|
||||
(sleep-for company-async-wait)))
|
||||
(if ok
|
||||
res
|
||||
(error res))))
|
||||
|
||||
(defun lean-server-sync (&optional buf)
|
||||
"Synchronizes the state of BUF (or the current buffer, if nil) with the lean server"
|
||||
(with-demoted-errors "lean server sync: %s"
|
||||
(with-current-buffer (or buf (current-buffer))
|
||||
(lean-server-sync-roi)
|
||||
(lean-server-send-command
|
||||
'sync (list :file_name (buffer-file-name)
|
||||
:content (buffer-string))))))
|
||||
|
||||
(defvar-local lean-server-sync-timer nil)
|
||||
|
||||
(defun lean-server-change-hook (begin end len)
|
||||
(save-match-data
|
||||
(when lean-server-sync-timer (cancel-timer lean-server-sync-timer))
|
||||
(setq lean-server-sync-timer
|
||||
(run-at-time "50 milliseconds" nil #'lean-server-sync (current-buffer)))))
|
||||
|
||||
(defun lean-server-compute-roi (sess)
|
||||
"Compute the region of interest for the session SESS."
|
||||
(--mapcat (with-current-buffer it
|
||||
(when (eq lean-server-session sess)
|
||||
(list (cons (buffer-file-name)
|
||||
(--map (cons (line-number-at-pos (window-start it))
|
||||
(line-number-at-pos (window-end it t)))
|
||||
(get-buffer-window-list))))))
|
||||
(buffer-list)))
|
||||
|
||||
(defun lean-server-session-send-roi (sess roi)
|
||||
(setf (lean-server-session-current-roi sess) roi)
|
||||
(lean-server-send-command
|
||||
'roi (list :mode lean-server-check-mode
|
||||
:files (--map (list (cons :file_name (car it))
|
||||
(cons :ranges (--map (list (cons :begin_line (car it))
|
||||
(cons :end_line (cdr it)))
|
||||
(cdr it))))
|
||||
roi))))
|
||||
|
||||
(defun lean-server-roi-subset-p (as bs)
|
||||
(--all? (let ((b (cdr (assq (car it) bs))))
|
||||
(and b (-all? (lambda (ar) (--any? (and (<= (car it) (car ar))
|
||||
(<= (cdr ar) (cdr it)))
|
||||
b))
|
||||
(cdr it))))
|
||||
as))
|
||||
|
||||
(defun lean-server-roi-extend (roi delta)
|
||||
(--map `(,(car it) .
|
||||
,(--map `(,(max 1 (- (car it) delta)) . ,(+ (cdr it) delta)) (cdr it)))
|
||||
roi))
|
||||
|
||||
(defun lean-server-roi-ok (old-roi new-roi)
|
||||
(and (lean-server-roi-subset-p new-roi old-roi)
|
||||
(lean-server-roi-subset-p old-roi (lean-server-roi-extend new-roi 10))))
|
||||
|
||||
(defun lean-server-sync-roi (&optional force)
|
||||
(when lean-server-session
|
||||
(let ((old-roi (lean-server-session-current-roi lean-server-session))
|
||||
(new-roi (lean-server-compute-roi lean-server-session)))
|
||||
(when (or force (eq old-roi 'not-yet-sent) (not (lean-server-roi-ok old-roi new-roi)))
|
||||
(lean-server-session-send-roi lean-server-session
|
||||
(lean-server-roi-extend new-roi 5))))))
|
||||
|
||||
(defun lean-server-window-scroll-function-hook (wnd new-start-pos)
|
||||
(let ((buf (window-buffer wnd)))
|
||||
(with-demoted-errors "lean scroll hook: %s"
|
||||
(with-current-buffer buf
|
||||
(lean-server-ensure-alive)
|
||||
(lean-server-sync-roi)))))
|
||||
|
||||
(defun lean-set-check-mode (mode)
|
||||
(setq lean-server-check-mode mode)
|
||||
(lean-server-sync-roi t))
|
||||
|
||||
(defun lean-check-nothing ()
|
||||
"Check nothing"
|
||||
(interactive)
|
||||
(lean-set-check-mode 'nothing))
|
||||
|
||||
(defun lean-check-visible-lines ()
|
||||
"Check visible lines"
|
||||
(interactive)
|
||||
(lean-set-check-mode 'visible-lines))
|
||||
|
||||
(defun lean-check-visible-lines-and-above ()
|
||||
"Check visible lines and above"
|
||||
(interactive)
|
||||
(lean-set-check-mode 'visible-lines-and-above))
|
||||
|
||||
(defun lean-check-visible-files ()
|
||||
"Check visible files"
|
||||
(interactive)
|
||||
(lean-set-check-mode 'visible-files))
|
||||
|
||||
(defun lean-check-open-files ()
|
||||
"Check visible files"
|
||||
(interactive)
|
||||
(lean-set-check-mode 'open-files))
|
||||
|
||||
(provide 'lean-server)
|
||||
|
|
@ -1,147 +0,0 @@
|
|||
;; 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
|
||||
('gnu "lean")
|
||||
('gnu/linux "lean")
|
||||
('gnu/kfreebsd "lean")
|
||||
('darwin "lean")
|
||||
('ms-dos "lean")
|
||||
('windows-nt "lean.exe")
|
||||
('cygwin "lean.exe"))
|
||||
"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-company-use t
|
||||
"Use company mode for lean."
|
||||
:group 'lean
|
||||
:type 'boolean)
|
||||
|
||||
(defcustom lean-company-type-foreground (face-foreground 'font-lock-keyword-face)
|
||||
"Color of type parameter in auto-complete candidates"
|
||||
:group 'lean
|
||||
:type 'color)
|
||||
|
||||
(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-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-pkg-configure"
|
||||
:group 'lean-keybinding :type 'key-sequence)
|
||||
(defcustom lean-keybinding-leanpkg-build (kbd "C-c C-p C-b")
|
||||
"Lean Keybinding for lean-pkg-build"
|
||||
:group 'lean-keybinding :type 'key-sequence)
|
||||
(defcustom lean-keybinding-leanpkg-test (kbd "C-c C-p C-t")
|
||||
"Lean Keybinding for lean-pkg-test"
|
||||
:group 'lean-keybinding :type 'key-sequence)
|
||||
(defcustom lean-keybinding-lean-helm-definitions (kbd "C-c C-d")
|
||||
"Lean Keybinding for lean-helm-definitions"
|
||||
:group 'lean-keybinding :type 'key-sequence)
|
||||
(provide 'lean-settings)
|
||||
|
|
@ -1,194 +0,0 @@
|
|||
;; 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"
|
||||
"open" "export" "axiom" "axioms" "inductive" "coinductive" "with" "without" "inout"
|
||||
"structure" "universe" "universes"
|
||||
"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)
|
||||
|
|
@ -1,96 +0,0 @@
|
|||
;; 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-get-rootdir ()
|
||||
(or
|
||||
lean-rootdir
|
||||
(error
|
||||
(concat "'lean-rootdir' is not defined."
|
||||
"Please have (customize-set-variable 'lean-rootdir \"~/work/lean\") "
|
||||
"in your emacs configuration. "
|
||||
"Also make sure that your (custom-set-variable ...) "
|
||||
" comes before (require 'lean-mode)"))))
|
||||
|
||||
(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)
|
||||
Binary file not shown.
|
|
@ -1,64 +0,0 @@
|
|||
(setq inhibit-startup-screen t)
|
||||
|
||||
(if (getenv "LEAN_ROOTDIR")
|
||||
(setq lean-rootdir (getenv "LEAN_ROOTDIR"))
|
||||
(error "LEAN_ROOTDIR environment variable must be set"))
|
||||
|
||||
(if (getenv "LEAN_EMACS_PATH")
|
||||
(setq-local lean-emacs-path (getenv "LEAN_EMACS_PATH"))
|
||||
(error "LEAN_EMACS_PATH environment variable must be set"))
|
||||
|
||||
(setq lean-logo
|
||||
(condition-case nil
|
||||
(create-image (format "%s/lean.pgm" lean-emacs-path))
|
||||
(error nil)))
|
||||
|
||||
(setq lean-required-packages '(company dash dash-functional f
|
||||
flycheck let-alist s seq unicode-fonts))
|
||||
|
||||
(require 'package)
|
||||
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/"))
|
||||
(package-initialize)
|
||||
(let ((need-to-refresh t))
|
||||
(dolist (p lean-required-packages)
|
||||
(when (not (package-installed-p p))
|
||||
(when need-to-refresh
|
||||
(package-refresh-contents)
|
||||
(setq need-to-refresh nil))
|
||||
(package-install p))))
|
||||
|
||||
; This enables out-of-the-box support for characters such as ℕ at least on Windows.
|
||||
(require 'unicode-fonts)
|
||||
(unicode-fonts-setup)
|
||||
|
||||
(setq load-path (cons lean-emacs-path load-path))
|
||||
|
||||
(require 'lean-mode)
|
||||
|
||||
(defun lean-welcome ()
|
||||
(let ((cbuf (current-buffer))
|
||||
(buf (get-buffer-create "Lean Welcome"))
|
||||
(cpoint (point-min)))
|
||||
(set-buffer buf)
|
||||
(setq fill-column (window-width))
|
||||
(if buffer-read-only (toggle-read-only))
|
||||
(erase-buffer)
|
||||
(insert "\n\n")
|
||||
(insert " ")
|
||||
(when lean-logo (insert-image lean-logo))
|
||||
(setq cpoint (1+ (point)))
|
||||
(insert "\n")
|
||||
(insert "\n\nPlease check our website periodically for news of later versions")
|
||||
(insert "\nat http://leanprover.github.io")
|
||||
(insert "\n\nBug reports and suggestions for improvement should be posted at")
|
||||
(insert "\nhttps://github.com/leanprover/lean/issues")
|
||||
(insert "\n\nTo start using Lean, open a .lean file")
|
||||
(set-buffer-modified-p nil)
|
||||
(text-mode)
|
||||
(toggle-read-only)
|
||||
(goto-char (point-min))
|
||||
(switch-to-buffer buf)
|
||||
(set-buffer cbuf)
|
||||
buf))
|
||||
|
||||
(lean-welcome)
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
;; Released under Apache 2.0 license as described in the file LICENSE.
|
||||
;;
|
||||
;; Author: Soonho Kong
|
||||
;;
|
||||
|
||||
(defconst lean-test/test-path
|
||||
(f-parent (f-this-file)))
|
||||
|
||||
(defconst lean-test/root-path
|
||||
(f-parent lean-test/test-path))
|
||||
|
||||
(add-to-list 'load-path lean-test/root-path)
|
||||
|
||||
;; Avoid Emacs 23 interupting the tests with:
|
||||
;; File bar-autoloads.el changed on disk. Reread from disk? (yes or no)
|
||||
(fset 'y-or-n-p (lambda (_) t))
|
||||
(fset 'yes-or-no-p (lambda (_) t))
|
||||
Loading…
Add table
Reference in a new issue