1
1
mirror of https://github.com/github/semantic.git synced 2024-12-19 12:51:52 +03:00
semantic/prototype/UI/index.html
2015-10-21 12:59:47 -04:00

109 lines
2.9 KiB
HTML

<!doctype html>
<html>
<head>
<title>semantic-diff</title>
<style type="text/css">
body {
margin: 0;
padding: 0;
}
#before {
width: 50%;
background: #ffecec;
float: left;
white-space: pre-wrap;
}
#after {
width: 50%;
background: #eaffea;
float: right;
white-space: pre-wrap;
}
.insert {
background-color: #eaffea;
outline: 1px solid #c1e9c1;
margin-left: 50%;
}
.delete {
background-color: #ffecec;
outline: 1px solid #f1c0c0;
margin-right: 50%;
}
.replace {
background-color: #eee;
}
</style>
<script type="text/javascript">
function loadJSON(path, callback) {
var request = new XMLHttpRequest();
request.overrideMimeType("application/json");
request.open('GET', '' + path, true);
request.onreadystatechange = function () {
if (request.readyState == 4 && (request.status == "200" || request.status == 0)) {
callback(JSON.parse(request.responseText));
}
};
request.send(null);
}
function wrap(tagName, element) {
if (element == null) { return null; }
var node = document.createElement(tagName);
node.appendChild(element);
return node;
}
function term(term, element) {
if (term["extract"] == null || term["unwrap"] == null) { return; }
// fixme: do something…?
}
function patch(patch) {
var before = document.getElementById("before");
var after = document.getElementById("after");
// fixme: handle annotated terms
if (patch["delete"] != null) {}
if (patch["insert"] != null) {}
if (patch["replace"] != null) {}
}
function indexed(array, continuation) {
for (index in array) {
continuation(array[index]);
}
}
function keyed(object, continuation) {
for (key in object) {
continuation(object[key]);
}
}
function syntax(json, continuation) {
if (json instanceof Array) { return indexed(json, continuation); }
if (json instanceof Object) { return keyed(json, continuation); }
// fixme: handle leaves
}
function diff(json) {
if (json["pure"] != null) { return patch(json["pure"]); }
if (json["roll"] != null) { return syntax(json["roll"], diff); }
}
</script>
</head>
<body>
<div id="before"></div>
<div id="after"></div>
<div id="diff"></div>
<script type="text/javascript">
loadJSON('diff.json', function (json) {
document.getElementById("before").textContent = json.a;
document.getElementById("after").textContent = json.b;
console.log(json["diff"]);
diff(json["diff"]);
});
</script>
</body>
</html>