semantic/prototype/UI/index.html

<!doctype html>
<html>
  <head>
  	<title>semantic-diff</title>
    <style type="text/css">
    #before, #after {
        width: 50%;
    }
    #before {
        float: left;
    }
    #after {
        float: right;
    }
    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: #ffffec;
        outline: 1px solid #e9e9c0;
    }

    .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" src="term.js"></script>
    <script type="text/javascript" src="patch.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)) {
                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;
    }

    /// Diff -> String -> String -> DOM
    function diffToDOM(diff, which, source) {
        if (diff.pure != null) { return diff.pure; }
        function getRange(diff) {
            if (diff.pure != null) { return diff.pure["data-range"]; }
            if (diff.roll != null) { return diff.roll.extract[which]; }
        }
        return rangeAndSyntaxToDOM(getRange(diff), diff.roll.unwrap, source, getRange, function(diff) { return diffToDOM(diff, which, source); })
    }

    /// Range -> Syntax a -> String -> (a -> Range) -> (a -> DOM) -> DOM
    function rangeAndSyntaxToDOM(range, syntax, source, getRange, recur) {
        recur = recur || function (term) { return rangeAndSyntaxToDOM(term.range, term.unwrap, source); }
        var element;
        if (syntax.leaf != null) {
            element = document.createElement("span");
            element.textContent = source.substr(range[0], range[1]);
        } else if (syntax.indexed != null || syntax.fixed != null) {
            var values = syntax.indexed || syntax.fixed;
            element = document.createElement("ul");
            var previous = range[0];
            for (i in values) {
                var child = values[i];
                if (child.pure == "") continue;
                var childRange = getRange(child);
                element.appendChild(document.createTextNode(source.substr(previous, childRange[0] - previous)));
                element.appendChild(wrap("li", recur(child)));
                previous = childRange[0] + childRange[1];
            }
            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) {
                if (syntax.keyed.values[k].pure == "") continue;
                values.push([ k, syntax.keyed.values[k] ]);
            }
            values.sort(function(a, b) {
                if (getRange(a[1])[0] < getRange(b[1])[0]) {
                    return -1;
                } else if (getRange(a[1])[0] > getRange(b[1])[0]) {
                    return 1;
                }
                return 0;
            });

            var previous = range[0];
            for (i in values) {
                var pair = values[i];
                var key = pair[0];
                var child = pair[1];
                var childRange = getRange(child);
                element.appendChild(document.createTextNode(source.substr(previous, childRange[0] - previous)));
                element.appendChild(wrap("dt", document.createTextNode(key)));
                element.appendChild(wrap("dd", recur(child)));
                previous = childRange[0] + childRange[1];
            }
            element.appendChild(document.createTextNode(source.substr(previous, range[0] + range[1] - previous)));
        }
        element["data-range"] = range;
        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.indexed.map(continuation); }
        if (json.fixed != null) { this.fixed = json.fixed.map(continuation); }
        if (json.keyed != null) { this.keyed = (new Dictionary(json.keyed)).map(continuation); }
        if (json.leaf != null) { this.leaf = json.leaf; }
        return this;
    }

    // forall a b. Syntax a -> (a -> b) -> Syntax b
    Syntax.prototype.map = function(transform) {
        if (this.leaf != null) { return new Syntax({ leaf: this.leaf }, transform); }
        if (this.indexed != null) { return new Syntax({ indexed: this.indexed }, transform); }
        if (this.fixed != null) { return new Syntax({ fixed: this.fixed }, transform); }
        if (this.keyed != null) { return new Syntax({ keyed: this.keyed.values }, transform); }
    }

    function diffFromJSON(json) {
        if (json.pure != null) { return new Diff({ pure: new Patch(json.pure) }); }
        if (json.roll != null) {
            return new Diff({ roll: { extract: json.roll.extract, unwrap: new Syntax(json.roll.unwrap, function(x) { return diffFromJSON(x); }) } });
        }
    }

    function Diff(object) {
        if (object.pure != null) { this.pure = object.pure; }
        if (object.roll != null) { this.roll = object.roll; }
        return this;
    }

    // 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: {
                    extract: this.roll.extract,
                    unwrap: this.roll.unwrap.map(function(x) { return x.map(transform); })
                }
            });
        }
    }

    // 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); }))
        }
    }
    </script>
  </head>
  <body>
    <div id="before" class="diff"></div>
    <div id="after" class="diff"></div>
    <script type="text/javascript">
    loadJSON('diff.json', function (json) {
        var diff = diffFromJSON(json.diff);
        var before = diff.map(function(value) {
            var element;
            if (value.before != null) {
                element = termToDOM(value.before, "before", json["before"]);
                element.classList.add("delete");
                if (value.after != null) {
                    element.classList.add("replace");
                }
            }
            return element || "";
        });
        var after = diff.map(function(value) {
            var element;
            if (value.after != null) {
                element = termToDOM(value.after, "after", json["after"]);
                element.classList.add("insert")
                if (value.before != null) {
                    element.classList.add("replace");
                }
            }
            return element || "";
        });
        document.getElementById("before").appendChild(diffToDOM(before, "before", json["before"]));
        document.getElementById("after").appendChild(diffToDOM(after, "after", json["after"]));
    });
    </script>
  </body>
