tree-sitter/cli/src/web_ui.html

112 lines
2.4 KiB
HTML
Raw Normal View History

2019-05-13 21:51:17 -07:00
<head>
<title>Tree-sitter</title>
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.45.0/codemirror.min.css">
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/clusterize.js/0.18.0/clusterize.min.css">
</head>
<body>
<div id="playground-container">
<header>
<div class=header-item>
<label for="logging-checkbox">Log</label>
<input id="logging-checkbox" type="checkbox"></input>
</div>
<div class=header-item>
<label for="update-time">Update time: </label>
<span id="update-time"></span>
</div>
</header>
<main>
<select id="language-select" style="display: none;">
<option value="parser">Parser</option>
</select>
<textarea id="code-input"></textarea>
<div id="output-container-scroll">
<pre id="output-container" class="highlight"></pre>
</div>
</main>
</div>
<script
src="https://code.jquery.com/jquery-3.3.1.min.js"
crossorigin="anonymous">
</script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.45.0/codemirror.min.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/clusterize.js/0.18.0/clusterize.min.js"></script>
<script>LANGUAGE_BASE_URL = "";</script>
<script src=tree-sitter.js></script>
<script src=playground.js></script>
<style>
#playground-container {
position: absolute;
top: 0;
bottom: 0;
left: 0;
right: 0;
display: flex;
flex-direction: column;
}
header {
box-sizing: border-box;
display: flex;
padding: 20px;
height: 60px;
border-bottom: 1px solid #aaa;
}
main {
display: flex;
height: 100%;
flex-direction: row;
}
.header-item {
margin-right: 20px;
}
.CodeMirror {
width: 50%;
height: 100%;
border-right: 1px solid #aaa;
}
#output-container-scroll {
width: 50%;
height: 100%;
padding: 0;
overflow: auto;
}
#output-container {
padding: 0 10px;
margin: 0;
}
h4, select, .field {
display: inline-block;
margin-right: 20px;
}
#logging-checkbox {
height: 15px;
}
.CodeMirror div.CodeMirror-cursor {
border-left: 3px solid red;
}
a.highlighted {
background-color: #ddd;
text-decoration: underline;
}
</style>
</body>