diff --git a/prototype/UI/dictionary.js b/prototype/UI/dictionary.js
new file mode 100644
index 000000000..205320473
--- /dev/null
+++ b/prototype/UI/dictionary.js
@@ -0,0 +1,16 @@
+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;
+}
diff --git a/prototype/UI/diff.js b/prototype/UI/diff.js
new file mode 100644
index 000000000..8cc195aed
--- /dev/null
+++ b/prototype/UI/diff.js
@@ -0,0 +1,77 @@
+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);
+ }))
+ }
+}
+
+/// 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);
+ })
+}
diff --git a/prototype/UI/dom.js b/prototype/UI/dom.js
new file mode 100644
index 000000000..7104cb8e0
--- /dev/null
+++ b/prototype/UI/dom.js
@@ -0,0 +1,63 @@
+function wrap(tagName, element) {
+ if (element == null) {
+ return null;
+ }
+ var node = document.createElement(tagName);
+ node.appendChild(element);
+ return node;
+}
+
+/// 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;
+}
diff --git a/prototype/UI/index.html b/prototype/UI/index.html
index 3e388c47b..0e8eaeac4 100644
--- a/prototype/UI/index.html
+++ b/prototype/UI/index.html
@@ -41,6 +41,12 @@
display: none;
}
+
+
+
+
+
+
diff --git a/prototype/UI/patch.js b/prototype/UI/patch.js
new file mode 100644
index 000000000..1b029d5df
--- /dev/null
+++ b/prototype/UI/patch.js
@@ -0,0 +1,13 @@
+function Patch(patch) {
+ if (patch.delete != null) {
+ this.before = termFromJSON(patch.delete);
+ }
+ if (patch.insert != null) {
+ this.after = termFromJSON(patch.insert);
+ }
+ if (patch.replace != null) {
+ this.before = termFromJSON(patch.replace.before);
+ this.after = termFromJSON(patch.replace.after);
+ }
+ return this;
+}
diff --git a/prototype/UI/syntax.js b/prototype/UI/syntax.js
new file mode 100644
index 000000000..ce55b32c6
--- /dev/null
+++ b/prototype/UI/syntax.js
@@ -0,0 +1,39 @@
+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);
+ }
+}
diff --git a/prototype/UI/term.js b/prototype/UI/term.js
new file mode 100644
index 000000000..1e2cf6f96
--- /dev/null
+++ b/prototype/UI/term.js
@@ -0,0 +1,23 @@
+function termFromJSON(json) {
+ return new Term({
+ extract: json.extract,
+ unwrap: new Syntax(json.unwrap, function(x) {
+ return termFromJSON(x);
+ })
+ });
+}
+
+function Term(object) {
+ this.range = object.extract;
+ this.unwrap = object.unwrap;
+ return this;
+}
+
+/// Term -> String -> DOM
+function termToDOM(term, which, source) {
+ return rangeAndSyntaxToDOM(term.range, term.unwrap, source, function(term) {
+ return term.range;
+ }, function(term) {
+ return termToDOM(term, which, source);
+ });
+}