feat(emacs/lean-input): add lean-input-export-translations

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 "};")))