Initial commit

.gitignore

@@ -0,0 +1,8 @@
+__pycache__
+build/
+.eggs
+*.egg-info/
+fonts/
+katex/
+highlight/
+*.pex

README.md

@@ -0,0 +1,9 @@
+# Functionality
+
+## Client
+
+
+
+## Server
+
+## Webpage

Server/MarkdownPreviewer/__init__.py

@@ -4,5 +4,12 @@ import argparse
 import sys
 
 def launcher():
-    print(sys.argv)
-    asyncio.run(main())
+    parser = argparse.ArgumentParser(
+            prog="MarkdownPreviewer",
+            description="Server to allow live rendering of markdown")
+
+    parser.add_argument('--base', help="base directoy of the server")
+
+    result = parser.parse_args()
+
+    asyncio.run(main(result.base))

Server/MarkdownPreviewer/pandoc.py

@@ -125,3 +125,19 @@ class PString:
                 't' : 'Str',
                 'c' : self.content
                 }
+
+class Image:
+    def __init__(self, attr, caption, url):
+        self.attr = attr
+        self.caption = caption
+        self.url = url
+
+    def toJson(self):
+        return {
+                't' : 'Image',
+                'c' : [
+                    self.attr.toJson(),
+                    self.caption,
+                    [self.url, ""]
+                ]
+                }

Server/MarkdownPreviewer/render_pipeline.py

@@ -2,7 +2,14 @@
 # Allows filtering and mapping based on blocks and meta keys.
 # 
 
-import pandoc
+from .pandoc import Pandoc
+
+class CallbackClass:
+    def __init__(self):
+        pass
+
+    def clear(self):
+        pass
 
 class MetaCallback:
     def __init__(self, key, callback, replace=False):
@@ -13,7 +20,10 @@ class MetaCallback:
     def __call__(self, data):
         return self.callback(data)
 
-class MultiCallback:
+    def clear(self):
+        pass
+
+class MultiCallback(CallbackClass):
     def __init__(self, filter):
         self.filter = filter
         self.callbacks = dict()
@@ -32,10 +42,15 @@ class MultiCallback:
         else:
             return block
 
+    def clear(self):
+        for key,value in self.callbacks.items():
+            if isinstance(value, CallbackClass):
+                value.clear()
+
 
 class RenderPipeline:
     def __init__(self):
-        self.pandoc = pandoc.Pandoc()
+        self.pandoc = Pandoc()
         self.metacallbacks = dict()
         self.callbacks = dict()
 
@@ -45,6 +60,13 @@ class RenderPipeline:
     def AddCallback(self, key, callback, replace=False):
         self.callbacks[key] = {'cb' : callback, 'replace' : replace}
 
+    def ClearState(self):
+        for key,value in self.metacallbacks.items():
+            value.clear()
+        for key,value in self.callbacks.items():
+            if isinstance(value['cb'], CallbackClass):
+                value['cb'].clear()
+
     def ParseBlock(self, block):
 
         if 'c' not in block:
@@ -76,6 +98,7 @@ class RenderPipeline:
         return output_list
 
     def __call__(self, data):
+        self.ClearState()
         json_data = self.pandoc.ConvertToJson(data)
 
         for meta_key, meta_value in json_data['meta'].items():

Server/MarkdownPreviewer/server.py

