From 711150f4ac08a7f4bfc7f0e98ed532148346f635 Mon Sep 17 00:00:00 2001 From: Maxime Coste Date: Thu, 28 Jun 2018 22:19:02 +1000 Subject: [PATCH] Allow removing region from regions highlighter --- src/highlighters.cc | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/highlighters.cc b/src/highlighters.cc index 5e6a2045..c21fa23d 100644 --- a/src/highlighters.cc +++ b/src/highlighters.cc @@ -1814,6 +1814,15 @@ public: ++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 { auto sep_it = find(path, '/');