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

243 lines
8.0 KiB
HTML

<!doctype html>
<html>
<head>
<title>semantic-diff</title>
<style type="text/css">
#before, #after {
width: 50%;
}
#before {
margin-right: 50%;
float: left;
background-color: #ffecec;
}
#after {
margin-left: 50%;
float: right;
background-color: #eaffea;
}
body {
margin: 0;
padding: 0;
font-family: monospace;
}
.insert {
background-color: #eaffea;
outline: 1px solid #c1e9c1;
}
.delete {
background-color: #ffecec;
outline: 1px solid #f1c0c0;
}
.replace {
background-color: #eee;
}
#diff div, #diff ul, #diff li, #diff dl, #diff dd, #diff span {
white-space: pre-wrap;
display: inline;
margin: 0;
padding: 0;
}
#diff dt {
display: none;
}
</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 Patch(patch) {
if (patch.delete != null) { this.before = new Term(patch.delete); }
if (patch.insert != null) { this.after = new Term(patch.insert); }
if (patch.replace != null) {
this.before = new Term(patch.replace.before);
this.after = new Term(patch.replace.after);
}
return this;
}
function Term(json) {
this.range = json.extract;
this.unwrap = new Syntax(json.unwrap, function(x) { return new Term(x); });
return this;
}
// forall a. Term -> (Syntax a -> a) -> a
Term.prototype.cata = function(transform) {
return transform(this.unwrap.map(function(term) { term.cata(transform) }))
}
function toDOM(model, stateName, source) {
var element;
if (model instanceof Delete) {
element = document.createElement("div");
element.classList.add("patch");
element.classList.add("delete");
element.appendChild(toDOM(model.before));
}
if (model instanceof Insert) {
element = document.createElement("div");
element.classList.add("patch");
element.classList.add("insert");
element.appendChild(toDOM(model.after));
}
if (model instanceof Replace) {
element = document.createElement("div");
element.classList.add("patch");
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);
}
if (model instanceof Diff) {
element = document.createElement("div");
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));
}
}
if (model instanceof Indexed) {
element = document.createElement("ul");
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)));
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)));
} else {
for (i in model.values) {
element.appendChild(wrap("li", toDOM(model.values[i])));
}
}
}
if (model instanceof Keyed) {
element = document.createElement("dl");
if (model.source != null && model.range != null) {
var values = [];
for (k in model.values) {
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];
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)));
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])));
}
}
}
return element;
}
function Dictionary(object) {
this.values = {};
for (key in object) {
this.values[key] = object[key];
}
return this;
}
// forall a b. Dictionary String a -> (a -> b) -> Dictionary String b
Dictionary.prototype.map = function(transform) {
var copy = new Dictionary();
for (key in this.values) {
copy.values[key] = transform(this.values[key], key);
}
return copy;
}
function Syntax(json, continuation) {
if (json.indexed != null) { this.indexed = json.map(continuation); }
if (json.keyed != null) { this.keyed = (new Dictionary(json)).map(continuation); }
if (json.leaf != null) { this.leaf = json; }
return this;
}
// forall a b. Syntax a -> (a -> b) -> Syntax b
Syntax.prototype.map = function(transform) {
if (this.indexed != null) { return new Syntax(this, transform); }
if (this.keyed != null) { return new Syntax(this, transform); }
if (this.leaf != null) { return new Syntax(this, transform); }
}
function Diff(json) {
if (json.pure != null) {
this.pure = new Patch(json.pure);
}
if (json.roll != null) {
this.ranges = json.roll.extract;
this.roll = new Syntax(json.roll.unwrap, function(x) { return new Diff(x); });
}
return this;
}
</script>
</head>
<body>
<div id="before"></div>
<div id="after"></div>
<script type="text/javascript">
loadJSON('diff.json', function (json) {
var model = new Diff(json.diff);
document.getElementById("before").appendChild(toDOM(model, "before", json["before"]));
document.getElementById("after").appendChild(toDOM(model, "after", json["after"]));
});
</script>
</body>
</html>