Server/MarkdownPreviewer/admonition.py

@@ -1,153 +0,0 @@
-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

Server/MarkdownPreviewer/image.py

@@ -1,31 +0,0 @@
-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

Server/MarkdownPreviewer/penrose.py

@@ -1,54 +0,0 @@
-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

Server/MarkdownPreviewer/server.py

@@ -10,8 +10,6 @@ import re
 import tempfile
 import subprocess
 import os
-import hashlib
-from pathlib import Path
 
 import time
 from datetime import datetime
@@ -19,9 +17,87 @@ from datetime import datetime
 from .render_pipeline import RenderPipeline, MultiCallback, CallbackClass
 from .pandoc import Pandoc, Div, Span, Header, Attr, Plain, PString, Inline, Image
 
-from .admonition import blockquote_filter, create_warning, create_information, Theorem, Proof
+blockquote_re = re.compile('!\\[([a-z]+)\\]')
-from .penrose import Penrose
+
-from .image import ImageFilter
+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
 
 def parse_title(content):
     if content['t'] == 'MetaString':
@@ -62,6 +138,108 @@ 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()
 
@@ -168,45 +346,13 @@ 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):
@@ -252,7 +398,5 @@ 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()

data/css/style.css

@@ -115,7 +115,7 @@ blockquote {
 .page-container {
     width: var(--page-width);
     max-width: 100%;
-    min-height: 90vh;
+    min-height: 100vh;
     padding: var(--page-margin);
     background-color: white;
 }
@@ -286,29 +286,3 @@ 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;
-}

data/penrose/set.domain

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

data/penrose/set.style

@@ -3,8 +3,29 @@ 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 {}
+    shape x.icon = Circle {
+        strokeWidth : 0.0
+    }
     shape x.text = Equation {
         string : x.label
         fontSize : "32px"
@@ -12,16 +33,5 @@ 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)
 }

lua/MarkdownPreviewer/app.lua

@@ -47,14 +47,6 @@ 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

lua/MarkdownPreviewer/init.lua

@@ -28,7 +28,6 @@ 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('.'))
 

template/index.html

@@ -75,10 +75,12 @@
             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.scrollHeight
+                            var height = window.innerHeight
-                            || document.body.scrollHeight;
+                            || document.documentElement.clientHeight
+                            || document.body.clientHeight;
 
                             window.scrollTo({left : 0, top: height * v, behavior: 'smooth'});
                             break;