feat(emacs/lean-company): add lean-company

src/emacs/lean-company.el

@@ -1,81 +1,61 @@
+;; -*- lexical-binding: t; -*-
+;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+;; Released under Apache 2.0 license as described in the file LICENSE.
+;;
+;; Author: Soonho Kong
+;;
 (require 'company)
-(defun company-lean ()
-  (set (make-local-variable 'company-backends) '(company-lean))
-  (company-mode))
-(add-hook 'lean-mode-hook 'company-lean)
+(require 'company-etags)
+(require 'dash)
+(require 'dash-functional)
+(require 'lean-tags)
+(require 'lean-server)
 
-(setq company-tooltip-limit 20)                      ; bigger popup window
-(setq company-idle-delay .3)                         ; decrease delay before autocompletion popup shows
-(setq company-echo-delay 0)                          ; remove annoying blinking
-(setq company-begin-commands '(self-insert-command)) ; start autocompletion only after typing
+(defun company-lean-hook ()
+  (set (make-local-variable 'company-backends) '(company-lean))
+  (setq-local company-tooltip-limit 20)                      ; bigger popup window
+  (setq-local company-idle-delay .3)                         ; decrease delay before autocompletion popup shows
+  (setq-local company-echo-delay 0)                          ; remove annoying blinking
+  (setq-local company-begin-commands '(self-insert-command)) ; start autocompletion only after typing
+  (company-mode t))
 
 (defun company-lean--prefix ()
   "Returns the symbol to complete. Also, if point is on a dot,
 triggers a completion immediately."
-  (if company-lean-begin-after-member-access
-      (company-grab-symbol-cons "\\." 1)
-    (company-grab-symbol)))
+  (let ((prefix (company-grab-symbol)))
+    (when (or
+           (> (length prefix) 3))
+      prefix)))
 
-(defun company-go--invoke-autocomplete ()
-  (let ((temp-buffer (generate-new-buffer "*leancompany*")))
-    (prog2
-	(call-process-region (point-min)
-			     (point-max)
-			     "leancompany"
-			     nil
-			     temp-buffer
-			     nil
-			     "-f=csv"
-			     "autocomplete"
-			     (or (buffer-file-name) "")
-			     (concat "c" (int-to-string (- (point) 1))))
-	(with-current-buffer temp-buffer (buffer-string))
-      (kill-buffer temp-buffer))))
+(defun company-lean--make-candidate (arg)
+  (propertize (car arg) 'type (cdr arg)))
 
-(defun company-lean--candidates ()
-  (company-lean--get-candidates (split-string (company-lean--invoke-autocomplete) "\n" t)))
+(defun company-lean--candidates (prefix)
+  (let ((line-number (line-number-at-pos)))
+    (lean-server-send-cmd-sync (lean-cmd-findp line-number prefix)
+                               (lambda (candidates)
+                                 (-map 'company-lean--make-candidate candidates)))))
+
+(defun company-lean--location (arg)
+  (lean-generate-tags)
+  (let ((tags-table-list (company-etags-buffer-table)))
+    (when (fboundp 'find-tag-noselect)
+      (save-excursion
+        (let ((buffer (find-tag-noselect arg)))
+          (cons buffer (with-current-buffer buffer (point))))))))
+
+(defun company-lean--annotation (candidate)
+  (let ((type (get-text-property 0 'type candidate)))
+    (when type
+      (format " : %s" type))))
 
 ;;;###autoload
 (defun company-lean (command &optional arg &rest ignored)
   (case command
-    (prefix (and (derived-mode-p 'lean-mode)
-                 (not (company-in-string-or-comment))
-                 (or (company-lean--prefix) 'stop)))
-    (candidates (company-lean--candidates))
-    (meta (get-text-property 0 'meta arg))
-    (annotation
-     (when company-lean-show-annotation
-       (get-text-property 0 'meta arg)))
+    (prefix (company-lean--prefix))
+    (candidates (company-lean--candidates arg))
+    (annotation (company-lean--annotation arg))
     (location (company-lean--location arg))
     (sorted t)))
 
-(provide 'company-lean)
-
-(defun company-lean--doc-buffer (candidate)
-    (message "doc candidate = %S" candidate)
-  (company-doc-buffer (get-text-property 0 'doc candidate)))
-
-(defun company-lean--annotation (candidate)
-  (message "annotation candidate = %S" candidate)
-    (let ((anno (get-text-property 0 'kind candidate)))
-      (when anno (concat " blabla" anno)))
-    " : annotation1")
-
-(defun company-lean--candidates (prefix)
-  (cl-loop for x in '("foobar" "foobaz" "foobarbaz")
-           collect x
-           ))
-
-(defun company-my-backend (command &optional arg &rest ignored)
-  (interactive (list 'interactive))
-  (case command
-    (interactive (company-begin-backend 'company-my-backend))
-    (prefix (when (looking-back "foo\\>")
-              (match-string 0)))
-    (candidates (company-lean--candidates arg))
-    (annotation (company-lean--annotation arg))
-    ))
-
-(set (make-local-variable 'company-backends) '(company-my-backend))
-(company-mode)
-
+(provide 'lean-company)

src/emacs/lean-mode.el

@@ -26,6 +26,7 @@
 (require 'lean-option)
 (require 'lean-syntax)
 (require 'lean-mmm-lua)
+(require 'lean-company)
 
 (defun lean-compile-string (exe-name args file-name)
   "Concatenate exe-name, args, and file-name"
@@ -108,7 +109,7 @@
     ;; ;; Immediately show error popups when navigating to an error
     ;; (next-error-hook                  . lean-display-error-at-point))
     )
-    "Hooks which lean-mode needs to hook in.
+  "Hooks which lean-mode needs to hook in.
 
 The `car' of each pair is a hook variable, the `cdr' a function
 to be added or removed from the hook variable if Flycheck mode is
@@ -139,9 +140,7 @@ enabled and disabled respectively.")
     (lean-eldoc-documentation-function))
   ;; company-mode
   (when lean-company-use
-    (require 'company)
-    (company-mode t)
-    (set (make-local-variable 'company-backends) '(company-etags))))
+    (company-lean-hook)))
 
 ;; Automode List
 ;;;###autoload