329 lines
12 KiB
JavaScript
329 lines
12 KiB
JavaScript
|
"use strict";
|
||
|
|
var __read = (this && this.__read) || function (o, n) {
|
||
|
|
var m = typeof Symbol === "function" && o[Symbol.iterator];
|
||
|
|
if (!m) return o;
|
||
|
|
var i = m.call(o), r, ar = [], e;
|
||
|
|
try {
|
||
|
|
while ((n === void 0 || n-- > 0) && !(r = i.next()).done) ar.push(r.value);
|
||
|
|
}
|
||
|
|
catch (error) { e = { error: error }; }
|
||
|
|
finally {
|
||
|
|
try {
|
||
|
|
if (r && !r.done && (m = i["return"])) m.call(i);
|
||
|
|
}
|
||
|
|
finally { if (e) throw e.error; }
|
||
|
|
}
|
||
|
|
return ar;
|
||
|
|
};
|
||
|
|
var __values = (this && this.__values) || function(o) {
|
||
|
|
var s = typeof Symbol === "function" && Symbol.iterator, m = s && o[s], i = 0;
|
||
|
|
if (m) return m.call(o);
|
||
|
|
if (o && typeof o.length === "number") return {
|
||
|
|
next: function () {
|
||
|
|
if (o && i >= o.length) o = void 0;
|
||
|
|
return { value: o && o[i++], done: !o };
|
||
|
|
}
|
||
|
|
};
|
||
|
|
throw new TypeError(s ? "Object is not iterable." : "Symbol.iterator is not defined.");
|
||
|
|
};
|
||
|
|
var __importDefault = (this && this.__importDefault) || function (mod) {
|
||
|
|
return (mod && mod.__esModule) ? mod : { "default": mod };
|
||
|
|
};
|
||
|
|
var _a;
|
||
|
|
Object.defineProperty(exports, "__esModule", { value: true });
|
||
|
|
exports.clearDocument = exports.saveDocument = exports.makeBsprAttributes = exports.removeProperty = exports.getProperty = exports.setProperty = exports.balanceRules = void 0;
|
||
|
|
var NodeUtil_js_1 = __importDefault(require("../NodeUtil.js"));
|
||
|
|
var ParseUtil_js_1 = __importDefault(require("../ParseUtil.js"));
|
||
|
|
var doc = null;
|
||
|
|
var item = null;
|
||
|
|
var getBBox = function (node) {
|
||
|
|
item.root = node;
|
||
|
|
var width = doc.outputJax.getBBox(item, doc).w;
|
||
|
|
return width;
|
||
|
|
};
|
||
|
|
var getRule = function (node) {
|
||
|
|
var i = 0;
|
||
|
|
while (node && !NodeUtil_js_1.default.isType(node, 'mtable')) {
|
||
|
|
if (NodeUtil_js_1.default.isType(node, 'text')) {
|
||
|
|
return null;
|
||
|
|
}
|
||
|
|
if (NodeUtil_js_1.default.isType(node, 'mrow')) {
|
||
|
|
node = node.childNodes[0];
|
||
|
|
i = 0;
|
||
|
|
continue;
|
||
|
|
}
|
||
|
|
node = node.parent.childNodes[i];
|
||
|
|
i++;
|
||
|
|
}
|
||
|
|
return node;
|
||
|
|
};
|
||
|
|
var getPremises = function (rule, direction) {
|
||
|
|
return rule.childNodes[direction === 'up' ? 1 : 0].childNodes[0].
|
||
|
|
childNodes[0].childNodes[0].childNodes[0];
|
||
|
|
};
|
||
|
|
var getPremise = function (premises, n) {
|
||
|
|
return premises.childNodes[n].childNodes[0].childNodes[0];
|
||
|
|
};
|
||
|
|
var firstPremise = function (premises) {
|
||
|
|
return getPremise(premises, 0);
|
||
|
|
};
|
||
|
|
var lastPremise = function (premises) {
|
||
|
|
return getPremise(premises, premises.childNodes.length - 1);
|
||
|
|
};
|
||
|
|
var getConclusion = function (rule, direction) {
|
||
|
|
return rule.childNodes[direction === 'up' ? 0 : 1].childNodes[0].childNodes[0].childNodes[0];
|
||
|
|
};
|
||
|
|
var getColumn = function (inf) {
|
||
|
|
while (inf && !NodeUtil_js_1.default.isType(inf, 'mtd')) {
|
||
|
|
inf = inf.parent;
|
||
|
|
}
|
||
|
|
return inf;
|
||
|
|
};
|
||
|
|
var nextSibling = function (inf) {
|
||
|
|
return inf.parent.childNodes[inf.parent.childNodes.indexOf(inf) + 1];
|
||
|
|
};
|
||
|
|
var previousSibling = function (inf) {
|
||
|
|
return inf.parent.childNodes[inf.parent.childNodes.indexOf(inf) - 1];
|
||
|
|
};
|
||
|
|
var getParentInf = function (inf) {
|
||
|
|
while (inf && (0, exports.getProperty)(inf, 'inference') == null) {
|
||
|
|
inf = inf.parent;
|
||
|
|
}
|
||
|
|
return inf;
|
||
|
|
};
|
||
|
|
var getSpaces = function (inf, rule, right) {
|
||
|
|
if (right === void 0) { right = false; }
|
||
|
|
var result = 0;
|
||
|
|
if (inf === rule) {
|
||
|
|
return result;
|
||
|
|
}
|
||
|
|
if (inf !== rule.parent) {
|
||
|
|
var children_1 = inf.childNodes;
|
||
|
|
var index_1 = right ? children_1.length - 1 : 0;
|
||
|
|
if (NodeUtil_js_1.default.isType(children_1[index_1], 'mspace')) {
|
||
|
|
result += getBBox(children_1[index_1]);
|
||
|
|
}
|
||
|
|
inf = rule.parent;
|
||
|
|
}
|
||
|
|
if (inf === rule) {
|
||
|
|
return result;
|
||
|
|
}
|
||
|
|
var children = inf.childNodes;
|
||
|
|
var index = right ? children.length - 1 : 0;
|
||
|
|
if (children[index] !== rule) {
|
||
|
|
result += getBBox(children[index]);
|
||
|
|
}
|
||
|
|
return result;
|
||
|
|
};
|
||
|
|
var adjustValue = function (inf, right) {
|
||
|
|
if (right === void 0) { right = false; }
|
||
|
|
var rule = getRule(inf);
|
||
|
|
var conc = getConclusion(rule, (0, exports.getProperty)(rule, 'inferenceRule'));
|
||
|
|
var w = getSpaces(inf, rule, right);
|
||
|
|
var x = getBBox(rule);
|
||
|
|
var y = getBBox(conc);
|
||
|
|
return w + ((x - y) / 2);
|
||
|
|
};
|
||
|
|
var addSpace = function (config, inf, space, right) {
|
||
|
|
if (right === void 0) { right = false; }
|
||
|
|
if ((0, exports.getProperty)(inf, 'inferenceRule') ||
|
||
|
|
(0, exports.getProperty)(inf, 'labelledRule')) {
|
||
|
|
var mrow = config.nodeFactory.create('node', 'mrow');
|
||
|
|
inf.parent.replaceChild(mrow, inf);
|
||
|
|
mrow.setChildren([inf]);
|
||
|
|
moveProperties(inf, mrow);
|
||
|
|
inf = mrow;
|
||
|
|
}
|
||
|
|
var index = right ? inf.childNodes.length - 1 : 0;
|
||
|
|
var mspace = inf.childNodes[index];
|
||
|
|
if (NodeUtil_js_1.default.isType(mspace, 'mspace')) {
|
||
|
|
NodeUtil_js_1.default.setAttribute(mspace, 'width', ParseUtil_js_1.default.Em(ParseUtil_js_1.default.dimen2em(NodeUtil_js_1.default.getAttribute(mspace, 'width')) + space));
|
||
|
|
return;
|
||
|
|
}
|
||
|
|
mspace = config.nodeFactory.create('node', 'mspace', [], { width: ParseUtil_js_1.default.Em(space) });
|
||
|
|
if (right) {
|
||
|
|
inf.appendChild(mspace);
|
||
|
|
return;
|
||
|
|
}
|
||
|
|
mspace.parent = inf;
|
||
|
|
inf.childNodes.unshift(mspace);
|
||
|
|
};
|
||
|
|
var moveProperties = function (src, dest) {
|
||
|
|
var props = ['inference', 'proof', 'maxAdjust', 'labelledRule'];
|
||
|
|
props.forEach(function (x) {
|
||
|
|
var value = (0, exports.getProperty)(src, x);
|
||
|
|
if (value != null) {
|
||
|
|
(0, exports.setProperty)(dest, x, value);
|
||
|
|
(0, exports.removeProperty)(src, x);
|
||
|
|
}
|
||
|
|
});
|
||
|
|
};
|
||
|
|
var adjustSequents = function (config) {
|
||
|
|
var sequents = config.nodeLists['sequent'];
|
||
|
|
if (!sequents) {
|
||
|
|
return;
|
||
|
|
}
|
||
|
|
for (var i = sequents.length - 1, seq = void 0; seq = sequents[i]; i--) {
|
||
|
|
if ((0, exports.getProperty)(seq, 'sequentProcessed')) {
|
||
|
|
(0, exports.removeProperty)(seq, 'sequentProcessed');
|
||
|
|
continue;
|
||
|
|
}
|
||
|
|
var collect = [];
|
||
|
|
var inf = getParentInf(seq);
|
||
|
|
if ((0, exports.getProperty)(inf, 'inference') !== 1) {
|
||
|
|
continue;
|
||
|
|
}
|
||
|
|
collect.push(seq);
|
||
|
|
while ((0, exports.getProperty)(inf, 'inference') === 1) {
|
||
|
|
inf = getRule(inf);
|
||
|
|
var premise = firstPremise(getPremises(inf, (0, exports.getProperty)(inf, 'inferenceRule')));
|
||
|
|
var sequent = ((0, exports.getProperty)(premise, 'inferenceRule')) ?
|
||
|
|
getConclusion(premise, (0, exports.getProperty)(premise, 'inferenceRule')) :
|
||
|
|
premise;
|
||
|
|
if ((0, exports.getProperty)(sequent, 'sequent')) {
|
||
|
|
seq = sequent.childNodes[0];
|
||
|
|
collect.push(seq);
|
||
|
|
(0, exports.setProperty)(seq, 'sequentProcessed', true);
|
||
|
|
}
|
||
|
|
inf = premise;
|
||
|
|
}
|
||
|
|
adjustSequentPairwise(config, collect);
|
||
|
|
}
|
||
|
|
};
|
||
|
|
var addSequentSpace = function (config, sequent, position, direction, width) {
|
||
|
|
var mspace = config.nodeFactory.create('node', 'mspace', [], { width: ParseUtil_js_1.default.Em(width) });
|
||
|
|
if (direction === 'left') {
|
||
|
|
var row = sequent.childNodes[position].childNodes[0];
|
||
|
|
mspace.parent = row;
|
||
|
|
row.childNodes.unshift(mspace);
|
||
|
|
}
|
||
|
|
else {
|
||
|
|
sequent.childNodes[position].appendChild(mspace);
|
||
|
|
}
|
||
|
|
(0, exports.setProperty)(sequent.parent, 'sequentAdjust_' + direction, width);
|
||
|
|
};
|
||
|
|
var adjustSequentPairwise = function (config, sequents) {
|
||
|
|
var top = sequents.pop();
|
||
|
|
while (sequents.length) {
|
||
|
|
var bottom = sequents.pop();
|
||
|
|
var _a = __read(compareSequents(top, bottom), 2), left = _a[0], right = _a[1];
|
||
|
|
if ((0, exports.getProperty)(top.parent, 'axiom')) {
|
||
|
|
addSequentSpace(config, left < 0 ? top : bottom, 0, 'left', Math.abs(left));
|
||
|
|
addSequentSpace(config, right < 0 ? top : bottom, 2, 'right', Math.abs(right));
|
||
|
|
}
|
||
|
|
top = bottom;
|
||
|
|
}
|
||
|
|
};
|
||
|
|
var compareSequents = function (top, bottom) {
|
||
|
|
var tr = getBBox(top.childNodes[2]);
|
||
|
|
var br = getBBox(bottom.childNodes[2]);
|
||
|
|
var tl = getBBox(top.childNodes[0]);
|
||
|
|
var bl = getBBox(bottom.childNodes[0]);
|
||
|
|
var dl = tl - bl;
|
||
|
|
var dr = tr - br;
|
||
|
|
return [dl, dr];
|
||
|
|
};
|
||
|
|
var balanceRules = function (arg) {
|
||
|
|
var e_1, _a;
|
||
|
|
item = new arg.document.options.MathItem('', null, arg.math.display);
|
||
|
|
var config = arg.data;
|
||
|
|
adjustSequents(config);
|
||
|
|
var inferences = config.nodeLists['inference'] || [];
|
||
|
|
try {
|
||
|
|
for (var inferences_1 = __values(inferences), inferences_1_1 = inferences_1.next(); !inferences_1_1.done; inferences_1_1 = inferences_1.next()) {
|
||
|
|
var inf = inferences_1_1.value;
|
||
|
|
var isProof = (0, exports.getProperty)(inf, 'proof');
|
||
|
|
var rule = getRule(inf);
|
||
|
|
var premises = getPremises(rule, (0, exports.getProperty)(rule, 'inferenceRule'));
|
||
|
|
var premiseF = firstPremise(premises);
|
||
|
|
if ((0, exports.getProperty)(premiseF, 'inference')) {
|
||
|
|
var adjust_1 = adjustValue(premiseF);
|
||
|
|
if (adjust_1) {
|
||
|
|
addSpace(config, premiseF, -adjust_1);
|
||
|
|
var w_1 = getSpaces(inf, rule, false);
|
||
|
|
addSpace(config, inf, adjust_1 - w_1);
|
||
|
|
}
|
||
|
|
}
|
||
|
|
var premiseL = lastPremise(premises);
|
||
|
|
if ((0, exports.getProperty)(premiseL, 'inference') == null) {
|
||
|
|
continue;
|
||
|
|
}
|
||
|
|
var adjust = adjustValue(premiseL, true);
|
||
|
|
addSpace(config, premiseL, -adjust, true);
|
||
|
|
var w = getSpaces(inf, rule, true);
|
||
|
|
var maxAdjust = (0, exports.getProperty)(inf, 'maxAdjust');
|
||
|
|
if (maxAdjust != null) {
|
||
|
|
adjust = Math.max(adjust, maxAdjust);
|
||
|
|
}
|
||
|
|
var column = void 0;
|
||
|
|
if (isProof || !(column = getColumn(inf))) {
|
||
|
|
addSpace(config, (0, exports.getProperty)(inf, 'proof') ? inf : inf.parent, adjust - w, true);
|
||
|
|
continue;
|
||
|
|
}
|
||
|
|
var sibling = nextSibling(column);
|
||
|
|
if (sibling) {
|
||
|
|
var pos = config.nodeFactory.create('node', 'mspace', [], { width: adjust - w + 'em' });
|
||
|
|
sibling.appendChild(pos);
|
||
|
|
inf.removeProperty('maxAdjust');
|
||
|
|
continue;
|
||
|
|
}
|
||
|
|
var parentRule = getParentInf(column);
|
||
|
|
if (!parentRule) {
|
||
|
|
continue;
|
||
|
|
}
|
||
|
|
adjust = (0, exports.getProperty)(parentRule, 'maxAdjust') ?
|
||
|
|
Math.max((0, exports.getProperty)(parentRule, 'maxAdjust'), adjust) : adjust;
|
||
|
|
(0, exports.setProperty)(parentRule, 'maxAdjust', adjust);
|
||
|
|
}
|
||
|
|
}
|
||
|
|
catch (e_1_1) { e_1 = { error: e_1_1 }; }
|
||
|
|
finally {
|
||
|
|
try {
|
||
|
|
if (inferences_1_1 && !inferences_1_1.done && (_a = inferences_1.return)) _a.call(inferences_1);
|
||
|
|
}
|
||
|
|
finally { if (e_1) throw e_1.error; }
|
||
|
|
}
|
||
|
|
};
|
||
|
|
exports.balanceRules = balanceRules;
|
||
|
|
var property_prefix = 'bspr_';
|
||
|
|
var blacklistedProperties = (_a = {},
|
||
|
|
_a[property_prefix + 'maxAdjust'] = true,
|
||
|
|
_a);
|
||
|
|
var setProperty = function (node, property, value) {
|
||
|
|
NodeUtil_js_1.default.setProperty(node, property_prefix + property, value);
|
||
|
|
};
|
||
|
|
exports.setProperty = setProperty;
|
||
|
|
var getProperty = function (node, property) {
|
||
|
|
return NodeUtil_js_1.default.getProperty(node, property_prefix + property);
|
||
|
|
};
|
||
|
|
exports.getProperty = getProperty;
|
||
|
|
var removeProperty = function (node, property) {
|
||
|
|
node.removeProperty(property_prefix + property);
|
||
|
|
};
|
||
|
|
exports.removeProperty = removeProperty;
|
||
|
|
var makeBsprAttributes = function (arg) {
|
||
|
|
arg.data.root.walkTree(function (mml, _data) {
|
||
|
|
var attr = [];
|
||
|
|
mml.getPropertyNames().forEach(function (x) {
|
||
|
|
if (!blacklistedProperties[x] && x.match(RegExp('^' + property_prefix))) {
|
||
|
|
attr.push(x + ':' + mml.getProperty(x));
|
||
|
|
}
|
||
|
|
});
|
||
|
|
if (attr.length) {
|
||
|
|
NodeUtil_js_1.default.setAttribute(mml, 'semantics', attr.join(';'));
|
||
|
|
}
|
||
|
|
});
|
||
|
|
};
|
||
|
|
exports.makeBsprAttributes = makeBsprAttributes;
|
||
|
|
var saveDocument = function (arg) {
|
||
|
|
doc = arg.document;
|
||
|
|
if (!('getBBox' in doc.outputJax)) {
|
||
|
|
throw Error('The bussproofs extension requires an output jax with a getBBox() method');
|
||
|
|
}
|
||
|
|
};
|
||
|
|
exports.saveDocument = saveDocument;
|
||
|
|
var clearDocument = function (_arg) {
|
||
|
|
doc = null;
|
||
|
|
};
|
||
|
|
exports.clearDocument = clearDocument;
|
||
|
|
//# sourceMappingURL=BussproofsUtil.js.map
|