588 lines
21 KiB
Python
Executable file
588 lines
21 KiB
Python
Executable file
#!/usr/bin/python3.11
|
|
# -*- coding: utf-8 -*-
|
|
|
|
|
|
import asyncio
|
|
import contextlib
|
|
import enum
|
|
import itertools
|
|
import os
|
|
import re
|
|
import signal
|
|
import sys
|
|
|
|
import fill3.terminal as terminal
|
|
import termstr
|
|
|
|
|
|
__version__ = "v2024.03.10"
|
|
|
|
|
|
##########################
|
|
# Widgets
|
|
|
|
def appearance_is_valid(appearance):
|
|
return (all(isinstance(line, (str, termstr.TermStr)) and len(line) > 0 for line in appearance)
|
|
and len(set(len(line) for line in appearance)) < 2)
|
|
|
|
|
|
def appearance_resize(appearance, dimensions, pad_char=" "):
|
|
width, height = dimensions
|
|
result = [line[:width].ljust(width, pad_char) for line in appearance[:height]]
|
|
if len(result) < height:
|
|
result.extend([pad_char * width] * (height - len(result)))
|
|
return result
|
|
|
|
|
|
def appearance_dimensions(appearance):
|
|
try:
|
|
return len(appearance[0]), len(appearance)
|
|
except IndexError:
|
|
return 0, 0
|
|
|
|
|
|
def join_horizontal(appearances):
|
|
heights = set(len(appearance) for appearance in appearances)
|
|
assert len(heights) == 1, heights
|
|
return [termstr.join("", parts) for parts in zip(*appearances)]
|
|
|
|
|
|
def even_widths(column_widgets, width):
|
|
column_count = len(column_widgets)
|
|
widths = []
|
|
for index, column_widget in enumerate(column_widgets):
|
|
start_pos = round(float(width) / column_count * index)
|
|
end_pos = round(float(width) / column_count * (index+1))
|
|
widths.append(end_pos - start_pos)
|
|
return widths
|
|
|
|
|
|
def appearance_as_html(appearance):
|
|
lines = []
|
|
all_styles = set()
|
|
for line in appearance:
|
|
html, styles = termstr.TermStr(line).as_html()
|
|
all_styles.update(styles)
|
|
lines.append(html)
|
|
return ("\n".join(style.as_html() for style in all_styles) +
|
|
"\n<pre>" + "<br>".join(lines) + "</pre>")
|
|
|
|
|
|
class Row:
|
|
|
|
def __init__(self, widgets, widths_func=even_widths):
|
|
self.widgets = widgets
|
|
self.widths_func = widths_func
|
|
|
|
def appearance_for(self, dimensions):
|
|
width, height = dimensions
|
|
widths = self.widths_func(self.widgets, width)
|
|
assert sum(widths) == width, (sum(widths), width)
|
|
return join_horizontal([column_widget.appearance_for((item_width, height))
|
|
for column_widget, item_width in zip(self.widgets, widths)])
|
|
|
|
def appearance(self):
|
|
appearances = [column_widget.appearance() for column_widget in self.widgets]
|
|
dimensions = [appearance_dimensions(appearance) for appearance in appearances]
|
|
max_height = max(height for width, height in dimensions)
|
|
return join_horizontal([appearance_resize(appearance, (width, max_height))
|
|
for appearance, (width, height) in zip(appearances, dimensions)])
|
|
|
|
|
|
def even_partition(row_widgets, height):
|
|
row_count = len(row_widgets)
|
|
heights = []
|
|
for index, row_widget in enumerate(row_widgets):
|
|
start_pos = round(float(height) / row_count * index)
|
|
end_pos = round(float(height) / row_count * (index+1))
|
|
heights.append(end_pos - start_pos)
|
|
return heights
|
|
|
|
|
|
def join_vertical(appearances):
|
|
result = []
|
|
for appearance in appearances:
|
|
result.extend(appearance)
|
|
return result
|
|
|
|
|
|
class Column:
|
|
|
|
def __init__(self, widgets, partition_func=even_partition, background_char=" "):
|
|
self.widgets = widgets
|
|
self.partition_func = partition_func
|
|
self.background_char = background_char
|
|
|
|
def appearance_for(self, dimensions):
|
|
width, height = dimensions
|
|
if len(self.widgets) == 0: # FIX: Really allow zero widgets?
|
|
return [self.background_char * width] * height
|
|
heights = self.partition_func(self.widgets, height)
|
|
assert sum(heights) == height, (sum(heights), height)
|
|
return join_vertical([row_widget.appearance_for((width, item_height))
|
|
for row_widget, item_height in zip(self.widgets, heights)])
|
|
|
|
@staticmethod
|
|
def _appearance_list(widgets):
|
|
if widgets == []:
|
|
return []
|
|
appearances = [row_widget.appearance() for row_widget in widgets]
|
|
dimensions = [appearance_dimensions(appearance) for appearance in appearances]
|
|
max_width = max(width for width, height in dimensions)
|
|
padded_appearances = [appearance_resize(appearance, (max_width, height))
|
|
for appearance, (width, height) in zip(appearances, dimensions)]
|
|
result = []
|
|
for appearance in padded_appearances:
|
|
result.extend(appearance)
|
|
return result
|
|
|
|
def appearance_interval(self, interval):
|
|
start_y, end_y = interval
|
|
return self._appearance_list(self.widgets[start_y:end_y])
|
|
|
|
def appearance(self):
|
|
return self._appearance_list(self.widgets)
|
|
|
|
|
|
class Filler:
|
|
|
|
def __init__(self, widget):
|
|
self.widget = widget
|
|
|
|
def appearance_for(self, dimensions):
|
|
return appearance_resize(self.widget.appearance(), dimensions)
|
|
|
|
|
|
class ScrollBar:
|
|
|
|
_PARTIAL_CHARS = (["█", "▇", "▆", "▅", "▄", "▃", "▂", "▁"],
|
|
[" ", "▏", "▎", "▍", "▌", "▋", "▊", "▉"])
|
|
DEFAULT_BAR_COLOR = termstr.Color.grey_100
|
|
DEFAULT_BACKGROUND_COLOR = termstr.Color.grey_30
|
|
|
|
def __init__(self, is_horizontal, interval=(0, 0), bar_color=None, background_color=None):
|
|
self._is_horizontal = is_horizontal
|
|
self.interval = interval
|
|
bar_color = bar_color or ScrollBar.DEFAULT_BAR_COLOR
|
|
background_color = background_color or ScrollBar.DEFAULT_BACKGROUND_COLOR
|
|
self._bar_char = termstr.TermStr("█", fg_color=bar_color)
|
|
self._background_char = termstr.TermStr(" ", bg_color=background_color)
|
|
if self._is_horizontal:
|
|
bar_color, background_color = background_color, bar_color
|
|
self._partial_chars = [
|
|
(termstr.TermStr(char, fg_color=bar_color, bg_color=background_color),
|
|
termstr.TermStr(char, fg_color=background_color, bg_color=bar_color))
|
|
for char in self._PARTIAL_CHARS[self._is_horizontal]]
|
|
|
|
def appearance_for(self, dimensions):
|
|
width, height = dimensions
|
|
assert width == 1 or height == 1, (width, height)
|
|
length = width if self._is_horizontal else height
|
|
assert all(0 <= fraction <= 1 for fraction in self.interval), self.interval
|
|
(start_index, start_remainder), (end_index, end_remainder) = \
|
|
[divmod(fraction * length * 8, 8) for fraction in self.interval]
|
|
start_index, end_index = int(start_index), int(end_index)
|
|
start_remainder, end_remainder = int(start_remainder), int(end_remainder)
|
|
if start_index == end_index:
|
|
end_index, end_remainder = start_index + 1, start_remainder
|
|
elif end_index == start_index + 1:
|
|
end_remainder = max(start_remainder, end_remainder)
|
|
bar = (self._background_char * start_index + self._partial_chars[start_remainder][0] +
|
|
self._bar_char * (end_index - start_index - 1) +
|
|
self._partial_chars[end_remainder][1] +
|
|
self._background_char * (length - end_index - 1))[:length]
|
|
return [bar] if self._is_horizontal else [char for char in bar]
|
|
|
|
|
|
class Alignment(enum.Enum):
|
|
left = enum.auto()
|
|
right = enum.auto()
|
|
top = enum.auto()
|
|
bottom = enum.auto()
|
|
center = enum.auto()
|
|
|
|
|
|
class Portal:
|
|
|
|
def __init__(self, widget, position=(0, 0), background_char=" ",
|
|
is_scroll_limited=False, x_alignment=Alignment.left, y_alignment=Alignment.top):
|
|
self.widget = widget
|
|
self.position = position
|
|
self.background_char = background_char
|
|
self.is_scroll_limited = is_scroll_limited
|
|
self.x_alignment = x_alignment
|
|
self.y_alignment = y_alignment
|
|
self.last_dimensions = 0, 0
|
|
|
|
def _scroll_half_pages(self, dx, dy):
|
|
x, y = self.position
|
|
width, height = self.last_dimensions
|
|
self.position = (max(x + dx * (width // 2), 0), max(y + dy * (height // 2), 0))
|
|
|
|
def scroll_up(self):
|
|
self._scroll_half_pages(0, -1)
|
|
|
|
def scroll_down(self):
|
|
self._scroll_half_pages(0, 1)
|
|
|
|
def scroll_left(self):
|
|
self._scroll_half_pages(-1, 0)
|
|
|
|
def scroll_right(self):
|
|
self._scroll_half_pages(1, 0)
|
|
|
|
def limit_scroll(self, portal_dimensions, appearance_dimensions):
|
|
portal_width, portal_height = portal_dimensions
|
|
widget_width, widget_height = appearance_dimensions
|
|
x, y = self.position
|
|
if widget_width <= portal_width:
|
|
match self.x_alignment:
|
|
case Alignment.left:
|
|
x = 0
|
|
case Alignment.center:
|
|
x = (widget_width - portal_width) // 2
|
|
case Alignment.right:
|
|
x = widget_width - portal_width
|
|
case _:
|
|
raise NotImplementedError
|
|
elif x < 0:
|
|
x = 0
|
|
elif x > (widget_width - portal_width):
|
|
x = widget_width - portal_width
|
|
if widget_height <= portal_height:
|
|
match self.y_alignment:
|
|
case Alignment.top:
|
|
y = 0
|
|
case Alignment.center:
|
|
y = (widget_height - portal_height) // 2
|
|
case Alignment.bottom:
|
|
y = widget_height - portal_height
|
|
case _:
|
|
raise NotImplementedError
|
|
elif y < 0:
|
|
y = 0
|
|
elif y > (widget_height - portal_height):
|
|
y = widget_height - portal_height
|
|
self.position = x, y
|
|
|
|
def appearance_for(self, portal_dimensions):
|
|
width, height = portal_dimensions
|
|
try:
|
|
widget_dimensions = self.widget.appearance_dimensions()
|
|
if self.is_scroll_limited:
|
|
self.limit_scroll(portal_dimensions, widget_dimensions)
|
|
x, y = self.position
|
|
widget_appearance = self.widget.appearance_interval((max(y, 0), y + height))
|
|
except AttributeError:
|
|
widget_appearance = self.widget.appearance()
|
|
widget_dimensions = appearance_dimensions(self.widget.appearance())
|
|
if self.is_scroll_limited:
|
|
self.limit_scroll(portal_dimensions, widget_dimensions)
|
|
x, y = self.position
|
|
widget_appearance = widget_appearance[max(y, 0):y + height]
|
|
self.last_dimensions = portal_dimensions
|
|
top = [self.background_char * width] * -y if y < 0 else []
|
|
bottom = appearance_resize([row[max(x, 0):x + width] for row in widget_appearance],
|
|
(width + min(x, 0), height + min(y, 0)),
|
|
self.background_char)
|
|
if x < 0:
|
|
padding = self.background_char * -x
|
|
bottom = [padding + line for line in bottom]
|
|
return top + bottom
|
|
|
|
|
|
class View:
|
|
|
|
def __init__(self, portal, horizontal_scrollbar, vertical_scrollbar, hide_scrollbars=True,
|
|
is_left_scrollbar=False):
|
|
self.portal = portal
|
|
self.horizontal_scrollbar = horizontal_scrollbar
|
|
self.vertical_scrollbar = vertical_scrollbar
|
|
self.hide_scrollbars = hide_scrollbars
|
|
self.is_left_scrollbar = is_left_scrollbar
|
|
|
|
@classmethod
|
|
def from_widget(cls, widget):
|
|
return cls(Portal(widget), ScrollBar(is_horizontal=True), ScrollBar(is_horizontal=False))
|
|
|
|
@property
|
|
def position(self):
|
|
return self.portal.position
|
|
|
|
@position.setter
|
|
def position(self, position):
|
|
self.portal.position = position
|
|
|
|
@property
|
|
def widget(self):
|
|
return self.portal.widget
|
|
|
|
@widget.setter
|
|
def widget(self, widget):
|
|
self.portal.widget = widget
|
|
|
|
def appearance_for(self, dimensions):
|
|
width, height = dimensions
|
|
try:
|
|
full_width, full_height = self.portal.widget.appearance_dimensions()
|
|
except AttributeError:
|
|
full_appearance = self.portal.widget.appearance()
|
|
full_width, full_height = appearance_dimensions(full_appearance)
|
|
if full_width == 0 or full_height == 0:
|
|
return self.portal.appearance_for(dimensions)
|
|
x, y = self.portal.position
|
|
hide_scrollbar_vertical = self.hide_scrollbars and (full_height <= height or y < 0)
|
|
hide_scrollbar_horizontal = self.hide_scrollbars and (full_width <= width or x < 0)
|
|
if not hide_scrollbar_horizontal:
|
|
full_width = max(full_width, x + width)
|
|
self.horizontal_scrollbar.interval = (x / full_width, (x + width) / full_width)
|
|
height -= 1
|
|
if not hide_scrollbar_vertical:
|
|
full_height = max(full_height, y + height)
|
|
self.vertical_scrollbar.interval = (y / full_height, (y + height) / full_height)
|
|
width -= 1
|
|
portal_appearance = self.portal.appearance_for((width, height))
|
|
if hide_scrollbar_vertical:
|
|
result = portal_appearance
|
|
else:
|
|
scrollbar_v_appearance = self.vertical_scrollbar.appearance_for((1, height))
|
|
parts = ([scrollbar_v_appearance, portal_appearance] if self.is_left_scrollbar
|
|
else [portal_appearance, scrollbar_v_appearance])
|
|
result = join_horizontal(parts)
|
|
if not hide_scrollbar_horizontal:
|
|
scrollbar_h_appearance = self.horizontal_scrollbar.appearance_for((width, 1))
|
|
spacer = "" if hide_scrollbar_vertical else " "
|
|
result.append(spacer + scrollbar_h_appearance[0] if self.is_left_scrollbar
|
|
else scrollbar_h_appearance[0] + spacer)
|
|
return result
|
|
|
|
|
|
def str_to_appearance(text, pad_char=" "):
|
|
lines = text.splitlines()
|
|
if len(lines) == 0:
|
|
return []
|
|
max_width = max(len(line) for line in lines)
|
|
height = len(lines)
|
|
return appearance_resize(lines, (max_width, height), pad_char)
|
|
|
|
|
|
class Text:
|
|
|
|
def __init__(self, text, pad_char=" "):
|
|
self.text = str_to_appearance(text, pad_char)
|
|
|
|
def appearance(self):
|
|
return self.text
|
|
|
|
def appearance_for(self, dimensions):
|
|
return appearance_resize(self.appearance(), dimensions)
|
|
|
|
|
|
class Table:
|
|
|
|
def __init__(self, table, pad_char=" "):
|
|
self._widgets = table
|
|
self._pad_char = pad_char
|
|
|
|
def appearance(self):
|
|
if self._widgets == []:
|
|
return []
|
|
appearances = [[cell.appearance() for cell in row] for row in self._widgets]
|
|
row_heights = [0] * len(self._widgets)
|
|
column_widths = [0] * len(self._widgets[0])
|
|
for y, row in enumerate(appearances):
|
|
for x, appearance in enumerate(row):
|
|
width, height = appearance_dimensions(appearance)
|
|
row_heights[y] = max(row_heights[y], height)
|
|
column_widths[x] = max(column_widths[x], width)
|
|
return join_vertical([join_horizontal(
|
|
[appearance_resize(appearance, (column_widths[x], row_heights[y]),
|
|
pad_char=self._pad_char)
|
|
for x, appearance in enumerate(row)])
|
|
for y, row in enumerate(appearances)])
|
|
|
|
|
|
class Border:
|
|
|
|
THIN = ["─", "─", "│", "│", "┌", "└", "┘", "┐"]
|
|
THICK = ["━", "━", "┃", "┃", "┏", "┗", "┛", "┓"]
|
|
ROUNDED = ["─", "─", "│", "│", "╭", "╰", "╯", "╮"]
|
|
DOUBLE = ["═", "═", "║", "║", "╔", "╚", "╝", "╗"]
|
|
|
|
def __init__(self, widget, title=None, characters=THIN):
|
|
self.widget = widget
|
|
self.title = title
|
|
self.set_style(characters)
|
|
|
|
def set_style(self, characters):
|
|
(self.top, self.bottom, self.left, self.right, self.top_left,
|
|
self.bottom_left, self.bottom_right, self.top_right) = characters
|
|
|
|
def _add_border(self, body_content):
|
|
content_width, content_height = appearance_dimensions(body_content)
|
|
if self.title is None:
|
|
title_bar = self.top * content_width
|
|
else:
|
|
padded_title = " " + ("…" + self.title[-(content_width-3):]
|
|
if len(self.title) > content_width - 2
|
|
else self.title) + " "
|
|
try:
|
|
title_bar = padded_title.center(content_width, self.top)
|
|
except TypeError:
|
|
padded_title = termstr.TermStr(padded_title)
|
|
title_bar = padded_title.center(content_width, self.top)
|
|
result = [self.top_left + title_bar + self.top_right]
|
|
result.extend(self.left + line + self.right for line in body_content)
|
|
result.append(self.bottom_left + self.bottom * content_width + self.bottom_right)
|
|
return result
|
|
|
|
def appearance(self):
|
|
return self._add_border(self.widget.appearance())
|
|
|
|
def appearance_for(self, dimensions):
|
|
width, height = dimensions
|
|
return self._add_border(self.widget.appearance_for((width-2, height-2)))
|
|
|
|
|
|
class Placeholder:
|
|
|
|
def __init__(self, widget=None):
|
|
self.widget = widget
|
|
|
|
def appearance(self):
|
|
return self.widget.appearance()
|
|
|
|
def appearance_for(self, dimensions):
|
|
return self.widget.appearance_for(dimensions)
|
|
|
|
|
|
class Fixed:
|
|
|
|
def __init__(self, appearance):
|
|
self.appearance_ = appearance
|
|
self.dimensions = appearance_dimensions(appearance)
|
|
|
|
def appearance(self):
|
|
return self.appearance_
|
|
|
|
def appearance_dimensions(self):
|
|
return self.dimensions
|
|
|
|
|
|
##########################
|
|
# Infrastructure
|
|
|
|
_EXCEPTION = None
|
|
_LAST_APPEARANCE = []
|
|
|
|
|
|
def handle_exception(func):
|
|
def wrapper(*args):
|
|
try:
|
|
return func(*args)
|
|
except Exception as exc:
|
|
global _EXCEPTION
|
|
_EXCEPTION = exc
|
|
SHUTDOWN_EVENT.set()
|
|
return wrapper
|
|
|
|
|
|
@handle_exception
|
|
def draw_screen(widget):
|
|
global _LAST_APPEARANCE
|
|
appearance = widget.appearance_for(os.get_terminal_size())
|
|
print(terminal.move(0, 0), *appearance, sep="", end="", flush=True)
|
|
_LAST_APPEARANCE = appearance
|
|
|
|
|
|
@handle_exception
|
|
def patch_screen(widget):
|
|
global _LAST_APPEARANCE
|
|
appearance = widget.appearance_for(os.get_terminal_size())
|
|
zip_func = (itertools.zip_longest if len(appearance) > len(_LAST_APPEARANCE) else zip)
|
|
changed_lines = (str(terminal.move(0, row_index)) + line for row_index, (line, old_line)
|
|
in enumerate(zip_func(appearance, _LAST_APPEARANCE)) if line != old_line)
|
|
print(*changed_lines, sep="", end="", flush=True)
|
|
_LAST_APPEARANCE = appearance
|
|
|
|
|
|
async def update_screen(screen_widget):
|
|
while True:
|
|
patch_screen(screen_widget)
|
|
await asyncio.sleep(0.01) # Limit the update rate
|
|
await APPEARANCE_CHANGED_EVENT.wait()
|
|
APPEARANCE_CHANGED_EVENT.clear()
|
|
|
|
|
|
_INPUT_REGEX = re.compile("\x1b[^\x00-\x1f]+|[\x00-\x1f]|[^\x00-\x1f]+")
|
|
|
|
|
|
@handle_exception
|
|
def on_terminal_input(screen_widget):
|
|
for part in _INPUT_REGEX.findall(sys.stdin.read()):
|
|
if part.startswith(terminal.MOUSE):
|
|
screen_widget.on_mouse_input(part[3:])
|
|
else:
|
|
screen_widget.on_keyboard_input(part)
|
|
|
|
|
|
@contextlib.contextmanager
|
|
def signal_handler(loop, signal_, func):
|
|
loop.add_signal_handler(signal_, func)
|
|
try:
|
|
yield
|
|
finally:
|
|
loop.remove_signal_handler(signal_)
|
|
|
|
|
|
async def tui(title, screen_widget, input_handler=on_terminal_input):
|
|
global APPEARANCE_CHANGED_EVENT
|
|
global SHUTDOWN_EVENT
|
|
APPEARANCE_CHANGED_EVENT = asyncio.Event()
|
|
SHUTDOWN_EVENT = asyncio.Event()
|
|
loop = asyncio.get_running_loop()
|
|
with (signal_handler(loop, signal.SIGWINCH, lambda: draw_screen(screen_widget)),
|
|
signal_handler(loop, signal.SIGINT, SHUTDOWN_EVENT.set),
|
|
signal_handler(loop, signal.SIGTERM, SHUTDOWN_EVENT.set), terminal.title(title),
|
|
terminal.alternate_buffer(), terminal.raw(), terminal.mouse_tracking()):
|
|
update_task = asyncio.create_task(update_screen(screen_widget))
|
|
try:
|
|
loop.add_reader(sys.stdin, input_handler, screen_widget)
|
|
try:
|
|
await SHUTDOWN_EVENT.wait()
|
|
finally:
|
|
loop.remove_reader(sys.stdin)
|
|
finally:
|
|
update_task.cancel()
|
|
if _EXCEPTION is not None:
|
|
raise _EXCEPTION
|
|
|
|
|
|
##########################
|
|
# Example application
|
|
|
|
class _Screen:
|
|
|
|
def __init__(self):
|
|
self.content = Filler(Text("Hello World"))
|
|
|
|
def appearance_for(self, dimensions):
|
|
return self.content.appearance_for(dimensions)
|
|
|
|
def on_keyboard_input(self, term_code):
|
|
if term_code in ["q", terminal.ESC, terminal.CTRL_C]:
|
|
SHUTDOWN_EVENT.set()
|
|
elif term_code == "e":
|
|
raise AssertionError # Program should shutdown and show exception.
|
|
else:
|
|
self.content = Filler(Text(repr(term_code)))
|
|
APPEARANCE_CHANGED_EVENT.set()
|
|
|
|
def on_mouse_input(self, term_code):
|
|
mouse_code = terminal.decode_mouse_input(term_code)
|
|
self.content = Filler(Text(repr(term_code) + " " + repr(mouse_code)))
|
|
APPEARANCE_CHANGED_EVENT.set()
|
|
|
|
|
|
if __name__ == "__main__":
|
|
asyncio.run(tui("Hello World", _Screen()))
|