2015-10-09 21:31:06 +03:00
|
|
|
<!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
|
|
|
float: left;
|
|
|
|
}
|
2015-10-23 23:53:02 +03:00
|
|
|
#after {
|
2015-10-23 21:00:25 +03:00
|
|
|
float: right;
|
|
|
|
}
|
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 {
|
2015-10-13 18:43:25 +03:00
|
|
|
background-color: #eaffea;
|
2015-10-13 18:43:17 +03:00
|
|
|
outline: 1px solid #c1e9c1;
|
2015-10-13 18:07:40 +03:00
|
|
|
}
|
|
|
|
.delete {
|
2015-10-13 18:43:25 +03:00
|
|
|
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-24 04:19:19 +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
|
|
|
|
2015-10-24 04:19:19 +03:00
|
|
|
.diff dt {
|
2015-10-22 01:07:08 +03:00
|
|
|
display: none;
|
|
|
|
}
|
2015-10-09 22:27:44 +03:00
|
|
|
</style>
|
2015-10-09 21:31:06 +03:00
|
|
|
<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));
|
2015-10-09 21:31:06 +03:00
|
|
|
}
|
|
|
|
};
|
|
|
|
request.send(null);
|
|
|
|
}
|
2015-10-13 16:47:47 +03:00
|
|
|
|
2015-10-13 18:10:54 +03:00
|
|
|
function wrap(tagName, element) {
|
2015-10-13 18:22:56 +03:00
|
|
|
if (element == null) { return null; }
|
2015-10-13 18:10:54 +03:00
|
|
|
var node = document.createElement(tagName);
|
|
|
|
node.appendChild(element);
|
|
|
|
return node;
|
|
|
|
}
|
|
|
|
|
2015-10-23 20:48:44 +03:00
|
|
|
function Patch(patch) {
|
2015-10-24 03:37:58 +03:00
|
|
|
if (patch.delete != null) { this.before = termFromJSON(patch.delete); }
|
|
|
|
if (patch.insert != null) { this.after = termFromJSON(patch.insert); }
|
2015-10-24 01:26:24 +03:00
|
|
|
if (patch.replace != null) {
|
2015-10-24 03:37:58 +03:00
|
|
|
this.before = termFromJSON(patch.replace.before);
|
|
|
|
this.after = termFromJSON(patch.replace.after);
|
2015-10-24 01:26:24 +03:00
|
|
|
}
|
2015-10-21 22:50:06 +03:00
|
|
|
return this;
|
|
|
|
}
|
|
|
|
|
2015-10-24 03:37:58 +03:00
|
|
|
function termFromJSON(json) {
|
2015-10-24 03:51:31 +03:00
|
|
|
return new Term({ extract: json.extract, unwrap: new Syntax(json.unwrap, function(x) { return termFromJSON(x); }) });
|
2015-10-24 03:37:58 +03:00
|
|
|
}
|
|
|
|
|
|
|
|
function Term(object) {
|
|
|
|
this.range = object.extract;
|
|
|
|
this.unwrap = object.unwrap;
|
2015-10-21 22:58:00 +03:00
|
|
|
return this;
|
|
|
|
}
|
|
|
|
|
2015-10-24 03:23:53 +03:00
|
|
|
/// Term -> String -> DOM
|
2015-10-24 04:22:28 +03:00
|
|
|
function termToDOM(term, which, source) {
|
|
|
|
return rangeAndSyntaxToDOM(term.range, term.unwrap, source, function(term) { return term.range; }, function(term) { return termToDOM(term, which, source); });
|
2015-10-24 03:23:53 +03:00
|
|
|
}
|
|
|
|
|
2015-10-24 04:05:20 +03:00
|
|
|
/// Diff -> String -> String -> DOM
|
|
|
|
function diffToDOM(diff, which, source) {
|
2015-10-24 04:19:37 +03:00
|
|
|
if (diff.pure != null) { return diff.pure; }
|
|
|
|
function getRange(diff) {
|
2015-10-24 04:05:20 +03:00
|
|
|
if (diff.pure != null) { return diff.pure["data-range"]; }
|
|
|
|
if (diff.roll != null) { return diff.roll.extract[which]; }
|
2015-10-24 04:19:37 +03:00
|
|
|
}
|
|
|
|
return rangeAndSyntaxToDOM(getRange(diff), diff.roll.unwrap, source, getRange, function(diff) { return diffToDOM(diff, which, source); })
|
2015-10-24 04:05:20 +03:00
|
|
|
}
|
|
|
|
|
|
|
|
/// Range -> Syntax a -> String -> (a -> Range) -> (a -> DOM) -> DOM
|
|
|
|
function rangeAndSyntaxToDOM(range, syntax, source, getRange, recur) {
|
2015-10-24 03:23:35 +03:00
|
|
|
recur = recur || function (term) { return rangeAndSyntaxToDOM(term.range, term.unwrap, source); }
|
2015-10-21 23:43:18 +03:00
|
|
|
var element;
|
2015-10-24 02:24:13 +03:00
|
|
|
if (syntax.leaf != null) {
|
|
|
|
element = document.createElement("span");
|
|
|
|
element.textContent = source.substr(range[0], range[1]);
|
|
|
|
} else if (syntax.indexed != null) {
|
|
|
|
element = document.createElement("ul");
|
|
|
|
var previous = range[0];
|
|
|
|
for (i in syntax.indexed) {
|
|
|
|
var child = syntax.indexed[i];
|
2015-10-24 04:19:43 +03:00
|
|
|
if (child.pure == "") continue;
|
2015-10-24 04:05:20 +03:00
|
|
|
var childRange = getRange(child);
|
|
|
|
element.appendChild(document.createTextNode(source.substr(previous, childRange[0] - previous)));
|
2015-10-24 02:24:13 +03:00
|
|
|
element.appendChild(wrap("li", recur(child)));
|
2015-10-24 04:05:20 +03:00
|
|
|
previous = childRange[0] + childRange[1];
|
2015-10-24 02:24:13 +03:00
|
|
|
}
|
|
|
|
element.appendChild(document.createTextNode(source.substr(previous, range[0] + range[1] - previous)));
|
|
|
|
} else if (syntax.keyed != null) {
|
|
|
|
element = document.createElement("dl");
|
|
|
|
var values = [];
|
|
|
|
for (k in syntax.keyed.values) {
|
2015-10-24 04:19:43 +03:00
|
|
|
if (syntax.keyed.values[k].pure == "") continue;
|
2015-10-24 02:24:13 +03:00
|
|
|
values.push([ k, syntax.keyed.values[k] ]);
|
|
|
|
}
|
|
|
|
values.sort(function(a, b) {
|
2015-10-24 04:05:20 +03:00
|
|
|
if (getRange(a[1])[0] < getRange(b[1])[0]) {
|
2015-10-24 02:24:13 +03:00
|
|
|
return -1;
|
2015-10-24 04:05:20 +03:00
|
|
|
} else if (getRange(a[1])[0] > getRange(b[1])[0]) {
|
2015-10-24 02:24:13 +03:00
|
|
|
return 1;
|
|
|
|
}
|
|
|
|
return 0;
|
|
|
|
});
|
2015-10-21 23:43:18 +03:00
|
|
|
|
2015-10-24 02:24:13 +03:00
|
|
|
var previous = range[0];
|
|
|
|
for (i in values) {
|
|
|
|
var pair = values[i];
|
|
|
|
var key = pair[0];
|
|
|
|
var child = pair[1];
|
2015-10-24 04:05:20 +03:00
|
|
|
var childRange = getRange(child);
|
|
|
|
element.appendChild(document.createTextNode(source.substr(previous, childRange[0] - previous)));
|
2015-10-24 02:24:13 +03:00
|
|
|
element.appendChild(wrap("dt", document.createTextNode(key)));
|
|
|
|
element.appendChild(wrap("dd", recur(child)));
|
2015-10-24 04:05:20 +03:00
|
|
|
previous = childRange[0] + childRange[1];
|
2015-10-24 02:24:13 +03:00
|
|
|
}
|
|
|
|
element.appendChild(document.createTextNode(source.substr(previous, range[0] + range[1] - previous)));
|
2015-10-21 22:50:13 +03:00
|
|
|
}
|
2015-10-24 04:05:30 +03:00
|
|
|
element["data-range"] = range;
|
2015-10-21 23:43:18 +03:00
|
|
|
return element;
|
2015-10-21 22:50:13 +03:00
|
|
|
}
|
|
|
|
|
2015-10-24 00:16:19 +03:00
|
|
|
function Dictionary(object) {
|
2015-10-21 23:16:11 +03:00
|
|
|
this.values = {};
|
2015-10-21 18:17:25 +03:00
|
|
|
for (key in object) {
|
2015-10-24 00:16:19 +03:00
|
|
|
this.values[key] = object[key];
|
2015-10-21 18:17:25 +03:00
|
|
|
}
|
2015-10-21 23:16:11 +03:00
|
|
|
return this;
|
2015-10-21 18:17:25 +03:00
|
|
|
}
|
2015-10-21 18:17:33 +03:00
|
|
|
|
2015-10-24 00:19:00 +03:00
|
|
|
// 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) {
|
2015-10-24 01:21:09 +03:00
|
|
|
copy.values[key] = transform(this.values[key], key);
|
2015-10-24 00:19:00 +03:00
|
|
|
}
|
|
|
|
return copy;
|
2015-10-21 23:22:19 +03:00
|
|
|
}
|
|
|
|
|
2015-10-23 23:54:49 +03:00
|
|
|
function Syntax(json, continuation) {
|
2015-10-24 02:22:14 +03:00
|
|
|
if (json.indexed != null) { this.indexed = json.indexed.map(continuation); }
|
2015-10-24 02:20:06 +03:00
|
|
|
if (json.keyed != null) { this.keyed = (new Dictionary(json.keyed)).map(continuation); }
|
2015-10-24 02:22:22 +03:00
|
|
|
if (json.leaf != null) { this.leaf = json.leaf; }
|
2015-10-23 23:54:49 +03:00
|
|
|
return this;
|
2015-10-21 18:17:33 +03:00
|
|
|
}
|
2015-10-21 18:59:48 +03:00
|
|
|
|
2015-10-24 00:19:07 +03:00
|
|
|
// forall a b. Syntax a -> (a -> b) -> Syntax b
|
|
|
|
Syntax.prototype.map = function(transform) {
|
2015-10-24 02:17:02 +03:00
|
|
|
if (this.leaf != null) { return new Syntax({ leaf: this.leaf }, transform); }
|
|
|
|
if (this.indexed != null) { return new Syntax({ indexed: this.indexed }, transform); }
|
2015-10-24 02:19:22 +03:00
|
|
|
if (this.keyed != null) { return new Syntax({ keyed: this.keyed.values }, transform); }
|
2015-10-24 00:19:07 +03:00
|
|
|
}
|
|
|
|
|
2015-10-24 01:54:24 +03:00
|
|
|
function diffFromJSON(json) {
|
|
|
|
if (json.pure != null) { return new Diff({ pure: new Patch(json.pure) }); }
|
|
|
|
if (json.roll != null) {
|
2015-10-24 01:55:30 +03:00
|
|
|
return new Diff({ roll: { extract: json.roll.extract, unwrap: new Syntax(json.roll.unwrap, function(x) { return diffFromJSON(x); }) } });
|
2015-10-24 01:54:24 +03:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2015-10-24 01:56:07 +03:00
|
|
|
function Diff(object) {
|
|
|
|
if (object.pure != null) { this.pure = object.pure; }
|
|
|
|
if (object.roll != null) { this.roll = object.roll; }
|
2015-10-21 23:24:56 +03:00
|
|
|
return this;
|
2015-10-21 18:59:48 +03:00
|
|
|
}
|
2015-10-24 01:59:24 +03:00
|
|
|
|
|
|
|
// forall a b. Diff a -> (a -> b) -> Diff b
|
|
|
|
Diff.prototype.map = function(transform) {
|
|
|
|
if (this.pure != null) { return new Diff({ pure: transform(this.pure) }); }
|
|
|
|
if (this.roll != null) {
|
|
|
|
return new Diff({
|
|
|
|
roll: {
|
2015-10-24 02:09:52 +03:00
|
|
|
extract: this.roll.extract,
|
|
|
|
unwrap: this.roll.unwrap.map(function(x) { return x.map(transform); })
|
2015-10-24 01:59:24 +03:00
|
|
|
}
|
|
|
|
});
|
|
|
|
}
|
|
|
|
}
|
2015-10-24 03:27:12 +03:00
|
|
|
|
|
|
|
// forall a. Diff a -> (Syntax a -> a) -> a
|
|
|
|
Diff.prototype.cata = function(transform) {
|
|
|
|
if (this.pure != null) { return this.pure; }
|
|
|
|
if (this.roll != null) {
|
|
|
|
return transform(this.roll.unwrap.map(function(diff) { return diff.cata(transform); }))
|
|
|
|
}
|
|
|
|
}
|
2015-10-09 21:31:06 +03:00
|
|
|
</script>
|
|
|
|
</head>
|
|
|
|
<body>
|
2015-10-24 04:19:19 +03:00
|
|
|
<div id="before" class="diff"></div>
|
|
|
|
<div id="after" class="diff"></div>
|
2015-10-09 21:31:06 +03:00
|
|
|
<script type="text/javascript">
|
2015-10-21 00:52:04 +03:00
|
|
|
loadJSON('diff.json', function (json) {
|
2015-10-24 02:08:10 +03:00
|
|
|
var diff = diffFromJSON(json.diff);
|
2015-10-24 04:05:51 +03:00
|
|
|
var before = diff.map(function(value) {
|
2015-10-24 04:19:25 +03:00
|
|
|
return value.before != null ? termToDOM(value.before, "before", json["before"]) : "";
|
2015-10-24 02:08:10 +03:00
|
|
|
});
|
2015-10-24 04:05:51 +03:00
|
|
|
var after = diff.map(function(value) {
|
2015-10-24 04:19:25 +03:00
|
|
|
return value.after != null ? termToDOM(value.after, "after", json["after"]) : "";
|
2015-10-24 04:05:51 +03:00
|
|
|
});
|
|
|
|
document.getElementById("before").appendChild(diffToDOM(before, "before", json["before"]));
|
|
|
|
document.getElementById("after").appendChild(diffToDOM(after, "after", json["after"]));
|
2015-10-09 21:31:06 +03:00
|
|
|
});
|
|
|
|
</script>
|
|
|
|
</body>
|
|
|
|
</html>
|