@@ -0,0 +1,396 @@
+from tornado.ioloop import IOLoop
+from tornado.web import Application, RequestHandler, StaticFileHandler
+from tornado.websocket import WebSocketHandler
+from tornado.template import Loader
+import sys
+import asyncio
+import msgpack
+import json
+import re
+import tempfile
+import subprocess
+import os
+
+import time
+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
+
+def parse_title(content):
+    if content['t'] == 'MetaString':
+        data = content['c']
+    elif content['t'] == 'MetaInlines':
+        data = ""
+        for inline in content['c']:
+            if inline['t'] == 'Str':
+                data += inline['c']
+            elif inline['t'] == 'Space':
+                data += " "
+
+    Publisher.publish("title", data)
+
+def parse_course(content):
+    if content['t'] == 'MetaString':
+        data = content['c']
+    elif content['t'] == 'MetaInlines':
+        data = ""
+        for inline in content['c']:
+            if inline['t'] == 'Str':
+                data += inline['c']
+            elif inline['t'] == 'Space':
+                data += " "
+
+    Publisher.publish("course", data)
+
+def parse_date(content):
+    if content['t'] == 'MetaString':
+        data = content['c']
+    elif content['t'] == 'MetaInlines':
+        data = ""
+        for inline in content['c']:
+            if inline['t'] == 'Str':
+                data += inline['c']
+            elif inline['t'] == 'Space':
+                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:
+    topics = dict()
+
+    @classmethod
+    def publish(cls, topic, content):
+        if topic in Publisher.topics:
+            for client in Publisher.topics[topic]:
+                client["callback"](content)
+
+    @classmethod
+    def subscribe(cls, id, topic, callback):
+        if topic in Publisher.topics:
+            Publisher.topics[topic].append({"id":id, "callback":callback})
+        else:
+            Publisher.topics[topic] = [{"id":id, "callback":callback}]
+
+class MainBodyHandler(RequestHandler):
+    body = ""
+    title = ""
+    date = ""
+    course = ""
+
+    @classmethod
+    def update_body(cls, content):
+        MainBodyHandler.body = content
+
+    @classmethod
+    def update_title(cls, content):
+        MainBodyHandler.title = content
+
+    @classmethod
+    def update_date(cls, content):
+        MainBodyHandler.date = content
+
+    @classmethod
+    def update_course(cls, content):
+        MainBodyHandler.course = content
+
+    def initialize(self, loader):
+        self.loader = loader
+        self.template = loader.load("index.html")
+
+    def get(self):
+        self.write(
+                self.template.generate(body_content=MainBodyHandler.body,
+                                  title=MainBodyHandler.title,
+                                  date=MainBodyHandler.date,
+                                  course=MainBodyHandler.course)
+                )
+
+websockets = []
+
+class PushPull(WebSocketHandler):
+    def check_origin(self, origin):
+        return True
+
+    @classmethod
+    def update_body(cls, content):
+        for socket in websockets:
+            socket.write_message({"show" : content})
+
+    @classmethod
+    def update_title(cls, content):
+        for socket in websockets:
+            socket.write_message({"title" : content})
+
+    @classmethod
+    def update_date(cls, content):
+        for socket in websockets:
+            socket.write_message({"date" : content})
+
+    @classmethod
+    def update_course(cls, content):
+        for socket in websockets:
+            socket.write_message({"course" : content})
+
+    def open(self):
+        if self not in websockets:
+            websockets.append(self)
+
+    def on_message(self, message):
+        print(message)
+
+    def on_close(self):
+        if self in websockets:
+            websockets.remove(self)
+
+def on_stdin(fd, pipeline):
+    res = fd.read(4)
+
+    size = res[3] + (res[2]<<8) + (res[1]<<16) + (res[0]<<24)
+
+    read_data = fd.read(size)
+    data = msgpack.unpackb(read_data)
+
+    for key,value in data.items():
+        if key == "show":
+            Publisher.publish(key, pipeline(value))
+        else:
+            Publisher.publish(key, value)
+
+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"})
+    ]
+
+def codeblock_filter(block):
+    return block['c'][0][1][0]
+
+async def main(base_path):
+    loader = Loader("{}/template".format(base_path))
+    pipeline = RenderPipeline()
+
+    pipeline.AddMetaCallback('title', parse_title)
+    pipeline.AddMetaCallback('course', parse_course)
+    pipeline.AddMetaCallback('date', parse_date)
+
+    blockquote = MultiCallback(blockquote_filter)
+    blockquote.AddCallback('warning', create_warning)
+    blockquote.AddCallback('information', create_information)
+
+    theo = Theorem()
+    proo = Proof()
+
+    blockquote.AddCallback('theorem', theo)
+    blockquote.AddCallback('proof', proo)
+
+    codeblock = MultiCallback(codeblock_filter)
+
+    pen = Penrose(base_path)
+
+    codeblock.AddCallback("penrose", pen)
+
+    pipeline.AddCallback('BlockQuote', blockquote, replace=True)
+    pipeline.AddCallback('CodeBlock', codeblock, replace=True)
+
+    loop = asyncio.get_event_loop()
+    fd = open(sys.stdin.fileno(), 'rb', buffering=0)
+    loop.add_reader(fd, on_stdin, fd, pipeline)
+    application = Application(route_handler(base_path, loader))
+    Publisher.subscribe("MainbodyHandler", "show", MainBodyHandler.update_body)
+    Publisher.subscribe("MainbodyHandler", "title", MainBodyHandler.update_title)
+    Publisher.subscribe("MainbodyHandler", "course", MainBodyHandler.update_course)
+    Publisher.subscribe("MainbodyHandler", "date", MainBodyHandler.update_date)
+    Publisher.subscribe("PushPull", "show", PushPull.update_body)
+    Publisher.subscribe("PushPull", "title", PushPull.update_title)
+    Publisher.subscribe("PushPull", "course", PushPull.update_course)
+    Publisher.subscribe("PushPull", "date", PushPull.update_date)
+    application.listen(8888)
+    await asyncio.Event().wait()

data/css/style.css

@@ -17,6 +17,7 @@
     --secondary-color: #34A853;
     --accent-color: #EA4335;
     --background-color: white;
+    --quote-bg-color: #F5F5F5;
     --text-color: #222222;
     --light-gray: #ECF0F1;
     --dark-gray: #303333;
@@ -40,9 +41,13 @@
     --spacing-medium: 1rem;
     --spacing-large: 2rem;
 
+    --quote-blue: #0726b0;
+
     --border-radius: 4px;
     --border-width: 2px;
 
+    --blockquote-width: 8px;
+
     --shadow-small: 0 1px 3px rgba(0, 0, 0, 0.12);
     --shadow-medium: 0 2px 6px rgba(0,0,0,0.12);
 
@@ -62,6 +67,17 @@ body {
     padding: 0;
 }
 