</html>
Add a simple scaffold web page loading the doubt-swift JSON output fixture. 2015-10-09 21:31:06 +03:00			`<!doctype html>`
			`<html>`
			`<head>`
			`<title>semantic-diff</title>`
Add left/right divs. 2015-10-09 22:27:44 +03:00			`<style type="text/css">`
Rename left/right to before/after. 2015-10-23 23:53:02 +03:00			`#before, #after {`
Re-add the left/right column divs. 2015-10-23 21:00:25 +03:00			`width: 50%;`
			`}`
Rename left/right to before/after. 2015-10-23 23:53:02 +03:00			`#before {`
Re-add the left/right column divs. 2015-10-23 21:00:25 +03:00			`float: left;`
			`}`
Rename left/right to before/after. 2015-10-23 23:53:02 +03:00			`#after {`
Re-add the left/right column divs. 2015-10-23 21:00:25 +03:00			`float: right;`
			`}`
No margin/padding. 2015-10-21 18:48:46 +03:00			`body {`
			`margin: 0;`
			`padding: 0;`
Monospace. 2015-10-22 01:06:45 +03:00			`font-family: monospace;`
No margin/padding. 2015-10-21 18:48:46 +03:00			`}`
Style insertions/deletions a little. 2015-10-13 18:07:40 +03:00			`.insert {`
Background colours for insertions/deletions. 2015-10-13 18:43:25 +03:00			`background-color: #eaffea;`
Change up the outline colours. 2015-10-13 18:43:17 +03:00			`outline: 1px solid #c1e9c1;`
Style insertions/deletions a little. 2015-10-13 18:07:40 +03:00			`}`
			`.delete {`
Background colours for insertions/deletions. 2015-10-13 18:43:25 +03:00			`background-color: #ffecec;`
Change up the outline colours. 2015-10-13 18:43:17 +03:00			`outline: 1px solid #f1c0c0;`
Style insertions/deletions a little. 2015-10-13 18:07:40 +03:00			`}`
HIghlight replacements. 2015-10-13 18:25:20 +03:00			`.replace {`
Replacements are yellow. 2015-10-24 04:29:02 +03:00			`background-color: #ffffec;`
			`outline: 1px solid #e9e9c0;`
HIghlight replacements. 2015-10-13 18:25:20 +03:00			`}`
Respect source whitespace in #diff. 2015-10-22 00:34:10 +03:00
Use classes to signal diffs. 2015-10-24 04:19:19 +03:00			`.diff div, .diff ul, .diff li, .diff dl, .diff dd, .diff span {`
Respect source whitespace in #diff. 2015-10-22 00:34:10 +03:00			`white-space: pre-wrap;`
Diff elements are displayed inline. 2015-10-22 00:35:12 +03:00			`display: inline;`
No margin or padding on diff elements. 2015-10-22 00:53:57 +03:00			`margin: 0;`
			`padding: 0;`
