feat(emacs): use s-join instead of string-join

Because string-join was introduced at Emacs 24.4 and subr-x.el must be
loaded for using it.

src/emacs/lean-info.el

@@ -7,6 +7,7 @@
 (require 'cl-lib)
 (require 'dash)
 (require 'dash-functional)
+(require 's)
 (require 'lean-util)
 (require 'lean-debug)
 
@@ -33,7 +34,7 @@
 (defun lean-info-type-body (typeinfo)
   (cl-third typeinfo))
 (defun lean-info-type-body-str (typeinfo)
-  (string-join (lean-info-type-body typeinfo) "\n"))
+  (s-join "\n" (lean-info-type-body typeinfo)))
 
 ;; Overload Information
 ;; --------------------
@@ -48,7 +49,7 @@
   (cl-second overload))
 (defun lean-info-overload-names (overload)
   (cl-loop for seq in (cl-third overload)
-           collect (string-join seq "\n")))
+           collect (s-join "\n" seq)))
 (defun lean-info-overload-parse-header (str)
   (let ((items (split-string str "|")))
     (list (string-to-number (cl-second items))
@@ -82,7 +83,7 @@
 (defun lean-info-synth-body (synth)
   (cl-third synth))
 (defun lean-info-synth-body-str (synth)
-  (string-join (lean-info-synth-body synth) "\n"))
+  (s-join "\n" (lean-info-synth-body synth)))
 
 ;; Coercion Information
 ;; ----------------
@@ -109,11 +110,11 @@
 (defun lean-info-coercion-expr (coercion)
   (cl-third coercion))
 (defun lean-info-coercion-expr-str (coercion)
-  (string-join (lean-info-coercion-expr coercion) "\n"))
+  (s-join "\n" (lean-info-coercion-expr coercion)))
 (defun lean-info-coercion-type (coercion)
   (cl-fourth coercion))
 (defun lean-info-coercion-type-str (coercion)
-  (string-join (lean-info-coercion-type coercion) "\n"))
+  (s-join "\n" (lean-info-coercion-type coercion)))
 
 ;; Extra Information
 ;; ----------------
@@ -140,11 +141,11 @@
 (defun lean-info-extra-expr (extra)
   (cl-third extra))
 (defun lean-info-extra-expr-str (extra)
-  (string-join (lean-info-extra-expr extra) "\n"))
+  (s-join "\n" (lean-info-extra-expr extra)))
 (defun lean-info-extra-type (extra)
   (cl-fourth extra))
 (defun lean-info-extra-type-str (extra)
-  (string-join (lean-info-extra-type extra) "\n"))
+  (s-join "\n" (lean-info-extra-type extra)))
 
 ;; Identifier Information
 ;; ----------------------
@@ -169,7 +170,7 @@
 (defun lean-info-identifier-body (identifier)
   (cl-third identifier))
 (defun lean-info-identifier-body-str (identifier)
-  (string-join (lean-info-identifier-body identifier) "\n"))
+  (s-join "\n" (lean-info-identifier-body identifier)))
 
 
 ;; Symbol Information
