From c105802b2d1504f757fec27b401fbee8964263df Mon Sep 17 00:00:00 2001
From: Max Brunsfeld <maxbrunsfeld@gmail.com>
Date: Tue, 22 Mar 2022 11:43:30 -0700
Subject: [PATCH] Allow customizing the pane's following border width in the
 theme

---
 crates/theme/src/theme.rs           | 1 +
 crates/workspace/src/pane_group.rs  | 2 +-
 crates/zed/assets/themes/_base.toml | 3 ++-
 3 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/crates/theme/src/theme.rs b/crates/theme/src/theme.rs
index 61d0bf3f67e3799b4a3c8364b9eea9815f210bb2..d10c282e3526056acd397794b184491bd17a43b6 100644
--- a/crates/theme/src/theme.rs
+++ b/crates/theme/src/theme.rs
@@ -36,6 +36,7 @@ pub struct Workspace {
     pub active_tab: Tab,
     pub pane_divider: Border,
     pub leader_border_opacity: f32,
+    pub leader_border_width: f32,
     pub left_sidebar: Sidebar,
     pub right_sidebar: Sidebar,
     pub status_bar: StatusBar,
diff --git a/crates/workspace/src/pane_group.rs b/crates/workspace/src/pane_group.rs
index c3f4d2d3a6e8a5086a5c78d183a47fbbfe940551..d34613df4ac19633a9659d59b33580f38d4825ad 100644
--- a/crates/workspace/src/pane_group.rs
+++ b/crates/workspace/src/pane_group.rs
@@ -111,7 +111,7 @@ impl Member {
                         .editor
                         .replica_selection_style(leader.replica_id)
                         .cursor;
-                    border = Border::all(1.0, leader_color);
+                    border = Border::all(theme.workspace.leader_border_width, leader_color);
                     border
                         .color
                         .fade_out(1. - theme.workspace.leader_border_opacity);
diff --git a/crates/zed/assets/themes/_base.toml b/crates/zed/assets/themes/_base.toml
index d0368d69338911a66669b9f9f88c0c107dc95ac8..7bd0c59045fa6f99dee87429d5eef38b327f0137 100644
--- a/crates/zed/assets/themes/_base.toml
+++ b/crates/zed/assets/themes/_base.toml
@@ -4,7 +4,8 @@ base = { family = "Zed Sans", size = 14 }
 [workspace]
 background = "$surface.0"
 pane_divider = { width = 1, color = "$border.0" }
-leader_border_opacity = 0.6
+leader_border_opacity = 0.7
+leader_border_width = 2.0
 
 [workspace.titlebar]
 height = 32