fix(playground): backport new playground
This commit is contained in:
parent
1a983b7e2c
commit
62feed0715
2 changed files with 281 additions and 123 deletions
|
|
@ -19,6 +19,11 @@
|
|||
<input id="logging-checkbox" type="checkbox"></input>
|
||||
</div>
|
||||
|
||||
<div class=header-item>
|
||||
<label for="anonymous-nodes-checkbox">show anonymous nodes</label>
|
||||
<input id="anonymous-nodes-checkbox" type="checkbox"></input>
|
||||
</div>
|
||||
|
||||
<div class=header-item>
|
||||
<label for="query-checkbox">query</label>
|
||||
<input id="query-checkbox" type="checkbox"></input>
|
||||
|
|
@ -67,6 +72,12 @@
|
|||
<script src=tree-sitter.js></script>
|
||||
<script src=playground.js></script>
|
||||
|
||||
<script>
|
||||
setTimeout(() => {
|
||||
window.initializePlayground({local: true});
|
||||
}, 1000);
|
||||
</script>
|
||||
|
||||
<style>
|
||||
body {
|
||||
margin: 0;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue