Compare commits

..

7 Commits

Author SHA1 Message Date
Folkert Kevelam
6cbe1bb7cd Add logic for penrose, image, and admonitions 2025-08-31 21:23:54 +02:00
Folkert Kevelam
7bfdc63512 Initial commit 2025-08-31 21:23:34 +02:00
Folkert Kevelam
3ff93e4d1f Add scroll option 2025-08-31 21:23:10 +02:00
Folkert Kevelam
5ddd2896a1 Send base command when opening 2025-08-31 21:22:35 +02:00
Folkert Kevelam
ade996d26d Add base command 2025-08-31 21:21:35 +02:00
Folkert Kevelam
0042f1fca0 Update set penrose 2025-08-31 21:20:54 +02:00
Folkert Kevelam
5c0dbcd494 Fix page container height and add table styling 2025-08-31 21:20:33 +02:00
10 changed files with 329 additions and 213 deletions

View File

@ -0,0 +1,153 @@
import re
from .render_pipeline import CallbackClass
from .pandoc import Div, Span, Header, Attr, Plain, PString, Inline, Image
blockquote_re = re.compile('!\\[([a-z]+)\\]')
panel_content = Attr("", classes=["panel-content"])
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
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

View File

@ -0,0 +1,31 @@
from pathlib import Path
class ImageFilter:
def __init__(self, base_path=None):
self.base_path = ""
if base_path is not None:
self.base_path = Path(base_path)
if not self.base_path.is_dir():
self.base_path = self.base_path.parent
def set_base_path(self, base_path):
if isinstance(base_path, str):
self.base_path = Path(base_path)
elif isinstance(base_path, Path):
self.base_path = base_path
if not self.base_path.is_dir():
self.base_path = self.base_path.parent
def __call__(self, content):
path = Path(content['c'][2][0])
if path.is_absolute():
return content
new_path = (self.base_path / path).resolve()
print(new_path)
content['c'][2][0] = str(new_path)
return content

View File

@ -0,0 +1,54 @@
from .render_pipeline import CallbackClass
from .pandoc import Attr, Image, Plain
import hashlib
import subprocess
import tempfile
import os
import re
class Penrose(CallbackClass):
def __init__(self, base_path):
self.data_path = base_path + "/data/penrose/"
self.image_cache = dict()
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):
hashinput = re.sub(r"\s+", "", content['c'][1], flags=re.UNICODE).encode("utf-8")
hash = hashlib.md5()
hash.update(hashinput)
digest = hash.hexdigest()
if digest in self.image_cache:
return self.image_cache[digest]
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()
self.image_cache[digest] = wrapper
return wrapper

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()

View File

@ -115,7 +115,7 @@ blockquote {
.page-container { .page-container {
width: var(--page-width); width: var(--page-width);
max-width: 100%; max-width: 100%;
min-height: 100vh; min-height: 90vh;
padding: var(--page-margin); padding: var(--page-margin);
background-color: white; background-color: white;
} }
@ -286,3 +286,29 @@ h6 {
.page-content h6:not(.panel-title) { .page-content h6:not(.panel-title) {
border-left-width: 2px; border-left-width: 2px;
} }
table {
border-collapse: collapse;
width: 100%;
}
td, th {
border: 1px solid #ddd;
padding: 8px;
}
tr:nth-child(even) {
background-color: #f2f2f2;
}
tr:hover {
background-color: #ddd;
}
th {
padding-top: 12px;
padding-bottom: 12px;
text-align: left;
background-color: var(--caribbean-current);
color: white;
}

View File

@ -2,4 +2,3 @@ type Set
predicate SubSet(Set s1, Set s2) predicate SubSet(Set s1, Set s2)
predicate Disjoint(Set s1, Set s2) predicate Disjoint(Set s1, Set s2)
predicate Union(Set s1, Set s2)

View File

@ -3,29 +3,8 @@ canvas {
height = 500 height = 500
} }
forall Set A; Set B
where SubSet(A, B) {
ensure disjoint(B.text, A.icon, 10.0)
ensure contains(A.icon, B.icon, 5.0)
layer A.icon above B.icon
}
forall Set A; Set B
where Disjoint(A, B) {
ensure disjoint(A.icon, B.icon)
}
forall Set A; Set B
where Union(A,B) {
ensure overlapping(A.icon, B.icon)
ensure disjoint(A.text, B.icon)
ensure disjoint(B.text, A.icon)
}
forall Set x { forall Set x {
shape x.icon = Circle { shape x.icon = Circle {}
strokeWidth : 0.0
}
shape x.text = Equation { shape x.text = Equation {
string : x.label string : x.label
fontSize : "32px" fontSize : "32px"
@ -33,5 +12,16 @@ forall Set x {
ensure contains(x.icon, x.text) ensure contains(x.icon, x.text)
encourage norm(x.text.center - x.icon.center) == 0 encourage norm(x.text.center - x.icon.center) == 0
layer x.text above x.icon layer x.text above x.icon
ensure x.icon.r > 25.0 }
forall Set x; Set y
where SubSet(x, y) {
ensure disjoint(y.text, x.icon, 10.0)
ensure contains(y.icon, x.icon, 5.0)
layer x.icon above y.icon
}
forall Set x; Set y
where Disjoint(x, y) {
ensure disjoint(x.icon, y.icon)
} }

View File

@ -47,6 +47,14 @@ function app:init(on_exit)
}) })
end end
function app:base(content)
if self.channel == nil then
return
end
chansend(self.channel, Message({base = content}))
end
function app:show(content) function app:show(content)
if self.channel == nil then if self.channel == nil then
return return

View File

@ -28,6 +28,7 @@ function module.open()
end) end)
local bufnr = vim.api.nvim_get_current_buf() local bufnr = vim.api.nvim_get_current_buf()
server_connection:base(vim.fn.fnamemodify(vim.uri_to_fname(vim.uri_from_bufnr(bufnr)), 'p:h'))
server_connection:show(get_buf_content(bufnr)) server_connection:show(get_buf_content(bufnr))
server_connection:scroll(vim.fn.line('.')) server_connection:scroll(vim.fn.line('.'))

View File

@ -75,12 +75,10 @@
socket.addEventListener("message", (event) => { socket.addEventListener("message", (event) => {
var data = JSON.parse(event.data); var data = JSON.parse(event.data);
Object.entries(data).forEach(([k,v]) => { Object.entries(data).forEach(([k,v]) => {
console.log(k,v);
switch (k) { switch (k) {
case "scroll": case "scroll":
var height = window.innerHeight var height = window.scrollHeight
|| document.documentElement.clientHeight || document.body.scrollHeight;
|| document.body.clientHeight;
window.scrollTo({left : 0, top: height * v, behavior: 'smooth'}); window.scrollTo({left : 0, top: height * v, behavior: 'smooth'});
break; break;