diff --git a/prototype/UI/index.html b/prototype/UI/index.html
index 4ae471054..e4dfa403b 100644
--- a/prototype/UI/index.html
+++ b/prototype/UI/index.html
@@ -80,33 +80,57 @@
return this;
}
+ /// Range -> Syntax a -> String, (a -> DOM) -> DOM
+ function rangeAndSyntaxToDOM(range, syntax, source, recur) {
+ var element;
+ 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];
+ element.appendChild(document.createTextNode(source.substr(previous, child.range[0] - previous)));
+ element.appendChild(wrap("li", recur(child)));
+ previous = child.range[0] + child.range[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) {
+ values.push([ k, syntax.keyed.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 = range[0];
+ for (i in values) {
+ var pair = values[i];
+ var key = pair[0];
+ var child = pair[1];
+ element.appendChild(document.createTextNode(source.substr(previous, child.range[0] - previous)));
+ element.appendChild(wrap("dt", document.createTextNode(key)));
+ element.appendChild(wrap("dd", recur(child)));
+ previous = child.range[0] + child.range[1];
+ }
+ element.appendChild(document.createTextNode(source.substr(previous, range[0] + range[1] - previous)));
+ }
+ return element;
+ }
+
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 Term) {
+ element = rangeAndSyntaxToDOM(model.range, model.unwrap, source, function(child) { return toDOM(child, stateName, source); });
}
if (model instanceof Diff) {