github/semantic
1
1
Fork 0
mirror of https://github.com/github/semantic.git synced 2024-11-25 11:04:00 +03:00
Code Issues Projects Releases Wiki Activity

Get ranges for children.

Browse Source
This commit is contained in:
Rob Rix 2015-10-23 21:05:20 -04:00
parent b3dfee8fc0
commit b7ac783e19
1 changed files with 19 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
prototype/UI/index.html
View File

@ -86,11 +86,19 @@
/// Term -> String -> DOM /// Term -> String -> DOM
function termToDOM(term, source) { 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 /// Diff -> String -> String -> DOM
function rangeAndSyntaxToDOM(range, syntax, source, recur) { 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); } recur = recur || function (term) { return rangeAndSyntaxToDOM(term.range, term.unwrap, source); }
var element; var element;
if (syntax.leaf != null) { if (syntax.leaf != null) {
@ -101,9 +109,10 @@
var previous = range[0]; var previous = range[0];
for (i in syntax.indexed) { for (i in syntax.indexed) {
var child = syntax.indexed[i]; 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))); 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))); element.appendChild(document.createTextNode(source.substr(previous, range[0] + range[1] - previous)));
} else if (syntax.keyed != null) { } else if (syntax.keyed != null) {
@ -113,9 +122,9 @@
values.push([ k, syntax.keyed.values[k] ]); values.push([ k, syntax.keyed.values[k] ]);
} }
values.sort(function(a, b) { 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; 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 1;
} }
return 0; return 0;
@ -126,10 +135,11 @@
var pair = values[i]; var pair = values[i];
var key = pair[0]; var key = pair[0];
var child = pair[1]; 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("dt", document.createTextNode(key)));
element.appendChild(wrap("dd", recur(child))); 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))); element.appendChild(document.createTextNode(source.substr(previous, range[0] + range[1] - previous)));
} }