feat(shell/server, emacs): bring back basic completion
This commit is contained in:
Sebastian Ullrich
Leonardo de Moura
parent
2a5616d2b9
commit
7e570d7777
6 changed files with 606 additions and 4 deletions
378
src/emacs/lean-company.el
Normal file
378
src/emacs/lean-company.el
Normal file
|
|
@ -0,0 +1,378 @@
|
|||
;; -*- lexical-binding: t; -*-
|
||||
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
;; Released under Apache 2.0 license as described in the file LICENSE.
|
||||
;;
|
||||
;; Authors: Soonho Kong, Sebastian Ullrich
|
||||
;;
|
||||
(require 'company)
|
||||
(require 'company-etags)
|
||||
(require 'dash)
|
||||
(require 'dash-functional)
|
||||
(require 'f)
|
||||
(require 's)
|
||||
(require 'cl-lib)
|
||||
(require 'lean-util)
|
||||
(require 'lean-server)
|
||||
|
||||
(defun company-lean-hook ()
|
||||
(set (make-local-variable 'company-backends) '(;company-lean--import
|
||||
;company-lean--option-name
|
||||
;company-lean--findg
|
||||
company-lean--findp))
|
||||
(setq-local company-tooltip-limit 20) ; bigger popup window
|
||||
(setq-local company-minimum-prefix-length 5)
|
||||
;(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--check-prefix ()
|
||||
"Check whether to use company-lean or not"
|
||||
(or ;(company-lean--import-prefix)
|
||||
;(company-lean--option-name-prefix)
|
||||
;(company-lean--findg-prefix)
|
||||
(company-lean--findp-prefix)))
|
||||
|
||||
(defun company-lean--import-remove-lean (file-name)
|
||||
(cond
|
||||
((s-ends-with? "/default.lean" file-name)
|
||||
(s-left (- (length file-name)
|
||||
(length "/default.lean"))
|
||||
file-name))
|
||||
((s-ends-with? "/default.hlean" file-name)
|
||||
(s-left (- (length file-name)
|
||||
(length "/default.hlean"))
|
||||
file-name))
|
||||
((s-ends-with? ".lean" file-name)
|
||||
(s-left (- (length file-name)
|
||||
(length ".lean"))
|
||||
file-name))
|
||||
((s-ends-with? ".hlean" file-name)
|
||||
(s-left (- (length file-name)
|
||||
(length ".hlean"))
|
||||
file-name))
|
||||
(t file-name)))
|
||||
|
||||
(defun company-lean--import-candidates-main (root-dir)
|
||||
(when root-dir
|
||||
(let* ((dummy (message "finding files under %s..." root-dir))
|
||||
(lean-files (with-timeout (lean-company-import-timeout
|
||||
(message "finding files under %s... timeout (%S sec)"
|
||||
root-dir lean-company-import-timeout) nil)
|
||||
(lean-find-files root-dir
|
||||
(lambda (file) (equal (f-ext file) "lean"))
|
||||
t)))
|
||||
(lean-files-r (--map (f-relative it root-dir) lean-files))
|
||||
(candidates
|
||||
(--map (s-replace-all `((,(f-path-separator) . "."))
|
||||
(company-lean--import-remove-lean it))
|
||||
lean-files-r)))
|
||||
(--zip-with (propertize it 'file-name other) candidates lean-files))))
|
||||
|
||||
(defun company-lean--import-prefix ()
|
||||
"Import auto-completion is triggered when it looks at 'import ...'"
|
||||
(when (looking-back
|
||||
(rx "import"
|
||||
(* (+ white)
|
||||
(+ (or alnum digit "." "_")))
|
||||
(? (+ white))))
|
||||
(company-grab-symbol)))
|
||||
|
||||
(defun company-lean--import-candidates (prefix)
|
||||
(let* ((cur-dir (f-dirname (buffer-file-name)))
|
||||
(parent-dir (f-parent cur-dir))
|
||||
(candidates
|
||||
(cond
|
||||
;; prefix = ".."
|
||||
((and parent-dir (s-starts-with? ".." prefix))
|
||||
(--map (concat ".." it)
|
||||
(company-lean--import-candidates-main parent-dir)))
|
||||
;; prefix = "."
|
||||
((s-starts-with? "." prefix)
|
||||
(--map (concat "." it)
|
||||
(company-lean--import-candidates-main cur-dir)))
|
||||
;; normal prefix
|
||||
(t (-flatten
|
||||
(-map 'company-lean--import-candidates-main
|
||||
(lean-path-list)))))))
|
||||
(--filter (s-starts-with? prefix it) candidates)))
|
||||
|
||||
(defun company-lean--import-location (arg)
|
||||
(let ((file-name (get-text-property 0 'file-name arg)))
|
||||
`(,file-name . 1)))
|
||||
|
||||
(defun company-lean--import (command &optional arg &rest ignored)
|
||||
(cl-case command
|
||||
(prefix (company-lean--import-prefix))
|
||||
(candidates (company-lean--import-candidates arg))
|
||||
(location (company-lean--import-location arg))
|
||||
(sorted t)))
|
||||
|
||||
;; OPTION
|
||||
;; ======
|
||||
(defun company-lean--option-name-prefix ()
|
||||
"Option auto-completion is triggered when it looks at 'set-option '"
|
||||
(when (looking-back (rx "set_option" (+ white) (* (or alnum digit "." "_"))))
|
||||
(company-grab-symbol)))
|
||||
|
||||
(defun company-lean--option-make-candidate (arg)
|
||||
(let* ((text (car arg))
|
||||
(option (cdr arg))
|
||||
(type (lean-option-record-type option))
|
||||
(value (lean-option-record-value option))
|
||||
(desc (lean-option-record-desc option)))
|
||||
(propertize text
|
||||
'type type
|
||||
'value value
|
||||
'desc desc)))
|
||||
|
||||
(defun company-lean--option-name-meta (candidate)
|
||||
(get-text-property 0 'desc candidate))
|
||||
|
||||
(defun company-lean--option-name-annotation (candidate)
|
||||
(let* ((type (get-text-property 0 'type candidate))
|
||||
(value (get-text-property 0 'value candidate)))
|
||||
(format " : %s = %s" type value)))
|
||||
|
||||
(defun company-lean--option-name-candidates (prefix)
|
||||
(let ((candidates
|
||||
(lean-get-options-sync-with-cont
|
||||
(lambda (option-record-alist)
|
||||
(-map 'company-lean--option-make-candidate option-record-alist)))))
|
||||
(--filter (s-starts-with? prefix it) candidates)))
|
||||
|
||||
(defun company-lean--option-name (command &optional arg &rest ignored)
|
||||
(cl-case command
|
||||
(prefix (company-lean--option-name-prefix))
|
||||
(candidates (company-lean--option-name-candidates arg))
|
||||
(meta (company-lean--option-name-meta arg))
|
||||
(annotation (company-lean--option-name-annotation arg))
|
||||
(no-cache t)
|
||||
(sorted t)))
|
||||
|
||||
;; FINDG
|
||||
;; =====
|
||||
|
||||
(defun company-lean--findg-prefix ()
|
||||
"FINDG is triggered when it looks at '_'"
|
||||
(when (looking-at (rx symbol-start "_")) ""))
|
||||
|
||||
(defun company-lean--findg-candidates (prefix)
|
||||
(let ((line-number (line-number-at-pos))
|
||||
(column-number (lean-line-offset))
|
||||
pattern)
|
||||
(lean-server-send-cmd-sync (lean-cmd-wait) '(lambda () ()))
|
||||
(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-debug "executing continuation for FINDG")
|
||||
(--map (company-lean--findp-make-candidate it prefix) candidates)))))
|
||||
|
||||
(defun company-lean--findg-pre-completion (args)
|
||||
"Delete current '_' before filling the selected AC candidate"
|
||||
(when (looking-at (rx "_"))
|
||||
(delete-forward-char 1)))
|
||||
|
||||
(defun company-lean--findg (command &optional arg &rest ignored)
|
||||
(cl-case command
|
||||
(prefix (company-lean--findg-prefix))
|
||||
(candidates (company-lean--findg-candidates arg))
|
||||
(annotation (company-lean--findp-annotation arg))
|
||||
(location (company-lean--findp-location arg))
|
||||
(pre-completion (company-lean--findg-pre-completion arg))
|
||||
(sorted t)))
|
||||
|
||||
;; FINDP
|
||||
;; -----
|
||||
(defun company-lean--need-autocomplete ()
|
||||
(interactive)
|
||||
(cond ((looking-back (rx "print" (+ white) "definition" (+ white) (* (not white))))
|
||||
t)
|
||||
((looking-back
|
||||
(rx (or "theorem" "definition" "lemma" "axiom" "parameter"
|
||||
"variable" "hypothesis" "conjecture"
|
||||
"corollary" "open")
|
||||
(+ white)
|
||||
(* (not white))))
|
||||
nil)
|
||||
((looking-back (rx "set_option"
|
||||
(+ white)
|
||||
(+ (or alnum digit "." "_"))
|
||||
(+ white)
|
||||
(* (or alnum digit "." "_"))))
|
||||
nil)
|
||||
(t t)))
|
||||
|
||||
(defun company-lean--findp-prefix ()
|
||||
"Returns the symbol to complete. Also, if point is on a dot,
|
||||
triggers a completion immediately."
|
||||
(let ((prefix (lean-grab-hname)))
|
||||
(when (and
|
||||
prefix
|
||||
(company-lean--need-autocomplete)
|
||||
(or
|
||||
(>= (length prefix) 1)
|
||||
(string-match "[_.]" prefix)))
|
||||
(when (s-starts-with? "@" prefix)
|
||||
(setq prefix (substring prefix 1)))
|
||||
prefix)))
|
||||
|
||||
(cl-defun company-lean--findp-make-candidate (prefix &key text type)
|
||||
(let ((start (s-index-of prefix text)))
|
||||
(propertize text
|
||||
'type type
|
||||
'start start
|
||||
'prefix prefix)))
|
||||
|
||||
(defun company-lean--handle-singleton-candidate (prefix candidates)
|
||||
"Handle singleton candidate. If the candidate does not start
|
||||
with prefix, we add prefix itself as a candidate to prevent
|
||||
from auto-completion."
|
||||
(let ((candidate (car candidates)))
|
||||
(cond ((s-prefix? prefix candidate) candidates)
|
||||
(t `(,candidate ,prefix)))))
|
||||
|
||||
(defun company-lean--findp-candidates (prefix callback)
|
||||
(let ((line-number (line-number-at-pos)))
|
||||
(lean-server-sync)
|
||||
(lean-server-send-command
|
||||
(list :command "complete"
|
||||
:line line-number
|
||||
:pattern prefix)
|
||||
(cl-function
|
||||
(lambda (&key completions)
|
||||
(let ((candidates completions))
|
||||
(lean-debug "executing continuation for FINDP")
|
||||
(setq candidates
|
||||
(--map (apply 'company-lean--findp-make-candidate prefix it)
|
||||
candidates))
|
||||
(when (= (length candidates) 1)
|
||||
(setq candidates
|
||||
(company-lean--handle-singleton-candidate prefix candidates)))
|
||||
(funcall callback candidates))))
|
||||
(lambda (&rest)
|
||||
(funcall callback nil)))))
|
||||
|
||||
(defun company-lean--findp-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--findp-annotation (candidate)
|
||||
(let ((type (get-text-property 0 'type candidate)))
|
||||
(when type
|
||||
(let* ((annotation-str (format " : %s" type))
|
||||
(annotation-len (length annotation-str))
|
||||
(candidate-len (length candidate))
|
||||
(entry-width (+ candidate-len
|
||||
annotation-len))
|
||||
(allowed-width (truncate (* 0.90 (window-body-width)))))
|
||||
(when (> entry-width allowed-width)
|
||||
(setq annotation-str
|
||||
(concat
|
||||
(substring-no-properties annotation-str
|
||||
0
|
||||
(- allowed-width candidate-len 3))
|
||||
"...")))
|
||||
annotation-str))))
|
||||
|
||||
(defun company-lean--findp-match (arg)
|
||||
"Return the end of matched region"
|
||||
(let ((prefix (get-text-property 0 'prefix arg))
|
||||
(start (get-text-property 0 'start arg)))
|
||||
(if start
|
||||
(+ start (length prefix))
|
||||
0)))
|
||||
|
||||
(defun company-lean--findp (command &optional arg &rest ignored)
|
||||
(cl-case command
|
||||
(prefix (company-lean--findp-prefix))
|
||||
(candidates (cons :async (lambda (cb) (company-lean--findp-candidates arg cb))))
|
||||
(annotation (company-lean--findp-annotation arg))
|
||||
(location (company-lean--findp-location arg))
|
||||
(match (company-lean--findp-match arg))
|
||||
(no-cache t)
|
||||
(require-match 'never)
|
||||
(sorted t)))
|
||||
|
||||
;; ADVICES
|
||||
;; =======
|
||||
|
||||
(defadvice company--window-width
|
||||
(after lean-company--window-width activate)
|
||||
(when (eq major-mode 'lean-mode)
|
||||
(setq ad-return-value (truncate (* 0.95 (window-body-width))))))
|
||||
|
||||
(defun replace-regex-return-position (regex rep string &optional start)
|
||||
"Find regex and replace with rep on string.
|
||||
|
||||
Return replaced string and start and end positions of replacement."
|
||||
(let* ((start (or start 0))
|
||||
(len (length string))
|
||||
(m-start (string-match regex string start))
|
||||
(m-end (match-end 0))
|
||||
pre-string post-string matched-string replaced-string result)
|
||||
(cond (m-start
|
||||
(setq pre-string (substring string 0 m-start))
|
||||
(setq matched-string (substring string m-start m-end))
|
||||
(setq post-string (substring string m-end))
|
||||
(string-match regex matched-string)
|
||||
(setq replaced-string
|
||||
(replace-match rep nil nil matched-string))
|
||||
(setq result (concat pre-string
|
||||
replaced-string
|
||||
post-string))
|
||||
`(,result ,m-start ,(+ m-start (length replaced-string)))
|
||||
))))
|
||||
|
||||
(defun replace-regex-add-properties-all (regex rep string properties)
|
||||
"Find all occurrences of regex in string, and replace them with
|
||||
rep. Then, add text-properties on the replaced region."
|
||||
(let ((replace-result-items (replace-regex-return-position regex rep string))
|
||||
(result string))
|
||||
(while replace-result-items
|
||||
(pcase replace-result-items
|
||||
(`(,replaced-string ,m-start ,m-end)
|
||||
(setq result replaced-string)
|
||||
(add-text-properties m-start m-end properties result)
|
||||
(setq replace-result-items
|
||||
(replace-regex-return-position regex rep result m-end)))))
|
||||
result))
|
||||
|
||||
(eval-after-load 'company
|
||||
'(defadvice company-fill-propertize
|
||||
(after lean-company-fill-propertize activate)
|
||||
(when (eq major-mode 'lean-mode)
|
||||
(let* ((selected (ad-get-arg 3))
|
||||
(foreground-color lean-company-type-foreground)
|
||||
(background-color (if selected (face-background 'company-tooltip-selection)
|
||||
(face-background 'company-tooltip)))
|
||||
(face-attrs
|
||||
(cond (background-color `(:foreground ,foreground-color
|
||||
:background ,background-color))
|
||||
(t `(:foreground ,foreground-color))))
|
||||
(properties `(face ,face-attrs
|
||||
mouse-face company-tooltip))
|
||||
(old-return ad-return-value)
|
||||
(old-len (length old-return))
|
||||
new-return new-len)
|
||||
(setq new-return
|
||||
(replace-regex-add-properties-all
|
||||
(rx "?" word-start (group (+ (not white))) word-end)
|
||||
"\\1"
|
||||
ad-return-value
|
||||
properties))
|
||||
(setq new-len (length new-return))
|
||||
(while (< (length new-return) old-len)
|
||||
(setq new-return
|
||||
(concat new-return " ")))
|
||||
(when background-color
|
||||
(add-text-properties new-len old-len properties new-return))
|
||||
(setq ad-return-value new-return)))))
|
||||
|
||||
(provide 'lean-company)
|
||||
|
|
@ -24,6 +24,7 @@
|
|||
(require 'lean-option)
|
||||
(require 'lean-syntax)
|
||||
(require 'lean-project)
|
||||
(require 'lean-company)
|
||||
(require 'lean-server)
|
||||
|
||||
(defun lean-server-split-buffer (buf-str beg-regex end-regex)
|
||||
|
|
@ -233,6 +234,7 @@ placeholder, call lean-server with --hole option, otherwise call
|
|||
(local-set-key lean-keybinding-show-key 'quail-show-key)
|
||||
(local-set-key lean-keybinding-set-option 'lean-set-option)
|
||||
(local-set-key lean-keybinding-eval-cmd 'lean-eval-cmd)
|
||||
(local-set-key lean-keybinding-tab-indent-or-complete 'lean-tab-indent-or-complete)
|
||||
(local-set-key lean-keybinding-lean-show-goal-at-pos 'lean-show-goal-at-pos)
|
||||
(local-set-key lean-keybinding-lean-show-id-keyword-info 'lean-show-id-keyword-info)
|
||||
(local-set-key lean-keybinding-lean-next-error-mode 'lean-next-error-mode)
|
||||
|
|
|
|||
|
|
@ -39,6 +39,16 @@
|
|||
:group 'lean
|
||||
:type 'string)
|
||||
|
||||
(defcustom lean-company-use t
|
||||
"Use company mode for lean."
|
||||
:group 'lean
|
||||
:type 'boolean)
|
||||
|
||||
(defcustom lean-company-type-foreground (face-foreground 'font-lock-keyword-face)
|
||||
"Color of type parameter in auto-complete candidates"
|
||||
:group 'lean
|
||||
:type 'color)
|
||||
|
||||
(defcustom lean-eldoc-use t
|
||||
"Use eldoc mode for lean."
|
||||
:group 'lean
|
||||
|
|
@ -147,6 +157,9 @@ false (nil)."
|
|||
(defcustom lean-keybinding-eval-cmd (kbd "C-c C-e")
|
||||
"Lean Keybinding for eval-cmd"
|
||||
:group 'lean-keybinding :type 'key-sequence)
|
||||
(defcustom lean-keybinding-tab-indent-or-complete (kbd "TAB")
|
||||
"Lean Keybinding for tab-indent-or-complete"
|
||||
:group 'lean-keybinding :type 'key-sequence)
|
||||
(defcustom lean-keybinding-lean-show-goal-at-pos (kbd "C-c C-g")
|
||||
"Lean Keybinding for show-goal-at-pos"
|
||||
:group 'lean-keybinding :type 'key-sequence)
|
||||
|
|
|
|||
|
|
@ -219,8 +219,20 @@ EMSCRIPTEN_BINDINGS(LEAN_JS) {
|
|||
}
|
||||
int main() { return 0; }
|
||||
#else
|
||||
class initializer {
|
||||
private:
|
||||
lean::initializer m_init;
|
||||
public:
|
||||
initializer() {
|
||||
lean::initialize_server();
|
||||
}
|
||||
~initializer() {
|
||||
lean::finalize_server();
|
||||
}
|
||||
};
|
||||
|
||||
int main(int argc, char ** argv) {
|
||||
lean::initializer init;
|
||||
initializer init;
|
||||
bool export_objects = false;
|
||||
unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL+1;
|
||||
bool smt2 = false;
|
||||
|
|
|
|||
|
|
@ -2,16 +2,36 @@
|
|||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Gabriel Ebner
|
||||
Authors: Gabriel Ebner, Leonardo de Moura, Sebastian Ullrich
|
||||
*/
|
||||
#if defined(LEAN_SERVER)
|
||||
#include <list>
|
||||
#include <string>
|
||||
#include "frontends/lean/parser.h"
|
||||
#include "library/module.h"
|
||||
#include "shell/server.h"
|
||||
#include <list>
|
||||
#include "util/sexpr/option_declarations.h"
|
||||
#include "frontends/lean/util.h"
|
||||
#include "library/protected.h"
|
||||
#include "library/scoped_ext.h"
|
||||
#include "util/bitap_fuzzy_search.h"
|
||||
#include "library/type_context.h"
|
||||
#include "kernel/instantiate.h"
|
||||
|
||||
#ifndef LEAN_DEFAULT_AUTO_COMPLETION_MAX_RESULTS
|
||||
#define LEAN_DEFAULT_AUTO_COMPLETION_MAX_RESULTS 100
|
||||
#endif
|
||||
|
||||
#define LEAN_FUZZY_MAX_ERRORS 3
|
||||
#define LEAN_FUZZY_MAX_ERRORS_FACTOR 3
|
||||
#define LEAN_COMPLETE_CONSUME_IMPLICIT true // lean will add metavariables for implicit arguments in serialize_decl()
|
||||
|
||||
namespace lean {
|
||||
static name * g_auto_completion_max_results = nullptr;
|
||||
|
||||
unsigned get_auto_completion_max_results(options const & o) {
|
||||
return o.get_unsigned(*g_auto_completion_max_results, LEAN_DEFAULT_AUTO_COMPLETION_MAX_RESULTS);
|
||||
}
|
||||
|
||||
class null_message_stream : public message_stream {
|
||||
public:
|
||||
|
|
@ -57,6 +77,8 @@ json server::handle_request(json const & req) {
|
|||
return handle_sync(req);
|
||||
} else if (command == "check") {
|
||||
return handle_check(req);
|
||||
} else if (command == "complete") {
|
||||
return handle_complete(req);
|
||||
}
|
||||
|
||||
json res;
|
||||
|
|
@ -147,5 +169,173 @@ json server::handle_check(json const &) {
|
|||
return res;
|
||||
}
|
||||
|
||||
snapshot const * server::get_closest_snapshot(unsigned line) {
|
||||
snapshot const * ret = nullptr;
|
||||
for (snapshot const & snap : m_snapshots) {
|
||||
if (snap.m_pos.first <= line)
|
||||
ret = &snap;
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
/** \brief Return an (atomic) name if \c n can be referenced by this atomic
|
||||
name in the given environment. */
|
||||
optional<name> is_essentially_atomic(environment const & env, name const & n) {
|
||||
if (n.is_atomic())
|
||||
return optional<name>(n);
|
||||
list<name> const & ns_list = get_namespaces(env);
|
||||
for (name const & ns : ns_list) {
|
||||
if (is_prefix_of(ns, n)) {
|
||||
auto n_prime = n.replace_prefix(ns, name());
|
||||
if (n_prime.is_atomic() && !is_protected(env, n))
|
||||
return optional<name>(n_prime);
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (auto it = is_uniquely_aliased(env, n))
|
||||
if (it->is_atomic())
|
||||
return it;
|
||||
return optional<name>();
|
||||
}
|
||||
|
||||
unsigned get_fuzzy_match_max_errors(unsigned prefix_sz) {
|
||||
unsigned r = (prefix_sz / LEAN_FUZZY_MAX_ERRORS_FACTOR);
|
||||
if (r > LEAN_FUZZY_MAX_ERRORS)
|
||||
return LEAN_FUZZY_MAX_ERRORS;
|
||||
return r;
|
||||
}
|
||||
|
||||
optional<name> exact_prefix_match(environment const & env, std::string const & pattern, declaration const & d) {
|
||||
if (auto it = is_essentially_atomic(env, d.get_name())) {
|
||||
std::string it_str = it->to_string();
|
||||
// if pattern "perfectly" matches beginning of declaration name, we just display d on the top of the list
|
||||
if (it_str.compare(0, pattern.size(), pattern) == 0)
|
||||
return it;
|
||||
} else {
|
||||
std::string d_str = d.get_name().to_string();
|
||||
if (d_str.compare(0, pattern.size(), pattern) == 0)
|
||||
return optional<name>(d.get_name());
|
||||
}
|
||||
return optional<name>();
|
||||
}
|
||||
|
||||
json server::serialize_decl(name const & short_name, name const & long_name, environment const & env, options const & o) {
|
||||
declaration const & d = env.get(long_name);
|
||||
type_context tc(env);
|
||||
io_state_stream out = regular(env, m_ios, tc).update_options(o);
|
||||
expr type = d.get_type();
|
||||
if (LEAN_COMPLETE_CONSUME_IMPLICIT) {
|
||||
while (true) {
|
||||
if (!is_pi(type))
|
||||
break;
|
||||
if (!binding_info(type).is_implicit() && !binding_info(type).is_inst_implicit())
|
||||
break;
|
||||
std::string q("?");
|
||||
q += binding_name(type).to_string();
|
||||
expr m = mk_constant(name(q.c_str()));
|
||||
type = instantiate(binding_body(type), m);
|
||||
}
|
||||
}
|
||||
json completion;
|
||||
completion["text"] = short_name.to_string();
|
||||
std::ostringstream ss;
|
||||
ss << mk_pair(flatten(out.get_formatter()(type)), o);
|
||||
completion["type"] = ss.str();
|
||||
return completion;
|
||||
}
|
||||
|
||||
json server::serialize_decl(name const & d, environment const & env, options const & o) {
|
||||
// using namespace override resolution rule
|
||||
list<name> const & ns_list = get_namespaces(env);
|
||||
for (name const & ns : ns_list) {
|
||||
name new_d = d.replace_prefix(ns, name());
|
||||
if (new_d != d &&
|
||||
!new_d.is_anonymous() &&
|
||||
(!new_d.is_atomic() || !is_protected(env, d))) {
|
||||
return serialize_decl(new_d, d, env, o);
|
||||
}
|
||||
}
|
||||
// if the alias is unique use it
|
||||
if (auto it = is_uniquely_aliased(env, d)) {
|
||||
return serialize_decl(*it, d, env, o);
|
||||
} else {
|
||||
return serialize_decl(d, d, env, o);
|
||||
}
|
||||
}
|
||||
|
||||
json server::handle_complete(json const & req) {
|
||||
std::string pattern = req["pattern"];
|
||||
unsigned line = req["line"];
|
||||
std::vector<json> completions;
|
||||
|
||||
if (snapshot const * snap = get_closest_snapshot(line)) {
|
||||
environment const & env = snap->m_env;
|
||||
options const & opts = snap->m_options;
|
||||
unsigned max_results = get_auto_completion_max_results(opts);
|
||||
unsigned max_errors = get_fuzzy_match_max_errors(pattern.size());
|
||||
std::vector<pair<name, name>> exact_matches;
|
||||
std::vector<pair<std::string, name>> selected;
|
||||
bitap_fuzzy_search matcher(pattern, max_errors);
|
||||
env.for_each_declaration([&](declaration const & d) {
|
||||
/*if (is_projection(env, d.get_name()))
|
||||
return;*/
|
||||
if (auto it = exact_prefix_match(env, pattern, d)) {
|
||||
exact_matches.emplace_back(*it, d.get_name());
|
||||
} else {
|
||||
std::string text = d.get_name().to_string();
|
||||
if (matcher.match(text))
|
||||
selected.emplace_back(text, d.get_name());
|
||||
}
|
||||
});
|
||||
unsigned num_results = 0;
|
||||
if (!exact_matches.empty()) {
|
||||
std::sort(exact_matches.begin(), exact_matches.end(),
|
||||
[](pair<name, name> const & p1, pair<name, name> const & p2) {
|
||||
return p1.first.size() < p2.first.size();
|
||||
});
|
||||
for (pair<name, name> const & p : exact_matches) {
|
||||
completions.push_back(serialize_decl(p.first, p.second, env, opts));
|
||||
num_results++;
|
||||
if (num_results >= max_results)
|
||||
break;
|
||||
}
|
||||
}
|
||||
unsigned sz = selected.size();
|
||||
if (sz == 1) {
|
||||
completions.push_back(serialize_decl(selected[0].second, env, opts));
|
||||
} else if (sz > 1) {
|
||||
std::vector<pair<std::string, name>> next_selected;
|
||||
for (unsigned k = 0; k <= max_errors && num_results < max_results; k++) {
|
||||
bitap_fuzzy_search matcher(pattern, k);
|
||||
for (auto const & s : selected) {
|
||||
if (matcher.match(s.first)) {
|
||||
completions.push_back(serialize_decl(s.second, env, opts));
|
||||
num_results++;
|
||||
if (num_results >= max_results)
|
||||
break;
|
||||
} else {
|
||||
next_selected.push_back(s);
|
||||
}
|
||||
}
|
||||
std::swap(selected, next_selected);
|
||||
next_selected.clear();
|
||||
}
|
||||
}
|
||||
}
|
||||
json res;
|
||||
res["response"] = "ok";
|
||||
res["completions"] = completions;
|
||||
return res;
|
||||
}
|
||||
|
||||
void initialize_server() {
|
||||
g_auto_completion_max_results = new name{"auto_completion", "max_results"};
|
||||
register_unsigned_option(*g_auto_completion_max_results, LEAN_DEFAULT_AUTO_COMPLETION_MAX_RESULTS,
|
||||
"(auto-completion) maximum number of results returned");
|
||||
}
|
||||
|
||||
void finalize_server() {
|
||||
delete g_auto_completion_max_results;
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Gabriel Ebner
|
||||
Authors: Gabriel Ebner, Sebastian Ullrich
|
||||
*/
|
||||
#pragma once
|
||||
#include "kernel/pos_info_provider.h"
|
||||
|
|
@ -28,11 +28,15 @@ class server {
|
|||
list<message> m_messages;
|
||||
snapshot_vector m_snapshots;
|
||||
|
||||
snapshot const * get_closest_snapshot(unsigned linenum);
|
||||
json handle_request(json const & req);
|
||||
|
||||
json handle_sync(json const & req);
|
||||
json handle_check(json const & req);
|
||||
json handle_complete(json const & req);
|
||||
|
||||
json serialize_decl(name const & short_name, name const & long_name, environment const & env, options const & o);
|
||||
json serialize_decl(name const & d, environment const & env, options const & o);
|
||||
public:
|
||||
server(unsigned num_threads, environment const & intial_env, io_state const & ios);
|
||||
~server();
|
||||
|
|
@ -40,4 +44,7 @@ public:
|
|||
void run();
|
||||
};
|
||||
|
||||
void initialize_server();
|
||||
void finalize_server();
|
||||
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue