<commit_before>;; -*- lexical-binding: t; -*-
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: <NAME>
;;
(require 'company)
(require 'company-etags)
(require 'dash)
(require 'dash-functional)
(require 'lean-tags)
(require 'lean-server)

(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 nil)                         ; 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--need-autocomplete ()
  (not (looking-back
        (rx (or "theorem" "definition" "lemma" "axiom" "parameter"
                "abbreviation" "variable" "hypothesis" "conjecture"
                "corollary")
            (+ white)
            (* (not white))))))

(defun company-lean--prefix ()
  "Returns the symbol to complete. Also, if point is on a dot,
triggers a completion immediately."
  (let ((prefix (company-grab-symbol)))
    (cond ((looking-at (rx symbol-start "_")) "")
          ((and
            (company-lean--need-autocomplete)
            (or
             (> (length prefix) 3)
             (string-match "[_.]" 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))
        (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)))))))

(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<commit_msg>feat(emacs/lean-company): "c-u TAB" asks filter for FINDG<commit_after>;; -*- lexical-binding: t; -*-
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
;; Released under Apache 2.0 license as described in the file LICENSE.
;;
;; Author: <NAME>
;;
(require 'company)
(require 'company-etags)
(require 'dash)
(require 'dash-functional)
(require 'lean-tags)
(require 'lean-server)

(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 nil)                         ; 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--need-autocomplete ()
  (not (looking-back
        (rx (or "theorem" "definition" "lemma" "axiom" "parameter"
                "abbreviation" "variable" "hypothesis" "conjecture"
                "corollary")
            (+ white)
            (* (not white))))))

(defun company-lean--prefix ()
  "Returns the symbol to complete. Also, if point is on a dot,
triggers a completion immediately."
  (let ((prefix (company-grab-symbol)))
    (cond ((looking-at (rx symbol-start "_")) "")
          ((and
            (company-lean--need-autocomplete)
            (or
             (> (length prefix) 3)
             (string-match "[_.]" 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))
        (column-number (current-column))
        pattern)
    (lean-server-send-cmd-sync (lean-cmd-wait))
    (cond
     ((looking-at (rx symbol-start "_"))
      (setq pattern (if current-prefix-arg
                        (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)))))))

(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
{'fraction_non_alphanumeric': 0.1410488245931284, 'fraction_numerical': 0.003616636528028933, 'mean_word_length': 2.241342567927544, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3483930', 'n_tokens_mistral': 1812, 'n_tokens_neox': 1781, 'n_words': 451}