michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(emacs/lean-input.el): add exclude-list to lean-input-export-translations

Browse source
This commit is contained in:
Soonho Kong 2016-06-04 05:43:38 -04:00
parent d2b9fd073f
commit 3941cc1839
1 changed files with 14 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/emacs/lean-input.el
View file

@ -1139,24 +1139,23 @@ Suitable for use in the :set field of `defcustom'."
(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/js/input-method.js"
leanprover.github.io/tutorial/js/input-method.js"
(interactive)
(with-current-buffer
(get-buffer-create "*lean-translations*")
(insert "var corrections = {")
(--each
(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 "};")))
(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)