From 403234f29eb9861f73ebfa028954cccd83d4b683 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 1 Aug 2017 18:42:31 +0100
Subject: [PATCH] fix(frontends/lean/interactive): fix empty prefix in
 autocompletion

---
 src/frontends/lean/interactive.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp
index acdcf9ace2..991af0d116 100644
--- a/src/frontends/lean/interactive.cpp
+++ b/src/frontends/lean/interactive.cpp
@@ -60,7 +60,8 @@ void report_completions(environment const & env, options const & opts, pos_info
                         search_path const & path, char const * mod_path, break_at_pos_exception const & e, json & j) {
     g_context = e.m_token_info.m_context;
     unsigned offset = pos.second - e.m_token_info.m_pos.second;
-    std::string prefix = e.m_token_info.m_token.to_string();
+    // TODO(gabriel): this is broken with french quotes
+    std::string prefix = e.m_token_info.m_token == name("") ? "" : e.m_token_info.m_token.to_string();
     if (auto stop = utf8_char_pos(prefix.c_str(), offset))
         prefix = prefix.substr(0, *stop);
     switch (e.m_token_info.m_context) {