mirror of
https://github.com/github/semantic.git
synced 2024-12-26 16:33:03 +03:00
Merge branch 'master' into fix-dictionary-ranges
This commit is contained in:
joshvera
commit
81f4112aca
16
prototype/UI/dictionary.js
vendored
Normal file
16
prototype/UI/dictionary.js
vendored
Normal file
@ -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;
|
||||
}
|
||||
77
prototype/UI/diff.js
vendored
Normal file
77
prototype/UI/diff.js
vendored
Normal file
@ -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);
|
||||
})
|
||||
}
|
||||
63
prototype/UI/dom.js
vendored
Normal file
63
prototype/UI/dom.js
vendored
Normal file
@ -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;
|
||||
}
|
||||
@ -41,6 +41,12 @@
|
||||
display: none;
|
||||
}
|
||||
</style>
|
||||
<script type="text/javascript" src="dictionary.js"></script>
|
||||
<script type="text/javascript" src="diff.js"></script>
|
||||
<script type="text/javascript" src="dom.js"></script>
|
||||
<script type="text/javascript" src="patch.js"></script>
|
||||
<script type="text/javascript" src="syntax.js"></script>
|
||||
<script type="text/javascript" src="term.js"></script>
|
||||
<script type="text/javascript">
|
||||
function loadJSON(path, callback) {
|
||||
var request = new XMLHttpRequest();
|
||||
@ -53,168 +59,6 @@
|
||||
};
|
||||
request.send(null);
|
||||
}
|
||||
|
||||
function wrap(tagName, element) {
|
||||
if (element == null) { return null; }
|
||||
var node = document.createElement(tagName);
|
||||
node.appendChild(element);
|
||||
return node;
|
||||
}
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
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); });
|
||||
}
|
||||
|
||||
/// 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); })
|
||||
}
|
||||
|
||||
/// 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;
|
||||
}
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
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); }
|
||||
}
|
||||
|
||||
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); }))
|
||||
}
|
||||
}
|
||||
</script>
|
||||
</head>
|
||||
<body>
|
||||
|
||||
13
prototype/UI/patch.js
vendored
Normal file
13
prototype/UI/patch.js
vendored
Normal file
@ -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;
|
||||
}
|
||||
39
prototype/UI/syntax.js
vendored
Normal file
39
prototype/UI/syntax.js
vendored
Normal file
@ -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);
|
||||
}
|
||||
}
|
||||
23
prototype/UI/term.js
vendored
Normal file
23
prototype/UI/term.js
vendored
Normal file
@ -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);
|
||||
});
|
||||
}
|
||||
Loading…
Reference in New Issue
Block a user