diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index b27b3bc508..482574544c 100644 --- a/src/emacs/lean-server.el +++ b/src/emacs/lean-server.el @@ -7,6 +7,7 @@ (require 'json) (require 'tq) (require 'lean-debug) +(require 'lean-project) (defvar-local lean-server-process nil "Lean server process for the current buffer") @@ -25,9 +26,10 @@ (when (or (not lean-server-process) (not (equal (process-status lean-server-process) 'run))) (setq lean-server-process - (start-file-process "lean-server" - (format "*lean-server (%s)*" (buffer-name)) - "lean" "--server")) + (let* ((default-directory (or (lean-project-find-root) default-directory))) + (start-file-process "lean-server" + (format "*lean-server (%s)*" (buffer-name)) + "lean" "--server"))) (set-process-query-on-exit-flag lean-server-process nil) (setq lean-server-handler-tq (tq-create lean-server-process)))) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index a44abd6eed..adecb98a43 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -399,7 +399,7 @@ int main(int argc, char ** argv) { } if (server) { - lean::server(base_dir, num_threads, env, ios).run(); + lean::server(num_threads, env, ios).run(); return 0; } diff --git a/src/shell/server.cpp b/src/shell/server.cpp index e29e858fa8..d27789eae1 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -16,9 +16,8 @@ public: void report(message const &) override {} }; -server::server(optional const & base_dir, int num_threads, environment const & initial_env, io_state const & ios) : - m_base_dir(base_dir), m_num_threads(num_threads), - m_initial_env(initial_env), m_ios(ios) { +server::server(unsigned num_threads, environment const & initial_env, io_state const & ios) : + m_num_threads(num_threads), m_initial_env(initial_env), m_ios(ios) { m_ios.set_regular_channel(std::make_shared()); m_ios.set_diagnostic_channel(std::make_shared()); m_ios.set_message_channel(std::make_shared()); @@ -120,8 +119,9 @@ json server::handle_check(json const &) { std::istringstream in(m_content); bool use_exceptions = false; + optional base_dir; parser p(m_initial_env, m_ios, in, m_file_name.c_str(), - m_base_dir, use_exceptions, m_num_threads, + base_dir, use_exceptions, m_num_threads, new_snapshots.empty() ? nullptr : &new_snapshots.back(), &new_snapshots); // TODO(gabriel): definition caches? diff --git a/src/shell/server.h b/src/shell/server.h index 4cf14e8a54..c7ff5c0bb6 100644 --- a/src/shell/server.h +++ b/src/shell/server.h @@ -14,7 +14,6 @@ Author: Gabriel Ebner namespace lean { class server { - optional m_base_dir; unsigned m_num_threads; options m_opts; environment m_initial_env; @@ -35,7 +34,7 @@ class server { json handle_check(json const & req); public: - server(optional const & base_dir, int num_threads, environment const & intial_env, io_state const & ios); + server(unsigned num_threads, environment const & intial_env, io_state const & ios); ~server(); void run();