From 5efa1b829cfb4df5e5f4ddaec96c6d8707d24236 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 3 Oct 2017 16:11:35 +0200 Subject: [PATCH] chore(src/emacs): move lean-mode to https://github.com/leanprover/lean-mode Closes #410 --- README.md | 1 - bin/.gitignore | 2 - bin/leanemacs.bat.in | 4 - bin/leanemacs.in | 8 - bin/leanemacs_build | 8 - bin/leanemacs_build.bat | 4 - bin/test_leanemacs | 9 - doc/bin/README.md | 13 +- doc/changes.md | 2 + src/CMakeLists.txt | 23 - src/emacs/.gitignore | 2 - src/emacs/CMakeLists.txt | 2 - src/emacs/Cask | 14 - src/emacs/Makefile | 17 - src/emacs/README.md | 165 --- src/emacs/eri.el | 206 --- src/emacs/features/emacs.feature | 11 - .../features/step-definitions/emacs-steps.el | 28 - src/emacs/features/support/env.el | 32 - src/emacs/lean-company.el | 187 --- src/emacs/lean-debug.el | 47 - src/emacs/lean-dev.el | 16 - src/emacs/lean-hole.el | 151 --- src/emacs/lean-info.el | 118 -- src/emacs/lean-input.el | 1167 ----------------- src/emacs/lean-message-boxes.el | 124 -- src/emacs/lean-mode.el | 233 ---- src/emacs/lean-pkg.el | 93 -- src/emacs/lean-require.el | 32 - src/emacs/lean-right-click.el | 84 -- src/emacs/lean-server.el | 487 ------- src/emacs/lean-settings.el | 147 --- src/emacs/lean-syntax.el | 194 --- src/emacs/lean-util.el | 96 -- src/emacs/lean.pgm | Bin 40219 -> 0 bytes src/emacs/load-lean.el | 64 - src/emacs/test/test-helper.el | 18 - 37 files changed, 3 insertions(+), 3806 deletions(-) delete mode 100644 bin/leanemacs.bat.in delete mode 100644 bin/leanemacs.in delete mode 100755 bin/leanemacs_build delete mode 100644 bin/leanemacs_build.bat delete mode 100755 bin/test_leanemacs delete mode 100644 src/emacs/.gitignore delete mode 100644 src/emacs/CMakeLists.txt delete mode 100644 src/emacs/Cask delete mode 100644 src/emacs/Makefile delete mode 100644 src/emacs/README.md delete mode 100644 src/emacs/eri.el delete mode 100644 src/emacs/features/emacs.feature delete mode 100644 src/emacs/features/step-definitions/emacs-steps.el delete mode 100644 src/emacs/features/support/env.el delete mode 100644 src/emacs/lean-company.el delete mode 100644 src/emacs/lean-debug.el delete mode 100644 src/emacs/lean-dev.el delete mode 100644 src/emacs/lean-hole.el delete mode 100644 src/emacs/lean-info.el delete mode 100644 src/emacs/lean-input.el delete mode 100644 src/emacs/lean-message-boxes.el delete mode 100644 src/emacs/lean-mode.el delete mode 100644 src/emacs/lean-pkg.el delete mode 100644 src/emacs/lean-require.el delete mode 100644 src/emacs/lean-right-click.el delete mode 100644 src/emacs/lean-server.el delete mode 100644 src/emacs/lean-settings.el delete mode 100644 src/emacs/lean-syntax.el delete mode 100644 src/emacs/lean-util.el delete mode 100644 src/emacs/lean.pgm delete mode 100644 src/emacs/load-lean.el delete mode 100644 src/emacs/test/test-helper.el diff --git a/README.md b/README.md index c3c44adb2d..141fc19cd8 100644 --- a/README.md +++ b/README.md @@ -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). diff --git a/bin/.gitignore b/bin/.gitignore index 092ee93bcf..3d8d939615 100644 --- a/bin/.gitignore +++ b/bin/.gitignore @@ -1,4 +1,2 @@ lean lean.exe -leanemacs -leanemacs.bat diff --git a/bin/leanemacs.bat.in b/bin/leanemacs.bat.in deleted file mode 100644 index 229370621f..0000000000 --- a/bin/leanemacs.bat.in +++ /dev/null @@ -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 diff --git a/bin/leanemacs.in b/bin/leanemacs.in deleted file mode 100644 index 3238b9a7a4..0000000000 --- a/bin/leanemacs.in +++ /dev/null @@ -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 $* diff --git a/bin/leanemacs_build b/bin/leanemacs_build deleted file mode 100755 index ea1fe78f1b..0000000000 --- a/bin/leanemacs_build +++ /dev/null @@ -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 $* diff --git a/bin/leanemacs_build.bat b/bin/leanemacs_build.bat deleted file mode 100644 index 6000c8c2c2..0000000000 --- a/bin/leanemacs_build.bat +++ /dev/null @@ -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 diff --git a/bin/test_leanemacs b/bin/test_leanemacs deleted file mode 100755 index 448cc3d96a..0000000000 --- a/bin/test_leanemacs +++ /dev/null @@ -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 $* diff --git a/doc/bin/README.md b/doc/bin/README.md index 586389e980..6fb6537690 100644 --- a/doc/bin/README.md +++ b/doc/bin/README.md @@ -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/. diff --git a/doc/changes.md b/doc/changes.md index d6744ec191..02537f17ee 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -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` diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1866200fb2..2abb6800f2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -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} $) @@ -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. diff --git a/src/emacs/.gitignore b/src/emacs/.gitignore deleted file mode 100644 index 433da842b5..0000000000 --- a/src/emacs/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -.cask -*.elc diff --git a/src/emacs/CMakeLists.txt b/src/emacs/CMakeLists.txt deleted file mode 100644 index 5267bb812d..0000000000 --- a/src/emacs/CMakeLists.txt +++ /dev/null @@ -1,2 +0,0 @@ -FILE(GLOB LEAN_MODE_FILES *.el) -install(FILES ${LEAN_MODE_FILES} DESTINATION "${EMACS_LISP_DIR}") diff --git a/src/emacs/Cask b/src/emacs/Cask deleted file mode 100644 index bbe6d6bd0c..0000000000 --- a/src/emacs/Cask +++ /dev/null @@ -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")) diff --git a/src/emacs/Makefile b/src/emacs/Makefile deleted file mode 100644 index dcdf9350d8..0000000000 --- a/src/emacs/Makefile +++ /dev/null @@ -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 diff --git a/src/emacs/README.md b/src/emacs/README.md deleted file mode 100644 index 8b9dff8300..0000000000 --- a/src/emacs/README.md +++ /dev/null @@ -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 | -|--------------------|---------------------------------------------------------------------------------| -| M-. | jump to definition in source file (`lean-find-definition`) | -| S-SPC | auto complete identifiers, options, imports, etc. (`company-complete`) | -| C-c C-k | shows the keystroke needed to input the symbol under the cursor | -| C-c C-x | execute lean in stand-alone mode (`lean-std-exe`) | -| C-c SPC | run a command on the hole at point (`lean-hole`) -| C-c C-g | toggle showing current tactic proof goal (`lean-toggle-show-goal`) | -| C-c C-n | toggle showing next error in dedicated buffer (`lean-toggle-next-error`) | -| C-c C-b | toggle showing output in inline boxes (`lean-message-boxes-toggle`) | -| C-c C-r | restart the lean server (`lean-server-restart`) | -| C-c ! n | flycheck: go to next error | -| C-c ! p | flycheck: go to previous error | -| C-c ! l | flycheck: show list of errors | - -In the default configuration, the Flycheck annotation `FlyC:n/n` indicates the -number of errors / responses from Lean; clicking on `FlyC` opens the Flycheck menu. - - -Message Boxes -================ -To view the output of commands such as `check` and `print` in boxes in the buffer, enable the feature using C-c C-b. -If you then type -```lean -#check id -``` -a box appears after the line showing the type of `id`. Customize `lean-message-boxes-enabled-captions` to choose categories of boxes. -In particular, add `"trace output"` to the list to see proof states and other traces in the buffer. - -Requirements -============ - -``lean-mode`` requires [Emacs 24][emacs24] or later and the following -packages, which can be installed via M-x package-install: -[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 diff --git a/src/emacs/eri.el b/src/emacs/eri.el deleted file mode 100644 index d76307feaa..0000000000 --- a/src/emacs/eri.el +++ /dev/null @@ -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 diff --git a/src/emacs/features/emacs.feature b/src/emacs/features/emacs.feature deleted file mode 100644 index 979516d84d..0000000000 --- a/src/emacs/features/emacs.feature +++ /dev/null @@ -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" diff --git a/src/emacs/features/step-definitions/emacs-steps.el b/src/emacs/features/step-definitions/emacs-steps.el deleted file mode 100644 index 21bddec130..0000000000 --- a/src/emacs/features/step-definitions/emacs-steps.el +++ /dev/null @@ -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) - ;; ... - )) diff --git a/src/emacs/features/support/env.el b/src/emacs/features/support/env.el deleted file mode 100644 index aa09e4813d..0000000000 --- a/src/emacs/features/support/env.el +++ /dev/null @@ -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 - ) diff --git a/src/emacs/lean-company.el b/src/emacs/lean-company.el deleted file mode 100644 index 1d8bd1d261..0000000000 --- a/src/emacs/lean-company.el +++ /dev/null @@ -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) diff --git a/src/emacs/lean-debug.el b/src/emacs/lean-debug.el deleted file mode 100644 index 196fed44c9..0000000000 --- a/src/emacs/lean-debug.el +++ /dev/null @@ -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) diff --git a/src/emacs/lean-dev.el b/src/emacs/lean-dev.el deleted file mode 100644 index 2502132fa5..0000000000 --- a/src/emacs/lean-dev.el +++ /dev/null @@ -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) diff --git a/src/emacs/lean-hole.el b/src/emacs/lean-hole.el deleted file mode 100644 index 864dfd241b..0000000000 --- a/src/emacs/lean-hole.el +++ /dev/null @@ -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 diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el deleted file mode 100644 index 6eb96d4f2f..0000000000 --- a/src/emacs/lean-info.el +++ /dev/null @@ -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 -;; Maintainer: Gabriel Ebner -;; Created: Oct 29, 2016 -;; Keywords: languages -;; Version: 0.1 -;; URL: https://github.com/leanprover/lean/blob/master/src/emacs -;; -;; Released under Apache 2.0 license as described in the file LICENSE. -;; - -;; 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) diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el deleted file mode 100644 index dcbfdddf76..0000000000 --- a/src/emacs/lean-input.el +++ /dev/null @@ -1,1167 +0,0 @@ -;;; lean-input.el --- The Lean input method (based/copied from Agda) -;;; -;;; DISCLAIMER: This file is based on agda-input.el provided with the Agda language. -;;; We did minor modifications -;; -;;; Commentary: -;; -;;;; A highly customisable input method which can inherit from other -;; Quail input methods. By default the input method is geared towards -;; the input of mathematical and other symbols in Lean programs. -;; -;; Use M-x customize-group lean-input to customise this input method. -;; Note that the functions defined under "Functions used to tweak -;; translation pairs" below can be used to tweak both the key -;; translations inherited from other input methods as well as the -;; ones added specifically for this one. -;; -;; Use lean-input-show-translations to see all the characters which -;; can be typed using this input method (except for those -;; corresponding to ASCII characters). - -;;; Code: - -(require 'quail) - -(eval-when-compile - (require 'cl)) -;; Quail is quite stateful, so be careful when editing this code. Note -;; that with-temp-buffer is used below whenever buffer-local state is -;; modified. - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Utility functions - -(defun lean-input-concat-map (f xs) - "Concat (map F XS)." - (apply 'append (mapcar f xs))) - -(defun lean-input-to-string-list (s) - "Convert a string S to a list of one-character strings, after -removing all space and newline characters." - (lean-input-concat-map - (lambda (c) (if (member c (string-to-list " \n")) - nil - (list (string c)))) - (string-to-list s))) - -(defun lean-input-character-range (from to) - "A string consisting of the characters from FROM to TO." - (let (seq) - (dotimes (i (1+ (- to from))) - (setq seq (cons (+ from i) seq))) - (concat (nreverse seq)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Functions used to tweak translation pairs - -;; lexical-let is used since Elisp lacks lexical scoping. - -(defun lean-input-compose (f g) - "\x -> concatMap F (G x)" - (lexical-let ((f1 f) (g1 g)) - (lambda (x) (lean-input-concat-map f1 (funcall g1 x))))) - -(defun lean-input-or (f g) - "\x -> F x ++ G x" - (lexical-let ((f1 f) (g1 g)) - (lambda (x) (append (funcall f1 x) (funcall g1 x))))) - -(defun lean-input-nonempty () - "Only keep pairs with a non-empty first component." - (lambda (x) (if (> (length (car x)) 0) (list x)))) - -(defun lean-input-prepend (prefix) - "Prepend PREFIX to all key sequences." - (lexical-let ((prefix1 prefix)) - (lambda (x) `((,(concat prefix1 (car x)) . ,(cdr x)))))) - -(defun lean-input-prefix (prefix) - "Only keep pairs whose key sequence starts with PREFIX." - (lexical-let ((prefix1 prefix)) - (lambda (x) - (if (equal (substring (car x) 0 (length prefix1)) prefix1) - (list x))))) - -(defun lean-input-suffix (suffix) - "Only keep pairs whose key sequence ends with SUFFIX." - (lexical-let ((suffix1 suffix)) - (lambda (x) - (if (equal (substring (car x) - (- (length (car x)) (length suffix1))) - suffix1) - (list x))))) - -(defun lean-input-drop (ss) - "Drop pairs matching one of the given key sequences. -SS should be a list of strings." - (lexical-let ((ss1 ss)) - (lambda (x) (unless (member (car x) ss1) (list x))))) - -(defun lean-input-drop-beginning (n) - "Drop N characters from the beginning of each key sequence." - (lexical-let ((n1 n)) - (lambda (x) `((,(substring (car x) n1) . ,(cdr x)))))) - -(defun lean-input-drop-end (n) - "Drop N characters from the end of each key sequence." - (lexical-let ((n1 n)) - (lambda (x) - `((,(substring (car x) 0 (- (length (car x)) n1)) . - ,(cdr x)))))) - -(defun lean-input-drop-prefix (prefix) - "Only keep pairs whose key sequence starts with PREFIX. -This prefix is dropped." - (lean-input-compose - (lean-input-drop-beginning (length prefix)) - (lean-input-prefix prefix))) - -(defun lean-input-drop-suffix (suffix) - "Only keep pairs whose key sequence ends with SUFFIX. -This suffix is dropped." - (lexical-let ((suffix1 suffix)) - (lean-input-compose - (lean-input-drop-end (length suffix1)) - (lean-input-suffix suffix1)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Customization - -;; The :set keyword is set to 'lean-input-incorporate-changed-setting -;; so that the input method gets updated immediately when users -;; customize it. However, the setup functions cannot be run before all -;; variables have been defined. Hence the :initialize keyword is set to -;; 'custom-initialize-default to ensure that the setup is not performed -;; until lean-input-setup is called at the end of this file. - -(defgroup lean-input nil - "The Lean input method. -After tweaking these settings you may want to inspect the resulting -translations using `lean-input-show-translations'." - :group 'lean - :group 'leim) - -(defcustom lean-input-tweak-all - '(lean-input-compose - (lean-input-prepend "\\") - (lean-input-nonempty)) - "An expression yielding a function which can be used to tweak -all translations before they are included in the input method. -The resulting function (if non-nil) is applied to every -\(KEY-SEQUENCE . TRANSLATION) pair and should return a list of such -pairs. (Note that the translations can be anything accepted by -`quail-defrule'.) - -If you change this setting manually (without using the -customization buffer) you need to call `lean-input-setup' in -order for the change to take effect." - :group 'lean-input - :set 'lean-input-incorporate-changed-setting - :initialize 'custom-initialize-default - :type 'sexp) - -(defcustom lean-input-inherit - `(("TeX" . (lean-input-compose - (lean-input-drop '("geq" "leq" "bullet" "qed" "par")) - (lean-input-or - (lean-input-drop-prefix "\\") - (lean-input-or - (lean-input-compose - (lean-input-drop '("^o")) - (lean-input-prefix "^")) - (lean-input-prefix "_"))))) - ) - "A list of Quail input methods whose translations should be -inherited by the Lean input method (with the exception of -translations corresponding to ASCII characters). - -The list consists of pairs (qp . tweak), where qp is the name of -a Quail package, and tweak is an expression of the same kind as -`lean-input-tweak-all' which is used to tweak the translation -pairs of the input method. - -The inherited translation pairs are added last, after -`lean-input-user-translations' and `lean-input-translations'. - -If you change this setting manually (without using the -customization buffer) you need to call `lean-input-setup' in -order for the change to take effect." - :group 'lean-input - :set 'lean-input-incorporate-changed-setting - :initialize 'custom-initialize-default - :type '(repeat (cons (string :tag "Quail package") - (sexp :tag "Tweaking function")))) - -(defcustom lean-input-translations - (let ((max-lisp-eval-depth 2800)) `( - - ;; Negation - - ("not" . ("¬")) - - ;; Equality and similar symbols. - - ("eq" . ,(lean-input-to-string-list "=∼∽≈≋∻∾∿≀≃⋍≂≅ ≌≊≡≣≐≑≒≓≔≕≖≗≘≙≚≛≜≝≞≟≍≎≏≬⋕")) - ("eqn" . ,(lean-input-to-string-list "≠≁ ≉ ≄ ≇≆ ≢ ≭ ")) - ("equiv" . ,(lean-input-to-string-list "≃⋍")) - ("iso" . ,(lean-input-to-string-list "≅≌")) - - ("=n" . ("≠")) - ("~" . ("∼")) ("~n" . ("≁")) ("homotopy" . ("∼")) - ("~~" . ("≈")) ("~~n" . ("≉")) - ("~~~" . ("≋")) - (":~" . ("∻")) - ("~-" . ("≃")) ("~-n" . ("≄")) - ("-~" . ("≂")) - ("~=" . ("≅")) ("~=n" . ("≇")) - ("~~-" . ("≊")) - ("==" . ("≡")) ("==n" . ("≢")) - ("===" . ("≣")) - (".=" . ("≐")) (".=." . ("≑")) - (":=" . ("≔")) ("=:" . ("≕")) - ("=o" . ("≗")) - ("(=" . ("≘")) - ("and=" . ("≙")) ("or=" . ("≚")) - ("*=" . ("≛")) - ("t=" . ("≜")) - ("def=" . ("≝")) - ("m=" . ("≞")) - ("?=" . ("≟")) - - ("pr" . ("↣")) - - ("1" . ("₁")) - ("2" . ("₂")) - ("3" . ("₃")) - ("4" . ("₄")) - ("5" . ("₅")) - ("6" . ("₆")) - ("7" . ("₇")) - ("8" . ("₈")) - ("9" . ("₉")) - ("0" . ("₀")) - - ;; Inequality and similar symbols. - - ("leq" . ,(lean-input-to-string-list "≤≦≲<≪⋘ ≶≺≼≾⊂⊆ ⋐⊏⊑ ⊰⊲⊴⋖⋚⋜⋞")) - ("leqn" . ,(lean-input-to-string-list "≰≨≮≴⋦ ≸⊀ ⋨⊄⊈⊊ ⋢⋤ ⋪⋬ ⋠")) - ("geq" . ,(lean-input-to-string-list "≥≧≳>≫⋙ ≷≻≽≿⊃⊇ ⋑⊐⊒ ⊱⊳⊵⋗⋛⋝⋟")) - ("geqn" . ,(lean-input-to-string-list "≱≩≯≵⋧ ≹ ⊁ ⋩⊅⊉⊋ ⋣⋥ ⋫⋭ ⋡")) - - ("<=" . ("≤")) (">=" . ("≥")) - ("<=n" . ("≰")) (">=n" . ("≱")) - ("len" . ("≰")) ("gen" . ("≱")) - ("n" . ("≯")) - ("<~" . ("≲")) (">~" . ("≳")) - ("<~n" . ("⋦")) (">~n" . ("⋧")) - ("<~nn" . ("≴")) (">~nn" . ("≵")) - - ("ssub" . ("⊂")) ("ssup" . ("⊃")) - ("ssubn" . ("⊄")) ("ssupn" . ("⊅")) - ("sub" . ("⊆")) ("sup" . ("⊇")) - ("subn" . ("⊈")) ("supn" . ("⊉")) - ("ssqub" . ("⊏")) ("ssqup" . ("⊐")) - ("squb" . ("⊑")) ("squp" . ("⊒")) - ("squbn" . ("⋢")) ("squpn" . ("⋣")) - - ;; Set membership etc. - - ("member" . ,(lean-input-to-string-list "∈∉∊∋∌∍⋲⋳⋴⋵⋶⋷⋸⋹⋺⋻⋼⋽⋾⋿")) - ("mem" . ("∈")) - - ("inn" . ("∉")) - ("nin" . ("∌")) - - ;; Types - - ("T1" . ("Type₁")) - ("T2" . ("Type₂")) - ("T+" . ("Type₊")) - - ;; Intersections, unions etc. - - ("intersection" . ,(lean-input-to-string-list "∩⋂∧⋀⋏⨇⊓⨅⋒∏ ⊼ ⨉")) - ("union" . ,(lean-input-to-string-list "∪⋃∨⋁⋎⨈⊔⨆⋓∐⨿⊽⊻⊍⨃⊎⨄⊌∑⅀")) - - ("and" . ("∧")) ("or" . ("∨")) - ("And" . ("⋀")) ("Or" . ("⋁")) - ("i" . ("∩")) ("un" . ("∪")) ("u+" . ("⊎")) ("u." . ("⊍")) - ("I" . ("⋂")) ("Un" . ("⋃")) ("U+" . ("⨄")) ("U." . ("⨃")) - ("glb" . ("⊓")) ("lub" . ("⊔")) - ("Glb" . ("⨅")) ("Lub" . ("⨆")) - - ;; Entailment etc. - - ("entails" . ,(lean-input-to-string-list "⊢⊣⊤⊥⊦⊧⊨⊩⊪⊫⊬⊭⊮⊯")) - - ("|-" . ("⊢")) ("|-n" . ("⊬")) - ("-|" . ("⊣")) - ("|=" . ("⊨")) ("|=n" . ("⊭")) - ("||-" . ("⊩")) ("||-n" . ("⊮")) - ("||=" . ("⊫")) ("||=n" . ("⊯")) - ("|||-" . ("⊪")) - - ;; Divisibility, parallelity. - - ("|" . ("∣")) ("|n" . ("∤")) - ("||" . ("∥")) ("||n" . ("∦")) - - ;; Some symbols from logic and set theory. - - ("all" . ("∀")) - ("ex" . ("∃")) - ("exn" . ("∄")) - ("0" . ("∅")) - ("empty" . ("∅")) - ("C" . ("∁")) - ("powerset" . ("𝒫")) - - ;; Corners, ceilings and floors. - - ("c" . ,(lean-input-to-string-list "⌜⌝⌞⌟⌈⌉⌊⌋")) - ("cu" . ,(lean-input-to-string-list "⌜⌝ ⌈⌉ ")) - ("cl" . ,(lean-input-to-string-list " ⌞⌟ ⌊⌋")) - - ("cul" . ("⌜")) ("cuL" . ("⌈")) - ("cur" . ("⌝")) ("cuR" . ("⌉")) - ("cll" . ("⌞")) ("clL" . ("⌊")) - ("clr" . ("⌟")) ("clR" . ("⌋")) - - ;; Various operators/symbols. - ("tr" . ,(lean-input-to-string-list "⬝▹")) - ("trans" . ,(lean-input-to-string-list "▹⬝")) - ("transport" . ("▹")) - ("con" . ("⬝")) - ("cdot" . ("⬝")) - ("dot" . ("⬝")) - ("sy" . ("⁻¹")) - ("inv" . ("⁻¹")) - ("-1" . ("⁻¹" "₋₁")) - ("-1e" . ("⁻¹ᵉ")) - ("-1f" . ("⁻¹ᶠ")) - ("-1g" . ("⁻¹ᵍ")) - ("-1h" . ("⁻¹ʰ")) - ("-1i" . ("⁻¹ⁱ")) - ("-1m" . ("⁻¹ᵐ")) - ("-1o" . ("⁻¹ᵒ")) - ("-1r" . ("⁻¹ʳ")) - ("-1p" . ("⁻¹ᵖ")) - ("-1s" . ("⁻¹ˢ")) - ("-1v" . ("⁻¹ᵛ")) - ("-1E" . ("⁻¹ᴱ")) - ("-2" . ("⁻²" "₋₂")) - ("-2o" . ("⁻²ᵒ")) - ("-3" . ("⁻³")) - ("qed" . ("∎")) - ("x" . ("×")) - ("o" . ("∘")) - ("comp" . ("∘")) - ("." . ("∙")) - ("*" . ("⋆")) - (".+" . ("∔")) - (".-" . ("∸")) - (":" . ("∶")) - ("::" . ("∷")) - ("::-" . ("∺")) - ("-:" . ("∹")) - ("+ " . ("⊹")) - ("surd3" . ("∛")) - ("surd4" . ("∜")) - ("increment" . ("∆")) - ("inf" . ("∞")) - ("&" . ("⅋")) - ("op" . ("ᵒᵖ")) - ("opf" . ("ᵒᵖᶠ")) - - ;; Circled operators. - - ("o+" . ("⊕")) - ("o--" . ("⊖")) - ("ox" . ("⊗")) - ("o/" . ("⊘")) - ("o." . ("⊙")) - ("oo" . ("⊚")) - ("o*" . ("∘*" "⊛")) - ("o=" . ("⊜")) - ("o-" . ("⊝")) - - ("O+" . ("⨁")) - ("Ox" . ("⨂")) - ("O." . ("⨀")) - ("O*" . ("⍟")) - - ;; Boxed operators. - - ("b+" . ("⊞")) - ("b-" . ("⊟")) - ("bx" . ("⊠")) - ("b." . ("⊡")) - - ;; Various symbols. - - ("integral" . ,(lean-input-to-string-list "∫∬∭∮∯∰∱∲∳")) - ("angle" . ,(lean-input-to-string-list "∟∡∢⊾⊿")) - ("join" . ,(lean-input-to-string-list "⋈⋉⋊⋋⋌⨝⟕⟖⟗")) - - ;; Arrows. - ("iff" . ("↔")) ("imp" . ("→")) - ("l" . ,(lean-input-to-string-list "←⇐⇚⇇⇆↤⇦↞↼↽⇠⇺↜⇽⟵⟸↚⇍⇷ ↹ ↢↩↫⇋⇜⇤⟻⟽⤆↶↺⟲ ")) - ("r" . ,(lean-input-to-string-list "→⇒⇛⇉⇄↦⇨↠⇀⇁⇢⇻↝⇾⟶⟹↛⇏⇸⇶ ↴ ↣↪↬⇌⇝⇥⟼⟾⤇↷↻⟳⇰⇴⟴⟿ ➵➸➙➔➛➜➝➞➟➠➡➢➣➤➧➨➩➪➫➬➭➮➯➱➲➳➺➻➼➽➾⊸")) - ("u" . ,(lean-input-to-string-list "↑⇑⟰⇈⇅↥⇧↟↿↾⇡⇞ ↰↱➦ ⇪⇫⇬⇭⇮⇯ ")) - ("d" . ,(lean-input-to-string-list "↓⇓⟱⇊⇵↧⇩↡⇃⇂⇣⇟ ↵↲↳➥ ↯ ")) - ("ud" . ,(lean-input-to-string-list "↕⇕ ↨⇳ ")) - ("lr" . ,(lean-input-to-string-list "↔⇔ ⇼↭⇿⟷⟺↮⇎⇹ ")) - ("ul" . ,(lean-input-to-string-list "↖⇖ ⇱↸ ")) - ("ur" . ,(lean-input-to-string-list "↗⇗ ➶➹➚ ")) - ("dr" . ,(lean-input-to-string-list "↘⇘ ⇲ ➴➷➘ ")) - ("dl" . ,(lean-input-to-string-list "↙⇙ ")) - ("==>" . ("⟹")) ("nattrans" . ("⟹")) ("nat_trans" . ("⟹")) - - ("l-" . ("←")) ("<-" . ("←")) ("l=" . ("⇐")) - ("r-" . ("→")) ("->" . ("→")) ("r=" . ("⇒")) ("=>" . ("⇒")) ("functor" . ("⇒")) - ("u-" . ("↑")) ("u=" . ("⇑")) - ("d-" . ("↓")) ("d=" . ("⇓")) - ("ud-" . ("↕")) ("ud=" . ("⇕")) - ("lr-" . ("↔")) ("<->" . ("↔")) ("lr=" . ("⇔")) ("<=>" . ("⇔")) - ("ul-" . ("↖")) ("ul=" . ("⇖")) - ("ur-" . ("↗")) ("ur=" . ("⇗")) - ("dr-" . ("↘")) ("dr=" . ("⇘")) - ("dl-" . ("↙")) ("dl=" . ("⇙")) - - ("l==" . ("⇚")) ("l-2" . ("⇇")) ("l-r-" . ("⇆")) - ("r==" . ("⇛")) ("r-2" . ("⇉")) ("r-3" . ("⇶")) ("r-l-" . ("⇄")) - ("u==" . ("⟰")) ("u-2" . ("⇈")) ("u-d-" . ("⇅")) - ("d==" . ("⟱")) ("d-2" . ("⇊")) ("d-u-" . ("⇵")) - - ("l--" . ("⟵")) ("<--" . ("⟵")) ("l~" . ("↜" "⇜")) - ("r--" . ("⟶")) ("-->" . ("⟶")) ("r~" . ("↝" "⇝" "⟿")) ("hom" . ("⟶")) - ("lr--" . ("⟷")) ("<-->" . ("⟷")) ("lr~" . ("↭")) - - ("l-n" . ("↚")) ("<-n" . ("↚")) ("l=n" . ("⇍")) - ("r-n" . ("↛")) ("->n" . ("↛")) ("r=n" . ("⇏")) ("=>n" . ("⇏")) - ("lr-n" . ("↮")) ("<->n" . ("↮")) ("lr=n" . ("⇎")) ("<=>n" . ("⇎")) - - ("l-|" . ("↤")) ("ll-" . ("↞")) - ("r-|" . ("↦")) ("rr-" . ("↠")) - ("u-|" . ("↥")) ("uu-" . ("↟")) - ("d-|" . ("↧")) ("dd-" . ("↡")) - ("ud-|" . ("↨")) - - ("l->" . ("↢")) - ("r->" . ("↣")) - - ("r-o" . ("⊸")) ("-o" . ("⊸")) - - ("dz" . ("↯")) - - ;; Ellipsis. - - ("..." . ,(lean-input-to-string-list "⋯⋮⋰⋱")) - - ;; Box-drawing characters. - - ("---" . ,(lean-input-to-string-list "─│┌┐└┘├┤┬┼┴╴╵╶╷╭╮╯╰╱╲╳")) - ("--=" . ,(lean-input-to-string-list "═║╔╗╚╝╠╣╦╬╩ ╒╕╘╛╞╡╤╪╧ ╓╖╙╜╟╢╥╫╨")) - ("--_" . ,(lean-input-to-string-list "━┃┏┓┗┛┣┫┳╋┻╸╹╺╻ - ┍┯┑┕┷┙┝┿┥┎┰┒┖┸┚┠╂┨┞╀┦┟╁┧┢╈┪┡╇┩ - ┮┭┶┵┾┽┲┱┺┹╊╉╆╅╄╃ ╿╽╼╾")) - ("--." . ,(lean-input-to-string-list "╌╎┄┆┈┊ - ╍╏┅┇┉┋")) - - ;; Triangles. - - ;; Big/small, black/white. - - ("t" . ,(lean-input-to-string-list "▸▹►▻◂◃◄◅▴▵▾▿◢◿◣◺◤◸◥◹")) - ("Tr" . ,(lean-input-to-string-list "◀◁▶▷▲△▼▽◬◭◮")) - - ("tb" . ,(lean-input-to-string-list "◂▸▴▾◄►◢◣◤◥")) - ("tw" . ,(lean-input-to-string-list "◃▹▵▿◅▻◿◺◸◹")) - - ("Tb" . ,(lean-input-to-string-list "◀▶▲▼")) - ("Tw" . ,(lean-input-to-string-list "◁▷△▽")) - - ;; Squares. - - ("sq" . ,(lean-input-to-string-list "◾◽■□◼◻▣▢▤▥▦▧▨▩◧◨◩◪◫◰◱◲◳")) - ("sqb" . ,(lean-input-to-string-list "■◼◾")) - ("sqw" . ,(lean-input-to-string-list "□◻◽")) - ("sq." . ("▣")) - ("sqo" . ("▢")) - - ;; Rectangles. - - ("re" . ,(lean-input-to-string-list "▬▭▮▯")) - ("reb" . ,(lean-input-to-string-list "▬▮")) - ("rew" . ,(lean-input-to-string-list "▭▯")) - - ;; Parallelograms. - - ("pa" . ,(lean-input-to-string-list "▰▱")) - ("pab" . ("▰")) - ("paw" . ("▱")) - - ;; Diamonds. - - ("di" . ,(lean-input-to-string-list "◆◇◈")) - ("dib" . ("◆")) - ("diw" . ("◇")) - ("di." . ("◈")) - - ;; Circles. - - ("ci" . ,(lean-input-to-string-list "●○◎◌◯◍◐◑◒◓◔◕◖◗◠◡◴◵◶◷⚆⚇⚈⚉")) - ("cib" . ("●")) - ("ciw" . ("○")) - ("ci." . ("◎")) - ("ci.." . ("◌")) - ("ciO" . ("◯")) - - ;; Stars. - - ("st" . ,(lean-input-to-string-list "⋆✦✧✶✴✹ ★☆✪✫✯✰✵✷✸")) - ("st4" . ,(lean-input-to-string-list "✦✧")) - ("st6" . ("✶")) - ("st8" . ("✴")) - ("st12" . ("✹")) - - ;; Blackboard bold letters. - - ("bn" . ("ℕ")) - ("bz" . ("ℤ")) - ("bq" . ("ℚ")) - ("br" . ("ℝ")) - ("bc" . ("ℂ")) - ("bp" . ("ℙ")) - ("bb" . ("𝔹")) - ("bsum" . ("⅀")) - - ;; Blackboard bold numbers. - - ("b0" . ("𝟘")) - ("b1" . ("𝟙")) - ("b2" . ("𝟚")) - ("b3" . ("𝟛")) - ("b4" . ("𝟜")) - ("b5" . ("𝟝")) - ("b6" . ("𝟞")) - ("b7" . ("𝟟")) - ("b8" . ("𝟠")) - ("b9" . ("𝟡")) - - ;; Parentheses. - - ("(" . ,(lean-input-to-string-list "([{⁅⁽₍〈⎴⟅⟦⟨⟪⦃〈《‹«「『【〔〖〚︵︷︹︻︽︿﹁﹃﹙﹛﹝（［｛｢")) - (")" . ,(lean-input-to-string-list ")]}⁆⁾₎〉⎵⟆⟧⟩⟫⦄〉》›»」』】〕〗〛︶︸︺︼︾﹀﹂﹄﹚﹜﹞）］｝｣")) - - ("[[" . ("⟦")) - ("]]" . ("⟧")) - ("<" . ("⟨")) - (">" . ("⟩")) - ("<<" . ("⟪")) - (">>" . ("⟫")) - ("f<" . ("‹")) - ("f>" . ("›")) - ("f<<" . ("«")) - ("f>>" . ("»")) - ("{{" . ("⦃")) - ("}}" . ("⦄")) - - ("(b" . ("⟅")) - (")b" . ("⟆")) - - ("lbag" . ("⟅")) - ("rbag" . ("⟆")) - - ;; lambda - - ("fun" . ("λ")) - ("lam" . ("λ")) - - ("X" . ("⨯")) - - ;; Primes. - - ("'" . ,(lean-input-to-string-list "′″‴⁗")) - ("`" . ,(lean-input-to-string-list "‵‶‷")) - - ;; Fractions. - - ("frac" . ,(lean-input-to-string-list "¼½¾⅓⅔⅕⅖⅗⅘⅙⅚⅛⅜⅝⅞⅟")) - - ;; Bullets. - - ("bu" . ,(lean-input-to-string-list "•◦‣⁌⁍")) - ("bub" . ("•")) - ("buw" . ("◦")) - ("but" . ("‣")) - - ;; Types - ("nat" . ("ℕ")) - ("Nat" . ("ℕ")) - ("N" . ("ℕ")) - ("N-2" . ("ℕ₋₂")) - ("N-1" . ("ℕ₋₁")) - ("int" . ("ℤ")) - ("Int" . ("ℤ")) - ("Z" . ("ℤ")) - ("rat" . ("ℚ")) - ("Rat" . ("ℚ")) - ("Q" . ("ℚ")) - ("real" . ("ℝ")) - ("Real" . ("ℝ")) - ("R" . ("ℝ")) - ("Com" . ("ℂ")) - ("com" . ("ℂ")) - ("C" . ("ℂ")) - ("A" . ("𝔸")) - ("F" . ("𝔽")) - ("H" . ("ℍ")) - ("K" . ("𝕂")) - - ("a" . ("α")) - ("b" . ("β")) - ("g" . ("γ")) - - ;; Musical symbols. - - ("note" . ,(lean-input-to-string-list "♩♪♫♬")) - ("flat" . ("♭")) - ("#" . ("♯")) - - ;; Other punctuation and symbols. - - ("\\" . ("\\")) - ("en" . ("–")) - ("em" . ("—")) - ("^i" . ("ⁱ")) - ("^o" . ("ᵒ")) - ("!!" . ("‼")) - ("??" . ("⁇")) - ("?!" . ("‽" "⁈")) - ("!?" . ("⁉")) - ("die" . ,(lean-input-to-string-list "⚀⚁⚂⚃⚄⚅")) - ("asterisk" . ,(lean-input-to-string-list "⁎⁑⁂✢✣✤✥✱✲✳✺✻✼✽❃❉❊❋")) - ("8<" . ("✂" "✄")) - ("tie" . ("⁀")) - ("undertie" . ("‿")) - ("apl" . ,(lean-input-to-string-list "⌶⌷⌸⌹⌺⌻⌼⌽⌾⌿⍀⍁⍂⍃⍄⍅⍆⍇⍈ - ⍉⍊⍋⍌⍍⍎⍏⍐⍑⍒⍓⍔⍕⍖⍗⍘⍙⍚⍛ - ⍜⍝⍞⍟⍠⍡⍢⍣⍤⍥⍦⍧⍨⍩⍪⍫⍬⍭⍮ - ⍯⍰⍱⍲⍳⍴⍵⍶⍷⍸⍹⍺⎕")) - - ;; Some combining characters. - ;; - ;; The following combining characters also have (other) - ;; translations: - ;; ̀ ́ ̂ ̃ ̄ ̆ ̇ ̈ ̋ ̌ ̣ ̧ ̱ - - ("^--" . ,(lean-input-to-string-list"̅̿")) - ("_--" . ,(lean-input-to-string-list"̲̳")) - ("^~" . ,(lean-input-to-string-list"̃͌")) - ("_~" . ( "̰")) - ("^." . ,(lean-input-to-string-list"̇̈⃛⃜")) - ("_." . ,(lean-input-to-string-list"̣̤")) - ("^l" . ,(lean-input-to-string-list"⃖⃐⃔")) - ("^l-" . ( "⃖")) - ("^r" . ,(lean-input-to-string-list"⃗⃑⃕")) - ("^r-" . ( "⃗")) - ("^lr" . ( "⃡")) - ("_lr" . ( "͍")) - ("^^" . ,(lean-input-to-string-list"̂̑͆")) - ("_^" . ,(lean-input-to-string-list"̭̯̪")) - ("^v" . ,(lean-input-to-string-list"̌̆")) - ("_v" . ,(lean-input-to-string-list"̬̮̺")) - - ;; Shorter forms of many greek letters plus ƛ. - - ("Ga" . ("α")) ("GA" . ("Α")) - ("Gb" . ("β")) ("GB" . ("Β")) - ("Gg" . ("γ")) ("GG" . ("Γ")) - ("Gd" . ("δ")) ("GD" . ("Δ")) - ("Ge" . ("ε")) ("GE" . ("Ε")) ("eps" . ("ε")) - ("Gz" . ("ζ")) ("GZ" . ("Ζ")) - ;; \eta \Eta - ("Gth" . ("θ")) ("GTH" . ("Θ")) ("th" . ("θ")) - ("Gi" . ("ι")) ("GI" . ("Ι")) - ("Gk" . ("κ")) ("GK" . ("Κ")) - ("Gl" . ("λ")) ("GL" . ("Λ")) ("Gl-" . ("ƛ")) - ("Gm" . ("μ")) ("GM" . ("Μ")) - ("Gn" . ("ν")) ("GN" . ("Ν")) - ("Gx" . ("ξ")) ("GX" . ("Ξ")) - ;; \omicron \Omicron - ;; \pi \Pi - ("Gr" . ("ρ")) ("GR" . ("Ρ")) - ("Gs" . ("σ")) ("GS" . ("Σ")) - ("Gt" . ("τ")) ("GT" . ("Τ")) - ("Gu" . ("υ")) ("GU" . ("Υ")) - ("Gf" . ("φ")) ("GF" . ("Φ")) - ("Gc" . ("χ")) ("GC" . ("Χ")) - ("Gp" . ("ψ")) ("GP" . ("Ψ")) - ("Go" . ("ω")) ("GO" . ("Ω")) - ;; even shorter versions for central type constructors - ("S" . ("Σ")) ("P" . ("Π")) - - ;; Mathematical characters - - ("MiA" . ("𝐴")) - ("MiB" . ("𝐵")) - ("MiC" . ("𝐶")) - ("MiD" . ("𝐷")) - ("MiE" . ("𝐸")) - ("MiF" . ("𝐹")) - ("MiG" . ("𝐺")) - ("MiH" . ("𝐻")) - ("MiI" . ("𝐼")) - ("MiJ" . ("𝐽")) - ("MiK" . ("𝐾")) - ("MiL" . ("𝐿")) - ("MiM" . ("𝑀")) - ("MiN" . ("𝑁")) - ("MiO" . ("𝑂")) - ("MiP" . ("𝑃")) - ("MiQ" . ("𝑄")) - ("MiR" . ("𝑅")) - ("MiS" . ("𝑆")) - ("MiT" . ("𝑇")) - ("MiU" . ("𝑈")) - ("MiV" . ("𝑉")) - ("MiW" . ("𝑊")) - ("MiX" . ("𝑋")) - ("MiY" . ("𝑌")) - ("MiZ" . ("𝑍")) - ("Mia" . ("𝑎")) - ("Mib" . ("𝑏")) - ("Mic" . ("𝑐")) - ("Mid" . ("𝑑")) - ("Mie" . ("𝑒")) - ("Mif" . ("𝑓")) - ("Mig" . ("𝑔")) - ("Mii" . ("𝑖")) - ("Mij" . ("𝑗")) - ("Mik" . ("𝑘")) - ("Mil" . ("𝑙")) - ("Mim" . ("𝑚")) - ("Min" . ("𝑛")) - ("Mio" . ("𝑜")) - ("Mip" . ("𝑝")) - ("Miq" . ("𝑞")) - ("Mir" . ("𝑟")) - ("Mis" . ("𝑠")) - ("Mit" . ("𝑡")) - ("Miu" . ("𝑢")) - ("Miv" . ("𝑣")) - ("Miw" . ("𝑤")) - ("Mix" . ("𝑥")) - ("Miy" . ("𝑦")) - ("Miz" . ("𝑧")) - ("MIA" . ("𝑨")) - ("MIB" . ("𝑩")) - ("MIC" . ("𝑪")) - ("MID" . ("𝑫")) - ("MIE" . ("𝑬")) - ("MIF" . ("𝑭")) - ("MIG" . ("𝑮")) - ("MIH" . ("𝑯")) - ("MII" . ("𝑰")) - ("MIJ" . ("𝑱")) - ("MIK" . ("𝑲")) - ("MIL" . ("𝑳")) - ("MIM" . ("𝑴")) - ("MIN" . ("𝑵")) - ("MIO" . ("𝑶")) - ("MIP" . ("𝑷")) - ("MIQ" . ("𝑸")) - ("MIR" . ("𝑹")) - ("MIS" . ("𝑺")) - ("MIT" . ("𝑻")) - ("MIU" . ("𝑼")) - ("MIV" . ("𝑽")) - ("MIW" . ("𝑾")) - ("MIX" . ("𝑿")) - ("MIY" . ("𝒀")) - ("MIZ" . ("𝒁")) - ("MIa" . ("𝒂")) - ("MIb" . ("𝒃")) - ("MIc" . ("𝒄")) - ("MId" . ("𝒅")) - ("MIe" . ("𝒆")) - ("MIf" . ("𝒇")) - ("MIg" . ("𝒈")) - ("MIh" . ("𝒉")) - ("MIi" . ("𝒊")) - ("MIj" . ("𝒋")) - ("MIk" . ("𝒌")) - ("MIl" . ("𝒍")) - ("MIm" . ("𝒎")) - ("MIn" . ("𝒏")) - ("MIo" . ("𝒐")) - ("MIp" . ("𝒑")) - ("MIq" . ("𝒒")) - ("MIr" . ("𝒓")) - ("MIs" . ("𝒔")) - ("MIt" . ("𝒕")) - ("MIu" . ("𝒖")) - ("MIv" . ("𝒗")) - ("MIw" . ("𝒘")) - ("MIx" . ("𝒙")) - ("MIy" . ("𝒚")) - ("MIz" . ("𝒛")) - ("McA" . ("𝒜")) - ("McC" . ("𝒞")) - ("McD" . ("𝒟")) - ("McG" . ("𝒢")) - ("McJ" . ("𝒥")) - ("McK" . ("𝒦")) - ("McN" . ("𝒩")) - ("McO" . ("𝒪")) - ("McP" . ("𝒫")) - ("McQ" . ("𝒬")) - ("McS" . ("𝒮")) - ("McT" . ("𝒯")) - ("McU" . ("𝒰")) - ("McV" . ("𝒱")) - ("McW" . ("𝒲")) - ("McX" . ("𝒳")) - ("McY" . ("𝒴")) - ("McZ" . ("𝒵")) - ("Mca" . ("𝒶")) - ("Mcb" . ("𝒷")) - ("Mcc" . ("𝒸")) - ("Mcd" . ("𝒹")) - ("Mcf" . ("𝒻")) - ("Mch" . ("𝒽")) - ("Mci" . ("𝒾")) - ("Mcj" . ("𝒿")) - ("Mck" . ("𝓀")) - ("Mcl" . ("𝓁")) - ("Mcm" . ("𝓂")) - ("Mcn" . ("𝓃")) - ("Mcp" . ("𝓅")) - ("Mcq" . ("𝓆")) - ("Mcr" . ("𝓇")) - ("Mcs" . ("𝓈")) - ("Mct" . ("𝓉")) - ("Mcu" . ("𝓊")) - ("Mcv" . ("𝓋")) - ("Mcw" . ("𝓌")) - ("Mcx" . ("𝓍")) - ("Mcy" . ("𝓎")) - ("Mcz" . ("𝓏")) - ("MCA" . ("𝓐")) - ("MCB" . ("𝓑")) - ("MCC" . ("𝓒")) - ("MCD" . ("𝓓")) - ("MCE" . ("𝓔")) - ("MCF" . ("𝓕")) - ("MCG" . ("𝓖")) - ("MCH" . ("𝓗")) - ("MCI" . ("𝓘")) - ("MCJ" . ("𝓙")) - ("MCK" . ("𝓚")) - ("MCL" . ("𝓛")) - ("MCM" . ("𝓜")) - ("MCN" . ("𝓝")) - ("MCO" . ("𝓞")) - ("MCP" . ("𝓟")) - ("MCQ" . ("𝓠")) - ("MCR" . ("𝓡")) - ("MCS" . ("𝓢")) - ("MCT" . ("𝓣")) - ("MCU" . ("𝓤")) - ("MCV" . ("𝓥")) - ("MCW" . ("𝓦")) - ("MCX" . ("𝓧")) - ("MCY" . ("𝓨")) - ("MCZ" . ("𝓩")) - ("MCa" . ("𝓪")) - ("MCb" . ("𝓫")) - ("MCc" . ("𝓬")) - ("MCd" . ("𝓭")) - ("MCe" . ("𝓮")) - ("MCf" . ("𝓯")) - ("MCg" . ("𝓰")) - ("MCh" . ("𝓱")) - ("MCi" . ("𝓲")) - ("MCj" . ("𝓳")) - ("MCk" . ("𝓴")) - ("MCl" . ("𝓵")) - ("MCm" . ("𝓶")) - ("MCn" . ("𝓷")) - ("MCo" . ("𝓸")) - ("MCp" . ("𝓹")) - ("MCq" . ("𝓺")) - ("MCr" . ("𝓻")) - ("MCs" . ("𝓼")) - ("MCt" . ("𝓽")) - ("MCu" . ("𝓾")) - ("MCv" . ("𝓿")) - ("MCw" . ("𝔀")) - ("MCx" . ("𝔁")) - ("MCy" . ("𝔂")) - ("MCz" . ("𝔃")) - ("MfA" . ("𝔄")) - ("MfB" . ("𝔅")) - ("MfD" . ("𝔇")) - ("MfE" . ("𝔈")) - ("MfF" . ("𝔉")) - ("MfG" . ("𝔊")) - ("MfJ" . ("𝔍")) - ("MfK" . ("𝔎")) - ("MfL" . ("𝔏")) - ("MfM" . ("𝔐")) - ("MfN" . ("𝔑")) - ("MfO" . ("𝔒")) - ("MfP" . ("𝔓")) - ("MfQ" . ("𝔔")) - ("MfS" . ("𝔖")) - ("MfT" . ("𝔗")) - ("MfU" . ("𝔘")) - ("MfV" . ("𝔙")) - ("MfW" . ("𝔚")) - ("MfX" . ("𝔛")) - ("MfY" . ("𝔜")) - ("Mfa" . ("𝔞")) - ("Mfb" . ("𝔟")) - ("Mfc" . ("𝔠")) - ("Mfd" . ("𝔡")) - ("Mfe" . ("𝔢")) - ("Mff" . ("𝔣")) - ("Mfg" . ("𝔤")) - ("Mfh" . ("𝔥")) - ("Mfi" . ("𝔦")) - ("Mfj" . ("𝔧")) - ("Mfk" . ("𝔨")) - ("Mfl" . ("𝔩")) - ("Mfm" . ("𝔪")) - ("Mfn" . ("𝔫")) - ("Mfo" . ("𝔬")) - ("Mfp" . ("𝔭")) - ("Mfq" . ("𝔮")) - ("Mfr" . ("𝔯")) - ("Mfs" . ("𝔰")) - ("Mft" . ("𝔱")) - ("Mfu" . ("𝔲")) - ("Mfv" . ("𝔳")) - ("Mfw" . ("𝔴")) - ("Mfx" . ("𝔵")) - ("Mfy" . ("𝔶")) - ("Mfz" . ("𝔷")) - - ;; Some ISO8859-1 characters. - - (" " . (" ")) - ("!" . ("¡")) - ("cent" . ("¢")) - ("brokenbar" . ("¦")) - ("degree" . ("°")) - ("?" . ("¿")) - ("^a_" . ("ª")) - ("^o_" . ("º")) - - ;; Circled, parenthesised etc. numbers and letters. - - ( "(0)" . ,(lean-input-to-string-list " ⓪")) - ( "(1)" . ,(lean-input-to-string-list "⑴①⒈❶➀➊")) - ( "(2)" . ,(lean-input-to-string-list "⑵②⒉❷➁➋")) - ( "(3)" . ,(lean-input-to-string-list "⑶③⒊❸➂➌")) - ( "(4)" . ,(lean-input-to-string-list "⑷④⒋❹➃➍")) - ( "(5)" . ,(lean-input-to-string-list "⑸⑤⒌❺➄➎")) - ( "(6)" . ,(lean-input-to-string-list "⑹⑥⒍❻➅➏")) - ( "(7)" . ,(lean-input-to-string-list "⑺⑦⒎❼➆➐")) - ( "(8)" . ,(lean-input-to-string-list "⑻⑧⒏❽➇➑")) - ( "(9)" . ,(lean-input-to-string-list "⑼⑨⒐❾➈➒")) - ("(10)" . ,(lean-input-to-string-list "⑽⑩⒑❿➉➓")) - ("(11)" . ,(lean-input-to-string-list "⑾⑪⒒")) - ("(12)" . ,(lean-input-to-string-list "⑿⑫⒓")) - ("(13)" . ,(lean-input-to-string-list "⒀⑬⒔")) - ("(14)" . ,(lean-input-to-string-list "⒁⑭⒕")) - ("(15)" . ,(lean-input-to-string-list "⒂⑮⒖")) - ("(16)" . ,(lean-input-to-string-list "⒃⑯⒗")) - ("(17)" . ,(lean-input-to-string-list "⒄⑰⒘")) - ("(18)" . ,(lean-input-to-string-list "⒅⑱⒙")) - ("(19)" . ,(lean-input-to-string-list "⒆⑲⒚")) - ("(20)" . ,(lean-input-to-string-list "⒇⑳⒛")) - - ("(a)" . ,(lean-input-to-string-list "⒜Ⓐⓐ")) - ("(b)" . ,(lean-input-to-string-list "⒝Ⓑⓑ")) - ("(c)" . ,(lean-input-to-string-list "⒞Ⓒⓒ")) - ("(d)" . ,(lean-input-to-string-list "⒟Ⓓⓓ")) - ("(e)" . ,(lean-input-to-string-list "⒠Ⓔⓔ")) - ("(f)" . ,(lean-input-to-string-list "⒡Ⓕⓕ")) - ("(g)" . ,(lean-input-to-string-list "⒢Ⓖⓖ")) - ("(h)" . ,(lean-input-to-string-list "⒣Ⓗⓗ")) - ("(i)" . ,(lean-input-to-string-list "⒤Ⓘⓘ")) - ("(j)" . ,(lean-input-to-string-list "⒥Ⓙⓙ")) - ("(k)" . ,(lean-input-to-string-list "⒦Ⓚⓚ")) - ("(l)" . ,(lean-input-to-string-list "⒧Ⓛⓛ")) - ("(m)" . ,(lean-input-to-string-list "⒨Ⓜⓜ")) - ("(n)" . ,(lean-input-to-string-list "⒩Ⓝⓝ")) - ("(o)" . ,(lean-input-to-string-list "⒪Ⓞⓞ")) - ("(p)" . ,(lean-input-to-string-list "⒫Ⓟⓟ")) - ("(q)" . ,(lean-input-to-string-list "⒬Ⓠⓠ")) - ("(r)" . ,(lean-input-to-string-list "⒭Ⓡⓡ")) - ("(s)" . ,(lean-input-to-string-list "⒮Ⓢⓢ")) - ("(t)" . ,(lean-input-to-string-list "⒯Ⓣⓣ")) - ("(u)" . ,(lean-input-to-string-list "⒰Ⓤⓤ")) - ("(v)" . ,(lean-input-to-string-list "⒱Ⓥⓥ")) - ("(w)" . ,(lean-input-to-string-list "⒲Ⓦⓦ")) - ("(x)" . ,(lean-input-to-string-list "⒳Ⓧⓧ")) - ("(y)" . ,(lean-input-to-string-list "⒴Ⓨⓨ")) - ("(z)" . ,(lean-input-to-string-list "⒵Ⓩⓩ")) - ("y" . ("ɏ")) - - - )) - "A list of translations specific to the Lean input method. -Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS). -All the translation strings are possible translations -of the given key sequence; if there is more than one you can choose -between them using the arrow keys. - -Note that if you customize this setting you will not -automatically benefit (or suffer) from modifications to its -default value when the library is updated. If you just want to -add some bindings it is probably a better idea to customize -`lean-input-user-translations'. - -These translation pairs are included after those in -`lean-input-user-translations', but before the ones inherited -from other input methods (see `lean-input-inherit'). - -If you change this setting manually (without using the -customization buffer) you need to call `lean-input-setup' in -order for the change to take effect." - :group 'lean-input - :set 'lean-input-incorporate-changed-setting - :initialize 'custom-initialize-default - :type '(repeat (cons (string :tag "Key sequence") - (repeat :tag "Translations" string)))) - -(defcustom lean-input-user-translations nil - "Like `lean-input-translations', but more suitable for user -customizations since by default it is empty. - -These translation pairs are included first, before those in -`lean-input-translations' and the ones inherited from other input -methods." - :group 'lean-input - :set 'lean-input-incorporate-changed-setting - :initialize 'custom-initialize-default - :type '(repeat (cons (string :tag "Key sequence") - (repeat :tag "Translations" string)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Inspecting and modifying translation maps - -(defun lean-input-get-translations (qp) - "Return a list containing all translations from the Quail -package QP (except for those corresponding to ASCII). -Each pair in the list has the form (KEY-SEQUENCE . TRANSLATION)." - (with-temp-buffer - (activate-input-method qp) ; To make sure that the package is loaded. - (unless (quail-package qp) - (error "%s is not a Quail package." qp)) - (let ((decode-map (list 'decode-map))) - (quail-build-decode-map (list (quail-map)) "" decode-map 0) - (cdr decode-map)))) - -(defun lean-input-show-translations (qp) - "Display all translations used by the Quail package QP (a string). -\(Except for those corresponding to ASCII)." - (interactive (list (read-input-method-name - "Quail input method (default %s): " "Lean"))) - (let ((buf (concat "*" qp " input method translations*"))) - (with-output-to-temp-buffer buf - (with-current-buffer buf - (quail-insert-decode-map - (cons 'decode-map (lean-input-get-translations qp))))))) - -(defun lean-input-add-translations (trans) - "Add the given translations TRANS to the Lean input method. -TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION). The -translations are appended to the current translations." - (with-temp-buffer - (dolist (tr (lean-input-concat-map (eval lean-input-tweak-all) trans)) - (quail-defrule (car tr) (cdr tr) "Lean" t)))) - -(defun lean-input-inherit-package (qp &optional fun) - "Let the Lean input method inherit the translations from the -Quail package QP (except for those corresponding to ASCII). - -The optional function FUN can be used to modify the translations. -It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return -a list of such pairs." - (let ((trans (lean-input-get-translations qp))) - (lean-input-add-translations - (if fun (lean-input-concat-map fun trans) - trans)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Setting up the input method - -(defun lean-input-setup () - "Set up the Lean input method based on the customisable -variables and underlying input methods." - - ;; Create (or reset) the input method. - (with-temp-buffer - (quail-define-package "Lean" "UTF-8" "∏" t ; guidance - "Lean input method. -The purpose of this input method is to edit Lean programs, but -since it is highly customisable it can be made useful for other -tasks as well." - nil nil nil nil nil nil t ; maximum-shortest - )) - - (lean-input-add-translations - (mapcar (lambda (tr) (cons (car tr) (vconcat (cdr tr)))) - (append lean-input-user-translations - lean-input-translations))) - (dolist (def lean-input-inherit) - (lean-input-inherit-package (car def) - (eval (cdr def))))) - -(defun lean-input-incorporate-changed-setting (sym val) - "Update the Lean input method based on the customisable -variables and underlying input methods. -Suitable for use in the :set field of `defcustom'." - (set-default sym val) - (lean-input-setup)) - -;; Set up the input method. - -(lean-input-setup) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Administrative details - -(provide 'lean-input) -;;; lean-input.el ends here - -(defun lean-input-export-translations () - "Export the current translation, (input, output) pairs for -input-method, in a javascript format. It can be copy-pasted to -leanprover.github.io/tutorial/js/input-method.js" - (interactive) - (with-current-buffer - (get-buffer-create "*lean-translations*") - (let ((exclude-list '("\\newline"))) - (insert "var corrections = {") - (--each - (--filter (not (member (car it) exclude-list)) - (lean-input-get-translations "Lean")) - (let* ((input (substring (car it) 1)) - (outputs (cdr it))) - (insert (format "%s:\"" (prin1-to-string input))) - (cond ((vectorp outputs) - (insert (elt outputs 0))) - (t (insert-char outputs))) - (insert (format "\",\n" input)))) - (insert "};")))) - -(defun lean-input-export-translations-to-stdout () - (lean-input-export-translations) - (with-current-buffer "*lean-translations*" - (princ (buffer-string)))) diff --git a/src/emacs/lean-message-boxes.el b/src/emacs/lean-message-boxes.el deleted file mode 100644 index 35d97c701f..0000000000 --- a/src/emacs/lean-message-boxes.el +++ /dev/null @@ -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) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el deleted file mode 100644 index b009c8cffc..0000000000 --- a/src/emacs/lean-mode.el +++ /dev/null @@ -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 -;; Soonho Kong -;; Maintainer: Soonho Kong -;; 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 "") '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 diff --git a/src/emacs/lean-pkg.el b/src/emacs/lean-pkg.el deleted file mode 100644 index f3705b565d..0000000000 --- a/src/emacs/lean-pkg.el +++ /dev/null @@ -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) diff --git a/src/emacs/lean-require.el b/src/emacs/lean-require.el deleted file mode 100644 index f6929b5f8f..0000000000 --- a/src/emacs/lean-require.el +++ /dev/null @@ -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) diff --git a/src/emacs/lean-right-click.el b/src/emacs/lean-right-click.el deleted file mode 100644 index 7ef76192e3..0000000000 --- a/src/emacs/lean-right-click.el +++ /dev/null @@ -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 diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el deleted file mode 100644 index 25a3a9b2a7..0000000000 --- a/src/emacs/lean-server.el +++ /dev/null @@ -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) diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el deleted file mode 100644 index 1ef8b285db..0000000000 --- a/src/emacs/lean-settings.el +++ /dev/null @@ -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) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el deleted file mode 100644 index 61603004b8..0000000000 --- a/src/emacs/lean-syntax.el +++ /dev/null @@ -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) diff --git a/src/emacs/lean-util.el b/src/emacs/lean-util.el deleted file mode 100644 index 98c4d380b5..0000000000 --- a/src/emacs/lean-util.el +++ /dev/null @@ -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) diff --git a/src/emacs/lean.pgm b/src/emacs/lean.pgm deleted file mode 100644 index ac016135e80c3120e45da26839f23b8e6bc9fa55..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 40219 zcmeI5d3+An`oN#i+TGi#y0ukYZ7-^NT|r4hG^+OfqAI2KSVGVi?N2PFMeMg5s)Slf zTT3X_NQ*=)5g|lT!mW!mwk$%n=bqWmnK|>mGjHXTI;5GiTE5fA?`s{q_VDe|t*dYQkg=18PxS3OeBz{#@u9v=8aJu%j}|R_ zoA@=W@Q-HADqu+}Ay7h~gh25U$j;35EMR7~XDPGLv;Da!m3`x`i(JcDSxT7fo=qbx zmtq|K0$=ecy|k7IQw&O0&+-8t{<6&8XFzvJzgHCoF*%kM@HF`sSl)*<$4F9>dDdKA zdQFA^DL<<&jB)8{ni=`^7W--YhMG`mpJ`0bGDZ?8WlnommM%3Ff+RJ|7e><=|L<~R zfbqq0mn#iulc(l(FeDc))+nFIFC*ermX zG87yOutuM6NB1t2GXNjjsja#1&HB&@6)3k}fO1LZzHW283k7}Q)eN_FwBqnJz+n{% z?gZ$1-%2sQkC&kw0Ep&S%%(LEo+D2pq&|fdoec1q%?Omcm!aSj(3h%>$Kn-$Riv;A z1*-rgdmPQ%P$B?|;|WM#ccy|F|p3 z&-XeMd>LNmSIxThyHc=I^roTUHh|&QW6+-7hq4sPMbR~~FBb$uC8-nx1v>(KV?P=x z;e99wFwUc@tA$d_!uyiKLb+T8d{iepf&-w0LY1ODmK?8M)>$aH1)zf+7>ch0pxg#n zq*TYFZDklKm(xMP;Q-4$2uR&wgR-swi(nBP_Pd?_q)xCEAF2G{G!Or zy^msi2VjOGTiiMW$}a$OEmm0PcD(_-sF^q|1<9QuC|4)V)1~ALC|D0#dp0Yv8{mX? zfLti|9)4OoJFRoB{>k^yESFQYf>7J|;6LWRe+dEIV`zlx^i;HGO=R*4|mo(5=ri*+~C z90Y~j0NGoX1<+e}SgxQ5L!pm!{wAt}pkOy;royDII`dBeKj};^pLe&+ zRf+y6`IVNeO(0PJ&W39!7axP_t^%rgPJ)uwTv^nsR?mfyR0`(nvt2_$(h0q;FT&HE z1O-0;us-`ckkc=_fkNgDd^Yna=xkntl2PCIL!Yl@{TAhduR7bK9g;gJcWS_s78a>` z4N74nBNXfo^{y4>Jg|_2^(R*~8nWaL3X(_v|1^{`7>WbRsp!~4cGKYlbvaNH0iJHu zz)EWL7}PWzjH|($>`dkiHyO+6EX4pNw+(rF!joj^ClMRkh!dkb6r#FqDR}Ey0Jkrs z6$g}Vr7BmloBs4C;ItHBP08EK7r0IHS3e2$ILGE53PzW8e`i<>PzsOj*t^GW+P9Z? z`ryMqLzuAv7%jQ{(WwO}ILZCYK`}rvR@sV$+tDH}1kjJjc+tY4Vj{iku*zC zkgVNxy>`lJP;hG*_=0!5jI9~?ai9HLgOcA4z~!SA$3ely^72oH0;@z<=AL?1F3Dn` zqgCN~S96BWgEAK?a!(D7OWr{JV@M^>T1yeT^8rd3&enNQu#&sSlD|F$lQ@S$OjeS&O--sx%&uO>v;hTo0knI_-;EQY2oI3d1&@Ym4~A-{tJdv65$+64<_sMPfRu^%(>GhZtu+>s9@ez~dAI^jlYx)N5 z?Lc_e1ea|nNZxw?KVC3rLLoOm9kY1V#j^k#xEZ3+UQ59|e<;0;6V0Je$k^&1J;3#Fh5w9_B;zCXhUdK;sA0_Dz= zP+NCr=vXM^MYqcO1@-ShseA^4UhxD9k_qgfLMD=Pq1^I;X-rk|;uG)|Ytd^SK_Op; z5PG@))QJ{W1dLI)Lk1&3Te%PzqZCFt=I`hC*iYK4y-*F1*Ud z=TOlc32C$3PIkJaP@I8PjR5&L?A)hLsFAL4V&&}E6!Qf3s@f4J$-b`~c zl=NoMK>PjDEPPMM)0TpT0KVEwj82Av)9FWJBcO)%uC2z3kvxWii{!65iQya#CFw8P z8wocWT3BT3ITY+deR0mwP)Hx4zQj#l%1&Tf1y3mgluOS-P35_kv!TSPFOz0>g6DY{ zSX&XG2w$L4o`^de3f6_r(xRjN09#oAJgq2DaIiYCbvTr7!AH7OlJ&3b{RxkW=a*zL z8bC#9y`96MU|AR{RQMi$HKd+Qky;9#1ZXHmbUG9=Stty^=fPvV)sV#t1<8l^#W_Q# zLrJVCen-a#`ni5+AmJ%mOTp~s@W^Qr$>~sV2vkP=1}v-&Bu7(3D0md$mCXMEC}a|1 zE4G8i`ZI;A7Zr-|o*`M?>-d(E>kpmJR5e>4phHt+C`jICh;u#^(#O^afKv414jl8KloqSm@Gr5j!+i!g|}U}(}hOgqC*i@HH1bw9*VHM6G-o8CB5$c zwH3EvI)aaS?@3z91h)l>(V_5plU37(ePjRx8jO5HF|-s+uT6dgd3J^Td#tuAKbq%3 znzMGxX4`4&`dU_@V1Sj|9+6UUK*4<)lnepTADDcouN(4zcGVhL?TRY97W&fPH*@Xk zB6k2lTPgc))jyDkw5!=JDn@6etfVzpa+jifgi;NhUK3iVN{LWHpoBmPff52G1WE`v zfk4d3L?I=lO54O^H&Flfp`hQpbXiRoZcr6p-Jy1kHY@0LdRIGrEs&uq>UyS#j)>+vg@FgPs*Jg)zc zNT&(ogftVv#*4zJpRkqgb62Galk)G33QZ@ zeW7PahPFdNs*iZ9KWh@T_}9l@P|Rs>585lqu^%fo#7h%~3(BNq%_K+(uYH`$S`b5) zY-3G3$-^)u?d*Gyi1D8)I%3L@naboxbZ{6UBBe`{`W+Iaf)T1o&cQ9Saph)3k+uhy zYWk^u5p;8xGCFIfK{_aZL%iKZE3Qb}Uy4&iVVlxJs&njIEfV6A5Rx?^nsy{dH$P$* zYr%P|PpoB4JEv3n@10T+k1%U&$1Riczv#jsk8de18=mzwRaz7S?%;~$tnm=N3+yWv zWISv`iRnt}$)wKWY#s{*-#kj7#4vssHz&I%YdJCu_voNRy+^ww{*ypqZkrxVh!-59 zUZLHH{GZ-G3YI#;A1a+9KkJHrQ3fI&3a9n#e!tPGAlrpSIOV0Ti6W$Y2l8iCG!m~6r4s^detKGlk1@DWM9gOnv2I~(mTVX1rIT+E7_wy{oIRK z?g)Rhbh8JMUAGiGu3MLB8_K~B+72}-;xhx3oUl}0OTqm9T1!jqO8Q+rlqeR;gV*pF z+fpvQcON6gxjn4{lGI)3!}>DcNt+>D+uT4oJ4PSK=IIl_83-UA9e+=M`rIFLoeKqb zy{lHCt#C5yp)egS$#0FvW~n6v;o|h%oOcg1CRr(LPJ|s=e4=$0PANA~l0)V4>c$?F zf(jW$Lig?-5Ly2N84Vc~wkFrpXF2sb<%-&UH%qhgwP-(~_ z8drWHY}`OOG(!y_3p5nndCIvYf4fj$Uec%Tz&PfTj0xjNpR%9zjuZEOyPGtG`)QPz ztB0a%DN8o%u0HtXm$=u^3rIVP5Kfk*3Uo3$o*|r2?x0NBA(httQc#9!R#760iEimG zp&uHC0aBT7rt6^uoI?zYXCq2bFhLA@X9W3KNzy~nU4357(?Lleb{Xeu$Ia|vlh7ai zu&6*WrjAY*#LrhN25HM)lFz-RYYa?B8$9EKSz4OCtQz8d{~eL*l=R6>oTU5hm7OIF z*FhP$l4MPru~{v>=9?^(pC22lhk z@nbeDh=^GBemC(jBQ_{L>~^CB^cmTDwyPxYPM@F0MMgv{Tso~28$r@2D1&t8mW_^f z%1#l=t+rE>4;_k=Ityb*dr%#Peg4;-N@es=b~l|cOh`jVO~_IdqCPBMGLJkiZFyIp%Qe>|9Xu49$_9`%8cGK1!GUsiIP0QlBag_J z9_Pksrd15vd#97k~HD(@eoa>rI0hC zmMquOPtM~(!Sew!GCF`P+k=9E_c<{zE-XVCrvy`j3Oy91qh&(qq3oK@WD`Y%g1Nm{ zs~PvF#;P(UJZvs2-NahX6~{ru#D#*t2kxQDGNMf=@j*;!S&3Mo4fAKetqyuUgF<(- zVtfe-J`A0s?t7iu@u(&ubUY|)n}jBr*Zr2P@}Xe2^bGjIx;o*-1lRoR!ieMUHy zRVcWVjQYe>%uvW$(!p|MyzHw;>h_BNbyZ#*gSbdNJ4~VA#0hEn+ zeJ>a^D0sM~RJ~${f|2Se5%cmxwi*|@AJPoF7UQ*1>g}>Q6r9;hE2K%bq2QjE_G!ft z6T3)fCItl(dY=$n^p7L0b+m>iE%zznPB-@bx4iSnj>lw4+(frf8wSzu4!*xPRLwR# zjtp0`a9Qy0nxaTu@)QZJKDbUA5`0!EbYtj1`9cu)kroNh^@$-K`UlsC)p3eaoNRXs zLsTm5He7uY=wi|Rl4R$@Z@hU;Dfi2u!Q#)L==e_J0PSR2u}QUy0&`ouaqty3muSt% za~?Sbq$`rNeN;EaF(^XLf3U4XN}J*c z8FB!>A4xf4ym7!nErKVP5GDy7{Ebtmm6Uu^9#4u+Uw5rjvmHI!&Zn6Wm-C2)XOyz1 zPoFxS$)60%(|#2(uyMw$Ko|L1f#@jy+0edbozA>l_ldt~PIykM$LXZoSilm@H#QZj OY>8MxpoD;10{;bu@qmZ` diff --git a/src/emacs/load-lean.el b/src/emacs/load-lean.el deleted file mode 100644 index 15284eab1c..0000000000 --- a/src/emacs/load-lean.el +++ /dev/null @@ -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) diff --git a/src/emacs/test/test-helper.el b/src/emacs/test/test-helper.el deleted file mode 100644 index 9e93b343f5..0000000000 --- a/src/emacs/test/test-helper.el +++ /dev/null @@ -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))