+blockquote {
+    border-left: var(--blockquote-width) solid var(--quote-blue);
+    border-radius: var(--border-radius);
+    margin-left: 0px;
+    padding-left: 20px;
+    padding-top: 5px;
+    padding-bottom: 5px;
+    padding-right: 20px;
+    background-color: var(--quote-bg-color);
+}
+
 .page-header {
     margin-bottom: var(--spacing-large);
     text-align: center;

data/penrose/set.domain

@@ -0,0 +1,3 @@
+type Set
+
+predicate SubSet(Set s1, Set s2)

data/penrose/set.style

@@ -0,0 +1,17 @@
+canvas {
+    width = 100
+    height = 100
+}
+
+forall Set A; Set B
+where SubSet(A, B) {
+    ensure contains(A.icon, B.icon, 5.0)
+    A.icon above B.icon
+}
+
+forall Set x {
+    x.icon = Circle {
+        strokeWidth : 0.0
+    }
+    ensure x.icon.r > 25
+}

lua/MarkdownPreviewer/app.lua

@@ -20,7 +20,8 @@ end
 
 app = {
     cmd = nil,
-    channel = nil
+    channel = nil,
+    cwd = nil
 }
 
 function app:init(on_exit)
@@ -28,9 +29,9 @@ function app:init(on_exit)
         return
     end
 
-    local cwd = debug.getinfo(1, 'S').source:sub(2):match('(.*[/\\])')
+    self.cwd = debug.getinfo(1, 'S').source:sub(2):match('(.*[/\\])')
     self.channel = vim.fn.jobstart(self.cmd, {
-        cwd = cwd,
+        cwd = self.cwd,
         stderr_buffered = true,
         on_exit = function()
             vim.fn.chanclose(self.channel)
@@ -75,11 +76,13 @@ function module.setup()
     setmetatable(o, app)
     app.__index = app
 
+    local cwd = debug.getinfo(1, 'S').source:sub(2):match('(.*[/\\])')
+    local base_location = cwd:gsub("lua/MarkdownPreviewer", "")
+
     o.cmd = {
-        "../../Server/run.sh",
-        "../../Server/venv",
-        'python3',
-        '../../Server/server.py'
+        base_location .. "Server/test.pex",
+        "--base",
+        base_location
     }
 
     return o

template/index.html

@@ -1,21 +1,21 @@
 <!DOCTYPE html>
 <html lang="en">
     <head>
-        <link rel="stylesheet" href="highlight/styles/tokyo-night-dark.min.css">
-        <script src="highlight/highlight.min.js"></script>
-        <link href="katex/katex.min.css" rel="stylesheet" type="text/css">
-        <script src="katex/katex.min.js"></script>
-        <script src="katex/contrib/auto-render.min.js"></script>
-        <link rel="stylesheet" href="style.css">
+        <link rel="stylesheet" href="lib/highlight/styles/tokyo-night-dark.min.css">
+        <script src="lib/highlight/highlight.min.js"></script>
+        <link href="lib/katex/katex.min.css" rel="stylesheet" type="text/css">
+        <script src="lib/katex/katex.min.js"></script>
+        <script src="lib/katex/contrib/auto-render.min.js"></script>
+        <link rel="stylesheet" href="css/style.css">
         <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.4.0/css/all.min.css">
     </head>
     <body>
         <div class="page-container">
             <header class="page-header">
-                <h1 class="page-title">Your Note Title</h1>
+                <h1 id="page-title" class="page-title">{{ title }}</h1>
                 <div class="page-subtitle">
-                    <div class="page-author">Author: Your Name</div>
-                    <div class="page-date">Date: August 1, 2025</div>
+                    <div id="page-author" class="page-author">{{ course }}</div>
+                    <div class="page-date">Date: <span id="date">{{ date }}</span></div>
                 </div>
             </header>
 
@@ -42,11 +42,10 @@
                 socket.send("ping");
             });
 
-            socket.addEventListener("message", (event) => {
-                var data = JSON.parse(event.data);
-                var node = document.getElementById("page-content");
-                var wrapper = document.createElement('div');
-                wrapper.innerHTML = data['show'];
+            function change_body(v) {
+                const node = document.getElementById("page-content");
+                const wrapper = document.createElement("div");
+                wrapper.innerHTML = v;
                 node.replaceChildren(wrapper);
 
                 hljs.highlightAll();
@@ -60,6 +59,34 @@
                             {left: "\\(", right: "\\)", display: false}
                         ]
                     });
+            }
+
+            function change_header(k,v) {
+                const dict = {
+                    'title' : 'page-title',
+                    'date' : 'date',
+                    'course' : 'page-author'
+                }
+
+                const node = document.getElementById(dict[k])
+                node.replaceChildren(v);
+            }
+
+            socket.addEventListener("message", (event) => {
+                var data = JSON.parse(event.data);
+                Object.entries(data).forEach(([k,v]) => {
+                    console.log(k,v);
+                    switch (k) {
+                        case "show":
+                            change_body(v)
+                            break;
+                        case "title":
+                        case "date":
+                        case "course":
+                            change_header(k,v);
+                            break;
+                    }
+                })
             });
         </script>
     </body>