Add logic for penrose, image, and admonitions

This commit is contained in:
Folkert Kevelam 2025-08-31 21:23:54 +02:00
parent 7bfdc63512
commit 6cbe1bb7cd

View File

@ -10,6 +10,8 @@ import re
import tempfile import tempfile
import subprocess import subprocess
import os import os
import hashlib
from pathlib import Path
import time import time
from datetime import datetime from datetime import datetime
@ -17,87 +19,9 @@ from datetime import datetime
from .render_pipeline import RenderPipeline, MultiCallback, CallbackClass from .render_pipeline import RenderPipeline, MultiCallback, CallbackClass
from .pandoc import Pandoc, Div, Span, Header, Attr, Plain, PString, Inline, Image from .pandoc import Pandoc, Div, Span, Header, Attr, Plain, PString, Inline, Image
blockquote_re = re.compile('!\\[([a-z]+)\\]') from .admonition import blockquote_filter, create_warning, create_information, Theorem, Proof
from .penrose import Penrose
panel_content = Attr("", classes=["panel-content"]) from .image import ImageFilter
header_attr = Attr("", classes=["panel-title"])
warning_icon = Attr("", classes=["fas", "fa-exclamation-triangle", "panel-icon"])
information_icon = Attr("", classes=["fas", "fa-info-circle", "panel-icon"])
header_title_attr = Attr("", classes=["panel-header"])
outer_attr = Attr("", classes=["panel", "panel-warning"])
outer_info_attr = Attr("", classes=["panel", "panel-info"])
def blockquote_filter(block):
data = block['c']
if data[0]['t'] != 'Para':
return None
paragraph_content = data[0]['c']
if paragraph_content[0]['t'] != 'Str':
return None
string_content = paragraph_content[0]['c']
m = blockquote_re.match(string_content)
if m is None:
return None
return m.group(1)
def create_warning(content):
internal_content = content['c']
internal_content[0]['c'].pop(0)
internal_content[0]['c'].pop(0)
content_div = Div(panel_content, internal_content).toJson()
label = PString("Warning").toJson()
header = Header(header_attr, 3, [label]).toJson()
icon = Plain(Span(warning_icon, []).toJson()).toJson()
header_div = Div(header_title_attr,
[
icon,
header
]).toJson()
outer_div = Div(outer_attr,
[
header_div,
content_div
]).toJson()
return outer_div
def create_information(content):
internal_content = content['c']
internal_content[0]['c'].pop(0)
internal_content[0]['c'].pop(0)
content_div = Div(panel_content, internal_content).toJson()
label = PString("Information").toJson()
header = Header(header_attr, 3, [label]).toJson()
icon = Plain(Span(information_icon, []).toJson()).toJson()
header_div = Div(header_title_attr,
[
icon,
header
]).toJson()
outer_div = Div(outer_info_attr,
[
header_div,
content_div
]).toJson()
return outer_div
def parse_title(content): def parse_title(content):
if content['t'] == 'MetaString': if content['t'] == 'MetaString':
@ -138,108 +62,6 @@ def parse_date(content):
Publisher.publish("date", data) Publisher.publish("date", data)
class Theorem(CallbackClass):
def __init__(self):
self.counter = 1
def __call__(self, content):
internal_content = content['c']
internal_content[0]['c'].pop(0)
internal_content[0]['c'].pop(0)
outer_div_attr = Attr("", classes=["theorem"])
inner_div_attr = Attr("", classes=["theorem-content"])
bold_attr = Attr("", classes=["theorem-title"])
span_attr = Attr("")
theorem_string = "Theorem {}. ".format(self.counter)
title_content = Inline("Emph", [PString(theorem_string).toJson()]).toJson()
title = Span(span_attr, [title_content]).toJson()
internal_content[0]['c'].insert(0, title)
content_div = Div(inner_div_attr, internal_content).toJson()
outer_div = Div(outer_div_attr, [content_div]).toJson()
self.counter += 1
return outer_div
def clear(self):
self.counter = 1
class Proof(CallbackClass):
def __init__(self):
self.counter = 1
def clear(self):
self.counter = 1
def __call__(self, content):
internal_content = content['c']
internal_content[0]['c'].pop(0)
internal_content[0]['c'].pop(0)
outer_div_attr = Attr("", classes=["proof"])
inner_div_attr = Attr("", classes=["proof-content"])
span_attr = Attr("", classes=["proof-title"])
qed_attr = Attr("", classes=["proof-qed"])
proof_string = "Proof {}. ".format(self.counter)
title_content = Span(span_attr, [PString(proof_string).toJson()]).toJson()
title = Inline("Emph", [title_content]).toJson()
internal_content[0]['c'].insert(0, title)
qed_string = Plain(PString("").toJson()).toJson()
qed = Div(qed_attr, [qed_string]).toJson()
inner_div = Div(inner_div_attr, internal_content).toJson()
outer_div = Div(outer_div_attr, [inner_div, qed]).toJson()
return outer_div
class Penrose(CallbackClass):
def __init__(self, base_path):
self.data_path = base_path + "/data/penrose/"
def run(self, input_file_name, domain, style):
domain_path = self.data_path + domain + ".domain"
style_path = self.data_path + domain + ".style"
return subprocess.run(
["roger", "trio", input_file_name, domain_path, style_path, '--path', "/"],
text=True,
capture_output=True)
def __call__(self, content):
handle, file_path = tempfile.mkstemp(suffix=".substance", text=True)
text = content['c'][1]
with os.fdopen(handle, 'w') as f:
f.write(text)
data = self.run(file_path, "set", "set")
handle, file_path = tempfile.mkstemp(suffix=".svg", text=True)
with os.fdopen(handle, 'w') as f:
f.write(data.stdout)
img_attr = Attr("")
new_content = Image(img_attr, [{'t' : 'Str', 'c' : 'Penrose'}], "/generated/{}".format(file_path[5:])).toJson()
wrapper = Plain(new_content).toJson()
return wrapper
class Publisher: class Publisher:
topics = dict() topics = dict()
@ -346,13 +168,45 @@ def on_stdin(fd, pipeline):
else: else:
Publisher.publish(key, value) Publisher.publish(key, value)
class RuntimeImageHandler(StaticFileHandler):
base_path = None
@classmethod
def set_base_path(cls, path):
p = Path(path)
if not p.is_dir():
cls.base_path = p.parent
else:
cls.base_path = p
@classmethod
def get_absolute_path(cls, root, path):
if cls.base_path:
p = (cls.base_path / Path(path)).resolve()
else:
p = (Path(root) / Path(path)).resolve()
return str(p)
def validate_absolute_path(self, root, absolute_path):
p = Path(absolute_path)
if not p.exists():
raise HTTPError(404)
if not p.isfile():
raise HTTPError(403, "%s is not a file", self.path)
return absolute_path
def route_handler(base_path, loader): def route_handler(base_path, loader):
return [ return [
(r"/", MainBodyHandler, {"loader" : loader}), (r"/", MainBodyHandler, {"loader" : loader}),
(r"/ws", PushPull), (r"/ws", PushPull),
(r"/css/(.*)", StaticFileHandler, {"path" : r"{}/data/css".format(base_path)}), (r"/css/(.*)", StaticFileHandler, {"path" : r"{}/data/css".format(base_path)}),
(r"/lib/(.*)", StaticFileHandler, {"path" : r"{}/data/lib".format(base_path)}), (r"/lib/(.*)", StaticFileHandler, {"path" : r"{}/data/lib".format(base_path)}),
(r"/generated/(.*)", StaticFileHandler, {"path" : r"/tmp"}) (r"/generated/(.*)", StaticFileHandler, {"path" : r"/tmp"}),
(r"/(.*)", RuntimeImageHandler, {"path": r""})
] ]
def codeblock_filter(block): def codeblock_filter(block):
@ -398,5 +252,7 @@ async def main(base_path):
Publisher.subscribe("PushPull", "course", PushPull.update_course) Publisher.subscribe("PushPull", "course", PushPull.update_course)
Publisher.subscribe("PushPull", "date", PushPull.update_date) Publisher.subscribe("PushPull", "date", PushPull.update_date)
Publisher.subscribe("PushPull", "scroll", PushPull.update_scroll) Publisher.subscribe("PushPull", "scroll", PushPull.update_scroll)
Publisher.subscribe("MainBodyHandler", "base", MainBodyHandler.update_title)
Publisher.subscribe("RuntimeImageHandler", "base", RuntimeImageHandler.set_base_path)
application.listen(8888) application.listen(8888)
await asyncio.Event().wait() await asyncio.Event().wait()