diff --git a/prototype/UI/index.html b/prototype/UI/index.html
index b97b6b87b..e478eb647 100644
--- a/prototype/UI/index.html
+++ b/prototype/UI/index.html
@@ -86,11 +86,19 @@
/// Term -> String -> DOM
function termToDOM(term, source) {
- return rangeAndSyntaxToDOM(term.range, term.unwrap, source, function(term) { return termToDOM(term, source); });
+ return rangeAndSyntaxToDOM(term.range, term.unwrap, source, function(term) { return term.range; }, function(term) { return termToDOM(term, source); });
}
- /// Range -> Syntax a -> String, (a -> DOM) -> DOM
- function rangeAndSyntaxToDOM(range, syntax, source, recur) {
+ /// Diff -> String -> String -> DOM
+ function diffToDOM(diff, which, source) {
+ return rangeAndSyntaxToDOM(diff.roll.extract[which], diff.roll.unwrap, source, function(diff) {
+ if (diff.pure != null) { return diff.pure["data-range"]; }
+ if (diff.roll != null) { return diff.roll.extract[which]; }
+ }, 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) {
@@ -101,9 +109,10 @@
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)));
+ var childRange = getRange(child);
+ element.appendChild(document.createTextNode(source.substr(previous, childRange[0] - previous)));
element.appendChild(wrap("li", recur(child)));
- previous = child.range[0] + child.range[1];
+ previous = childRange[0] + childRange[1];
}
element.appendChild(document.createTextNode(source.substr(previous, range[0] + range[1] - previous)));
} else if (syntax.keyed != null) {
@@ -113,9 +122,9 @@
values.push([ k, syntax.keyed.values[k] ]);
}
values.sort(function(a, b) {
- if (a[1].range[0] < b[1].range[0]) {
+ if (getRange(a[1])[0] < getRange(b[1])[0]) {
return -1;
- } else if (a[1].range[0] > b[1].range[0]) {
+ } else if (getRange(a[1])[0] > getRange(b[1])[0]) {
return 1;
}
return 0;
@@ -126,10 +135,11 @@
var pair = values[i];
var key = pair[0];
var child = pair[1];
- element.appendChild(document.createTextNode(source.substr(previous, child.range[0] - previous)));
+ 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 = child.range[0] + child.range[1];
+ previous = childRange[0] + childRange[1];
}
element.appendChild(document.createTextNode(source.substr(previous, range[0] + range[1] - previous)));
}