-
-
Notifications
You must be signed in to change notification settings - Fork 46
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Add playground - Include the remote saving feature (on val.town) - Add tooltips
- Loading branch information
1 parent
37ede7a
commit 3c27ade
Showing
9 changed files
with
1,314 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,31 @@ | ||
name: Publish playground to GitHub pages | ||
|
||
on: | ||
workflow_dispatch | ||
|
||
jobs: | ||
build-and-publish: | ||
runs-on: ubuntu-latest | ||
|
||
steps: | ||
- uses: actions/checkout@v4 | ||
|
||
- uses: actions/setup-node@v4 | ||
with: | ||
node-version: 18 | ||
|
||
- name: build | ||
run: | | ||
npm i | ||
npm run build | ||
working-directory: src/playground | ||
|
||
- name: Deploy to GitHub Pages | ||
if: success() | ||
uses: crazy-max/ghaction-github-pages@v4 | ||
with: | ||
target_branch: gh-pages | ||
build_dir: src/playground/dist | ||
jekyll: false | ||
env: | ||
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,49 @@ | ||
body { | ||
margin: 0; | ||
background: black; | ||
color: white; | ||
font-family: 'Inter', sans-serif; | ||
padding: 48px; | ||
display: flex; | ||
flex-direction: column; | ||
/* This should be 100vh, but I don't know CSS layouts */ | ||
min-height: 70vh; | ||
} | ||
|
||
header { | ||
display: flex; | ||
align-items: center; | ||
gap: 20px; | ||
margin-bottom: 40px; | ||
} | ||
|
||
main { | ||
flex-grow: 1; | ||
} | ||
|
||
.diagnostics { | ||
display: flex; | ||
flex-direction: column; | ||
gap: 10px; | ||
padding-left: 26px; | ||
font-family: monospace; | ||
font-size: 16px; | ||
} | ||
|
||
a { | ||
color: rgb(255, 217, 80); | ||
} | ||
|
||
a:visited { | ||
color: coral; | ||
} | ||
|
||
hr { | ||
margin: 40px 0; | ||
} | ||
|
||
@media (max-width: 700px) { | ||
header { | ||
flex-direction: column; | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,46 @@ | ||
<!DOCTYPE html> | ||
<html lang="en"> | ||
|
||
<head> | ||
<meta charset="UTF-8"> | ||
<meta name="viewport" content="width=device-width, initial-scale=1.0"> | ||
<title>Ezno Playground</title> | ||
<link rel="stylesheet" href="assets/index.css"> | ||
<meta property="twitter:image" content="./assets/banner.svg"> | ||
<meta property="og:image" content="./assets/banner.svg"> | ||
<link rel="icon" href="./assets/ezno.svg"> | ||
</head> | ||
|
||
<body> | ||
<header> | ||
<img src="./assets/ezno.svg" alt="EZNO" height="40px"> | ||
<p> | ||
Playground for the Ezno type checker. See what Ezno supports <a | ||
href="https://github.com/kaleidawave/ezno/blob/main/checker/specification/specification.md">in its | ||
specification</a>. | ||
This is built using the <a href="https://www.npmjs.com/package/ezno">WASM JS build</a>, the native CLI tool | ||
can be <a href="https://github.com/kaleidawave/ezno/releases">downloaded from the latest release</a>. | ||
</p> | ||
</header> | ||
<main> | ||
<div id="editor"></div> | ||
<div> | ||
<h3>Diagnostics</h3> | ||
<ol class="diagnostics"> | ||
</ol> | ||
</div> | ||
<button id="share">Share</button> | ||
</main> | ||
<footer> | ||
<hr> | ||
<p> | ||
If you encounter any issues, please document them <a href="https://github.com/kaleidawave/ezno/">on the GH | ||
issue tracker</a>. If diagnostics don't update then a crash has occurred (check browser logs for | ||
reason). Editor built with <a | ||
href="https://codemirror.net/">codemirror</a> | ||
</p> | ||
</footer> | ||
<script type="module" src="./main.js"></script> | ||
</body> | ||
|
||
</html> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,182 @@ | ||
import { EditorView, keymap, hoverTooltip } from "@codemirror/view"; | ||
import { EditorState, Text } from "@codemirror/state"; | ||
import { linter } from "@codemirror/lint"; | ||
import { defaultKeymap, indentWithTab } from "@codemirror/commands"; | ||
import { parser as jsParser } from "@lezer/javascript"; | ||
import { tags } from "@lezer/highlight"; | ||
import { HighlightStyle, syntaxHighlighting, LanguageSupport, LRLanguage } from "@codemirror/language"; | ||
import { init as init_ezno, check_with_options, get_version } from "ezno"; | ||
import lz from "lz-string"; | ||
|
||
const diagnosticsEntry = document.querySelector(".diagnostics"); | ||
const editorParent = document.querySelector("#editor"); | ||
const shareButton = document.querySelector("#share"); | ||
|
||
const myHighlightStyle = HighlightStyle.define([ | ||
{ tag: tags.keyword, color: '#C792EA' }, | ||
{ tag: tags.comment, color: '#8b949e' }, | ||
{ tag: tags.controlKeyword, color: '#ffb993' }, | ||
{ tag: tags["function"], color: '#58bce3' }, | ||
{ tag: [tags.number, tags.bool], color: '#87c3e8' }, | ||
{ tag: tags.string, color: '#cae2a7' }, | ||
]); | ||
|
||
const theme = EditorView.theme({ | ||
"&": { | ||
backgroundColor: "#101010", | ||
padding: "20px", | ||
fontSize: "18px", | ||
borderRadius: "8px" | ||
}, | ||
".cm-content": { | ||
caretColor: "white" | ||
}, | ||
".cm-diagnostic": { | ||
color: "black" | ||
} | ||
}); | ||
|
||
const STORE = "https://kaleidawave-savednamedplaygrounds.web.val.run" | ||
|
||
|
||
let text = "const x: 2 = 3;"; | ||
|
||
const { searchParams } = new URL(location); | ||
const code = searchParams.get("code"); | ||
const id = searchParams.get("id"); | ||
|
||
if (code) { | ||
text = lz.decompressFromEncodedURIComponent(code); | ||
setup() | ||
} else if (id) { | ||
fetch(STORE + `?id=${id}`, { method: "GET" }).then(res => res.json()).then((result) => { | ||
if (result.content) { | ||
text = result.content | ||
setup() | ||
} else if (result.error) { | ||
alert(`Error getting code for id '${result.error}'`) | ||
} | ||
}) | ||
} else { | ||
setup() | ||
} | ||
|
||
let currentState = null; | ||
|
||
const ROOT_PATH = "index.tsx"; | ||
|
||
async function setup() { | ||
await init_ezno(); | ||
|
||
function getLinter() { | ||
return linter((args) => { | ||
text = args.state.doc.text.join("\n"); | ||
try { | ||
currentState = check_with_options(ROOT_PATH, (_) => text, { lsp_mode: true, store_type_mappings: true }); | ||
|
||
diagnosticsEntry.innerHTML = ""; | ||
for (const diagnostic of currentState.diagnostics) { | ||
const entry = document.createElement("li"); | ||
entry.innerText = diagnostic.reason; | ||
diagnosticsEntry.appendChild(entry); | ||
} | ||
|
||
return currentState.diagnostics.map(({ position, reason, kind }) => ({ | ||
from: position.start, | ||
to: position.end, | ||
message: reason, | ||
severity: kind.toLowerCase(), | ||
})); | ||
} catch (err) { | ||
alert(`Error: ${err}`) | ||
} | ||
}); | ||
} | ||
|
||
function getHover() { | ||
const cursor = hoverTooltip((view, pos, side) => { | ||
if (currentState) { | ||
const type = currentState.get_type_at_position(ROOT_PATH, pos); | ||
if (typeof type !== "undefined") { | ||
return { | ||
pos, | ||
end: pos, | ||
above: true, | ||
create(view) { | ||
let dom = document.createElement("div") | ||
dom.textContent = type | ||
// TODO! | ||
dom.style.color = "black"; | ||
return { dom } | ||
} | ||
} | ||
} else { | ||
return null | ||
} | ||
} else { | ||
return null | ||
} | ||
}); | ||
|
||
const cursorTooltipBaseTheme = EditorView.baseTheme({ | ||
".cm-tooltip.cm-tooltip-cursor": { | ||
backgroundColor: "#66b", | ||
color: "black", | ||
border: "2px solid red", | ||
padding: "2px 7px", | ||
borderRadius: "4px", | ||
"& .cm-tooltip-arrow:before": { | ||
borderTopColor: "#66b" | ||
}, | ||
"& .cm-tooltip-arrow:after": { | ||
borderTopColor: "transparent" | ||
} | ||
} | ||
}) | ||
|
||
return [cursor, cursorTooltipBaseTheme] | ||
} | ||
|
||
let editor = new EditorView({ | ||
state: EditorState.create({ | ||
doc: Text.of([text]), | ||
extensions: [ | ||
keymap.of([...defaultKeymap, indentWithTab]), | ||
EditorState.tabSize.of(4), | ||
new LanguageSupport(LRLanguage.define({ parser: jsParser.configure({ dialect: "ts" }) }), [getLinter()]), | ||
syntaxHighlighting(myHighlightStyle), | ||
getHover(), | ||
theme, | ||
], | ||
}), | ||
parent: editorParent, | ||
}); | ||
|
||
console.log("Editor ready") | ||
console.log(`Running ezno@${get_version()}`) | ||
|
||
shareButton.addEventListener("click", () => { | ||
const url = new URL(location); | ||
const text = editor.state.doc.toString(); | ||
const lzCompressCode = lz.compressToEncodedURIComponent(text); | ||
// TODO arbitrary length | ||
console.debug(`lzCompressCode.length=${lzCompressCode.length}`); | ||
if (lzCompressCode.length < 120) { | ||
url.searchParams.set("code", lzCompressCode); | ||
history.pushState({}, "", url); | ||
} else { | ||
fetch(STORE, { | ||
method: "POST", | ||
body: JSON.stringify({ content: text }) | ||
}).then(res => res.json()).then((result) => { | ||
if (result.id) { | ||
url.searchParams.set("id", result.id); | ||
history.pushState({}, "", url); | ||
} else if (result.error) { | ||
alert(`Error sharing code '${result.error}'`) | ||
} | ||
}) | ||
} | ||
// TODO also copy to clipboard and popup | ||
}) | ||
} |
Oops, something went wrong.