gregor/jprototerm
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

recover tab

Browse Source
This commit is contained in:
Gregor Lohaus
2026-05-31 16:23:36 +02:00
parent 9c98d87783
commit 0958c93b4f
1 changed files with 191 additions and 227 deletions
Download Patch File Download Diff File Expand all files Collapse all files

418
src/main/java/com/gregor/jprototerm/Tab.java
View File

@@ -1,262 +1,276 @@
package com.gregor.jprototerm; package com.gregor.jprototerm;
import javafx.scene.shape.Rectangle;
import javafx.scene.shape.Shape;
import java.util.ArrayList; import java.util.ArrayList;
import java.util.Comparator; import java.util.Comparator;
import java.util.List; import java.util.List;
import java.util.stream.Stream;
/** /**
* One tab: an isolated stack of panes (tiled + floating) with its own active pane and * One tab: a row of tiled panes with a group of floating panes shown over them. Floating panes
* stashed-floating state. {@link TerminalWorkspace} owns the list of tabs and renders only * are shown/hidden as a group ({@code floatingVisible}), and there is always at least one tiled
* the current one. Mutating methods return whether they actually changed anything so the * pane — a floating pane is promoted if the last tiled one closes — so the layout always has a
* workspace can bump its render version conditionally. * base. The {@link Compositor} owns the tabs and renders only the current one; mutating methods
* return whether they actually changed anything so it can bump its layout version.
*/ */
final class Tab implements AutoCloseable { final class Tab implements AutoCloseable {
private final AppConfig config; private final AppConfig config;
private final List<TerminalPane> panes = new ArrayList<>(); private final TerminalMetrics metrics;
private int activeIndex; private final List<TerminalPane> tiled = new ArrayList<>();
private int hiddenFloatingFocusIndex = -1; private final List<TerminalPane> floating = new ArrayList<>();
private boolean floatingVisible;
private TerminalPane active;
// The floating pane to re-focus when the group is shown again, and to prefer when promoting
// after the last tiled pane closes.
private TerminalPane lastFocusedFloating; private TerminalPane lastFocusedFloating;
// Last laid-out size, so a newly opened pane can be created at roughly its eventual rect
// (and thus grid). Seeded from the configured window size for the first pane, which is
// opened before any layout pass runs.
private double lastWidth;
private double lastHeight;
private double lastTopInset;
// Bumped whenever one of this tab's panes changes content; the compositor reads the current
// tab's value each frame as an O(1) "anything to repaint?" check.
private long contentVersion;
Tab(AppConfig config) { Tab(AppConfig config, TerminalMetrics metrics) {
this.config = config; this.config = config;
panes.add(openPane(false)); this.metrics = metrics;
this.lastWidth = config.windowWidth();
this.lastHeight = config.windowHeight();
TerminalPane first = openPane(false);
tiled.add(first);
active = first;
} }
TerminalPane activePane() { TerminalPane activePane() {
return panes.get(activeIndex); return active;
} }
boolean isEmpty() { boolean isEmpty() {
return panes.isEmpty(); return tiled.isEmpty() && floating.isEmpty();
} }
long contentVersion() {
return contentVersion;
}
/**
* Panes to composite, bottom-to-top: tiled first, then (when shown) the floating group with
* the active floating pane on top.
*/
List<TerminalPane> panes() { List<TerminalPane> panes() {
if (panes.isEmpty()) { if (!floatingVisible || floating.isEmpty()) {
return List.of(); return List.copyOf(tiled);
} }
List<TerminalPane> visible = panes.stream().filter(TerminalPane::visible).toList(); List<TerminalPane> ordered = new ArrayList<>(tiled.size() + floating.size());
if (visible.isEmpty()) { ordered.addAll(tiled);
return List.of(); for (TerminalPane pane : floating) {
} if (pane != active) {
// Draw order = z-order: all tiled panes first (they never overlap), then floating
// panes on top, with the active floating pane last (topmost). This holds regardless
// of creation order, so a tiled pane created after a floating one still sits behind.
TerminalPane active = activePane();
List<TerminalPane> ordered = new ArrayList<>(visible.size());
for (TerminalPane pane : visible) {
if (!pane.floating()) {
ordered.add(pane); ordered.add(pane);
} }
} }
for (TerminalPane pane : visible) { if (floating.contains(active)) {
if (pane.floating() && pane != active) { ordered.add(active); // active floating pane on top
ordered.add(pane);
}
}
if (active.visible() && active.floating()) {
ordered.add(active);
} }
return List.copyOf(ordered); return List.copyOf(ordered);
} }
boolean isActive(TerminalPane pane) { boolean isActive(TerminalPane pane) {
return !panes.isEmpty() && activePane() == pane; return pane != null && pane == active;
} }
boolean focus(TerminalPane pane) { boolean focus(TerminalPane pane) {
int index = panes.indexOf(pane); if (pane == active || !isFocusable(pane)) {
if (index >= 0 && pane.visible() && activeIndex != index) { return false;
setActive(index);
return true;
} }
return false; setActive(pane);
return true;
} }
void layout(double width, double height, double topInset) { void layout(double width, double height, double topInset) {
this.lastWidth = width;
this.lastHeight = height;
this.lastTopInset = topInset;
double availHeight = height - topInset; double availHeight = height - topInset;
List<TerminalPane> tiled = panes.stream()
.filter(TerminalPane::visible) double tileWidth = width / Math.max(1, tiled.size());
.filter(pane -> !pane.floating())
.toList();
int tileCount = Math.max(1, tiled.size());
double tileWidth = width / tileCount;
for (int i = 0; i < tiled.size(); i++) { for (int i = 0; i < tiled.size(); i++) {
tiled.get(i).bounds(i * tileWidth, topInset, tileWidth, availHeight); tiled.get(i).bounds(i * tileWidth, topInset, tileWidth, availHeight);
} }
List<TerminalPane> floating = panes.stream() double floatingWidth = Math.max(420, width * 0.58);
.filter(TerminalPane::visible) double floatingHeight = Math.max(260, availHeight * 0.58);
.filter(TerminalPane::floating)
.toList();
for (int i = 0; i < floating.size(); i++) { for (int i = 0; i < floating.size(); i++) {
TerminalPane pane = floating.get(i);
double floatingWidth = Math.max(420, width * 0.58);
double floatingHeight = Math.max(260, availHeight * 0.58);
double offset = i * 28.0; double offset = i * 28.0;
pane.bounds( floating.get(i).bounds(
Math.min(width - floatingWidth - 12.0, ((width - floatingWidth) / 2.0) + offset), Math.min(width - floatingWidth - 12.0, ((width - floatingWidth) / 2.0) + offset),
Math.min(height - floatingHeight - 12.0, topInset + ((availHeight - floatingHeight) / 2.0) + offset), Math.min(height - floatingHeight - 12.0, topInset + ((availHeight - floatingHeight) / 2.0) + offset),
floatingWidth, floatingWidth,
floatingHeight floatingHeight);
); }
assignClips();
}
// Give each pane its clip region for the next paints, so repainting a pane on a content
// frame can never bleed over one stacked on top of it. Each pane is clipped to its rect
// minus the union of the panes above it: floating panes are clipped by the floating panes
// higher in the stack, and tiled panes by the whole floating group. When nothing floats,
// every pane clips to its plain bounds.
private void assignClips() {
if (!floatingVisible || floating.isEmpty()) {
tiled.forEach(pane -> pane.setClip(null));
floating.forEach(pane -> pane.setClip(null));
return;
}
// Floating panes bottom-to-top, matching panes(): insertion order, active pane on top.
List<TerminalPane> order = new ArrayList<>(floating.size());
for (TerminalPane pane : floating) {
if (pane != active) {
order.add(pane);
}
}
if (floating.contains(active)) {
order.add(active);
}
// Walk top-to-bottom, accumulating the union of the panes above each one.
Shape above = null;
for (int i = order.size() - 1; i >= 0; i--) {
Rectangle rect = rectOf(order.get(i));
order.get(i).setClip(above == null ? null : Shape.subtract(rect, above));
above = (above == null) ? rect : Shape.union(above, rect);
}
// `above` is now the union of every floating pane; tiled panes sit under all of them.
for (TerminalPane pane : tiled) {
pane.setClip(Shape.subtract(rectOf(pane), above));
} }
} }
// Match the renderer's pixel snapping (round the origin, keep width/height) so the clip
// lines up exactly with where the floating panes are drawn.
private static Rectangle rectOf(TerminalPane pane) {
return new Rectangle(Math.round(pane.x()), Math.round(pane.y()), pane.width(), pane.height());
}
boolean navigate(Direction direction) { boolean navigate(Direction direction) {
TerminalPane current = activePane(); if (floating.contains(active) && navigateFloatingStack(direction)) {
if (current.floating() && navigateFloatingStack(direction)) {
return true; return true;
} }
TerminalPane target = focusable()
TerminalPane target = panes.stream() .filter(pane -> pane != active)
.filter(TerminalPane::visible) .filter(pane -> directionFilter(direction, active, pane))
.filter(pane -> pane != current) .min(Comparator.comparingDouble(pane -> distance(active, pane)))
.filter(pane -> directionFilter(direction, current, pane))
.min(Comparator.comparingDouble(pane -> distance(current, pane)))
.orElse(null); .orElse(null);
if (target != null) { if (target != null) {
setActive(panes.indexOf(target)); setActive(target);
return true; return true;
} }
return false; return false;
} }
void toggleFloating() { void toggleFloating() {
List<TerminalPane> floating = panes.stream()
.filter(TerminalPane::floating)
.toList();
if (floating.isEmpty()) { if (floating.isEmpty()) {
createFloatingPane(); createFloatingPane();
return; return;
} }
if (floatingVisible) {
boolean anyVisible = floating.stream().anyMatch(TerminalPane::visible); floatingVisible = false;
if (anyVisible) { if (floating.contains(active)) {
TerminalPane active = activePane(); setActive(tiled.get(0));
hiddenFloatingFocusIndex = active.floating() ? activeIndex : firstVisibleFloatingIndex(); }
floating.forEach(pane -> pane.setVisible(false));
setActive(firstVisibleNonFloatingIndex());
} else { } else {
floating.forEach(pane -> pane.setVisible(true)); floatingVisible = true;
setActive(visibleIndexOrFallback(hiddenFloatingFocusIndex, panes.indexOf(floating.get(floating.size() - 1)))); setActive(floating.contains(lastFocusedFloating) ? lastFocusedFloating : floating.get(floating.size() - 1));
hiddenFloatingFocusIndex = -1;
} }
} }
/** /** Adds a floating pane while the floating group is shown, otherwise a tiled pane. */
* "New pane": adds a floating pane while floating panes are shown, otherwise adds a
* tiled pane (the tiled row is redistributed equally by the layout).
*/
void createPane() { void createPane() {
if (anyFloatingVisible()) { if (floatingVisible) {
createFloatingPane(); createFloatingPane();
} else { } else {
TerminalPane pane = openPane(false); TerminalPane pane = openPane(false);
panes.add(pane); tiled.add(pane);
setActive(panes.size() - 1); setActive(pane);
} }
} }
void nextFloatingPane() { void nextFloatingPane() {
TerminalPane next = nextFloatingAfter(activeIndex); if (floating.isEmpty()) {
next.setVisible(true); createFloatingPane();
setActive(panes.indexOf(next)); return;
}
floatingVisible = true;
int current = floating.indexOf(active); // -1 when the active pane is tiled
setActive(floating.get((current + 1 + floating.size()) % floating.size()));
} }
void closeActivePane() { void closeActivePane() {
TerminalPane active = activePane(); TerminalPane closing = active;
int removed = activeIndex; boolean wasFloating = floating.remove(closing);
// When closing a floating pane, focus the next visible floating pane if there is one if (!wasFloating) {
// (don't jump to a tiled pane); otherwise fall back to the nearest visible pane. tiled.remove(closing);
int target = active.floating() ? nearestVisibleFloatingIndex(removed) : -1;
if (target < 0) {
target = previousVisibleIndex(removed);
} }
panes.remove(removed); if (closing == lastFocusedFloating) {
if (active == lastFocusedFloating) {
lastFocusedFloating = null; lastFocusedFloating = null;
} }
active.close(); closing.close();
if (panes.isEmpty()) {
activeIndex = 0; if (tiled.isEmpty() && floating.isEmpty()) {
active = null; // tab is now empty; the compositor drops it
return; return;
} }
activeIndex = adjustIndexAfterRemoval(target, removed);
hiddenFloatingFocusIndex = adjustHiddenFocusAfterRemoval(hiddenFloatingFocusIndex, removed);
// If the last tiled (main) pane was closed, promote a floating pane to be the new // Always keep a tiled base: if the last tiled pane just closed, promote a floating one
// main pane so the layout has a base and rendering continues normally. Prefer the // (preferring the last focused).
// most recently focused floating pane. if (tiled.isEmpty()) {
if (panes.stream().noneMatch(pane -> !pane.floating())) { TerminalPane promote = floating.contains(lastFocusedFloating) ? lastFocusedFloating : floating.get(0);
TerminalPane promote = (lastFocusedFloating != null && panes.contains(lastFocusedFloating)) var promoteIndex = floating.indexOf(promote);
? lastFocusedFloating var nextFocussed = promoteIndex == 0 ? 0 : promoteIndex - 1;
: panes.get(activeIndex); floating.remove(promote);
promote.setFloating(false); tiled.add(promote);
promote.setVisible(true); if (promote == lastFocusedFloating) {
activeIndex = panes.indexOf(promote); lastFocusedFloating = null;
lastFocusedFloating = null; if (!floating.isEmpty()) {
lastFocusedFloating = floating.isEmpty() ? null : floating.get(nextFocussed);
}
}
}
if (floating.isEmpty()) {
floatingVisible = false;
} }
// If only hidden panes remained, reveal the one we're focusing so the screen isn't setActive(wasFloating && floatingVisible ? floating.get(floating.size() - 1) : tiled.get(0));
// blank.
if (!panes.get(activeIndex).visible()) {
panes.get(activeIndex).setVisible(true);
}
} }
private void setActive(int index) { private void setActive(TerminalPane pane) {
activeIndex = index; active = pane;
if (index >= 0 && index < panes.size() && panes.get(index).floating()) { if (floating.contains(pane)) {
lastFocusedFloating = panes.get(index); lastFocusedFloating = pane;
} }
} }
private void createFloatingPane() { private void createFloatingPane() {
TerminalPane pane = openPane(true); TerminalPane pane = openPane(true);
panes.add(pane); floating.add(pane);
setActive(panes.size() - 1); floatingVisible = true;
} setActive(pane);
private boolean anyFloatingVisible() {
return panes.stream().anyMatch(pane -> pane.floating() && pane.visible());
}
private TerminalPane nextFloatingAfter(int index) {
for (int i = index + 1; i < panes.size(); i++) {
TerminalPane pane = panes.get(i);
if (pane.floating()) {
return pane;
}
}
for (int i = 0; i <= index && i < panes.size(); i++) {
TerminalPane pane = panes.get(i);
if (pane.floating()) {
return pane;
}
}
return createAndReturnFloatingPane();
}
private TerminalPane createAndReturnFloatingPane() {
TerminalPane pane = openPane(true);
panes.add(pane);
return pane;
} }
private boolean navigateFloatingStack(Direction direction) { private boolean navigateFloatingStack(Direction direction) {
List<TerminalPane> floating = panes.stream()
.filter(TerminalPane::visible)
.filter(TerminalPane::floating)
.toList();
if (floating.size() < 2) { if (floating.size() < 2) {
return false; return false;
} }
int current = floating.indexOf(active);
int current = floating.indexOf(activePane());
if (current < 0) { if (current < 0) {
return false; return false;
} }
int next = switch (direction) { int next = switch (direction) {
case LEFT, UP -> current - 1; case LEFT, UP -> current - 1;
case DOWN, RIGHT -> current + 1; case DOWN, RIGHT -> current + 1;
@@ -264,85 +278,35 @@ final class Tab implements AutoCloseable {
if (next < 0 || next >= floating.size()) { if (next < 0 || next >= floating.size()) {
return false; return false;
} }
setActive(floating.get(next));
setActive(panes.indexOf(floating.get(next)));
return true; return true;
} }
private int firstVisibleFloatingIndex() { private boolean isFocusable(TerminalPane pane) {
for (int i = 0; i < panes.size(); i++) { return tiled.contains(pane) || (floatingVisible && floating.contains(pane));
TerminalPane pane = panes.get(i);
if (pane.visible() && pane.floating()) {
return i;
}
}
return -1;
} }
private int firstVisibleNonFloatingIndex() { private Stream<TerminalPane> focusable() {
for (int i = 0; i < panes.size(); i++) { return floatingVisible ? Stream.concat(tiled.stream(), floating.stream()) : tiled.stream();
TerminalPane pane = panes.get(i);
if (pane.visible() && !pane.floating()) {
return i;
}
}
return 0;
} }
private int nearestVisibleFloatingIndex(int index) { private void markContentChanged() {
for (int i = index + 1; i < panes.size(); i++) { contentVersion++;
if (panes.get(i).visible() && panes.get(i).floating()) {
return i;
}
}
for (int i = index - 1; i >= 0; i--) {
if (panes.get(i).visible() && panes.get(i).floating()) {
return i;
}
}
return -1;
} }
private int previousVisibleIndex(int index) { private TerminalPane openPane(boolean asFloating) {
for (int i = index - 1; i >= 0; i--) { double availHeight = lastHeight - lastTopInset;
if (panes.get(i).visible()) { double widthPx;
return i; double heightPx;
} if (asFloating) {
widthPx = Math.max(420, lastWidth * 0.58);
heightPx = Math.max(260, availHeight * 0.58);
} else {
// A new tiled pane joins the row, so each gets 1/(n+1) of the width.
widthPx = lastWidth / (tiled.size() + 1);
heightPx = availHeight;
} }
for (int i = index + 1; i < panes.size(); i++) { return TerminalPane.create(config, metrics, this::markContentChanged, widthPx, heightPx);
if (panes.get(i).visible()) {
return i;
}
}
return firstVisibleNonFloatingIndex();
}
private int visibleIndexOrFallback(int index, int fallback) {
if (index >= 0 && index < panes.size() && panes.get(index).visible()) {
return index;
}
return fallback;
}
private static int adjustIndexAfterRemoval(int index, int removedIndex) {
if (index < 0) {
return 0;
}
return index > removedIndex ? index - 1 : index;
}
private static int adjustHiddenFocusAfterRemoval(int index, int removedIndex) {
if (index < 0 || index == removedIndex) {
return -1;
}
return index > removedIndex ? index - 1 : index;
}
private TerminalPane openPane(boolean floating) {
TerminalPane pane = TerminalPane.create(config.columns(), config.rows(), config.maxScrollback());
pane.setFloating(floating);
pane.attach(ShellSession.start(config.shell(), config.envOverride(), pane, config.columns(), config.rows()));
return pane;
} }
private static boolean directionFilter(Direction direction, TerminalPane current, TerminalPane candidate) { private static boolean directionFilter(Direction direction, TerminalPane current, TerminalPane candidate) {
@@ -367,9 +331,9 @@ final class Tab implements AutoCloseable {
@Override @Override
public void close() { public void close() {
for (TerminalPane pane : panes) { tiled.forEach(TerminalPane::close);
pane.close(); floating.forEach(TerminalPane::close);
} tiled.clear();
panes.clear(); floating.clear();
} }
} }