From 6b023d3b258643af9fa6d7e4c472ee0d7947b14a Mon Sep 17 00:00:00 2001 From: eidheim Date: Thu, 23 Oct 2025 08:46:59 +0200 Subject: [PATCH] Language client: improved support for lean --- src/source_base.cpp | 8 ++++++++ src/tooltips.cpp | 3 ++- tests/tooltips_test.cpp | 8 ++++++++ 3 files changed, 18 insertions(+), 1 deletion(-) diff --git a/src/source_base.cpp b/src/source_base.cpp index e78fa76..30766b1 100644 --- a/src/source_base.cpp +++ b/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) { diff --git a/src/tooltips.cpp b/src/tooltips.cpp index 3c4cdd1..bb54c93 100644 --- a/src/tooltips.cpp +++ b/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; } } diff --git a/tests/tooltips_test.cpp b/tests/tooltips_test.cpp index cab3618..2077f5b 100644 --- a/tests/tooltips_test.cpp +++ b/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");