thevar1able/ClickHouse
1
0
Fork 0
mirror of https://github.com/ClickHouse/ClickHouse.git synced 2024-09-20 00:30:49 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #27513 from ClickHouse/web-ui-better-block-characters

Browse Source 
Better block drawing characters in Web UI
This commit is contained in:
Maksim Kita 2021-08-10 11:48:42 +03:00 committed by GitHub
commit 9fa7f3ab5e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 11 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
programs/server/play.html
View File

@ -68,7 +68,7 @@
html, body
{
/* Personal choice. */
font-family: Sans-Serif;
font-family: Liberation Sans, DejaVu Sans, sans-serif, Noto Color Emoji, Apple Color Emoji, Segoe UI Emoji;
background: var(--background-color);
color: var(--text-color);
}
@ -96,11 +96,16 @@
.monospace
{
/* Prefer fonts that have full hinting info. This is important for non-retina displays.
Also I personally dislike "Ubuntu" font due to the similarity of 'r' and 'г' (it looks very ignorant).
*/
Also I personally dislike "Ubuntu" font due to the similarity of 'r' and 'г' (it looks very ignorant). */
font-family: Liberation Mono, DejaVu Sans Mono, MonoLisa, Consolas, Monospace;
}
.monospace-table
{
/* Liberation is worse than DejaVu for block drawing characters. */
font-family: DejaVu Sans Mono, Liberation Mono, MonoLisa, Consolas, Monospace;
}
.shadow
{
box-shadow: 0 0 1rem var(--shadow-color);
@ -325,8 +330,8 @@
<span id="toggle-dark">🌑</span><span id="toggle-light">🌞</span>
</div>
<div id="data_div">
<table class="monospace shadow" id="data-table"></table>
<pre class="monospace shadow" id="data-unparsed"></pre>
<table class="monospace-table shadow" id="data-table"></table>
<pre class="monospace-table shadow" id="data-unparsed"></pre>
</div>
<svg id="graph" fill="none"></svg>
<p id="error" class="monospace shadow">
@ -367,7 +372,7 @@
const server_address = document.getElementById('url').value;
const url = server_address +
(server_address.indexOf('?') >= 0 ? '&' : '?') +
(server_address.indexOf('?') >= 0 ? '&' : '?') +
/// Ask server to allow cross-domain requests.
'add_http_cors_header=1' +
'&user=' + encodeURIComponent(user) +