Respect source whitespace in #diff. 2015-10-22 00:34:10 +03:00			`}`
No really, hide terms. 2015-10-22 01:07:08 +03:00
Use classes to signal diffs. 2015-10-24 04:19:19 +03:00			`.diff dt {`
No really, hide terms. 2015-10-22 01:07:08 +03:00			`display: none;`
			`}`
Add left/right divs. 2015-10-09 22:27:44 +03:00			`</style>`
Term is in its own file. 2015-10-27 18:08:28 +03:00			`<script type="text/javascript" src="term.js"></script>`
Patch is in its own file. 2015-10-27 18:09:16 +03:00			`<script type="text/javascript" src="patch.js"></script>`
Add a simple scaffold web page loading the doubt-swift JSON output fixture. 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)) {`
Parse the response text. 2015-10-09 21:36:18 +03:00			`callback(JSON.parse(request.responseText));`
Add a simple scaffold web page loading the doubt-swift JSON output fixture. 2015-10-09 21:31:06 +03:00			`}`
			`};`
			`request.send(null);`
			`}`
Add a function doing faux sum typing on JSON. 2015-10-13 16:47:47 +03:00
Add a function to wrap a node in another node. 2015-10-13 18:10:54 +03:00			`function wrap(tagName, element) {`
Only wrap elements that exist. 2015-10-13 18:22:56 +03:00			`if (element == null) { return null; }`
Add a function to wrap a node in another node. 2015-10-13 18:10:54 +03:00			`var node = document.createElement(tagName);`
			`node.appendChild(element);`
			`return node;`
			`}`

Get ranges for children. 2015-10-24 04:05:20 +03:00			`/// Diff -> String -> String -> DOM`
			`function diffToDOM(diff, which, source) {`
Map ranges and stuff correctly. 2015-10-24 04:19:37 +03:00			`if (diff.pure != null) { return diff.pure; }`
			`function getRange(diff) {`
Get ranges for children. 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]; }`
Map ranges and stuff correctly. 2015-10-24 04:19:37 +03:00			`}`
			`return rangeAndSyntaxToDOM(getRange(diff), diff.roll.unwrap, source, getRange, function(diff) { return diffToDOM(diff, which, source); })`
Get ranges for children. 2015-10-24 04:05:20 +03:00			`}`

			`/// Range -> Syntax a -> String -> (a -> Range) -> (a -> DOM) -> DOM`
			`function rangeAndSyntaxToDOM(range, syntax, source, getRange, recur) {`
Default recur parameter. 2015-10-24 03:23:35 +03:00			`recur = recur \|\| function (term) { return rangeAndSyntaxToDOM(term.range, term.unwrap, source); }`
Construct a single element. 2015-10-21 23:43:18 +03:00			`var element;`
Try to map terms into DOM. 2015-10-24 02:24:13 +03:00			`if (syntax.leaf != null) {`
			`element = document.createElement("span");`
			`element.textContent = source.substr(range[0], range[1]);`
Display Fixed nodes. 2015-10-26 16:35:54 +03:00			`} else if (syntax.indexed != null \|\| syntax.fixed != null) {`
			`var values = syntax.indexed \|\| syntax.fixed;`
Try to map terms into DOM. 2015-10-24 02:24:13 +03:00			`element = document.createElement("ul");`
			`var previous = range[0];`
Display Fixed nodes. 2015-10-26 16:35:54 +03:00			`for (i in values) {`
			`var child = values[i];`
Skip empty things. 2015-10-24 04:19:43 +03:00			`if (child.pure == "") continue;`
Get ranges for children. 2015-10-24 04:05:20 +03:00			`var childRange = getRange(child);`
			`element.appendChild(document.createTextNode(source.substr(previous, childRange[0] - previous)));`
