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 >
