1
1
mirror of https://github.com/github/semantic.git synced 2024-12-20 21:31:48 +03:00
semantic/prototype/UI/index.html

142 lines
4.0 KiB
HTML
Raw Normal View History

<!doctype html>
<html>
<head>
<title>semantic-diff</title>
2015-10-09 22:27:44 +03:00
<style type="text/css">
2015-10-21 18:48:46 +03:00
body {
margin: 0;
padding: 0;
}
2015-10-13 18:07:40 +03:00
.insert {
background-color: #eaffea;
2015-10-13 18:43:17 +03:00
outline: 1px solid #c1e9c1;
2015-10-13 18:24:55 +03:00
margin-left: 50%;
2015-10-13 18:07:40 +03:00
}
.delete {
background-color: #ffecec;
2015-10-13 18:43:17 +03:00
outline: 1px solid #f1c0c0;
2015-10-13 18:24:55 +03:00
margin-right: 50%;
2015-10-13 18:07:40 +03:00
}
2015-10-13 18:25:20 +03:00
.replace {
2015-10-13 20:17:18 +03:00
background-color: #eee;
2015-10-13 18:25:20 +03:00
}
2015-10-09 22:27:44 +03:00
</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)) {
2015-10-09 21:36:18 +03:00
callback(JSON.parse(request.responseText));
}
};
request.send(null);
}
function wrap(tagName, element) {
2015-10-13 18:22:56 +03:00
if (element == null) { return null; }
var node = document.createElement(tagName);
node.appendChild(element);
return node;
}
2015-10-21 22:50:06 +03:00
function Delete(before) {
this.before = before;
return this;
}
function Insert(after) {
this.after = after;
return this;
}
function Replace(before, after) {
this.before = before;
this.after = after;
return this;
}
2015-10-21 23:19:29 +03:00
function Term(json, a, b) {
this.range = json.extract;
this.syntax = syntax(json.unwrap, a, b, function(x, a, b) { return new Term(x, a, b); });
2015-10-21 22:58:00 +03:00
return this;
}
2015-10-21 22:50:13 +03:00
function toDOM(view) {
if (view instanceof Delete) {
var element = document.createElement("div");
element.classList.add("delete");
element.appendChild(toDOM(view.before));
return element;
2015-10-21 22:50:13 +03:00
}
2015-10-21 23:05:34 +03:00
if (view instanceof Term) {
var element = document.createElement("div");
element.classList.add("term");
if (view.syntax instanceof Indexed) {
2015-10-21 23:07:39 +03:00
for (i in view.syntax) {
element.appendChild(toDOM(view.syntax[i]));
}
} else if (view.syntax instanceof Keyed) {
2015-10-21 23:07:47 +03:00
for (k in view.syntax) {
element.appendChild(toDOM(view.syntax[k]));
}
2015-10-21 23:07:39 +03:00
}
2015-10-21 23:05:34 +03:00
return element;
}
2015-10-21 22:50:13 +03:00
}
function patch(patch, a, b) {
2015-10-21 23:19:29 +03:00
if (patch.delete != null) { return new Delete(new Term(patch.delete, a, b)); }
if (patch.insert != null) { return new Insert(new Term(patch.insert, a, b)); }
if (patch.replace != null) { return new Replace(new Term(patch.replace.before, a, b), new Term(patch.replace.after, a, b)); }
2015-10-21 18:49:03 +03:00
}
2015-10-21 23:16:11 +03:00
function Indexed(array, a, b, continuation) {
this.values = [];
for (index in array) {
2015-10-21 23:16:11 +03:00
this.values.push(continuation(array[index], a, b));
}
2015-10-21 23:16:11 +03:00
return this;
}
2015-10-21 23:16:11 +03:00
function Keyed(object, a, b, continuation) {
this.values = {};
for (key in object) {
2015-10-21 23:16:11 +03:00
this.values[key] = continuation(object[key], a, b);
}
2015-10-21 23:16:11 +03:00
return this;
}
2015-10-21 23:22:19 +03:00
function Leaf(object, a, b) {
return this;
}
function syntax(json, a, b, continuation) {
2015-10-21 23:16:11 +03:00
if (json instanceof Array) { return new Indexed(json, a, b, continuation); }
if (json instanceof Object) { return new Keyed(json, a, b, continuation); }
2015-10-21 23:22:19 +03:00
return new Leaf(json, a, b);
}
function diff(json, a, b) {
if (json.pure != null) { return patch(json.pure, a, b); }
if (json.roll != null) { return syntax(json.roll, a, b, diff); }
}
</script>
</head>
<body>
2015-10-13 18:05:13 +03:00
<div id="diff"></div>
<script type="text/javascript">
2015-10-21 00:52:04 +03:00
loadJSON('diff.json', function (json) {
2015-10-21 21:08:35 +03:00
console.log(json.diff);
var model = diff(json.diff, json.a, json.b);
var dom = toDOM(model);
var root = document.getElementById("diff");
root.appendChild(dom);
});
</script>
</body>
</html>