Try to map terms into DOM. 2015-10-24 02:24:13 +03:00			`element.appendChild(wrap("li", recur(child)));`
Get ranges for children. 2015-10-24 04:05:20 +03:00			`previous = childRange[0] + childRange[1];`
Try to map terms into DOM. 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) {`
Skip empty things. 2015-10-24 04:19:43 +03:00			`if (syntax.keyed.values[k].pure == "") continue;`
Try to map terms into DOM. 2015-10-24 02:24:13 +03:00			`values.push([ k, syntax.keyed.values[k] ]);`
			`}`
			`values.sort(function(a, b) {`
Get ranges for children. 2015-10-24 04:05:20 +03:00			`if (getRange(a[1])[0] < getRange(b[1])[0]) {`
Try to map terms into DOM. 2015-10-24 02:24:13 +03:00			`return -1;`
Get ranges for children. 2015-10-24 04:05:20 +03:00			`} else if (getRange(a[1])[0] > getRange(b[1])[0]) {`
Try to map terms into DOM. 2015-10-24 02:24:13 +03:00			`return 1;`
			`}`
			`return 0;`
			`});`
Construct a single element. 2015-10-21 23:43:18 +03:00
Try to map terms into DOM. 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];`
Get ranges for children. 2015-10-24 04:05:20 +03:00			`var childRange = getRange(child);`
			`element.appendChild(document.createTextNode(source.substr(previous, childRange[0] - previous)));`
Try to map terms into DOM. 2015-10-24 02:24:13 +03:00			`element.appendChild(wrap("dt", document.createTextNode(key)));`
			`element.appendChild(wrap("dd", recur(child)));`
Get ranges for children. 2015-10-24 04:05:20 +03:00			`previous = childRange[0] + childRange[1];`
Try to map terms into DOM. 2015-10-24 02:24:13 +03:00			`}`
			`element.appendChild(document.createTextNode(source.substr(previous, range[0] + range[1] - previous)));`
Map deletions into DOM. 2015-10-21 22:50:13 +03:00			`}`
Assign the range of patches. 2015-10-24 04:05:30 +03:00			`element["data-range"] = range;`
Construct a single element. 2015-10-21 23:43:18 +03:00			`return element;`
Map deletions into DOM. 2015-10-21 22:50:13 +03:00			`}`

Replaced `Keyed` with `Dictionary`. 2015-10-24 00:16:19 +03:00			`function Dictionary(object) {`
Indexed/Keyed construct objects. 2015-10-21 23:16:11 +03:00			`this.values = {};`
Add a function for processing keyed syntax elements. 2015-10-21 18:17:25 +03:00			`for (key in object) {`
Replaced `Keyed` with `Dictionary`. 2015-10-24 00:16:19 +03:00			`this.values[key] = object[key];`
Add a function for processing keyed syntax elements. 2015-10-21 18:17:25 +03:00			`}`
Indexed/Keyed construct objects. 2015-10-21 23:16:11 +03:00			`return this;`
Add a function for processing keyed syntax elements. 2015-10-21 18:17:25 +03:00			`}`
Add a function for processing syntax elements. 2015-10-21 18:17:33 +03:00
Map over dictionaries. 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) {`
Dictionary mapping passes a key to the transformation function. 2015-10-24 01:21:09 +03:00			`copy.values[key] = transform(this.values[key], key);`
Map over dictionaries. 2015-10-24 00:19:00 +03:00			`}`
			`return copy;`
Construct leaves. 2015-10-21 23:22:19 +03:00			`}`

Syntax is a type. 2015-10-23 23:54:49 +03:00			`function Syntax(json, continuation) {`
Correct Syntax.Indexed construction. 2015-10-24 02:22:14 +03:00			`if (json.indexed != null) { this.indexed = json.indexed.map(continuation); }`
Construct Fixed nodes. 2015-10-26 16:35:42 +03:00			`if (json.fixed != null) { this.fixed = json.fixed.map(continuation); }`
Correct Syntax.Keyed construction. 2015-10-24 02:20:06 +03:00			`if (json.keyed != null) { this.keyed = (new Dictionary(json.keyed)).map(continuation); }`
Correct Syntax.Leaf construction. 2015-10-24 02:22:22 +03:00			`if (json.leaf != null) { this.leaf = json.leaf; }`
Syntax is a type. 2015-10-23 23:54:49 +03:00			`return this;`
Add a function for processing syntax elements. 2015-10-21 18:17:33 +03:00			`}`
Call out to patch/syntax when processing a diff. 2015-10-21 18:59:48 +03:00
Map over Syntax. 2015-10-24 00:19:07 +03:00			`// forall a b. Syntax a -> (a -> b) -> Syntax b`
			`Syntax.prototype.map = function(transform) {`
