Allow removing region from regions highlighter

This commit is contained in:
Maxime Coste 2018-06-28 22:19:02 +10:00
parent f61bcef469
commit 711150f4ac

View File

@ -1814,6 +1814,15 @@ public:
++m_regions_timestamp; ++m_regions_timestamp;
} }
void remove_child(StringView id)
{
if (id == m_default_region)
m_default_region = String{};
m_regions.remove(id);
++m_regions_timestamp;
}
Completions complete_child(StringView path, ByteCount cursor_pos, bool group) const override Completions complete_child(StringView path, ByteCount cursor_pos, bool group) const override
{ {
auto sep_it = find(path, '/'); auto sep_it = find(path, '/');