diff --git a/src/emacs/lean-company.el b/src/emacs/lean-company.el
new file mode 100644
index 0000000000..2b72e99134
--- /dev/null
+++ b/src/emacs/lean-company.el
@@ -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)
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index d03bf1353d..9c297de0dc 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -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)
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index bcdac3c8de..1d7f9371dc 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -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)
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 6a9bc9fb85..ec1d754e59 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -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;
diff --git a/src/shell/server.cpp b/src/shell/server.cpp
index 3950539134..10bd2b18e1 100644
--- a/src/shell/server.cpp
+++ b/src/shell/server.cpp
@@ -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
diff --git a/src/shell/server.h b/src/shell/server.h
index c7ff5c0bb6..e7b8d87c4d 100644
--- a/src/shell/server.h
+++ b/src/shell/server.h
@@ -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();
+
 }