Language client: improved support for lean

src/source_base.cpp

@@ -896,6 +896,7 @@ bool Source::BaseView::is_token_char(gunichar chr) {
   return (chr >= 'A' && chr <= 'Z') || (chr >= 'a' && chr <= 'z') || (chr >= '0' && chr <= '9') || chr == '_' || (!is_latex && chr == '$') || chr >= 128 ||
          (language_id == "css" && chr == '-') ||
          (language_id == "rust" && chr == '!') ||
+         (language_id == "lean" && (chr == '#' || chr == '\\')) ||
          (is_latex && chr == '\\');
 }
 
@@ -999,6 +1000,13 @@ void Source::BaseView::paste() {
     }
   }
 
+  if(language_id == "lean") {
+    Gtk::Clipboard::get()->set_text(text);
+    get_buffer()->paste_clipboard(Gtk::Clipboard::get());
+    scroll_to_cursor_delayed(false, false);
+    return;
+  }
+
   // Exception for when pasted text is only whitespaces
   bool only_whitespaces = true;
   for(auto &chr : text) {

src/tooltips.cpp

@@ -966,7 +966,8 @@ void Tooltip::insert_markdown(const std::string &input) {
       if(i < input.size() && (input[i] == '#' ||
                               starts_with(input, i, "```") || starts_with(input, i, "- ") ||
                               starts_with(input, i, "+ ") || starts_with(input, i, "* ") ||
-                              starts_with(input, i, "1. "))) {
+                              starts_with(input, i, "1. ") ||
+                              starts_with(input, i, "***") || starts_with(input, i, "___"))) { // test\n---\ntest does not work for horizontal lines since it conflicts with headers
         break;
       }
     }

tests/tooltips_test.cpp

@@ -81,6 +81,14 @@ int main() {
     auto tooltip = get_markdown_tooltip("test\n\n***\n\ntest");
     g_assert(tooltip->buffer->get_text() == "test\n\n---\n\ntest");
   }
+  {
+    auto tooltip = get_markdown_tooltip("test\n***\ntest");
+    g_assert(tooltip->buffer->get_text() == "test\n---\ntest");
+  }
+  {
+    auto tooltip = get_markdown_tooltip("test\n___\ntest");
+    g_assert(tooltip->buffer->get_text() == "test\n---\ntest");
+  }
   {
     auto tooltip = get_markdown_tooltip("test\n\n___\n\ntest");
     g_assert(tooltip->buffer->get_text() == "test\n\n---\n\ntest");