Correct Syntax mapping. 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); }`
Map Fixed nodes. 2015-10-26 16:35:46 +03:00			`if (this.fixed != null) { return new Syntax({ fixed: this.fixed }, transform); }`
Correct Syntax.Keyed mapping. 2015-10-24 02:19:22 +03:00			`if (this.keyed != null) { return new Syntax({ keyed: this.keyed.values }, transform); }`
Map over Syntax. 2015-10-24 00:19:07 +03:00			`}`

Add a function to construct diffs from JSON. 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) {`
Correct the hash passed to Diff. 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); }) } });`
Add a function to construct diffs from JSON. 2015-10-24 01:54:24 +03:00			`}`
			`}`

Simplify the Diff constructor. 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; }`
Diffs are model objects. 2015-10-21 23:24:56 +03:00			`return this;`
Call out to patch/syntax when processing a diff. 2015-10-21 18:59:48 +03:00			`}`
Diff.map. 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: {`
Use the correct references. 2015-10-24 02:09:52 +03:00			`extract: this.roll.extract,`
			`unwrap: this.roll.unwrap.map(function(x) { return x.map(transform); })`
Diff.map. 2015-10-24 01:59:24 +03:00			`}`
			`});`
			`}`
			`}`
Diff catamorphisms. 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); }))`
			`}`
			`}`
Add a simple scaffold web page loading the doubt-swift JSON output fixture. 2015-10-09 21:31:06 +03:00			`</script>`
			`</head>`
			`<body>`
Use classes to signal diffs. 2015-10-24 04:19:19 +03:00			`<div id="before" class="diff"></div>`
			`<div id="after" class="diff"></div>`
Add a simple scaffold web page loading the doubt-swift JSON output fixture. 2015-10-09 21:31:06 +03:00			`<script type="text/javascript">`
Load diff.json. 2015-10-21 00:52:04 +03:00			`loadJSON('diff.json', function (json) {`
Map the original diff. 2015-10-24 02:08:10 +03:00			`var diff = diffFromJSON(json.diff);`
Map the before and after terms separately I guess. 2015-10-24 04:05:51 +03:00			`var before = diff.map(function(value) {`
Assign classes to deletions. 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");`
Classify replacements. 2015-10-24 04:29:21 +03:00			`if (value.after != null) {`
			`element.classList.add("replace");`
			`}`
Assign classes to deletions. 2015-10-24 04:25:55 +03:00			`}`
			`return element \|\| "";`
Map the original diff. 2015-10-24 02:08:10 +03:00			`});`
Map the before and after terms separately I guess. 2015-10-24 04:05:51 +03:00			`var after = diff.map(function(value) {`
Assign classes to insertions. 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")`
Classify replacements. 2015-10-24 04:29:21 +03:00			`if (value.before != null) {`
			`element.classList.add("replace");`
			`}`
Assign classes to insertions. 2015-10-24 04:27:11 +03:00			`}`
			`return element \|\| "";`
Map the before and after terms separately I guess. 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"]));`
Add a simple scaffold web page loading the doubt-swift JSON output fixture. 2015-10-09 21:31:06 +03:00			`});`
			`</script>`
			`</body>`
			`</html>`