the next generation of the in-browser educational proof assistant
1
2export interface Component {
3 toString(): string;
4 dependencyChanged(id: string, comp: Component, msg: any): void;
5}
6
7let toInitialise: Array<string> = [];
8
9export async function load(url: string): Promise<Handler> {
10 if (url in database) {
11 return database[url];
12 } else {
13 let requestURI = url.split('/').slice(0, -1).join("/");
14 let response = await fetch(requestURI);
15 let body = await response.text();
16 const parser = new DOMParser();
17 const htmldoc = parser.parseFromString(body, "text/html")
18 /*let host = document.createElement("div");
19 host.style.border = "1px solid red";
20 document.body.appendChild(host);
21 let shadow = host.attachShadow({ mode: "open" });
22 for (let x of knownTags) {
23 for (let y of htmldoc.querySelectorAll(x)) {
24 shadow.appendChild(document.adoptNode(y));
25 }
26 }*/
27 for (let x of knownTags) {
28 for (let y of htmldoc.querySelectorAll(x)) {
29 window.customElements.upgrade(document.adoptNode(y))
30 }
31 }
32 while (toInitialise.length) {
33 database[toInitialise.shift() ?? ""]?.initialise();
34 }
35 if (!(url in database)) {
36 throw "ERROR"
37 } else {
38 return database[url];
39 }
40 }
41}
42
43class Handler {
44 url: string;
45 component: Component | null;
46 subscribers: Array<Handler>;
47 deps: Record<string, Handler | null>;
48 status: "loading" | "ready";
49
50 addSubscriber(h: Handler) {
51 this.subscribers.push(h);
52 if (this.status == "ready") {
53 h.dependencyReady(this.url)
54 }
55 }
56 initialise: () => void;
57 dependencyReady: (url: string) => void;
58 notifySubscribers: (msg: any) => void;
59 constructor(
60 url: string,
61 textual: string,
62 deps: Array<string>,
63 maker: new (
64 data: string,
65 deps: Record<string, Component>,
66 signal: (msg: any) => void,
67 initialised: (msg: any) => void,
68 view?: HTMLElement) => Component,
69 view?: HTMLElement) {
70 this.url = url;
71 this.status = "loading";
72 this.deps = {};
73 let awaiting: Array<string> = [];
74 this.subscribers = [];
75 for (let dep of deps) {
76 if (dep != "") {
77 awaiting.push(dep);
78 this.deps[dep] = null;
79 }
80 }
81 this.component = null;
82 this.notifySubscribers = function(msg: any) {
83 console.log(this.url, this.subscribers)
84 if (this.component != null) {
85 for (let sub of this.subscribers) {
86 if (sub.component != null) {
87 sub.component.dependencyChanged(this.url, this.component, msg)
88 }
89 }
90 window.localStorage.setItem(this.url, this.component.toString())
91 }
92 }
93 this.initialise = function() {
94 for (let dep in this.deps) {
95 load(dep).then((h) => {
96 this.deps[dep] = h;
97 h.addSubscriber(this);
98 })
99 }
100 if (awaiting.length == 0) {
101 this.component = new maker(textual, {},
102 (msg) => { this.notifySubscribers(msg) }, (msg) => {
103 this.status = "ready";
104 for (let sub of this.subscribers) {
105 sub.dependencyReady(this.url);
106 }
107 }, view);
108 }
109 }
110 this.dependencyReady = function(url) {
111 let index = awaiting.indexOf(url);
112 if (index > -1) {
113 awaiting.splice(index, 1);
114 }
115
116 if (awaiting.length == 0) {
117 let deps2: Record<string, Component> = {};
118 for (let dep in this.deps) {
119 let v = this.deps[dep]?.component;
120 if (v != null && v != undefined) {
121 deps2[dep] = v;
122 }
123 }
124 this.component = new maker(textual, deps2,
125 (msg) => { this.notifySubscribers(msg) }, (msg) => {
126 this.status = "ready";
127 for (let sub of this.subscribers) {
128 sub.dependencyReady(this.url);
129 }
130 }, view);
131 }
132 }
133 }
134}
135
136let knownTags: Array<string> = [];
137export let database: Record<string, Handler> = {};
138
139export function setup(
140 spec: Record<string,
141 new (data: string,
142 deps: Record<string, Component>,
143 signal: (msg: any) => void,
144 initialised: (msg: any) => void,
145 view?: HTMLElement) => Component>) {
146 let promises = [];
147 for (const name in spec) {
148 const maker = spec[name];
149 knownTags.push(name);
150 window.customElements.define(name, class extends HTMLElement {
151 constructor() {
152 super();
153 let id = this.attributes.getNamedItem("id")?.value ?? "default";
154 toInitialise.push(id);
155 let deps = (this.attributes.getNamedItem("deps")?.value ?? "").split(" ");
156 let text = window.localStorage.getItem(id) ?? this.innerHTML;
157 this.innerHTML = "loading";
158 if (this.id in database) {
159 this.innerHTML = "duplicate element"
160 } else {
161 database[this.id] = new Handler(this.id, text, deps, maker, this);
162 }
163 }
164 });
165 promises.push(window.customElements.whenDefined(name))
166 }
167 Promise.all(promises).then(() => {
168 while (toInitialise.length) {
169 database[toInitialise.shift() ?? ""]?.initialise();
170 }
171 })
172}