From b7ac783e1987fb60660edc17c215b98c151e3f9c Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 23 Oct 2015 21:05:20 -0400 Subject: [PATCH] Get ranges for children. --- prototype/UI/index.html | 28 +++++++++++++++++++--------- 1 file changed, 19 insertions(+), 9 deletions(-) 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))); }