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

98 lines
2.9 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
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 {
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-24 04:29:02 +03:00
background-color: #ffffec;
outline: 1px solid #e9e9c0;
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-27 18:09:48 +03:00
<script type="text/javascript" src="dictionary.js"></script>
2015-10-27 18:11:45 +03:00
<script type="text/javascript" src="diff.js"></script>
2015-10-27 18:12:27 +03:00
<script type="text/javascript" src="dom.js"></script>
2015-10-27 18:09:16 +03:00
<script type="text/javascript" src="patch.js"></script>
2015-10-27 18:10:38 +03:00
<script type="text/javascript" src="syntax.js"></script>
<script type="text/javascript" src="term.js"></script>
<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);
}
</script>
</head>
<body>
2015-10-24 04:19:19 +03:00
<div id="before" class="diff"></div>
<div id="after" class="diff"></div>
<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);
var before = diff.map(function(value) {
2015-10-24 04:25:55 +03:00
var element;
if (value.before != null) {
element = termToDOM(value.before, "before", json["before"]);
element.classList.add("delete");
2015-10-24 04:29:21 +03:00
if (value.after != null) {
element.classList.add("replace");
}
2015-10-24 04:25:55 +03:00
}
return element || "";
2015-10-24 02:08:10 +03:00
});
var after = diff.map(function(value) {
2015-10-24 04:27:11 +03:00
var element;
if (value.after != null) {
element = termToDOM(value.after, "after", json["after"]);
element.classList.add("insert")
2015-10-24 04:29:21 +03:00
if (value.before != null) {
element.classList.add("replace");
}
2015-10-24 04:27:11 +03:00
}
return element || "";
});
document.getElementById("before").appendChild(diffToDOM(before, "before", json["before"]));
document.getElementById("after").appendChild(diffToDOM(after, "after", json["after"]));
});
</script>
</body>
</html>