1
1
mirror of https://github.com/github/semantic.git synced 2024-12-19 04:41:47 +03:00
semantic/prototype/UI/index.html

262 lines
8.2 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-23 23:53:02 +03:00
#before, #after {
2015-10-23 21:00:25 +03:00
width: 50%;
}
2015-10-23 23:53:02 +03:00
#before {
2015-10-23 21:00:25 +03:00
margin-right: 50%;
float: left;
background-color: #ffecec;
}
2015-10-23 23:53:02 +03:00
#after {
2015-10-23 21:00:25 +03:00
margin-left: 50%;
float: right;
background-color: #eaffea;
}
2015-10-21 18:48:46 +03:00
body {
margin: 0;
padding: 0;
2015-10-22 01:06:45 +03:00
font-family: monospace;
2015-10-21 18:48:46 +03:00
}
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:07:40 +03:00
}
.delete {
background-color: #ffecec;
2015-10-13 18:43:17 +03:00
outline: 1px solid #f1c0c0;
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-22 00:34:10 +03:00
2015-10-22 01:07:02 +03:00
#diff div, #diff ul, #diff li, #diff dl, #diff dd, #diff span {
2015-10-22 00:34:10 +03:00
white-space: pre-wrap;
2015-10-22 00:35:12 +03:00
display: inline;
2015-10-22 00:53:57 +03:00
margin: 0;
padding: 0;
2015-10-22 00:34:10 +03:00
}
2015-10-22 01:07:08 +03:00
#diff dt {
display: none;
}
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-23 20:48:44 +03:00
function Patch(patch) {
if (patch.delete != null) { this.patch = new Delete(patch.delete); }
if (patch.insert != null) { this.patch = new Insert(patch.insert); }
if (patch.replace != null) { this.patch = new Replace(patch.replace.before, patch.replace.after); }
return this;
2015-10-23 20:47:33 +03:00
}
function Delete(before) {
this.before = new Term(before);
2015-10-21 22:50:06 +03:00
return this;
}
function Insert(after) {
this.after = new Term(after);
2015-10-21 22:50:06 +03:00
return this;
}
function Replace(before, after) {
this.before = new Term(before);
this.after = new Term(after);
2015-10-21 22:50:06 +03:00
return this;
}
2015-10-23 20:32:54 +03:00
function Term(json) {
2015-10-21 23:19:29 +03:00
this.range = json.extract;
2015-10-23 23:56:39 +03:00
this.unwrap = syntax(json.unwrap, function(x) { return new Term(x); });
2015-10-21 22:58:00 +03:00
return this;
}
2015-10-23 23:53:02 +03:00
function toDOM(model, stateName, source) {
2015-10-21 23:43:18 +03:00
var element;
2015-10-21 23:25:46 +03:00
if (model instanceof Delete) {
2015-10-21 23:43:18 +03:00
element = document.createElement("div");
2015-10-22 00:37:28 +03:00
element.classList.add("patch");
2015-10-21 22:50:13 +03:00
element.classList.add("delete");
2015-10-21 23:25:46 +03:00
element.appendChild(toDOM(model.before));
2015-10-21 22:50:13 +03:00
}
2015-10-21 23:05:34 +03:00
2015-10-21 23:39:55 +03:00
if (model instanceof Insert) {
2015-10-21 23:43:18 +03:00
element = document.createElement("div");
2015-10-22 00:37:28 +03:00
element.classList.add("patch");
2015-10-21 23:39:55 +03:00
element.classList.add("insert");
element.appendChild(toDOM(model.after));
}
2015-10-21 23:40:02 +03:00
if (model instanceof Replace) {
2015-10-21 23:43:18 +03:00
element = document.createElement("div");
2015-10-22 00:37:28 +03:00
element.classList.add("patch");
2015-10-21 23:40:02 +03:00
element.classList.add("replace");
var before = toDOM(model.before);
before.classList.add("delete");
element.appendChild(before);
var after = toDOM(model.after);
after.classList.add("insert");
element.appendChild(after);
2015-10-21 23:40:02 +03:00
}
2015-10-21 23:25:46 +03:00
if (model instanceof Term) {
2015-10-21 23:43:18 +03:00
element = document.createElement("div");
2015-10-21 23:05:34 +03:00
element.classList.add("term");
2015-10-23 23:56:39 +03:00
element.appendChild(toDOM(model.unwrap));
2015-10-21 23:05:34 +03:00
}
2015-10-21 23:29:42 +03:00
if (model instanceof Diff) {
2015-10-21 23:43:18 +03:00
element = document.createElement("div");
2015-10-21 23:29:42 +03:00
element.classList.add("diff");
if (model.pure != null) {
element.classList.add("pure");
element.appendChild(toDOM(model.pure));
} else if(model.roll != null) {
element.classList.add("roll");
element.appendChild(toDOM(model.roll));
}
}
2015-10-21 23:31:53 +03:00
2015-10-21 23:37:08 +03:00
if (model instanceof Indexed) {
2015-10-21 23:43:18 +03:00
element = document.createElement("ul");
2015-10-22 00:32:48 +03:00
if (model.source != null && model.range != null) {
var previous = model.range[0];
for (i in model.values) {
var value = model.values[i];
element.appendChild(document.createTextNode(model.source.substr(previous, value.range[0] - previous)));
2015-10-22 00:51:57 +03:00
element.appendChild(wrap("li", toDOM(value)));
previous = value.range[0] + value.range[1];
}
element.appendChild(document.createTextNode(model.source.substr(previous, model.range[0] + model.range[1] - previous)));
2015-10-22 00:32:48 +03:00
} else {
for (i in model.values) {
element.appendChild(wrap("li", toDOM(model.values[i])));
}
2015-10-21 23:31:53 +03:00
}
}
2015-10-21 23:32:21 +03:00
2015-10-21 23:37:08 +03:00
if (model instanceof Keyed) {
2015-10-21 23:43:18 +03:00
element = document.createElement("dl");
if (model.source != null && model.range != null) {
2015-10-22 00:46:07 +03:00
var values = [];
for (k in model.values) {
2015-10-22 00:46:07 +03:00
values.push([ k, model.values[k] ]);
}
values.sort(function(a, b) {
if (a[1].range[0] < b[1].range[0]) {
return -1;
} else if (a[1].range[0] > b[1].range[0]) {
return 1;
}
return 0;
});
var previous = model.range[0];
2015-10-22 00:51:57 +03:00
for (i in values) {
var k = values[i][0];
var value = values[i][1];
element.appendChild(document.createTextNode(model.source.substr(previous, value.range[0] - previous)));
2015-10-22 00:51:57 +03:00
var dt = document.createElement("dt");
dt.textContent = k;
element.appendChild(dt);
element.appendChild(wrap("dd", toDOM(value)));
previous = value.range[0] + value.range[1];
}
element.appendChild(document.createTextNode(model.source.substr(previous, model.range[0] + model.range[1] - previous)));
} else {
for (k in model.values) {
var dt = document.createElement("dt");
dt.textContent = k;
element.appendChild(dt);
element.appendChild(wrap("dd", toDOM(model.values[k])));
}
}
}
2015-10-21 23:37:08 +03:00
if (model instanceof Leaf) {
2015-10-21 23:43:18 +03:00
element = document.createElement("span");
2015-10-22 00:28:38 +03:00
if (model.source != null && model.range != null) {
2015-10-22 00:31:56 +03:00
element.textContent = model.source.substr(model.range[0], model.range[1]);
2015-10-22 00:28:38 +03:00
}
2015-10-21 23:32:21 +03:00
// ?
}
2015-10-21 23:43:18 +03:00
return element;
2015-10-21 22:50:13 +03:00
}
function Indexed(array, continuation) {
2015-10-21 23:16:11 +03:00
this.values = [];
for (index in array) {
this.values.push(continuation(array[index]));
}
2015-10-21 23:16:11 +03:00
return this;
}
2015-10-24 00:16:19 +03:00
function Dictionary(object) {
2015-10-21 23:16:11 +03:00
this.values = {};
for (key in object) {
2015-10-24 00:16:19 +03:00
this.values[key] = object[key];
}
2015-10-21 23:16:11 +03:00
return this;
}
function Leaf(object) {
2015-10-21 23:52:09 +03:00
this.value = object;
2015-10-21 23:22:19 +03:00
return this;
}
2015-10-23 23:54:49 +03:00
function Syntax(json, continuation) {
2015-10-24 00:18:54 +03:00
if (json instanceof Array) { this.indexed = json.map(continuation); }
else if (json instanceof Object) { this.keyed = (new Dictionary(json)).map(continuation); }
else this.leaf = json;
2015-10-23 23:54:49 +03:00
return this;
}
function Diff(json) {
2015-10-23 18:14:45 +03:00
if (json.pure != null) {
2015-10-23 20:48:44 +03:00
this.pure = new Patch(json.pure);
2015-10-23 18:14:45 +03:00
}
2015-10-23 18:01:14 +03:00
if (json.roll != null) {
2015-10-23 18:04:03 +03:00
this.ranges = json.roll.extract;
2015-10-23 23:54:49 +03:00
this.roll = new Syntax(json.roll.unwrap, function(x) { return new Diff(x); });
2015-10-23 18:01:14 +03:00
}
2015-10-21 23:24:56 +03:00
return this;
}
</script>
</head>
<body>
2015-10-23 23:53:02 +03:00
<div id="before"></div>
<div id="after"></div>
<script type="text/javascript">
2015-10-21 00:52:04 +03:00
loadJSON('diff.json', function (json) {
var model = new Diff(json.diff);
2015-10-23 23:53:02 +03:00
document.getElementById("before").appendChild(toDOM(model, "before", json["before"]));
document.getElementById("after").appendChild(toDOM(model, "after", json["after"]));
});
</script>
</body>
</html>