webserver: Add a title header to result pages.

This commit is contained in:
Andrew Hamilton 2021-11-21 00:33:52 +10:00
parent 2e44fa42dc
commit 53408547f4
2 changed files with 12 additions and 4 deletions

View file

@ -749,7 +749,8 @@ def _charstyle_of_path(path):
@functools.lru_cache(maxsize=100)
def path_colored(path):
char_style = _charstyle_of_path(path)
path = path[2:]
if path.startswith("./"):
path = path[2:]
dirname, basename = os.path.split(path)
if dirname == "":
return termstr.TermStr(basename, char_style)

View file

@ -10,6 +10,8 @@ import pickle
import sys
import urllib.parse
import termstr
import eris.tools as tools
import fill3
@ -52,10 +54,15 @@ def make_main_body():
@functools.lru_cache(maxsize=100)
def make_listing_page(url_path):
unquoted_path = urllib.parse.unquote(url_path)
path, tool = os.path.split(unquoted_path)
result = index[(path, tool)]
path, tool_name = os.path.split(unquoted_path)
result = index[(path, tool_name)]
tool = getattr(tools, tool_name)
tool_name_colored = tools.tool_name_colored(tool, path)
header = fill3.appearance_as_html(
[tools.path_colored(path) + " - " + tool_name_colored,
termstr.TermStr(" ").underline() * 100])
body = fill3.appearance_as_html(result.appearance_min())
return make_page(body, f"{tool} of {path}")
return make_page(header + body, f"{path} - {tool_name}")
class Webserver(http.server.BaseHTTPRequestHandler):