Remove old, personal, unused developer code

lean4-input.el

@@ -308,37 +308,6 @@ Suitable for use in the :set field of `defcustom'."
 (cl-eval-when (load eval)
   (lean4-input-setup))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Export Translations
-
-(defun lean4-input-export-translations ()
-  "Export the current translations in a javascript format.
-Print (input, output) pairs in Javascript format to the buffer
-*lean4-translations*.  The output can be copy-pasted to
-leanprover.github.io/tutorial/js/input-method.js"
-  (interactive)
-  (with-current-buffer
-      (get-buffer-create "*lean4-translations*")
-    (let ((exclude-list '("\\newline")))
-      (insert "var corrections = {")
-      (--each
-          (--filter (not (member (car it) exclude-list))
-                    (lean4-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"))))
-      (insert "};"))))
-
-(defun lean4-input-export-translations-to-stdout ()
-  "Print current translations to stdout."
-  (lean4-input-export-translations)
-  (with-current-buffer "*lean4-translations*"
-    (princ (buffer-string))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Administrative details