From 5444395f34cc4c33e6e09835ba98107b8b31d284 Mon Sep 17 00:00:00 2001
From: dankeboy36 <dankeboy36@gmail.com>
Date: Tue, 27 Sep 2022 22:32:10 +0200
Subject: [PATCH] Better tooltips.

fixes #1503

Signed-off-by: dankeboy36 <dankeboy36@gmail.com>
---
 arduino-ide-extension/src/browser/style/main.css | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/arduino-ide-extension/src/browser/style/main.css b/arduino-ide-extension/src/browser/style/main.css
index ede6c726..4ebda8c4 100644
--- a/arduino-ide-extension/src/browser/style/main.css
+++ b/arduino-ide-extension/src/browser/style/main.css
@@ -11,7 +11,7 @@
 #theia-main-content-panel div[id^="code-editor-opener"] {
     z-index: auto;
 }
-    
+
 .p-TabBar-toolbar .item.arduino-tool-item {
     margin-left: 0;
 }
@@ -97,8 +97,7 @@
     display: flex;
     justify-content: center;
     align-items: center;
-    background-color: var(--theia-titleBar-activeBackground);   
-
+    background-color: var(--theia-titleBar-activeBackground);
 }
 
 #arduino-toolbar-container {
@@ -253,3 +252,10 @@
     outline: 1px solid var(--theia-contrastBorder);
     outline-offset: -1px;
 }
+
+.monaco-hover p {
+    margin: 8px 0;
+}
+.monaco-hover .monaco-tokenized-source {
+    margin-top: 8px;
+}