From cb83eca2f32597cd086839e89615495d7af6d7d1 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Mon, 27 Oct 2014 15:17:42 -0700 Subject: [PATCH] feat(emacs/lean-input): add lean-input-export-translations --- src/emacs/lean-input.el | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el index fbb043b32..ca4b5eddb 100644 --- a/src/emacs/lean-input.el +++ b/src/emacs/lean-input.el @@ -1091,3 +1091,25 @@ Suitable for use in the :set field of `defcustom'." (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/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 "};")))