@@ -195,12 +196,12 @@
 (defun lean-info-symbol-body (symbol)
   (cl-third symbol))
 (defun lean-info-symbol-body-str (symbol)
-  (string-join (lean-info-symbol-body symbol) "\n"))
+  (s-join "\n" (lean-info-symbol-body symbol)))
 
 (defun lean-info-id-symbol-body-str (info)
   (cl-case (lean-info-kind info)
-    ('IDENTIFIER (string-join (lean-info-symbol-body info) "\n"))
+    ('IDENTIFIER (s-join "\n" (lean-info-symbol-body info)))
-    ('SYMBOL     (string-join (lean-info-identifier-body info) "\n"))))
+    ('SYMBOL     (s-join "\n" (lean-info-identifier-body info)))))
 
 
 ;; Proofstate Information
@@ -227,7 +228,7 @@
 (defun lean-info-proofstate-states (proofstate)
   (cl-third proofstate))
 (defun lean-info-proofstate-state-str (string-seq)
-  (string-join string-seq "\n"))
+  (s-join "\n" string-seq))
 (defun lean-info-proofstate-extract-conclusion (string-seq)
   (--drop-while (not (s-starts-with? "⊢" it)) string-seq))
 (defun lean-info-proofstate-extract-premises (string-seq)
@@ -241,18 +242,18 @@
      (first-state
       (pcase display-style
         (`show-all
-         (string-join
+         (s-join
-          (-map 'lean-info-proofstate-state-str states)
+          "\n\n"
-          "\n\n"))
+          (-map 'lean-info-proofstate-state-str states)))
         (`show-first
          (lean-info-proofstate-state-str first-state))
         (`show-first-and-other-conclusions
-         (string-join
+         (s-join
+          "\n\n"
           (-map 'lean-info-proofstate-state-str
                 (cons first-state (-map
                                    'lean-info-proofstate-extract-conclusion
-                                   rest-states)))
+                                   rest-states)))))))
-          "\n\n"))))
      (t "No Goal"))))
 
 ;; Basic
@@ -470,13 +471,13 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
       (setq type-str (lean-info-type-body-str type)))
     (when (and name-str overload)
       (setq overload-str
-            (string-join
+            (s-join
-             (--remove
+	     ", "
-              (or
+	     (--remove
-               (and id  (string-prefix-p (lean-info-id-symbol-body-str id) it))
+	      (or
-               (and sym (string-prefix-p (lean-info-id-symbol-body-str sym) it)))
+	       (and id	(string-prefix-p (lean-info-id-symbol-body-str id) it))
-              (lean-info-overload-names overload))
+	       (and sym (string-prefix-p (lean-info-id-symbol-body-str sym) it)))
-             ", ")))
+	      (lean-info-overload-names overload)))))
     (when extra
       (setq str
             (cond (lean-show-only-type-in-parens (format ": %s" (lean-info-extra-type-str extra)))

src/emacs/lean-option.el

@@ -7,6 +7,7 @@
 
 (require 'dash)
 (require 'dash-functional)
+(require 's)
 
 (cl-defstruct lean-option-record name type value desc)
 
@@ -24,7 +25,7 @@
     (setq str-list
           (-take (- (length str-list) 2)
                  (-drop 1 str-list)))
-    (string-join str-list "\n")))
+    (s-join "\n" str-list)))
 
 (defun lean-option-string (&optional use-flycheck)
   "Return string of Lean options set by lean-set-option command"

src/emacs/lean-project.el

@@ -4,6 +4,7 @@
 ;; Author: Soonho Kong
 ;;
 
+(require 's)
 (require 'lean-util)
 
 (defconst lean-project-file-name ".project"
@@ -23,17 +24,17 @@
     (if (file-exists-p project-file)
         (user-error "project-file %s already exists" project-file))
     (find-file project-file)
-    (insert (string-join '("# Lean project file"
+    (insert (s-join "\n"
-                           ""
+                    '("# Lean project file"
-                           "# Include all .lean files under this directory"
+                      ""
-                           "+ *.lean"
+                      "# Include all .lean files under this directory"
-                           ""
+                      "+ *.lean"
-                           "# Exclude flycheck generated temp files"
+                      ""
-                           "- flycheck*.lean"
+                      "# Exclude flycheck generated temp files"
-                           ""
+                      "- flycheck*.lean"
-                           "# Exclude emacs temp files"
+                      ""
-                           "- .#*.lean")
+                      "# Exclude emacs temp files"
-                         "\n"))
+                      "- .#*.lean")))
     (save-buffer)))
 
 (provide 'lean-project)

src/emacs/lean-server.el

@@ -492,7 +492,7 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
     (setq str-list
           (-take (- (length str-list) 2)
                  (-drop 1 str-list)))
-    (string-join str-list "\n")))
+    (s-join "\n" str-list)))
 
 (defun lean-findp-parse-string (str)
   "Parse the output of findp command."

src/emacs/lean-type.el

@@ -8,6 +8,7 @@
 (require 'cl-lib)
 (require 'dash)
 (require 'dash-functional)
+(require 's)
 (require 'lean-variable)
 (require 'lean-util)
 (require 'lean-cmd)
@@ -65,7 +66,7 @@ buffer. It's used to avoid outputting the same message")
 (defun lean-eldoc-documentation-function-cont (info-record &optional add-to-kill-ring)
   "Continuation for lean-eldoc-documentation-function"
   (let* ((info-strings (lean-info-record-to-strings info-record))
-         (info-string-mini-buffer (and info-strings (string-join info-strings " ")))
+         (info-string-mini-buffer (and info-strings (s-join " " info-strings)))
          (info-string-info-buffer (and info-strings (-last-item info-strings)))
          (proofstate (lean-info-record-proofstate info-record)))
     (when info-strings
@@ -112,7 +113,7 @@ buffer. It's used to avoid outputting the same message")
     (setq str-list
           (-take (- (length str-list) 2)
                  (-drop 1 str-list)))
-    (string-join str-list "\n")))
+    (s-join "\n" str-list)))
 
 (defun lean-eval-cmd (lean-cmd)
   "Evaluate lean command."

src/emacs/test/lean-info-test.el

@@ -5,6 +5,7 @@
 ;;
 
 (require 'ert)
+(require 's)
 (require 'lean-info)
 
 (ert-deftest lean-test-info-type ()
@@ -291,7 +292,7 @@
                      "H_3 : c"
                      "⊢ and b c"))
                   'show-all)
-                 (string-join '("a : Prop,"
+                 (s-join "\n" '("a : Prop,"
                                 "b : Prop,"
                                 "c : Prop,"
                                 "H_1 : a,"
@@ -305,7 +306,7 @@
                                 "H_1 : a,"
                                 "H_2 : b,"
                                 "H_3 : c"
-                                "⊢ and b c") "\n")))
+                                "⊢ and b c"))))
   (should (equal (lean-info-proofstate-states-str
                   (lean-info-proofstate-parse
                    '("-- PROOF_STATE|6|17"
@@ -325,13 +326,13 @@
                      "H_3 : c"
                      "⊢ and b c"))
                   'show-first)
-                 (string-join '("a : Prop,"
+                 (s-join "\n" '("a : Prop,"
                                 "b : Prop,"
                                 "c : Prop,"
                                 "H_1 : a,"
                                 "H_2 : b,"
                                 "H_3 : c"
-                                "⊢ a") "\n")))
+                                "⊢ a"))))
   (should (equal (lean-info-proofstate-states-str
                   (lean-info-proofstate-parse
                    '("-- PROOF_STATE|6|17"
@@ -351,7 +352,7 @@
                      "H_3 : c"
                      "⊢ and b c"))
                   'show-first-and-other-conclusions)
-                 (string-join '("a : Prop,"
+                 (s-join "\n" '("a : Prop,"
                                 "b : Prop,"
                                 "c : Prop,"
                                 "H_1 : a,"
@@ -359,7 +360,7 @@
                                 "H_3 : c"
                                 "⊢ a"
                                 ""
-                                "⊢ and b c") "\n"))))
+                                "⊢ and b c")))))
 
 (ert-deftest lean-test-info-pos ()
   "Test lean-info-pos"