From 83824d2ab662391682fd838240e8d0498103be2e Mon Sep 17 00:00:00 2001 From: Konstantin Bulenkov Date: Tue, 31 May 2016 21:44:50 +0200 Subject: [PATCH] customize one pixel divider bg --- .../src/com/intellij/openapi/ui/OnePixelDivider.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/platform/platform-api/src/com/intellij/openapi/ui/OnePixelDivider.java b/platform/platform-api/src/com/intellij/openapi/ui/OnePixelDivider.java index d92d97b001b9..1312dabe6064 100644 --- a/platform/platform-api/src/com/intellij/openapi/ui/OnePixelDivider.java +++ b/platform/platform-api/src/com/intellij/openapi/ui/OnePixelDivider.java @@ -1,5 +1,5 @@ /* - * Copyright 2000-2015 JetBrains s.r.o. + * Copyright 2000-2016 JetBrains s.r.o. * * Licensed under the Apache License, Version 2.0 (the "License"); * you may not use this file except in compliance with the License. @@ -36,7 +36,10 @@ import java.awt.event.MouseEvent; * @author Konstantin Bulenkov */ public class OnePixelDivider extends Divider { - public static final Color BACKGROUND = new JBColor(Gray.xC5, Gray.x51); + public static final Color BACKGROUND = new JBColor(() -> { + final Color bg = UIManager.getColor("OnePixelDivider.background"); + return bg != null ? bg : new JBColor(Gray.xC5, Gray.x51); + }); private boolean myVertical; private Splittable mySplitter;