From 94e33c42f05f9571ab8b55b2f24c75849a33b01d Mon Sep 17 00:00:00 2001 From: "Mr.doob" Date: Sat, 14 Aug 2021 12:20:52 +0100 Subject: [PATCH] Improved editor buttons style and made them fadein/out. --- static/index.html | 29 +++++++++++------------------ 1 file changed, 11 insertions(+), 18 deletions(-) diff --git a/static/index.html b/static/index.html index 56d7088..3ba3066 100755 --- a/static/index.html +++ b/static/index.html @@ -7,31 +7,24 @@ @@ -166,6 +158,7 @@ void main( void ) { // toolbar = document.createElement( 'div' ); + toolbar.id = 'toolbar'; toolbar.style.position = 'absolute'; toolbar.style.top = '0px'; toolbar.style.padding = '25px'; @@ -453,7 +446,7 @@ void main( void ) { stopHideUITimer(); if (!isUIHidden && !isCodeVisible()) - hideUITimer = window.setTimeout(onHideUITimer, 1000 * 5 ); + hideUITimer = window.setTimeout(onHideUITimer, 1000 * 3 ); function onHideUITimer() { @@ -461,7 +454,7 @@ void main( void ) { if (!isUIHidden && !isCodeVisible()) { isUIHidden = true; - toolbar.style.display = 'none'; + toolbar.style.opacity = '0'; document.body.style.cursor = 'none'; } } @@ -481,7 +474,7 @@ void main( void ) { if (isUIHidden) { isUIHidden = false; - toolbar.style.display = ''; + toolbar.style.opacity = '1'; document.body.style.cursor = ''; } startHideUITimer();