From 414859d309df7282fbb044c5303f8ce7a32461c8 Mon Sep 17 00:00:00 2001 From: Přemysl Eric Janouch
Date: Wed, 21 Sep 2022 07:32:18 +0200
Subject: xP: improve paging
---
xP/public/xP.css | 23 +++++++++++++++++++++++
xP/public/xP.js | 37 +++++++++++++++++++------------------
2 files changed, 42 insertions(+), 18 deletions(-)
diff --git a/xP/public/xP.css b/xP/public/xP.css
index 041eb63..5c02d7e 100644
--- a/xP/public/xP.css
+++ b/xP/public/xP.css
@@ -53,8 +53,31 @@ body {
bottom: -1px;
background: #ccc;
}
+
+.toolbar {
+ display: flex;
+ align-items: baseline;
+ gap: .3em;
+}
button {
font: inherit;
+ background: transparent;
+ border: 1px solid transparent;
+}
+button:focus {
+ border: 1px dashed #000;
+}
+button:hover {
+ border-left: 1px solid #fff;
+ border-top: 1px solid #fff;
+ border-right: 1px solid #888;
+ border-bottom: 1px solid #888;
+}
+button:hover:active {
+ border-left: 1px solid #888;
+ border-top: 1px solid #888;
+ border-right: 1px solid #fff;
+ border-bottom: 1px solid #fff;
}
.middle {
diff --git a/xP/public/xP.js b/xP/public/xP.js
index cbc37d7..8820251 100644
--- a/xP/public/xP.js
+++ b/xP/public/xP.js
@@ -199,6 +199,7 @@ function bufferToggleUnimportant(name) {
}
function bufferToggleLog() {
+ // TODO: Try to restore the previous scroll offset.
if (bufferLog) {
setTimeout(() =>
document.getElementById('input')?.focus())
@@ -347,6 +348,7 @@ rpcEventHandlers.set(Relay.Event.BufferLine, e => {
let visible = document.visibilityState !== 'hidden' &&
bufferLog === undefined &&
+ bufferAutoscroll &&
(e.bufferName == bufferCurrent || e.leakToActive)
b.lines.push({...line})
if (!(visible || e.leakToActive) ||
@@ -427,21 +429,6 @@ let linkRE = [
/[^\[\](){}<>"'\s,.:]/,
].map(r => r.source).join('')
-let Toolbar = {
- toggleAutoscroll: () => {
- bufferAutoscroll = !bufferAutoscroll
- },
-
- view: vnode => {
- return m('.toolbar', {}, [
- m('button', {onclick: Toolbar.toggleAutoscroll},
- bufferAutoscroll ? 'Scroll lock' : 'Scroll unlock'),
- m('button', {onclick: event => bufferToggleLog()},
- bufferLog === undefined ? 'Show log' : 'Hide log'),
- ])
- },
-}
-
let BufferList = {
view: vnode => {
let highlighted = false
@@ -624,7 +611,11 @@ let Buffer = {
let dateMark = new Date().toLocaleDateString()
if (dateMark !== lastDateMark && lastDateMark !== undefined)
lines.push(m('.date', {}, dateMark))
- return m('.buffer', {}, lines)
+ return m('.buffer', {onscroll: event => {
+ const dom = event.target
+ bufferAutoscroll =
+ dom.scrollTop + dom.clientHeight + 0.5 >= dom.scrollHeight
+ }}, lines)
},
}
@@ -678,6 +669,16 @@ let BufferContainer = {
},
}
+let Toolbar = {
+ view: vnode => {
+ return m('.toolbar', {}, [
+ bufferLog === undefined && !bufferAutoscroll ? '⇩' : undefined,
+ m('button', {onclick: event => bufferToggleLog()},
+ bufferLog === undefined ? 'Log' : 'Hide log'),
+ ])
+ },
+}
+
let Status = {
view: vnode => {
let b = buffers.get(bufferCurrent)
@@ -687,7 +688,7 @@ let Status = {
let status = `${bufferCurrent}`
if (b.hideUnimportant)
status += `