https://starling-lang.org/editor/src/work.js

1/* global Worker, alert */
2
3const worker = new Worker('src/worker.js', { type: 'module' })
4
5document.getElementById('verify').onclick = async () => {
6  const snippet = document.querySelector('pre').innerText
7
8  alert(
9    "If you're verifying a proof which imports set.mm, this might take some time."
10  )
11  if (snippet.includes('set.mm')) {
12    const url =
13      'https://raw.githubusercontent.com/metamath/set.mm/develop/set.mm'
14    const res = await fetch(url, {})
15    if (!res.ok) throw new Error(`HTTP ${res.status}`)
16
17    const contentType = res.headers.get('content-type') || ''
18    const data = contentType.includes('application/json')
19      ? await res.json()
20      : await res.text()
21    worker.postMessage([data, snippet])
22  } else {
23    worker.postMessage(snippet)
24  }
25}
26
27worker.onmessage = (e) => {
28  if (e.data) {
29    alert(`${e.data}`)
30  }
31}