1 line
17 KiB
JavaScript
1 line
17 KiB
JavaScript
!function(e){var t={};function r(o){if(t[o])return t[o].exports;var n=t[o]={i:o,l:!1,exports:{}};return e[o].call(n.exports,n,n.exports,r),n.l=!0,n.exports}r.m=e,r.c=t,r.d=function(e,t,o){r.o(e,t)||Object.defineProperty(e,t,{enumerable:!0,get:o})},r.r=function(e){"undefined"!=typeof Symbol&&Symbol.toStringTag&&Object.defineProperty(e,Symbol.toStringTag,{value:"Module"}),Object.defineProperty(e,"__esModule",{value:!0})},r.t=function(e,t){if(1&t&&(e=r(e)),8&t)return e;if(4&t&&"object"==typeof e&&e&&e.__esModule)return e;var o=Object.create(null);if(r.r(o),Object.defineProperty(o,"default",{enumerable:!0,value:e}),2&t&&"string"!=typeof e)for(var n in e)r.d(o,n,function(t){return e[t]}.bind(null,n));return o},r.n=function(e){var t=e&&e.__esModule?function(){return e.default}:function(){return e};return r.d(t,"a",t),t},r.o=function(e,t){return Object.prototype.hasOwnProperty.call(e,t)},r.p="",r(r.s=15)}([function(e,t,r){"use strict";var o,n=this&&this.__read||function(e,t){var r="function"==typeof Symbol&&e[Symbol.iterator];if(!r)return e;var o,n,a=r.call(e),i=[];try{for(;(void 0===t||t-- >0)&&!(o=a.next()).done;)i.push(o.value)}catch(e){n={error:e}}finally{try{o&&!o.done&&(r=a.return)&&r.call(a)}finally{if(n)throw n.error}}return i},a=this&&this.__values||function(e){var t="function"==typeof Symbol&&Symbol.iterator,r=t&&e[t],o=0;if(r)return r.call(e);if(e&&"number"==typeof e.length)return{next:function(){return e&&o>=e.length&&(e=void 0),{value:e&&e[o++],done:!e}}};throw new TypeError(t?"Object is not iterable.":"Symbol.iterator is not defined.")};Object.defineProperty(t,"__esModule",{value:!0}),t.clearDocument=t.saveDocument=t.makeBsprAttributes=t.removeProperty=t.getProperty=t.setProperty=t.balanceRules=void 0;var i=r(10),l=r(4),u=null,f=null,s=function(e){return f.root=e,u.outputJax.getBBox(f,u).w},c=function(e){for(var t=0;e&&!i.default.isType(e,"mtable");){if(i.default.isType(e,"text"))return null;i.default.isType(e,"mrow")?(e=e.childNodes[0],t=0):(e=e.parent.childNodes[t],t++)}return e},d=function(e,t){return e.childNodes["up"===t?1:0].childNodes[0].childNodes[0].childNodes[0].childNodes[0]},p=function(e,t){return e.childNodes[t].childNodes[0].childNodes[0]},m=function(e){return p(e,0)},h=function(e){return p(e,e.childNodes.length-1)},y=function(e,t){return e.childNodes["up"===t?0:1].childNodes[0].childNodes[0].childNodes[0]},v=function(e){for(;e&&!i.default.isType(e,"mtd");)e=e.parent;return e},P=function(e){return e.parent.childNodes[e.parent.childNodes.indexOf(e)+1]},g=function(e){for(;e&&null==t.getProperty(e,"inference");)e=e.parent;return e},b=function(e,t,r){void 0===r&&(r=!1);var o=0;if(e===t)return o;if(e!==t.parent){var n=e.childNodes,a=r?n.length-1:0;i.default.isType(n[a],"mspace")&&(o+=s(n[a])),e=t.parent}if(e===t)return o;var l=e.childNodes,u=r?l.length-1:0;return l[u]!==t&&(o+=s(l[u])),o},x=function(e,r){void 0===r&&(r=!1);var o=c(e),n=y(o,t.getProperty(o,"inferenceRule"));return b(e,o,r)+(s(o)-s(n))/2},M=function(e,r,o,n){if(void 0===n&&(n=!1),t.getProperty(r,"inferenceRule")||t.getProperty(r,"labelledRule")){var a=e.nodeFactory.create("node","mrow");r.parent.replaceChild(a,r),a.setChildren([r]),_(r,a),r=a}var u=n?r.childNodes.length-1:0,f=r.childNodes[u];i.default.isType(f,"mspace")?i.default.setAttribute(f,"width",l.default.Em(l.default.dimen2em(i.default.getAttribute(f,"width"))+o)):(f=e.nodeFactory.create("node","mspace",[],{width:l.default.Em(o)}),n?r.appendChild(f):(f.parent=r,r.childNodes.unshift(f)))},_=function(e,r){["inference","proof","maxAdjust","labelledRule"].forEach((function(o){var n=t.getProperty(e,o);null!=n&&(t.setProperty(r,o,n),t.removeProperty(e,o))}))},w=function(e,r,o,n,a){var i=e.nodeFactory.create("node","mspace",[],{width:l.default.Em(a)});if("left"===n){var u=r.childNodes[o].childNodes[0];i.parent=u,u.childNodes.unshift(i)}else r.childNodes[o].appendChild(i);t.setProperty(r.parent,"sequentAdjust_"+n,a)},T=function(e,r){for(var o=r.pop();r.length;){var a=r.pop(),i=n(C(o,a),2),l=i[0],u=i[1];t.getProperty(o.parent,"axiom")&&(w(e,l<0?o:a,0,"left",Math.abs(l)),w(e,u<0?o:a,2,"right",Math.abs(u))),o=a}},C=function(e,t){var r=s(e.childNodes[2]),o=s(t.childNodes[2]);return[s(e.childNodes[0])-s(t.childNodes[0]),r-o]};t.balanceRules=function(e){var r,o;f=new e.document.options.MathItem("",null,e.math.display);var n=e.data;!function(e){var r=e.nodeLists.sequent;if(r)for(var o=r.length-1,n=void 0;n=r[o];o--)if(t.getProperty(n,"sequentProcessed"))t.removeProperty(n,"sequentProcessed");else{var a=[],i=g(n);if(1===t.getProperty(i,"inference")){for(a.push(n);1===t.getProperty(i,"inference");){i=c(i);var l=m(d(i,t.getProperty(i,"inferenceRule"))),u=t.getProperty(l,"inferenceRule")?y(l,t.getProperty(l,"inferenceRule")):l;t.getProperty(u,"sequent")&&(n=u.childNodes[0],a.push(n),t.setProperty(n,"sequentProcessed",!0)),i=l}T(e,a)}}}(n);var i=n.nodeLists.inference||[];try{for(var l=a(i),u=l.next();!u.done;u=l.next()){var s=u.value,p=t.getProperty(s,"proof"),_=c(s),w=d(_,t.getProperty(_,"inferenceRule")),C=m(w);if(t.getProperty(C,"inference")){var I=x(C);if(I){M(n,C,-I);var S=b(s,_,!1);M(n,s,I-S)}}var N=h(w);if(null!=t.getProperty(N,"inference")){var A=x(N,!0);M(n,N,-A,!0);var j=b(s,_,!0),L=t.getProperty(s,"maxAdjust");null!=L&&(A=Math.max(A,L));var k=void 0;if(!p&&(k=v(s))){var O=P(k);if(O){var J=n.nodeFactory.create("node","mspace",[],{width:A-j+"em"});O.appendChild(J),s.removeProperty("maxAdjust")}else{var B=g(k);B&&(A=t.getProperty(B,"maxAdjust")?Math.max(t.getProperty(B,"maxAdjust"),A):A,t.setProperty(B,"maxAdjust",A))}}else M(n,t.getProperty(s,"proof")?s:s.parent,A-j,!0)}}}catch(e){r={error:e}}finally{try{u&&!u.done&&(o=l.return)&&o.call(l)}finally{if(r)throw r.error}}};var I=((o={}).bspr_maxAdjust=!0,o);t.setProperty=function(e,t,r){i.default.setProperty(e,"bspr_"+t,r)},t.getProperty=function(e,t){return i.default.getProperty(e,"bspr_"+t)},t.removeProperty=function(e,t){e.removeProperty("bspr_"+t)},t.makeBsprAttributes=function(e){e.data.root.walkTree((function(e,t){var r=[];e.getPropertyNames().forEach((function(t){!I[t]&&t.match(RegExp("^bspr_"))&&r.push(t+":"+e.getProperty(t))})),r.length&&i.default.setAttribute(e,"semantics",r.join(";"))}))},t.saveDocument=function(e){if(!("getBBox"in(u=e.document).outputJax))throw Error("The bussproofs extension requires an output jax with a getBBox() method")},t.clearDocument=function(e){u=null}},function(e,t,r){"use strict";var o,n=this&&this.__extends||(o=function(e,t){return(o=Object.setPrototypeOf||{__proto__:[]}instanceof Array&&function(e,t){e.__proto__=t}||function(e,t){for(var r in t)t.hasOwnProperty(r)&&(e[r]=t[r])})(e,t)},function(e,t){function r(){this.constructor=e}o(e,t),e.prototype=null===t?Object.create(t):(r.prototype=t.prototype,new r)});Object.defineProperty(t,"__esModule",{value:!0}),t.ProofTreeItem=void 0;var a=r(3),i=r(8),l=r(9),u=r(0),f=function(e){function t(){var t=null!==e&&e.apply(this,arguments)||this;return t.leftLabel=null,t.rigthLabel=null,t.innerStack=new l.default(t.factory,{},!0),t}return n(t,e),Object.defineProperty(t.prototype,"kind",{get:function(){return"proofTree"},enumerable:!1,configurable:!0}),t.prototype.checkItem=function(e){if(e.isKind("end")&&"prooftree"===e.getName()){var t=this.toMml();return u.setProperty(t,"proof",!0),[[this.factory.create("mml",t),e],!0]}if(e.isKind("stop"))throw new a.default("EnvMissingEnd","Missing \\end{%1}",this.getName());return this.innerStack.Push(e),i.BaseItem.fail},t.prototype.toMml=function(){var t=e.prototype.toMml.call(this),r=this.innerStack.Top();if(r.isKind("start")&&!r.Size())return t;this.innerStack.Push(this.factory.create("stop"));var o=this.innerStack.Top().toMml();return this.create("node","mrow",[o,t],{})},t}(i.BaseItem);t.ProofTreeItem=f},function(e,t,r){"use strict";var o=this&&this.__read||function(e,t){var r="function"==typeof Symbol&&e[Symbol.iterator];if(!r)return e;var o,n,a=r.call(e),i=[];try{for(;(void 0===t||t-- >0)&&!(o=a.next()).done;)i.push(o.value)}catch(e){n={error:e}}finally{try{o&&!o.done&&(r=a.return)&&r.call(a)}finally{if(n)throw n.error}}return i},n=this&&this.__spread||function(){for(var e=[],t=0;t<arguments.length;t++)e=e.concat(o(arguments[t]));return e};Object.defineProperty(t,"__esModule",{value:!0});var a=r(3),i=r(12),l=r(4),u=r(0),f={Prooftree:function(e,t){return e.Push(t),e.itemFactory.create("proofTree").setProperties({name:t.getName(),line:"solid",currentLine:"solid",rootAtTop:!1})},Axiom:function(e,t){var r=e.stack.Top();if("proofTree"!==r.kind)throw new a.default("IllegalProofCommand","Proof commands only allowed in prooftree environment.");var o=s(e,e.GetArgument(t));u.setProperty(o,"axiom",!0),r.Push(o)}},s=function(e,t){var r=l.default.internalMath(e,l.default.trimSpaces(t),0);if(!r[0].childNodes[0].childNodes.length)return e.create("node","mrow",[]);var o=e.create("node","mspace",[],{width:".5ex"}),a=e.create("node","mspace",[],{width:".5ex"});return e.create("node","mrow",n([o],r,[a]))};function c(e,t,r,o,n,a,i){var l,f,s,c,d=e.create("node","mtr",[e.create("node","mtd",[t],{})],{}),p=e.create("node","mtr",[e.create("node","mtd",r,{})],{}),m=e.create("node","mtable",i?[p,d]:[d,p],{align:"top 2",rowlines:a,framespacing:"0 0"});if(u.setProperty(m,"inferenceRule",i?"up":"down"),o&&(l=e.create("node","mpadded",[o],{height:"+.5em",width:"+.5em",voffset:"-.15em"}),u.setProperty(l,"prooflabel","left")),n&&(f=e.create("node","mpadded",[n],{height:"+.5em",width:"+.5em",voffset:"-.15em"}),u.setProperty(f,"prooflabel","right")),o&&n)s=[l,m,f],c="both";else if(o)s=[l,m],c="left";else{if(!n)return m;s=[m,f],c="right"}return m=e.create("node","mrow",s),u.setProperty(m,"labelledRule",c),m}function d(e,t){if("$"!==e.GetNext())throw new a.default("IllegalUseOfCommand","Use of %1 does not match it's definition.",t);e.i++;var r=e.GetUpTo(t,"$");if(-1===r.indexOf("\\fCenter"))throw new a.default("IllegalUseOfCommand","Missing \\fCenter in %1.",t);var n=o(r.split("\\fCenter"),2),l=n[0],f=n[1],s=new i.default(l,e.stack.env,e.configuration).mml(),c=new i.default(f,e.stack.env,e.configuration).mml(),d=new i.default("\\fCenter",e.stack.env,e.configuration).mml(),p=e.create("node","mtd",[s],{}),m=e.create("node","mtd",[d],{}),h=e.create("node","mtd",[c],{}),y=e.create("node","mtr",[p,m,h],{}),v=e.create("node","mtable",[y],{columnspacing:".5ex",columnalign:"center 2"});return u.setProperty(v,"sequent",!0),e.configuration.addNode("sequent",y),v}f.Inference=function(e,t,r){var o=e.stack.Top();if("proofTree"!==o.kind)throw new a.default("IllegalProofCommand","Proof commands only allowed in prooftree environment.");if(o.Size()<r)throw new a.default("BadProofTree","Proof tree badly specified.");var n=o.getProperty("rootAtTop"),i=1!==r||o.Peek()[0].childNodes.length?r:0,l=[];do{l.length&&l.unshift(e.create("node","mtd",[],{})),l.unshift(e.create("node","mtd",[o.Pop()],{rowalign:n?"top":"bottom"})),r--}while(r>0);var f=e.create("node","mtr",l,{}),d=e.create("node","mtable",[f],{framespacing:"0 0"}),p=s(e,e.GetArgument(t)),m=o.getProperty("currentLine");m!==o.getProperty("line")&&o.setProperty("currentLine",o.getProperty("line"));var h=c(e,d,[p],o.getProperty("left"),o.getProperty("right"),m,n);o.setProperty("left",null),o.setProperty("right",null),u.setProperty(h,"inference",i),e.configuration.addNode("inference",h),o.Push(h)},f.Label=function(e,t,r){var o=e.stack.Top();if("proofTree"!==o.kind)throw new a.default("IllegalProofCommand","Proof commands only allowed in prooftree environment.");var n=l.default.internalMath(e,e.GetArgument(t),0),i=n.length>1?e.create("node","mrow",n,{}):n[0];o.setProperty(r,i)},f.SetLine=function(e,t,r,o){var n=e.stack.Top();if("proofTree"!==n.kind)throw new a.default("IllegalProofCommand","Proof commands only allowed in prooftree environment.");n.setProperty("currentLine",r),o&&n.setProperty("line",r)},f.RootAtTop=function(e,t,r){var o=e.stack.Top();if("proofTree"!==o.kind)throw new a.default("IllegalProofCommand","Proof commands only allowed in prooftree environment.");o.setProperty("rootAtTop",r)},f.AxiomF=function(e,t){var r=e.stack.Top();if("proofTree"!==r.kind)throw new a.default("IllegalProofCommand","Proof commands only allowed in prooftree environment.");var o=d(e,t);u.setProperty(o,"axiom",!0),r.Push(o)},f.FCenter=function(e,t){},f.InferenceF=function(e,t,r){var o=e.stack.Top();if("proofTree"!==o.kind)throw new a.default("IllegalProofCommand","Proof commands only allowed in prooftree environment.");if(o.Size()<r)throw new a.default("BadProofTree","Proof tree badly specified.");var n=o.getProperty("rootAtTop"),i=1!==r||o.Peek()[0].childNodes.length?r:0,l=[];do{l.length&&l.unshift(e.create("node","mtd",[],{})),l.unshift(e.create("node","mtd",[o.Pop()],{rowalign:n?"top":"bottom"})),r--}while(r>0);var f=e.create("node","mtr",l,{}),s=e.create("node","mtable",[f],{framespacing:"0 0"}),p=d(e,t),m=o.getProperty("currentLine");m!==o.getProperty("line")&&o.setProperty("currentLine",o.getProperty("line"));var h=c(e,s,[p],o.getProperty("left"),o.getProperty("right"),m,n);o.setProperty("left",null),o.setProperty("right",null),u.setProperty(h,"inference",i),e.configuration.addNode("inference",h),o.Push(h)},t.default=f},function(e,t,r){"use strict";Object.defineProperty(t,"__esModule",{value:!0}),t.default=MathJax._.input.tex.TexError.default},function(e,t,r){"use strict";Object.defineProperty(t,"__esModule",{value:!0}),t.default=MathJax._.input.tex.ParseUtil.default},function(e,t,r){"use strict";Object.defineProperty(t,"__esModule",{value:!0}),t.isObject=MathJax._.components.global.isObject,t.combineConfig=MathJax._.components.global.combineConfig,t.combineDefaults=MathJax._.components.global.combineDefaults,t.combineWithMathJax=MathJax._.components.global.combineWithMathJax,t.MathJax=MathJax._.components.global.MathJax},function(e,t,r){"use strict";var o;Object.defineProperty(t,"__esModule",{value:!0}),t.BussproofsConfiguration=void 0;var n=r(7),a=r(1),i=r(0);r(11),t.BussproofsConfiguration=n.Configuration.create("bussproofs",{handler:{macro:["Bussproofs-macros"],environment:["Bussproofs-environments"]},items:(o={},o[a.ProofTreeItem.prototype.kind]=a.ProofTreeItem,o),preprocessors:[[i.saveDocument,1]],postprocessors:[[i.clearDocument,3],[i.makeBsprAttributes,2],[i.balanceRules,1]]})},function(e,t,r){"use strict";Object.defineProperty(t,"__esModule",{value:!0}),t.Configuration=MathJax._.input.tex.Configuration.Configuration,t.ConfigurationHandler=MathJax._.input.tex.Configuration.ConfigurationHandler,t.ParserConfiguration=MathJax._.input.tex.Configuration.ParserConfiguration},function(e,t,r){"use strict";Object.defineProperty(t,"__esModule",{value:!0}),t.MmlStack=MathJax._.input.tex.StackItem.MmlStack,t.BaseItem=MathJax._.input.tex.StackItem.BaseItem},function(e,t,r){"use strict";Object.defineProperty(t,"__esModule",{value:!0}),t.default=MathJax._.input.tex.Stack.default},function(e,t,r){"use strict";Object.defineProperty(t,"__esModule",{value:!0}),t.default=MathJax._.input.tex.NodeUtil.default},function(e,t,r){"use strict";Object.defineProperty(t,"__esModule",{value:!0});var o=r(2),n=r(13),a=r(14);new a.CommandMap("Bussproofs-macros",{AxiomC:"Axiom",UnaryInfC:["Inference",1],BinaryInfC:["Inference",2],TrinaryInfC:["Inference",3],QuaternaryInfC:["Inference",4],QuinaryInfC:["Inference",5],RightLabel:["Label","right"],LeftLabel:["Label","left"],AXC:"Axiom",UIC:["Inference",1],BIC:["Inference",2],TIC:["Inference",3],RL:["Label","right"],LL:["Label","left"],noLine:["SetLine","none",!1],singleLine:["SetLine","solid",!1],solidLine:["SetLine","solid",!1],dashedLine:["SetLine","dashed",!1],alwaysNoLine:["SetLine","none",!0],alwaysSingleLine:["SetLine","solid",!0],alwaysSolidLine:["SetLine","solid",!0],alwaysDashedLine:["SetLine","dashed",!0],rootAtTop:["RootAtTop",!0],alwaysRootAtTop:["RootAtTop",!0],rootAtBottom:["RootAtTop",!1],alwaysRootAtBottom:["RootAtTop",!1],fCenter:"FCenter",Axiom:"AxiomF",UnaryInf:["InferenceF",1],BinaryInf:["InferenceF",2],TrinaryInf:["InferenceF",3],QuaternaryInf:["InferenceF",4],QuinaryInf:["InferenceF",5]},o.default),new a.EnvironmentMap("Bussproofs-environments",n.default.environment,{prooftree:["Prooftree",null,!1]},o.default)},function(e,t,r){"use strict";Object.defineProperty(t,"__esModule",{value:!0}),t.default=MathJax._.input.tex.TexParser.default},function(e,t,r){"use strict";Object.defineProperty(t,"__esModule",{value:!0}),t.default=MathJax._.input.tex.ParseMethods.default},function(e,t,r){"use strict";Object.defineProperty(t,"__esModule",{value:!0}),t.AbstractSymbolMap=MathJax._.input.tex.SymbolMap.AbstractSymbolMap,t.RegExpMap=MathJax._.input.tex.SymbolMap.RegExpMap,t.AbstractParseMap=MathJax._.input.tex.SymbolMap.AbstractParseMap,t.CharacterMap=MathJax._.input.tex.SymbolMap.CharacterMap,t.DelimiterMap=MathJax._.input.tex.SymbolMap.DelimiterMap,t.MacroMap=MathJax._.input.tex.SymbolMap.MacroMap,t.CommandMap=MathJax._.input.tex.SymbolMap.CommandMap,t.EnvironmentMap=MathJax._.input.tex.SymbolMap.EnvironmentMap},function(e,t,r){"use strict";r.r(t);var o=r(5),n=r(6),a=r(1),i=r(2),l=r(0);Object(o.combineWithMathJax)({_:{input:{tex:{bussproofs:{BussproofsConfiguration:n,BussproofsItems:a,BussproofsMethods:i,BussproofsUtil:l}}}}})}]); |