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 subprocess
import os
import hashlib
from pathlib import Path
import time
from datetime import datetime
@ -17,87 +19,9 @@ from datetime import datetime
from .render_pipeline import RenderPipeline, MultiCallback, CallbackClass
from .pandoc import Pandoc, 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
from .admonition import blockquote_filter, create_warning, create_information, Theorem, Proof
from .penrose import Penrose
from .image import ImageFilter
def parse_title(content):
if content['t'] == 'MetaString':
@ -138,108 +62,6 @@ def parse_date(content):
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:
topics = dict()
@ -346,13 +168,45 @@ def on_stdin(fd, pipeline):
else:
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):
return [
(r"/", MainBodyHandler, {"loader" : loader}),
(r"/ws", PushPull),
(r"/css/(.*)", StaticFileHandler, {"path" : r"{}/data/css".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):
@ -398,5 +252,7 @@ async def main(base_path):
Publisher.subscribe("PushPull", "course", PushPull.update_course)
Publisher.subscribe("PushPull", "date", PushPull.update_date)
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)
await asyncio.Event().wait()

View File

@ -115,7 +115,7 @@ blockquote {
.page-container {
width: var(--page-width);
max-width: 100%;
min-height: 100vh;
min-height: 90vh;
padding: var(--page-margin);
background-color: white;
}
@ -286,3 +286,29 @@ h6 {
.page-content h6:not(.panel-title) {
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 Disjoint(Set s1, Set s2)
predicate Union(Set s1, Set s2)

View File

@ -3,29 +3,8 @@ canvas {
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 {
shape x.icon = Circle {
strokeWidth : 0.0
}
shape x.icon = Circle {}
shape x.text = Equation {
string : x.label
fontSize : "32px"
@ -33,5 +12,16 @@ forall Set x {
ensure contains(x.icon, x.text)
encourage norm(x.text.center - x.icon.center) == 0
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
function app:base(content)
if self.channel == nil then
return
end
chansend(self.channel, Message({base = content}))
end
function app:show(content)
if self.channel == nil then
return

View File

@ -28,6 +28,7 @@ function module.open()
end)
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:scroll(vim.fn.line('.'))

View File

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