feat(emacs/lean-company): call FINDG if cursor is at "_"

src/emacs/lean-company.el

@@ -31,22 +31,34 @@
   "Returns the symbol to complete. Also, if point is on a dot,
 triggers a completion immediately."
   (let ((prefix (company-grab-symbol)))
-    (when (and
+    (cond ((looking-at (rx symbol-start "_")) "")
+          ((and
             (company-lean--need-autocomplete)
             (or
              (> (length prefix) 3)
              (string-match "[_.]" prefix)))
-      prefix)))
+           prefix))))
 
 (defun company-lean--make-candidate (arg)
   (propertize (car arg) 'type (cdr arg)))
 
 (defun company-lean--candidates (prefix)
-  (let ((line-number (line-number-at-pos)))
+  (let ((line-number (line-number-at-pos))
+        (column-number (current-column))
+        pattern)
+    (lean-server-send-cmd-sync (lean-cmd-wait))
+    (cond
+     ((looking-at (rx symbol-start "_"))
+      (setq pattern (read-string "Filter for find declarations (e.g: +intro -and): " "" nil ""))
+      (lean-server-send-cmd-sync (lean-cmd-findg line-number column-number pattern)
+                                 (lambda (candidates)
+                                   (lean-server-debug "executing continuation for FINDG")
+                                   (-map 'company-lean--make-candidate candidates))))
+     (t
       (lean-server-send-cmd-sync (lean-cmd-findp line-number prefix)
                                  (lambda (candidates)
                                    (lean-server-debug "executing continuation for FINDP")
-                                 (-map 'company-lean--make-candidate candidates)))))
+                                   (-map 'company-lean--make-candidate candidates)))))))
 
 (defun company-lean--location (arg)
   (lean-generate-tags)
@@ -74,6 +86,10 @@ triggers a completion immediately."
                  "...")))
         annotation-str))))
 
+(defun company-lean--pre-completion (args)
+  (when (looking-at (rx "_"))
+    (delete-forward-char 1)))
+
 ;;;###autoload
 (defun company-lean (command &optional arg &rest ignored)
   (case command
@@ -81,6 +97,7 @@ triggers a completion immediately."
     (candidates (company-lean--candidates arg))
     (annotation (company-lean--annotation arg))
     (location (company-lean--location arg))
+    (pre-completion (company-lean--pre-completion arg))
     (sorted t)))
 
 (defadvice company--window-width

src/emacs/lean-mode.el

@@ -54,12 +54,14 @@
 
 
 (defun lean-check-expansion ()
+  (interactive)
   (save-excursion
+    (if (looking-at (rx symbol-start "_")) t
       (if (looking-at "\\_>") t
         (backward-char 1)
         (if (looking-at "\\.") t
           (backward-char 1)
-        (if (looking-at "->") t nil)))))
+          (if (looking-at "->") t nil))))))
 
 (defun lean-tab-indent-or-complete ()
   (interactive)

src/emacs/lean-server.el

@@ -258,8 +258,10 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
     ('OPTIONS ())
     ('SHOW    (lean-server-check-current-file))
     ('VALID   (lean-server-check-current-file))
-    ('FINDP   (lean-server-check-current-file))
+    ('FINDP   (lean-flush-changed-lines)
-    ('FINDG   (lean-server-check-current-file))))
+              (lean-server-check-current-file))
+    ('FINDG   (lean-flush-changed-lines)
+              (lean-server-check-current-file))
     ('WAIT    (lean-server-check-current-file))))
 
 (defun lean-server-after-send-cmd (cmd)
@@ -278,7 +280,7 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
     ('SHOW    ())
     ('VALID   ())
     ('FINDP   ())
-    ('FINDG   ())))
+    ('FINDG   ())
     ('WAIT    ())))
 
 (defun lean-server-send-cmd (cmd)
@@ -361,7 +363,8 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
     (lean-server-set-timer-for-event-handler)))
 
 (defun lean-server-consume-all-async-tasks ()
-  (lean-server-debug "lean-server-consume-all-async-tasks")
+  (lean-server-debug "lean-server-consume-all-async-tasks: queue size = %d"
+                     (lean-server-async-task-queue-len))
   (while lean-global-async-task-queue
     (accept-process-output (lean-server-get-process) 0 50 t)
     (let* ((cont   (lean-server-async-task-queue-peek-front))
@@ -370,7 +373,9 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
         (`(PROCESSED ,ret)
          (lean-server-async-task-queue-pop-front)
          (lean-server-debug "lean-server-consume-all-sync-tasks: processed. queue size = %d"
-                            (lean-server-async-task-queue-len)))))))
+                            (lean-server-async-task-queue-len))))))
+  (lean-server-debug "lean-server-consume-all-async-tasks: over. queue size = %d"
+                     (lean-server-async-task-queue-len)))
 
 (defun lean-server-send-cmd-sync (cmd &optional cont)
   "Send cmd to lean-server (sync)."