turtle-web-editor/index.html

40 lines
1.6 KiB
HTML
Raw Permalink Normal View History

2015-07-14 19:23:35 +02:00
<html>
<head>
2020-04-29 15:43:06 +02:00
<title>Turtle Web Editor</title>
2020-04-29 14:04:01 +02:00
<script src="js/jquery-2.1.4.min.js"></script>
2015-07-14 19:23:35 +02:00
<script src="js/ttl.js"></script>
2020-04-29 15:43:06 +02:00
<script src="js/codemirror.js"></script>
<script src="js/turtle.min.js"></script>
2020-04-29 14:04:01 +02:00
<script src="js/bootstrap.min.js"></script>
2020-04-29 15:43:06 +02:00
<link rel="stylesheet" href="css/style.css">
<link rel="stylesheet" href="css/codemirror.css">
<link rel="stylesheet" href="css/bootstrap.min.css">
2020-04-29 17:18:49 +02:00
<style>
.CodeMirror {
border: 1px solid #eee;
2020-04-29 17:42:07 +02:00
height: 70%;
2020-04-29 17:18:49 +02:00
}
</style>
2015-07-14 19:23:35 +02:00
</head>
<body>
2016-11-29 11:18:21 +01:00
<div class="container">
2020-04-29 15:43:06 +02:00
<h1>Turtle Web Editor</h1>
2020-04-29 22:12:36 +02:00
<p>Online text editor with <a href="https://en.wikipedia.org/wiki/Turtle_(syntax)">Turtle</a> syntax highlighting and validation. This is a remix of <a href="https://github.com/IDLabResearch/TurtleValidator">IDLab Turtle Validator</a> using <a href="https://codemirror.net">Codemirror</a>. The code is <a href="https://github.com/felixlohmeier/turtle-web-editor">on GitHub</a>.
2016-11-29 11:18:21 +01:00
<form>
<div class="form-group">
2020-04-29 15:22:06 +02:00
<textarea class="area" id="ta_turtle"></textarea>
2016-11-29 11:18:21 +01:00
</div>
<div class="form-group">
2020-04-29 16:22:45 +02:00
<input type="button" id="btn_example" class="btn btn-default" value="Load Example"/>
2016-11-29 11:18:21 +01:00
<input type="button" id="btn_validate" class="btn btn-default" value="Validate!"/>
2020-04-29 16:22:45 +02:00
<input type="button" id="btn_download" class="btn btn-default" value="Download"/>
2016-11-29 11:18:21 +01:00
</div>
</form>
<ul id="errors"></ul>
<ul id="warnings"></ul>
<p id="results"></p>
<script src="js/app.js"></script>
</div>
2015-07-14 19:23:35 +02:00
</body>
</html>