diff --git a/lib/logo/isabelle_transparent-128.png b/lib/logo/isabelle_transparent-128.png
new file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..425abfb6ccf321bfdaa04becb1c209e5b9fb13c6
GIT binary patch
literal 18764
zc$}14RZ|>Hu-#pj;O-FI-GXaycMI+ioZtjm+}&LgoZzmDy9Rf64es~55BCS$hv})B
zs_vTUI(_;~RY#~ONuwYVA_4#a6j>Pwwf}a=|1S7X|JgoalQ95*3?M7<Rl_s;+yG8T
zV{zfGGc9ciX;uKHkL`9NsxZ(M{kJ@;R*g1Oc;|zZBd$angn5Z;p;T7kuLPD^b!~s!
zyYIzX&rB&jE6vHJ&*t{z8vXdVuGM+t)bgPM65zvo^Zla<_v4nxb8`c0%lD@;<l$Th
zxY7Io{(l^ZELK)l>VEva+*WkBqyp;7u$=R|og`D!(l)2W`bNNiyp?P&W-V>-f!OvC
zu26FXJgPJ`G{Clqh=}<vvV!azty8Zbu>iqgnz?qAJh<fb;+x&$cYT{OiC}?ffa~k^
zuQ=gZFJ*`a1mJ_VDQ(}ylz-ON(a{kP?^I(kmP#l{kophYvQcFq(Ei`8q7a~rk6~aN
z9JCXUKYGnt-^pD}I&&{R487aUhGHFDUoKwIuP)HHU_h=!lmJ^-A=OlXL?p;Y`^e^}
z4Ku>y#N0tQ+y^ra0H#VYi(Bpt`d}lH=zYadlgH=do=Z%?x8zIA?+RaVDqotyJ|B+>
znY5KRy2*RjcNF`%+YKgZj)Na|n-hCn{V&$KAdm#J^g<0ZeLm5_k!?m#76NZU{}?Ud
z%Ch@k5?Me#68TEIU;m^A$}a9&^g<EeZ@a(6Ssi-fz$b$yL}-I2tCLaS>b7_D-YYK=
zu57Pb4dubSeK2n>FZbtvygF7e(!(BanuoWeJmcX;(0?T>IamK}ve$!c^G$z+Ox5RK
z+TV@PN>5Z&G&8*UQ}q&kn0Toi%6u()6j4XScDd&;p4u_%pr(wx6-=NFi|ssaNt?X<
z9oCR2?7!Xne80SGfg~0E`KRM+i=+sPkzuObNB#T<EoR3xX>!2VPQy4r2NcG)OS3}j
zL@<>2_!UoZT14fddLXNRUkxN94RidSC(B;>d+Sm-!oA+|k3K0rI#3dpI{a1vop>HC
zL*2?@rOUUy?*os^b5|rE8y@7=gspM%Bwlogu%yayC|&CkO{Q>Rp|Qokjz<n-bGkn!
z?-CSbmS0E~r-CN06ZvJP)_`_tRlww^MwJJbSx@+3x<EYhk{@Fu5^Yevoe$`h1b3T+
z>mw&~2+MSNIOVTcYnY2h6b*J+!Ux>>@X*I&(e4CwWY>k%vcDA+mIg1EWqQ80vUDw(
zhcq~0S<^F$8fYSI82Y6rbKRYu1qNbonYVkSz&j4WCHg&qt!Hjf^BzE6Qx!pHH|Eva
z8umHq$?2%nl5WVz+ylE<{7^;j;XfZ+*UJ1$Ml&$tzOMNzwJ@#?ZWsi_K_eMRXsibM
z2};#BGwo8r%{xId-L5~LW9P;$Zw&Jjl-|O$16W+&S*k%pNA9%W;(t$7SFEORm^%%^
zaA^X4&NQ9uyK&$I9U9}~x2&Xsn;tE?Ng~6Jdq#ASas)<uMrTPzWGUIL+%LLjXD2pp
zGe3N_Wv&){;E(Z?pxSb95OcLQ|C#gWG!(RYc{exp+pV76%Tom8Eee~kU(|?DP5Q@=
z#P7^4E^(8ML#;5MhI39p(q{H_qa!_oD;VOl^|?$&YKEOImxesciytN3c^;X7%*@P6
z>5r_-^8oOD(ji=^PC2bOq;qztUfyiCplX-X(y*4TIRKNOv#{(3_}1SD(529>_^@8E
z%SHWKvx+?i7h%Gx5gJ-Y=+hz2W_OjWH-@WS&CIxJ^T>hOfzt13wn_Gp(?r8Iq_!$)
z&m9F~rm7E+_QYwCU$lR^66F!_pL_-85HZ0PRaW+pbGmGJxO2xIJ(}o^j~Lf&p3HBJ
zao@M(eS{2cmTixJQvdz9Dq32AYL7w;h8rNao&A@W#!@xTKv%lxyW!Y@f_N>}#r`f}
z#_1(Fwf_%kiP&ybySN!ow%fc-Sk?W&@#es{Hv;Q0$F1QqaMGUN#9U7M^@plB=BeYm
z5=e&V=j8my&MUjU#)QjP8;H>D+&uX-W})&PKw*;Zxue{sxg30s`%(30gY!S`{IS}`
zMO3ep+fS4w+2Q3F-i;nV0=8zqvo<<bVcXn2e==FWH2>jacAtHJzB<;p^|$Zj#8)nf
zmX+`5-~h-KG8ulS(KmIdAhYlReyp>BiuI*@><pcYVJo|dmIev(H#-I$)f5a*t&h_y
zf1NDm`~F7TH!_0b>>FylFy5<tdUDbxC$cH>M%;Z3ww^CfAso9aqVxbeQ6;(aKgbWo
z5*s{i2y0vBTNN;QjgB_C4v*^AHQVAT(+xA4Y>*iU^3F$GKKX+l@zNzO8YdeEB8p7Y
z5xz__vH?R{@36F3s?Rn>EGTZl&nii@^C!~?3tF*9tE}f~ILoaSu_WsyZ!~2+MAtOA
zv;d+;N=Ubb%flIWK$Rq!QIU(;ZzGZ%PK)5JKG9IS4g<mNA8p-6yhTnqHG<;N(wlT2
zPlg{IAeEnwIfxf$7&{xN7Iq5tVF(tu0e%t6|LTZDh?X2@r&e@7g`X6}23fG+f3`=Q
zm?S1+EdfvEcHxVd%r?Uo6&*tt&o{vo9SLCLMn7bI?&qP&nL9C1CXTxgSrBK|^B=0Z
z%Cy`xVSm%XQ7I%&>08&CzICj&IlZ!nO`DtUhu2fmo$c>lYn5Ds0|R3Eo5q2Hj(Xu-
z!B;mClHMQ7(|DO=P*sAo=I?5sW^k4L=K2@J^n$(8MWqXbZf_;vk>Yx@y`nO;{*;IF
zx*n<6j{J1I&INE-Rt0AWcXc^3VHm>+Ol-aZiQe~9dV@2InI2tVAC6}Jy6fmJQP2xx
z^03U$mYG4{_A${NWrU!ls$kivZhtil9$Sf)nk4`p9=y}9QA9q&dp4E7A+<}u72UQP
zwrMDVH!_RwTqS<XI*CUY``~@qrz;LkiI)Xp6Fa-muCib3_Hr|^b&-TT-iH(4PX%NF
zBsD6jRh?(za@~N1T>{|JIBDZASH1qt0g}IwdCzb24a|5Ss`n<A2Z2IbTHN@_!r*3y
zpzds1>KbZL1C^-AGYmK$^7v?~_u8RIgok^){i<)EuU{B<%9T3o-W;r>i6>^jSn81~
zefOD|BjQh<B4^P-f>-Ddq3CeVkdP|=Cm7hJ)pldiZs&(Irqa@l8k4XhJG!5=@X(;a
z&uws7B_&JiAI<Qh65q&@4q{Tyw_Wq_lKk%5SiOZuuS^c8C?G{Ji7yg6vt_X0SEjWO
zONQJv0g&Jds^FT$vgpyJ3e3poo?n-mPCvs4SgNpHw({~Ap+z{BEvmLrnnIOi8o1EW
zX;elj>z(Zfdn4gNGU{F~*z6Vi5J^hrZ3?a6@;ZLOHdy1{mM4*^+zj;&I|uR06naLz
z4`PW&0eG^UDUk`7HcjqSPR^mxjxsKl`rWUnzlKB(h~I@X+Pd6t)6eH-jcx~ICKX?e
zZ-@EXC7)B_Ynul{3=XivG@XA&QIHsx4q|z4QQjZ+=;i`G3huY%5w0G^7&&~TS{men
zZ*GEH*z&NANhl$FRf{W>i(?pVav)Cu{@vLjUFiBIh9N%2g%3bqrMG#%I30^IR7Me2
zm(crYo{{i4h-Nb<TeZ$=;kNCfIt%QN1YFufCMwzmb}9n|uKTA`4jyO4ln^nVnes|*
zHpj9zrI=%Ln<FOkwr<|i(DMhnrDC%esBo9brf0!;%~{(ceC!U6seS96?k(5$+<yFB
z_zzQQ=m<ZCi7E?Ir5Q~6uy*KWlvx`4*WW1g^{k*U)i23_v1q5pUP8v~KlvpTqUmvX
zlU(251HRI1kgmM~no-LOd}1jnex`plG9aMvWe)`XV*jz!amtvQIsjww;blPes0R-v
zY6oY~ull^}(>F#X?;526+oQEZ4_1UT5}-q_{tsyZtexZOwJkmK16V?Lch2s=$V2=U
z*EWhF0+qfB_VTu%1(Z0_wL|QH_BDBLZYupZz(Y6s)(N2tNWYuFhaMwS2vS0PI|3u|
z$#b`4eFZb(<JU5*(Ba5_YKylD(Z2d;^tAze-N+ncQ}b98@#6K0@)a6yTLd!Lu*><O
z|C*Hq)sd|60z2N6Xv)HMZDAa@{R)09+t-H_c?40aR>_CXX%U&pb9-37O!vX$j!=h-
zo-0n=?Hz6@fMhJ7xtSgVh)peFt=8Atr+#%_Ld|>gji9V&2+FE{lpZ6^GqiL671R>w
z{SKPp+~UE46a}PM4&T&;$QXo&14y$sX&<q`TdPxo7<4~dYSkefR0gHP9#RT<z_@>r
zr}i5*AepbGfYIm;U!_hTNVM2^vTDHB*W-l_(xWLFU&H%0MMdex5@jR(RBrRf=khj&
zc377&n>KfZ;O+?gH23takr31tMWGKvEK0y;6aCHwx7XV8N<{nHRf(G#Gc=@v$JtVx
zjb-xhE6yV(=xBR~!eFhmi44mc#uvvR`0;tCmwZ=57J!TTF6k$Ziq@qu(3yi+N@$H@
zkHZCi9uoQ1T6qyt{;+@nDT09a=rdH}8K?nc=f_=)g206aPxtA=5UKDS0q<MuA%bre
zC*BXS;>`{uM?7qAYaPqfX=mqcztTd;t1j4KSek~O_+cxv3L$yT48qjFO$W!MzBibA
zPgfI|+}9r@R!R=gI9P`kHtj5!mjN*PmUjwlsz63BL`+nnT2z0@YIut4^?Kvu(T8ZQ
zl)YzPpHZLXOOK$ov~{^P1r^=h$Y_eD@Ff`dm@BLl3P7^xv54Y+eD&8u@>4t1td<^1
zMLNJuee?|Jorc0Q$T6^?6F@7h;J?f@U>rJxNN+A}jXa_9cB>-%GR1cC4%(@ggJOsx
zY$m%6Hcp(FW7|7fweweD+sLbR;bB5T07ClA%}_Z3P8}pgjJ^FZb<(IurmZ;it<7Y9
zcW4YhA{Wx_@ttIghH+Sil9Eb_wv@G#zj<}(_0QA)fEjaneE7K1CGJ{YlnfrnyV~Ba
z5hXjiszYN|e9)?5$|EJ>M5ibaR(mNjnd~S!I@rKM{E;(VtjS2_#lL&utcM7sdQfB-
zKB<7bEk}BG=pl65Y43zP<;4y~;jjzp0vEaIw=RbMeI{o)WCNjZu~I@Y$*U@P#0xt4
zymbWn<~N9K@mgTgJ{S>Tx=S`77KG;9j&sweENt=7tW2DJ`}0-9bv1kN=otL)e3yZs
z;XvAY%Z~t81Jd>en|ZmE$()j=oPiJR*0;dG7513~a90;Rf-HUMpVe6Vthit1Zm=Dl
zK{6<F7?!pXQHsS-YB#~<ipXqdM10~3NDd?R^^=XHK9#0tjXJ_E7QLW?CbTc7Lw2ny
zhSBR&wHAb$LjO<0AU_dOON1iX91fW<1#*^_dk<^L9`!C#^*@-;kAIvGv4r$>O&(n#
z--~dnDxC+g8Rf0%%E+6hRIu^pes(m1J%wX$2m<~zgeMKx$Q@LDOh2j5;dU}yq$S%S
z6MZp$C3fLtygfUPLBWaPt+^z!TXzMeu^31XmP$@*HB(_(LtL^3Bmnk;YekWNqHwkx
z7~}dyVQ<k=O5(|;LP82uIsQu<ya2Kj-&7#Xp4U|ocxw>IV6UnGu35lV>Cg&|5QTde
zYBSwu)6V{bw>?sJ&+*j71YEK<mIoOrux}C`9?EmX+_<<MH4%rTIt<q}?Tk(pQhX|`
zwEOj<CkwbQ9yxAD9~RK@oATz3V`RKwI?&uAVf?q%CobLQm#KR-24x*y$4(Y@+Cixu
zM$gR^)~WlA9z!G|sW?Dxx8jN1?6A@IFJvAa@oYv@62s~=m}<<srP+YMs9L>$7+;p#
zsYwpur#5}>kR<Tu(W7zLtUBn70)(xz^O~K84heU54#9A6Y#a#fdS}!A8{8d*6#DqH
zXJ(X;pD^>P3AfNGU%0EfWbVpGPc6t_h?uJFnf!u8qc4R*TzLG5yZfTZ&Q{;>FKiOB
zVu2DO`d`{}S;Yz5!{%5($K0xFJJWh;L=|gN#6vDeU#EblBU>&h!~4|}+PK5w+~>N_
zoHjFPsP_h2M@PZS_1as*1%FE`_ybQ+;Ep}<H*>mz&-NSH*j>eggHTxPnkfLcEe)64
zjeBIU*%hkbdxiqbSPB{%M)XIH3}6YMttH!$Nfm+@0%=ufYILel3+D1`V$)g>RlD3M
zCH)*W`}G=sh88sGjykRN7xGI7%jMJYwreL1NzO+&5>j`zN>7R@<H^&fDO5IgP-Ptz
zsKvA}0YO86k&>U{P4;e3QOOYp=ozgizj!sa_uv6<jr9JG76E>-7=&f1&k*4rc%it;
zB8;_B&gghek7<Nyb9El-m8_^Kdxu}VA$U{+y}DlT|43cz8DAo<O_noQHVYaOLEyde
zU#<$5rAO4C>Ru@gpEHK_X^fphEM2D*_e_hyzL@S!0nNw@0c`OOPj^Z(O!xS7#4APR
zcFv;)*<n<0PNSavwsi!^KGm!3&V-C-3uE-G%Hi2swr>v_+OJj8xMk4VTs%#o8;8KM
zr16rEje=|<%fk_sf9h*DPh9_@1XN7Ws>Ib;tj^xO2~H#ZW*{>dRXpULxig&gdOtL>
z-R#<x<1Dsx{CAHSh~rzpX~o(fVYX@N(&vooNsqv-McOmZ*sPjtga)T)gpBquaQ-XR
z)2EhmqzzFTU<n>8W+?Pb1mU7-Lw^}CiL3NZW#KrN>4w{)tax@vqbwrnT;g>k1JZC$
zOqKIVo^8X8&8&mpXJ)MNbHhh@{WS*Q@@dEcjr8O?S(u^Az>TBwG8pZDNJwoNyQ>JH
zEiGHHFbXczNeXH5MPL>2%dNQ~92^u>M`B<pEgn`WyN{jK=|k0xabDq#&6!|=`0&D=
zEZ&cfBe$a^o0(p&{f*>RA|e7awF6hXO~2r%huK_KYG`qrS&PR5aN*B7Si8g+`Sd&x
zuD!pdT{%hq{32=2ze55D<IPCMtPd2?kk!~`k^SgGwnsi=k>~~}+GSTovf?F3OmXia
ziuldH;GJyGN%$&oWA>?S0*?3Ic~B#yaRLlwx3sCj+|4#NZnfm;v?XxT%)}Cm$EJ?S
z2rSIrus|&Vv&32i5!C6+YolYJ-~O->+@sIDgE~@IWLUH@)4DMI`r=_L`4;u9=XI3#
zdx5xhPG?~U6$b^5W$}T`c~&e8oRYECUs;VR5jx6`uxTBC_;z>S$kW9OGS+rnp*2d3
z1ItjyA9Hl`>P3c1YRbm-0c3D4UX^*pG8sS&<1l_yWp;^{0G4C{tgovcQio0F+h+FB
zKBPoG!sDN{@lKQWPQN_7)~nyuOiuuGbM}lK&BAux*-I^jj6QkB!pnAs1IX#PJR}@!
zg*;W`Q1K$Kzqe68@Uv1ue^5XP@ys(45j0dJWvb_B^_sqP3ejBASN(ALmVLS2{@}lK
zM#|+V1u}#cHcRQY%gr;oy9qdhOV($7QI`FBK3g+Q)zaGb%kkrj9o^>WNC)^)d;(lr
zaJt$|3ca2Z8S?rE$RG&0x<(9&Sb`7W)?MQ619yKR*dpQcO})sWQ|*sYjBM%FBR-Vt
z59h{<-%b=CKsK|}ISVJzvN@V=69Pvv;O|&QDO>(jTd|5bl@EUW-b7NjerrNr4M>oQ
zev+M8l2J3FK7VrdOJs|e>CE$fw{g+NF4v_nnnZs;;fJrQA4vOqW>m_g2HT>s6a9qC
zJ*_?;7^nP2Yrj&-&z|_+ttJw#mU;?|*5sXLK)Y2U(+Mc+kzG#dn3C6+jQp{<*WVN8
z+R%VbLJ~sUe!nw#C$Q9hQ(^TxFJP+5al;4j^ZxVp9Jz-D%#P__cE@*$y}iAjp$S;^
zUjw{)4zVu+bES)nKg?V7ts=h|`MTOH0>{EmKt`$?eig)3#Ea7R8a%FzRGLR~2&ojl
z<`V6{ER#8Z2ue7qsD_ZY-cld?s-|JCA^TZWlAa8rN}OL&X$*l2`j>#q_H@J=^%4bj
z1c9!%+h(>wN$U27N{|%X7L~I=3kv!4Q^f6^o!HxkYaTiI(-+15ezbQRidPHg5D4zg
z-^PhXZ^5Je*>gR3Cu!VIkJs-%?N=Ju{Rn`mO!QHRXfa`#ksKVfQ~fb|JUuLn5#YN<
zX?pPIEqIjy(r*=i_`}Qp!I-1QZ6yUsI~@#hViVpccq0du6(CTwhfjam#BFX~-PzUx
z9t?c{H6cxmj%OV3GcQAsxS{pUk-vOvP0NKTdLfXXr(q4lQcOt4+UBdWG$f)n!TK{g
z{qecll{6akevseJkdJhK{U_$5x6V@mH=+hp{N^(JS6#73zNPIk`UO^=faFhxOy{BB
zMk&HIH1aFS;I!fJexqgoqhc*7F!?)_x59-N-rxxX56$XesjLZ_*suS`N*}JU^UYhD
zIq%`qKZ(GpWp|dk(+5KdNa1Vf#*FHSineA?I0n}BdGn#u^J>)N*(2KH$(}N=-z_rn
zl*!a2YhF2!QsU|Bmj&O*s6)q{jZV1R$NF?`Uv{-;)W8DZ9YcYz6dWSEfEu3e?S30U
z5&;#*mgSfgqt~NNjsRS;O1DPzBLJq<HC4JIPFFm?D&Ts<K$VjWktivsb*|dM)!%M&
z4Kh)In@_=l9I}F|GcSk7C^9S6l}Jzm=xm4p-2VoAORXk@;8dmjG>weFXrLe0A;1@_
zEErI9ze5ZkXko9vWJ>S0#ITSm_75R^t)jj8C_w?fja!cSR9nIl|6E=;V_HvQS=jq2
zqSx%7hw_QtH2&$v>dxmie5>2&x?7jYNDU92cpc4VbTl0KG>S{Iz1G?tW}$i`&geoU
z__p`odt@EVgr$nNxuMD5LFLw6G^^^Z;o4n%t{;d`AS+iJ*05C4#-M;7w4c8*!mT}S
zQ77>*Q~hm!(A|Ca&|OkH3I>aamnJ^_Rack(5S|%Uh?MNvGC!-V?it#r*16n`@X^FF
zZ(bZ4P36~TRAHAUPasoJjs{2z_#}LPHw8J>M?bf8ZNT2V+86w)3{9?KQ;3QYRS*SK
zGBf9YHFt8mmvD9ME$Rp?lpKmBR{t;xziLN-Ht8i?)Y2kh!{kDUZ(g(F$sw-0p;M3Z
z!s~{2mPOU-I!i}Hc#C<IqB>4S<5`AL<1_m@ye^cn{@$NN-kngay1D}|m5q7}U`meH
zzWF%sz}Z!${SH&3UTQyO%ocV7l3uPw1V8q$;dlg;CnDbYNzP#(%Y<6{yBt)(c6&)M
zuJJKI@4ax3&dmXeZuaS!x)l9Wq)~&>WV?%S)P$DVXPjHwjhIf-mY}F%xZud>Ei0?I
zU4r74TM)<zMjUC0EQ$VL<(s&=DgwfcugWqHvL=0j4i_7OY)_9<O=D1O8^3<`Ivbns
z@N#1BKN-=w&+n|%5aeOm*Sb@e@y@YZC#|BNqL!|4>fn=e?v6diVO&U!fuLT8ar%Sg
z2PbR$hCs2hNGT@J8<wh|!5Gg{v1)LSeP2hg1UPo!*lVg5ES{Ggc(%Wka4Cx+ye-%}
zGUeBQuGejR+{^IjIoLBfO2nTjM%Q>A?nQv=>2r?8gq23!TeQGiuSuE&=M5d(fG<yG
zhA*|cUsxE@;bN~7Aat6Y!hpmMthf(f(n-N*i2CEvssaAuF#ysmS!M@n%`rmNTc$PC
zq&EAp=ZfyOqb=P!M9S60YdPpYm%R(uEb>68i=xWt&1%di2cPcl?nvKMF<)tbOV5J1
zLl*bPQ3(;(40ar0B!8n&PHMdUgu6BiPv1QEWz0+<njdnszJ6%Osm!ZKIEz+*3{f2L
z6Rokqh~fBT`8GT>*?6|}F8xa#vPIF)>j5hfC%>(;jIqa9pWcL^66f11k4N(lJe_U_
zqF2FBP>D_APhwcZjSgXz1*o1*npcN-QU9i1_J8ty)-?+m$JSnon49jh*IOcpV%MCC
z9D8X+hhjn2QD@P~re{cKIb)1u0H59;lI{|$>`}FS*#+C(`$D4&N)<2eTp<y$Zpo%q
zC37wbot&SBPoWBSfj!6SxlDRZ_u9qJ{xpEGU4$0hjB6k6Z+#;uBK{vpoc?nTW3exP
z&mEU9?;7GOw{PNEw%>)eLk$+HH_sCiv!xJ4!B_Ho@N8B#D0PDl(79*^ek~_+<KJ{T
zjWAw}nKi}6JW8JhRx3Y|I&LCWJ4DoQ--U{*gT3S)ICeFib{k$lniTX?;eV5f_?Jaj
zYoC%WNg*&$O{kx>Q)Yz#%HYUghOx<H)YHTuT*7(Qx3-|^bJCL2LWVU=l42S*E{?%D
z75_OJL4mqqF782eykIx2DxC!>y!H9UY5%RIp{FOe1AltpZ%B>MLlL91MVd8dN}9vm
zqmS7rv^dcJk|+_>Z8c@$P(SpFbGM$DG%E|#z`#roY#jK>=4eAKg*GXzzvpR=%-WOe
zoRZF8g_!Ycls#e2c(9*A4jAXW-0M-oVzOU{!iLc*t|yL1n5@J?Y#$J|>AHi&^)7wo
zC|4IebeMAW*nsJvQDOSK1a=Q+KEBE-;<ZW45a_D%`+JZNEY|G;PTyt^u91RwE}$)&
zb}7+3l!U*Hjf10iuhe*s>Jv8_tNbB8{^O~ykgDlfbjReNjwJYM5r>@J`Ej?m*E?!a
z3?RIr-C^uv>F!sjur4hB#6A5+TCbSB)O6whdoe9#o>pl>*Ujr9x{f08A~-quOKF7+
zwz1;2!+4%noC%CJbh1rgT;cQ9A}2=B3o{L-hUv;9p%RW3%Z4059|<DLOFX*`jzY{I
z@<mw^7inG4ri|IU5#arg|8~z}d5fx9c;0CUZ^C{s8>b%Ke^R%h77KADDmN5RK&eHi
zLMScz!~qh-0=YVe{QgkMWTzO9$**P=>ox@c=xAt$Gueg6`~$L=%AUuJI{9NC>r%Go
z2+O&iC9Fmy4?w{t+d(QSSGDs-N&o^JCzE_R+Xva%Z|8nU+{t57xA3>*b{Tk=L`*v0
z@p3*U*zM>aE3_BUNQ8boV+rV4J-+nkuqPM%-z<R1U~=Nv_V%^%oGcL3vC9XWE{_QH
zeoJ=7!H@p}XDDRKOR==-Nk(J(nI^_CtdbokTYC6&Cy+91BBZmE7;N5kKQ{=2_DM~S
zC!A={%Mxdr6#OwV|FM;Z1@<e#&?a(<sf$piZG{?HBXemAMRWb|3<VUK@-SU0h++T(
zCls7bgVXbnruW0Ij%Cawh>pcee}&CmIYnNYm_Jepb(=VSZc-u$S=S@1@g2}l=5sAE
ztX@20{;?M`y}I@ZBLSw?@9n<Z5NIxH+C8UA`wLXB*Rj{jZFhhqyxM(&B1>wN+0Er7
zqq{&!$-&9OV$f6WySDCYY-1|*olG49PTsrhokKWfWAhRwfHtP*EQcRs*|1aC;{?9J
zL3_txaf>HqVzMT^z*5Q1l-fO`vxuReOh5Dc)GQNiIlw!0h6ICo-t#F`*8Dw-VFFnD
zLnJ9;0X#hTTSuO7p5^fQRSf-fFhtnyY}PbT!rdyJDr003d!b;0h^u9E7=0=b+uw(C
zbFAOXkp)upc^+uW*bgycZh;d2PD>9RiSt5>3pJOXu4(4t2tp|AZ7UyD<T;?ftpoKb
zM3ak%3xEBs@xHUAfM7F$xMgSt{iTKU#h=ku8@~UdgH5)8sRMh>+j4VX@MH-(Kf!8S
zd9<{(m<&X6L=$k49u#X?FSb!j10vwaWJwc{uqc0?T<3<P5{J}^Bhg<hn&?V#ExuqC
z(wM4@`WR9(u=~o9&<FD&qr}wMPO&)2_xra>fR{v>L!!xwrbGk+Ryi&_61Qerm0H#%
zTAw+-&y=F`R4_Z4H&FY`-{$|J?uGZQu!65y=qDb?TsTrxBet=Du!crCc_jc!XrtKM
zOHf?-JwlU!^ipEHCy9Y7l3UueaAxvSg!kNYrkj)YrHT>K0d27VhUIG(Cmd)cs<QFD
z7!HoiPWv&8&sYAWR>uGYjhTyn-rl&q_5CKR_kBKcM_KJj`g4?WvHX&_xDDN`HS3;i
zC}ZqyXm$}_WHG4mktE^yv#RnFzrOeo3!$<=u9b}vYV!|JUo!V2e<(OED9At=pJ)YI
zuSXSnYt(B2Hx8#TQMy+LgG*zn#0=1*vJpLAEDjl=dNXjotid7iY2GO#6nsjZtoXQB
zb8g}q|0cP%Vj3;a80~fC*6J42Y-8_aUP<jk_jlR^Oop|j06}Y1wcI8rK)}u*TNwdu
zDzHJ7k^a;SF9J=exzZyfbnuBH`9Yl&3voMstabz$k)a6UHMZ)+O$s@|Zn*1w;v?__
zhCJGn=udLRbaQoIvwsow>O4J0#w=840rU-7u|9PrR?SgEQI^1H0@8-ivu1BU$pPA&
zG-k&2on0(McG=sx?>8+SIVkIXPXl~%hm&Odrfj|iEAY39qRtme<KvYF5DQVOSQc^J
z6S3PPLR7O_uFnzZ+2sG>mcxla%#uWc!q(bDMReXtZ!41E;zDh3ef^-t--6abzdL-D
z$DfKzhL+l?=nR?_8#)yNJ90N9($t&N3DT!8Y!Q)e_BzrM12CQuSx4qFv`x>Un_$09
zS%PX3L~)R?Ri<LNn<QMdk+MHq1e$(0)XYr>=5z|-S}96R<kMm6eWO$!gC|m_nBg^H
zYdT;R-;LKu#^)<gS<f_-pRQ!^`Zu@+Z&usHY+6Y?Q=x67p>^ReM5BVsOY?Fjji0v(
z4Y;!bZKPp~?KeZK%U9MNHY)G3e%`|ev}W*0#bky*ue_C(@s7vr_<HXl7daoY*L+x8
zmzLL~q}P~kTY?N{+X<kU@dO0r?3OY>iomdhSJo}aAvS~~uoB^kjk7+?ot6SBL$sAi
zesQ7RcmC&JOXnDP(W8C$!~spP%PV|i#VmqCP=^_4sD)9*c@@&4W;f1^l1AKqC?=Xh
zfEvRst*mK)2sDkxT@@CG_*l4LyMB=<&Beb4Vf^S1y_&-mQ>N<;42i1o?IYB9us}qQ
zV(tqwUX4b!%j6-@qd}p(BF-bwO^s$baRM9fBDLnkpgUd$3j5BEfVn&UV7Jt}^$A$7
za8@(lns<C}Zf15i8B-T3PxAO9IK5;eU}Wzfl1BKJ1w*@kzN9@qkC7%Me)(KJT7HBR
zFB)21NAP$^bb7~0Bf|l{_-p|>dwxvV11b=c#U~B5Nl;Qi&>!v@F@V_4R<>4a>kB}S
z=7yd-*5cihJ6m4=i!US_>(X*tqH@Ml#H2<?;YP7UJGumVv}8WTaxEEvl)*h<^tR%^
z>Jr;%<fM{s02rn){TB&7AQSff_PiDeMvhxP>$I3n97|~qI|&hmn98ciC!-wR$Wv|B
zor9QDUbR--flpeA`gwWk)--?{K=MaDHd~n3*M=0KLJByOx06K$0DZXmr}nx45&~BA
zYdvuMhEaC6h3kqaXmbfUV&qLluO8-(OFE0uXUXS%W8G+bt}HJeJxvKQUv8*JxyRRn
zQZij70O6Nh3$QR6<B4s~BQ(Drvs}6cg$&%{AsRplr~q3I<X0lUS|$Pgmj2?2*rD~V
zbGF{P`yZ?%(Rw(&FJbE&F!y_9piuZpLJ%qc0dV(#x8&&fW*ziIaPf4asEyzLJ=gr5
z2@S>cHOkp<Ir(L7MPzqG6dUQ}Sb0K6mXrq3^SI>JOR6U1p)9%i%NKG;Brqi=A5jJK
ztb&V<ksI3EyY7z$Jo@Jd@<k#AW&TDI_CtE@I2#Q36*}c>YGxmno(}%vuo9qr?|akG
z5EW~Oc{p5f>2&`xCL@cFN)5}0Oq3W<>1?4t<wx+CG!&1J-2(Kb2&JU<;#I@qNLX-W
z@d^Tjr_9$Dh#&!1T0B&8DFMx2DwWhQ##4jV*B25r3WP2$YN5YQU-;0gHadcK6=C(=
zu5PH;rZA!CVbU4B@?WvMy)DzNF9Lmj954TIt*!jSLZRt4+`tcAlt896V7{&8mh`gW
zwHdzE9DMmTw*kaa4d895LZ@xA>rZ>}Fj4OgnE3G_22#<X!(B2<N#!aWw?`-7dvv4*
za0ao@O?H$fzbp^Q=c*gF%{wl|fA?S-|AX=Qb7c9+#L}#1bkxhNDe3~lf^Q(Jh)9@=
zh@rI2j*P3#X6g?gEM%hWkXAbuV+B~a`<tz)be))`VO9OirOqsY%5mZ?YaB!#T2dV%
zeA7(^v>*Q@AmW&yJqsBdn9EB~_bJG#-4sM9)$?is{QA0VtY6lAxbq(MfZ!<yQRZYq
z&!?gK`#ttL*$W%<QGVsPM_UsKS4!&Wa6iC}9qb-VI*R3u@kpMCkSoy@o~#?t1skbg
zUrRnt>J=%qcN>$N;I}+D2+|^IF>Wo!p`f#fjaCr1ShnR3sG~Brj8E}=BRQTj+^`m)
z=6uQSHi8e>jp%r7<h?)k=(r{I2?b;kqHUd4`}LPOvY4uTT&u*NhBy7u?VTM*R<AoS
zzKCu#e`Uy=AQPwy$a@@C;9d5D$}maUDIm7BctJ(22PbGU5$<YPR}(Z0!r;jefPA~y
zt(rYk==rU+=jMB*ZpELCa`cF<>Ld%*(43s|$xYo9$jM;wnHy+aEW@c_nU^xNe&xAn
z@3plRLOYSlO<(g;qtqv-bQLMa-e780W)N)KT8za@(MIhAhmQz4HGufQ79foqQZQjA
z2Jo4jwff*L7Uq?puu`{Cme%Yxk<(z^yLW61j<2;MOZ#@1+rdP7g8b}l59{^uub18G
zEng^VE-J0G72Sx3)C>2Y{HpTcuR)(oHYzD1@5axyowiE)$03=4u&#{*GV-LMq0gOk
z%-^@<O8MQb(accn=YEht6t=!f#sV0J=yv{6NE)ME!um;qWZPBCCa|_}5LGN9-w-H}
zXPQIG+i=h38!;Tr;9L^Wt75Bk%+DZv44>$3PhvBZ(KXboS;KF|9Eq^NI{2ny%6J$0
zun8sxf#&F?qdfS0_IE~AfRFipZ+T_x$ZQM~(}=y_<Z%Z|Q@$3@Z*k~kj+(o@q94}q
zuC8p3J!<+bt^^{vouPkXhVqWz&b;lZ883ySi4}*Ybv&?<EVbiR6^808#%8J={f|x&
zrwi<fZf|e<AK8)E1u6(BXSI4q7SMDFK~yETeUk=>a`}C5-2<8PC^fZL0W#mPQp79i
zim)(%$<A@6@3%lieBu%aOlzWBKw{DM6p!RuDfg=)sKy!ccKr#z)B#zOi@Ma+CNB1T
zMND3kplNV$SdDAY+sdOVw1z)GH1;~=mkgfpfoby4GiA>R=9u@xR_t{wZYgD=hBq80
zFu0mZv^54zD{39x(mJyAXfF(Fi0RSx6!?w^sx)fmVjUL2r0|8YtK399-oI_eYe|l4
zJe(KRJ?XSRRm~Rg2c}i)iyJz?5)64-+m`;aAB!t(wx#^Si?}<eK%t2r2!X2X?Q0lo
z|HWIg_3?P-NZ7J<b&d=%l%~d(M55251$|c8H+>tOi5$+$hfw$7w7daN4(YcB4-T8-
zO!WFPU%7!NXU?YO%wqFkHf;DUV;dkbHMJ`l=21lj*~%QDd{B^T+6oa-S(@@c_kheq
ziq!jiQC~GyrlWZj*-0&Q+cL9If4o=#ju1@z8zx9*2yX$urBGrB)#MXRxUy2Gfb+@c
zAf8x&t(N0Aj3Yb*A!4D#eL^2)=-J~Vl8@gG9EbPfRbNI0@5f&hS!ScBo&!nJXn+E2
zm0{Na^V7zxCqAbotAwj7M>M^N<w1>EJNNX0hP1IUd}I`3?a!e!ecT>GMr1zsy)SL;
z1L8}nzyS;j3JCdyZ{c7FME@Vas44~Emp#5!Xo9$gN@2Hu^_ST^9MFhcO$KOuYI|%|
zf~Z%lZ5330vc*zYP&x{__U+wX|0B@Q;F@1t4#NBIN2!*iB20%mQnkQFRl~SMD3<u{
zg9!KOmaju`0Mj2D8Y~1uRqw}2E~*5F@o(4)n=X?=!7j2ZXtuhltaRFU7rw^C_ix}v
zXCYl|h4J_mHQmT+47CeUt>eRDeCOGUA0`nUjPWi&0f&mw54Eu1o^CO-$uG8E<UKfa
zkfvoRMD({+w2}k>?k6o%dR|zLV&1Q+XSN4HDM-*u_rQ#J3HsJL8ZN)smuP1)P`I;W
zo=rU*uM`R79GzmF;XtF6!mnI4`5G(%iP5U20%Xm0YUKw_4Xu!?d_ywjbYVKm3m)w1
zthF>|qM;q^o%)L;Mr;rsEEfFuR8aAUxh?#zg(;t#9$j9{ThvG#r5@DgR9us(vE7VK
z*8Yd&-)dA%ehRL)H3A!%Z+}i*UAag{-qxu$WOm{v5auP{OpovPpmI-O28#Zj(t9LL
z6(ni?-2ZJ}nOBm0`;^tcH{+7U<pwa0CL`3FYhbj!G*i#(w_`h=(TPk`n9GKt*As%g
z^Do7V*L5q)a#jZ6ihv$!HPjVmG}YxqleWe?nL8_r2n?eFKXwH&WB4xs>U@K8xq>Ai
z-lu7pqH3d(4-=UA3zEpB)Nc4032SJ|(&C#c4jDSc0j=EBpE-9aXZ|jrE`SW^R4q-d
zY@$)h60BuV#ljoey+FW_FvDcjPcraZ$5Ve8yffg2i_eT>6Uo;!<}rwKAt6YSC)c!o
z508yl`IUBmlMVek$rrmgrBDolch(GE?bbh4>UQAN)7EEp(dc)%R(wObSnr&gzvYx%
zk_f$^34u(-=8=OedKAtO6mhV4SKN96Ll~X5l2~g)jA&Tw6(sR9y566eD7?`E@G$mo
z+zhVweiE;(S4^JcI91DDr(AqIU~c`xH256-w`6YWa}#c=41E5rgOgzS&RZ4|pKW@j
z`V>nfA{04*Pf&xaRjv7pS|EFFYz-D7`mS;88JjZG**tM06WFsO8&J7Xb43Y!J|XNI
zT_D*VVtKkf>PlMi$A0Y&0fame)pfMrLiF1w@p*m_EMQ+0y>@oAw(+>kd5@=SNPg=<
zaA=M*lkOgpbs#$;)c)vpe9(UMTs1*f$o*usx}l;u7f^=4cS>LH^tx1bFfTe~i3Qiv
z2CeSq4~mC=b!v7Qq`ir`a)RrYKVtmqp9*LuG$H}9u+9zC7EmZ$TB4aHdXQRKRmz`C
zq&R+*$0zAZ=CjHrPp}myaoZuIBvdl?I-$YsN!>~mH#6D=^Xp)bV{K6*LZMbL3Z1Kr
zJ&W@&W>U;gWqxA;n+EW+J5OV$G@`0s2h2$ya<Qwa!8!&tC0>BTV;Ms}+^Lmli<>5s
z_h^1Qopw@@&9<Sko|r5ic9S)=qwoB^E4{?R8-Dm~PWa^&?g_ghPZdI-lT%cap(<sk
z`*GN_C3jFkz_F9tNhCZimye-c=!*dCn%eb83ZOFibWK5g{N_toLK8s9z#xGLuUGR%
z!&x%hFL5xLj2mE^-JY-V7tt$uHBKG7u-QtP$;F9$Xfp~4>(unMCb<K^8Oj9Kc)l&<
z{aE7#WPP(Mit5SvLN+^JwB|oPfnpK%^PQEq%N>-AtEKescp*t0GSh+JlMApbEOC5A
z?w5=n3dT5%ueT%OA%!yh6cO?!EQ>HJ=)=*oF8qLeIa~JtuQvP5bci;zKBSR~^$m(I
z{oEo`@_)cu7mg<D*5KuBgQkV=URsA{9#4WR(~*E{sZQOJkcn;@0L;gZAjZPbN{^N@
z9_qqEIu6cw%mw?hRgh4OIF^bC73$r0-<rvFVo6=@wQ<ARIzE~*0t)C9UR2VK3en||
z=6l^?9Y&8_ETE_KADWjXS-9f6dD5w}_Ciot1nj3<(wqEBbM>{4l>{RJ;E(!6D=&|`
z9Y12Tv#b5jK%Lh#Oo--fEPg{Iat>+q@Y0=fdd#;Zn-L}l2^I{Kr(UUO!VClhVrI{~
z+rHSG#E8t*-{?%7#&<ANakO?e<}a|sJ1ZyiT*DKr{j_kgrlZMTP82o8R7+d!cMC1u
z;z6tAd;1c`IHKHB7?2dFQ?pZ1y_O?HV>A080``K>khPN>bCACilRGxkP_AO5YbPlp
z7ZV?!m8Kwdd1`urBTPaUde3jr=`5B?A9rFr3;Q90#$U$Q@3>F~$k7wQiRqC|=`Y7_
zcAe(7@54p~JJtSFY*yzItj!nZp#4^KmCWu3ZLo3C#;@5QErFBiHS7~n!b?<B$<Z9q
z_`(=s0jS=vA=`UtC0AQLX8PTJS$fX{G|BFEFWIY<HI{wqTw8S@8>8G;AR4Jq{~tXM
zb}KD%F)@n#63W25dTK4@nt{fN`(#8L%%y*<WP!<mUQ3X^E}ewBzx?g=Ot7dP9D%Ay
zsnQvBg71G~$Xc*TfjA~7#%)QplVrY=GNI1~rWEeb9s8F`4>sprWqw&PGMA?2<KrV`
zl-fWh_CHjg;nD)+LSYK69pI4{-}xQ8&KSBWjzz!3!_eq}8<y_tNF&5w0EqZwl%rF>
z-T52z$Rvs$$x{_RKKhuGIvkbwEt)4?xB$^NDNH=>pZP<TP;Fa7E+fgeZf{a0U*G>;
zCD{8bEYA7nnV5yh_yu;@60E2v(ifpTwR5z6SzCY1sWHD`ws#a!Q+tMpVu2#ztz$N%
zro6V{(05Ml`9Oe4w{;jt>|~O_&O`0vRX~D@+$>gu@uDc|MRj)+=;jQ}9<vf^7H0mW
zh*V;-*|olu(fxT}$S0x1dTlMqg`W@|sK7SVA7R=8FoiKIWnlbTS`r8B1gT`^Ml(=|
z8FZ`IA;*1Hq7~nZU(H+j3cxyfdIw_Yv^Mx4_%>JT8$C&3h?;_gs7Z|Ry&!n#qH6Q%
z6Hfr6DX=Ub-becKw?_Oq|1Y;(T=``-fzH2DO)rx99dOX~@Sm@?DFwYiYn?86L<;5A
ze7!LYa#n;Hm>P8hg_U#BGEO%K%zJog(D72D<bBEb(^8N)Gs<t+Z@YVh+H0FtAx7?3
zdV`oihfAlP0gHu}Ivt1^r2_h&GSs5UfABxtp(_%RFRERo;rIJ;EzQwH;eVE+YATA6
ziFUE#<pDoJvR|i}r2+qdE-}R0#;1_<CBFx(-7ul1T31M0+b4bE&lm@!;dWABBN1$d
zZ^pQt(rAjz!LUOnljA!K&xS^=5%)yWklxo(rfL?FWY}Sovv3PcSo|AXPz{ALBN7kq
z%Kcui7$=Zsk(|$jjYn+|KAwvm4#|pZdUw%mppbb@%ej&2Devs<QyS}L?*x&D^W}!G
z!?Gue2wi{j_Su8B)6UX^PIDD%P?$M%bcslJbU{V^OHdaSTh}JD2FHfNqXr+3LGr)i
z&Z&b%L~3u_mW!oSLd7yktf1G}<EP|c_~b=EsX}lNqOZx$=c8>$k`et!-qPgsm1#~=
z+G!wD?KmxV1E(g2VlPG(_<7szGSH;2_@bhEUBvVKEU|AU0cQ9Ju?0sfp;J8J@*?Eb
z{TW_+UP{7Tu-FRc+)O0wMcc~3UmU(P`(m4d96C%MrP5+UOS+l&ACWzUf{}x(pn&yt
zF+MahYG~z1BmR;jRrK9bArj>RQhc+ifHdHMTBnFjk9wRV>_)_3XuTcH>Em5ozs)mh
zRV<ahr%7?Bb=9kN|LQI>FytHFQYLKQI^XA<mGJzf8GP=8_588|Nx69-iRGw{kOG8s
z5kVF<+v!IQ0WLu%RK);G_}%>0ro7hT`isV(${HGqcwfGT-6&yzVm+;~*`~xEW0st`
zQE_$@BdX??uL*SomWWK#^8>_vValuHrcc+qJpB8WrNjd6b2~o`+8;$FHhQJi@yH2R
zuH5dSzoS!zxb3Xf{E5H6oT35wPD?yIT*XV8a@Z;CF@B_SJHz~^4S>s^9}5D$!(S<R
z7cT{2<U7u?rAGv-XtVbQw%W#b|A3PQ9GfkjPK;KPXNUwppD4G={(fuk?!B{ZrvD-c
z9ZA|O_}u^^S?`;PfnR8hBDGWS?wJ?H&RHeMpYV6fFEAf@lZulXimgf34v5YE+(tle
z@|BdlZXDTU>f`|@nVp&fJFCPhUvLdgG0JKyjC5+}ppo(M`0T-2MqaWOs#V7`?E=HA
z&nyxGp^#KpQ0EEEDWaT(v*P{&oLJp=T=Sg%-m~VWczq2+>Uwzr6uD$WCgpz_FZY_4
zs<s_JXv8vhn;HC;YtS)Wpa>Uv&B^ZTb61U=Umt{aW*>3<YoVu4D6!ip5rNJ4r6f8i
zDoE%{IH0~5hdfUku)K)RZ4A3ZF_iDWqj14z$98;@l6U=hjpg$;@m)e11(KM}Ua8=-
zZHI-(*hiKg>78$8OTOYq2kB}ez6G~kY0f}7++6w@Pei|c1)j@dV5eZ4h|Y>^3?pjR
z2GF^=islxRqgFCQVPsf5E;jp$zxLJch-9+nKoiiR$n_H3PIWFlTRlmHM`aUP{5592
zLc%uIOJ}XtGo$33#mN>*89Gm4X+GVmU>)`6YoDo$&X$atvZTnY)B7SAQTA=Kf<M#}
z-kXxygf0BfE?dg@wS-s^=yp|P?C!|pij{OqL}mxcRtV7CKHNy%%vKdbKA0Xqm=?{x
zanc&}8sAksI(i!kA2ELpLm^|6BRC{yva@k9V}^@Zchcho5WF#+YiL(4`a4Z=dXY`!
zz$gv;S!E~-KZrLTfvA*vaAl(_`4G;;H=j0g{Lc)pJG$`dOmGt1{g$UV^MbC&AtINd
z6r^KPicW>n%<2Tps7{1T4GX9S)NL;RHCe%}emguc`Y@kfi92+2yADk#fLEv4PwcDS
z(YlcP={R*UbM+wC`^E1ot={qJDrbP+)d+ULz+(?gae`cnn4)a-aT1bh&A;#P#-~7U
zSCpW3c{WR>LTpxMqE8f@R6|Mw(Xw1R5~0rjg7trwpao<#3T4~%@`9H1f}sN=aFIVu
z8{S3X#O&eJ076UnL?-!3aB{HRbhRG+rkZBsi?uzOWJXnX@@-$mHPz5Ze|jY%eCdDQ
z5K=Wg97egVu~=oL0_cs)(i?ZBa#_YBG<>O}!s7MfeD6oz(36C4Nh&h7wLKS#uWDfj
zb+WnGbSbzw^1;<rQuIrj$Lpq(v-2l8Xgh<C@;HE~x3IS5@?wBhjJ@yhrCaw%#*9Ih
z7(l6_Lsdij=%sMywL(>?rkTDpat;ncrGqA?2Go!u6SB&fAQLML=pS~C->!<<eYoXv
z<!t$`obxLv`v&a={M7I`ojxktrvoU9!rk)HlD}Eya<Xg4XW{mRBETT&s<iIX_#_Mn
zjw7~8>Bww7Bw`r-dk{y~(NCKfB`o8&HiNz})JzoSA4}(}4Z&GaoE#j*X7?I?za8yh
z@%k*(dm|_poel}uEtSfp<aY2A9i^=+vQ+pr!q@g^(NzMj`{YMDmdW`n5!FmfdZrjL
znk2&i^Wd(=%*<AeP8Y7N;c0@vC<7ROk;!tR28*s^41SuNUYLf2&rZ;}NY6>Z7SM2k
z8|@55t`|9fPQ)bVC$5tchtG#PtXXf4VMCbr8Rp&kHDHJ${yxa8IKx=+cm4(Qx}K<n
zCHC4=Q-&)0?wv1ZdDrp}=mHb5UQF+AF%>3Ct(9KPwI9D&0nLw0e@R2fml6RSJ!{{J
z5}AzWyp`Cc;`gE?an}${xbMciMOMW^{}9+2(r|ZS`xfpRJ6fZ{RUE>LF5(EJi%Cyp
zuO?2a7{I=rwVCD=ah^O&=5ur19t%UOtt*q;=b(~_FWu1qh6A07!(b+RPW+P-3XZ}L
zrRQA3=Up8~A>eN+z&|})+y&n89L=?*=F4ztT-;QZGbT7vR#xOQfe0c{?syo)3eQId
zn~aMdhFj}i0$?^yhLv8gkSNCilb*_vr$-~~CqbW31Pl-^`wicuKk@ay{+>+1!i|AS
z!@XvTK@Vi2$Ex8*4OAH;V4zz6K`h`bJ{iI7pkuWPYimX&NnEK`@(jyR6L7Ix?6`dA
zWRx5q*|7!_kD$ReXoEszev+O5hi-OMGoyDT;JqDZ*2xKuPlRv=)4fa`6x(B9@lPHQ
z0|4+Z|2qpnqbNXtjXp5{Vq0db>OcayeXoyauS}=yQHTAX0PqM8_n1DR8WYDYK^GTy
zXsQ`v)>Ih+ka6Vp3b6I$LIT?{goOf44FQJqTOxTaUICI5Q{f;sBM%Vvi~=wc*qQ}V
z7SM$otP)ZfNTdH%9T$ip?)HeXGsEnFu1|@;gU^aNSuJ0NrxR)^3~&SxI=q|!+@=ot
zDCl5-@d|pRL{=C)WMnn?pSyjh3DDg5WnyQ}oKY<<s$D)LJrgD*%W@ss!ayh@=bwNv
z!<KO#Kr#*>*%EH>z-goac0>Rpj2*dx8y=S4$2NfU_K4+16Q@&4A@{GYriFe9vn1Qe
zvGs%*r5HM71YE70UO<3AZcxa@t~V@9>|mg!jm)3`ZhN+(C?AX?fCDX!(8E}SVci^1
z679p0fRQ0T!VA5uj7TZ`P#NKeQjz1U3pv{fkw+vL+>X*qCufWvpSkAmD9m|LXZ%|#
zf?o9|*bhIJS8nbzWpd6By?e!S@t2i)+p?9eAp<aNQYkXWl#!FKL2AMTiu1;>vvDOu
zm*1R5GJu`zz2My=hBAN#Zr`BZLFv#?*T&ePMG__9OkfE{kC}+TfCxBP_I`!{EG2Yz
z3qzoP9HpOOa2ATOEQsyT=g;+W2K4$^e=O?N4N>-H=xQiLqLU>S1a;%?kFYhxOj3yI
zNPm<HUrhi8et%UxI2svY#IUR<rE51P{gXKS{R;2`CN?%U=`C4Qx_tQ1DNnj~@qj|-
zPSn#?5a1U?x%_x!jLbz?@E}qE8^p%+LB^;R%^`wGyoH%F7Xtjflew`2fsO(BfE0c+
zNr?x@8ef6|14be$lEQ#x$gdQ@&O8KGrrzl8?u#xO+8FKRio$+<urXEgLlDwx9agek
zOsX)lha=bX{VfdPWom$4*2WwGN_6dC8Uk`!3b3G^0FD9yA|eK$pkQO>KMnprN`Pn8
z0RJs1*%Gi|LH5DK#N>yL_Kw^ztf5HERRMW>hCowQ1y<(fNFO`~S>x79*8h`dU@0J*
zMrP8_3}9r)2ySMvIkjZl#*HgN|Nf(p5SIpfi{NGga05c-z0oIZC=B)Oxc@0qR)VRz
z2Hc2n<D$b+(KmuC^r+^?0T>Y)l7q1!&L2~J++eDs2@`4sy?SDe=mjQ_4FR{-#f*-6
z@X--cIGcc_iz?R8Xa3-y2LFv9fRqIMm+|4wJ$u3zFIisSe_+~OAD<wI$Qx*?t8%{w
z+_u$6aB^_KgbCBg46a81#2GNqH^(?40=G3BDZ^BLAHn8qf*%J+Oc;W&-idIr4d;Mo
z1h6%wo^S367e{w!X{f{0*c=uXR%9YI(7tsm@+CsV1qEViay+sV!cddIuk0lf<c9Y|
zxQ!`1OhlOO?}o~#0IW82eU<<$?tiF_?A8JV%d5lIu`3qNU9$s!@tpo!Pk>(&q5h-B
z#yZC(OIA;rF+KbHF{5TZPE1UJt+g%Mw`mQ1JsnD+MsVB9INEwVlR3O-*N{nL3lY<2
z5arz|=;|0v1PFjN5x~^IliSk8NNkM6xS^Ogx8Uf)<x3~co4fLizjq{56qV4iLpxYn
zS|d6l8cT=-bp(Dsf$w7`#<-qN{OX<{RQ2hFH6~rT@-1lrNFMe4`RZoyRZ>TYZ*R<)
zw(3*%6L@b5_-`BmeoX}Yd&`zDI<G0-;jv}w$J6J`%KkbgI-L|jgG(X({CqKH%p_!t
zUPZFM?j<B(1SmpmpEQK@ii4|NB)R@zlKx;=7`u?dh><>MGFC3GF8kup_bTjve)ic}
zy*0&~mJb^`{zn%VSEwi{K}%B;o;^G<Jw6KSl0&hYvH@-x7pvrDRlV_{Sj!PWG7yx*
zR`AM+(Mv}k7FPC{F@4pAZ4F0X+qCXGMSvHPfnA!K_G!<ZT`+y%z+qq8+1Nq8Qzw#e
zGq5b8U(#eu9#{ISVP!^uiDL@5eTH0}0%6I;em_{5^dKcMM8A{?D9CLr0uD6~$VmU+
zm#0pd<`)*{O`J6Oc2r~(48>yTiww~}DhlgaH7^IeWJ}ljelaMw_vNyHRUheKshj}<
zwDd@23^8Wp{5u=UnnL)O{l~x4w~7ESBEz0NdlWOXW=~3t9e!J+XFx>gNJOwgWLQ6>
z_nl4Y;~KuMP|_xiDMi23F|aoGk{Cb}4~X={NQ@tj6-#T@mA$0MQhM&IufDRaZ`ihW
z`m`mFdboQ+O<f({?(P^H5rQ=-Vc5XN1yZAV1<*%sD_!*07DG>{hr#KY_sX7v|Hgga
zZ`>RDBSa`F+U7WR)Vw`CJ%T7+D{?8MvwaW5M5bZ%(B-5CWki5VOdh))L(`{0sO11>
zJ6~9uS&<=($NX7k+nbu2UO5{l8;;7$clMb-YxU<T$pg6ZF(X4m^a+o|(Bx#4#`eZ)
zp*?aHOfa;A2D%uVVffH#SiO4dfHxKVx0V31;1m^YYBOtk$>P+cQBNG~UC^OjYiJWV
zfqualKW;Y0j#$a<BRFjEEQs}7psA(-Kc8NhIV1Pv?%lgzxx3kmh)`GeiE>TVwjmi~
z=Uj5McZY_W8muWC4GN1yzNQ7{b`rvta{ZK)vB+MzIqOXZ|E(v06c~0aDcKk~Idkb(
z5fO1P5a~ma)WF8lhWtSy$^U3{>k^8NZB^l5?~JLFm)+b_bLda~9BcCcR?Q)U>C<xR
zqa)eR(HX;3po=Jh0o;{U5FaxHOBYuZl}Uf!?+y5#-dO_3g0gk%UbVcU)tM6}P5w4A
zB8nWoK6JG;AtWcR&{31pJtGWBn}z&UoBRH+J(GWK%XxDOM-LmC^`l33Pjqv3MQC6m
z=FKktm`#Jf>EORJ1bChZ?6>r)YBt8tU%2>KT+E=y9^HK*5U?7A;mBRSY0{tliM5yg
zzuMaE!o0lVq{T~f<5w=-IDOf&O^R;=`0pG6o(G1mx2i1P9=USa`m#X-Ge29rxQOi&
z-}0{pNAh}43pn2v@ZVViyod~6ehK*|H2vk^zwPb+&6n|}yYcq~c;DU=;C*{ffcNcn
s1OEKwpMFE{+doW*fBFr)Z~tujKex=z_g<_$Z2$lO07*qoM6N<$f{yLO)Bpeg

diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala
+++ b/src/Pure/Admin/build_release.scala
@@ -1,929 +1,925 @@
 /*  Title:      Pure/Admin/build_release.scala
     Author:     Makarius
 
 Build full Isabelle distribution from repository.
 */
 
 package isabelle
 
 
 object Build_Release
 {
   /** release info **/
 
   sealed case class Bundle_Info(
     platform: Platform.Family.Value,
     platform_description: String,
     name: String)
   {
     def path: Path = Path.explode(name)
   }
 
   class Release private[Build_Release](
     progress: Progress,
     val date: Date,
     val dist_name: String,
     val dist_dir: Path,
     val dist_version: String,
     val ident: String)
   {
     val isabelle_dir: Path = dist_dir + Path.explode(dist_name)
     val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
     val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
 
     def other_isabelle(dir: Path): Other_Isabelle =
       Other_Isabelle(dir + Path.explode(dist_name),
         isabelle_identifier = dist_name + "-build",
         progress = progress)
 
     def bundle_info(platform: Platform.Family.Value): Bundle_Info =
       platform match {
         case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
         case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
         case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
       }
   }
 
 
 
   /** generated content **/
 
   /* patch release */
 
   private val getsettings_path = Path.explode("lib/scripts/getsettings")
 
   private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r
 
   def patch_release(release: Release, is_official: Boolean)
   {
     val dir = release.isabelle_dir
 
     for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala"))
     {
       File.change(dir + Path.explode(name),
         _.replace("val is_identified = false", "val is_identified = true")
          .replace("val is_official = false", "val is_official = " + is_official))
     }
 
     File.change(dir + getsettings_path,
       _.replace("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
        .replace("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
 
     File.change(dir + Path.explode("lib/html/library_index_header.template"),
       _.replace("{ISABELLE}", release.dist_name))
 
     for {
       name <-
         List(
           "src/Pure/System/distribution.ML",
           "src/Pure/System/distribution.scala",
           "lib/Tools/version") }
     {
       File.change(dir + Path.explode(name), _.replace("repository version", release.dist_version))
     }
 
     File.change(dir + Path.explode("README"),
       _.replace("some repository version of Isabelle", release.dist_version))
   }
 
 
   /* ANNOUNCE */
 
   def make_announce(release: Release)
   {
     File.write(release.isabelle_dir + Path.explode("ANNOUNCE"),
 """
 IMPORTANT NOTE
 ==============
 
 This is a snapshot of Isabelle/""" + release.ident + """ from the repository.
 
 """)
   }
 
 
   /* NEWS */
 
   def make_news(other_isabelle: Other_Isabelle, dist_version: String)
   {
     val target = other_isabelle.isabelle_home + Path.explode("doc")
     val target_fonts = Isabelle_System.make_directory(target + Path.explode("fonts"))
     other_isabelle.copy_fonts(target_fonts)
 
     HTML.write_document(target, "NEWS.html",
       List(HTML.title("NEWS (" + dist_version + ")")),
       List(
         HTML.chapter("NEWS"),
         HTML.source(
           Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS"))))))
   }
 
 
   /* bundled components */
 
   class Bundled(platform: Option[Platform.Family.Value] = None)
   {
     def detect(s: String): Boolean =
       s.startsWith("#bundled") && !s.startsWith("#bundled ")
 
     def apply(name: String): String =
       "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name
 
     private val Pattern1 = ("""^#bundled:(.*)$""").r
     private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
 
     def unapply(s: String): Option[String] =
       s match {
         case Pattern1(name) => Some(name)
         case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name)
         case _ => None
       }
   }
 
   def record_bundled_components(dir: Path)
   {
     val catalogs =
       List("main", "bundled").map((_, new Bundled())) :::
       default_platform_families.flatMap(platform =>
         List(platform.toString, "bundled-" + platform.toString).
           map((_, new Bundled(platform = Some(platform)))))
 
     File.append(Components.components(dir),
       terminate_lines("#bundled components" ::
         (for {
           (catalog, bundled) <- catalogs.iterator
           path = Components.admin(dir) + Path.basic(catalog)
           if path.is_file
           line <- split_lines(File.read(path))
           if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
         } yield bundled(line)).toList))
   }
 
   def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) =
   {
     val Bundled = new Bundled(platform = Some(platform))
     val components =
       for {
         Bundled(name) <- Components.read_components(dir)
         if !name.startsWith("jedit_build")
       } yield name
     val jdk_component =
       components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
     (components, jdk_component)
   }
 
   def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String])
   {
     def contrib_name(name: String): String =
       Components.contrib(name = name).implode
 
     val Bundled = new Bundled(platform = Some(platform))
     Components.write_components(dir,
       Components.read_components(dir).flatMap(line =>
         line match {
           case Bundled(name) =>
             if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
             else None
           case _ => if (Bundled.detect(line)) None else Some(line)
         }) ::: more_names.map(contrib_name))
   }
 
   def make_contrib(dir: Path)
   {
     Isabelle_System.make_directory(Components.contrib(dir))
     File.write(Components.contrib(dir, "README"),
 """This directory contains add-on components that contribute to the main
 Isabelle distribution.  Separate licensing conditions apply, see each
 directory individually.
 """)
   }
 
 
 
   /** build release **/
 
   private def execute(dir: Path, script: String): Unit =
     Isabelle_System.bash(script, cwd = dir.file).check
 
   private def execute_tar(dir: Path, args: String): Unit =
     Isabelle_System.gnutar(args, dir = dir).check
 
 
   /* build heaps on remote server */
 
   private def remote_build_heaps(
     options: Options,
     platform: Platform.Family.Value,
     build_sessions: List[String],
     local_dir: Path)
   {
     val server_option = "build_host_" + platform.toString
     options.string(server_option) match {
       case SSH.Target(user, host) =>
         using(SSH.open_session(options, host = host, user = user))(ssh =>
         {
           Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar =>
           {
             execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
             ssh.with_tmp_dir(remote_dir =>
             {
               val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
               ssh.write_file(remote_tmp_tar, local_tmp_tar)
               val remote_commands =
                 List(
                   "cd " + File.bash_path(remote_dir),
                   "tar -xf tmp.tar",
                   "./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
                   "tar -cf tmp.tar heaps")
               ssh.execute(remote_commands.mkString(" && ")).check
               ssh.read_file(remote_tmp_tar, local_tmp_tar)
             })
             execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
           })
         })
       case s => error("Bad " + server_option + ": " + quote(s))
     }
   }
 
 
   /* Isabelle application */
 
   def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n")
   {
     val title = "# Java runtime options"
     File.write(path, (title :: options).map(_ + line_ending).mkString)
   }
 
   def make_isabelle_app(
     path: Path,
     isabelle_home_prefix: String,
     jdk_component: String,
     classpath: List[Path])
   {
     val script = """#!/usr/bin/env bash
 #
 # Author: Makarius
 #
 # Main Isabelle application script.
 
 # minimal Isabelle environment
 
 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/""" + isabelle_home_prefix + """"; pwd)"
 source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
 
 #paranoia settings -- avoid intrusion of alien options
 unset "_JAVA_OPTIONS"
 unset "JAVA_TOOL_OPTIONS"
 
 #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc.
 unset XMODIFIERS
 
 COMPONENT="$ISABELLE_HOME/contrib/""" + jdk_component + """"
 source "$COMPONENT/etc/settings"
 
 
 # main
 
 declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options"))
 
 exec "$ISABELLE_JDK_HOME/bin/java" \
   "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
   -classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \
   "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
   isabelle.Main "$@"
 """
     File.write(path, script)
     File.set_executable(path, true)
   }
 
 
   def make_isabelle_plist(path: Path, isabelle_name: String)
   {
     File.write(path, """<?xml version="1.0" ?>
 <!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
 <plist version="1.0">
 <dict>
 <key>CFBundleDevelopmentRegion</key>
 <string>English</string>
-<key>CFBundleIconFile</key>
-<string>isabelle.icns</string>
 <key>CFBundleIdentifier</key>
 <string>de.tum.in.isabelle.""" + isabelle_name + """</string>
 <key>CFBundleDisplayName</key>
 <string>""" + isabelle_name + """</string>
 <key>CFBundleInfoDictionaryVersion</key>
 <string>6.0</string>
 <key>CFBundleName</key>
 <string>""" + isabelle_name + """</string>
 <key>CFBundlePackageType</key>
 <string>APPL</string>
 <key>CFBundleShortVersionString</key>
 <string>1.0</string>
 <key>CFBundleSignature</key>
 <string>????</string>
 <key>CFBundleVersion</key>
 <string>1</string>
 <key>NSHumanReadableCopyright</key>
 <string></string>
 <key>LSMinimumSystemVersion</key>
 <string>10.7</string>
 <key>LSApplicationCategoryType</key>
 <string>public.app-category.developer-tools</string>
 <key>NSHighResolutionCapable</key>
 <string>true</string>
 <key>NSSupportsAutomaticGraphicsSwitching</key>
 <string>true</string>
 <key>CFBundleDocumentTypes</key>
 <array>
 <dict>
 <key>CFBundleTypeExtensions</key>
 <array>
 <string>thy</string>
 </array>
-<key>CFBundleTypeIconFile</key>
-<string>theory.icns</string>
 <key>CFBundleTypeName</key>
 <string>Isabelle theory file</string>
 <key>CFBundleTypeRole</key>
 <string>Editor</string>
 <key>LSTypeIsPackage</key>
 <false/>
 </dict>
 </array>
 </dict>
 </plist>
 """)
   }
 
 
   /* main */
 
   private val default_platform_families: List[Platform.Family.Value] =
     List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
 
   def build_release(base_dir: Path,
     options: Options,
     components_base: Path = Components.default_components_base,
     progress: Progress = new Progress,
     rev: String = "",
     afp_rev: String = "",
     official_release: Boolean = false,
     proper_release_name: Option[String] = None,
     platform_families: List[Platform.Family.Value] = default_platform_families,
     more_components: List[Path] = Nil,
     website: Option[Path] = None,
     build_sessions: List[String] = Nil,
     build_library: Boolean = false,
     parallel_jobs: Int = 1): Release =
   {
     val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME"))
 
     val release =
     {
       val date = Date.now()
       val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date))
       val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute
 
       val version = proper_string(rev) orElse proper_release_name getOrElse "tip"
       val ident =
         try { hg.id(version) }
         catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
 
       val dist_version =
         proper_release_name match {
           case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date)
           case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
         }
 
       new Release(progress, date, dist_name, dist_dir, dist_version, ident)
     }
 
 
     /* make distribution */
 
     if (release.isabelle_archive.is_file) {
       progress.echo_warning("Release archive already exists: " + release.isabelle_archive)
 
       val archive_ident =
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
           {
             val getsettings = Path.explode(release.dist_name) + getsettings_path
             execute_tar(tmp_dir, "-xzf " +
               File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
             split_lines(File.read(tmp_dir + getsettings))
               .collectFirst({ case ISABELLE_ID(ident) => ident })
               .getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive))
           })
 
       if (release.ident != archive_ident) {
         error("Mismatch of release identification " + release.ident +
           " vs. archive " + archive_ident)
       }
     }
     else {
       progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...")
 
       Isabelle_System.make_directory(release.dist_dir)
 
       if (release.isabelle_dir.is_dir)
         error("Directory " + release.isabelle_dir + " already exists")
 
 
       progress.echo_warning("Retrieving Mercurial repository version " + release.ident)
 
       hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files")
 
       for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
         (release.isabelle_dir + Path.explode(name)).file.delete
       }
 
 
       progress.echo_warning("Preparing distribution " + quote(release.dist_name))
 
       patch_release(release, proper_release_name.isDefined && official_release)
 
       if (proper_release_name.isEmpty) make_announce(release)
 
       make_contrib(release.isabelle_dir)
 
       execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
 
       record_bundled_components(release.isabelle_dir)
 
 
       /* build tools and documentation */
 
       val other_isabelle = release.other_isabelle(release.dist_dir)
 
       other_isabelle.init_settings(
         other_isabelle.init_components(components_base = components_base, catalogs = List("main")))
       other_isabelle.resolve_components(echo = true)
 
       try {
         val export_classpath =
           "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
         other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
         other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
       }
       catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
 
       try {
         other_isabelle.bash(
           "./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
       }
       catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
 
       make_news(other_isabelle, release.dist_version)
 
       for (name <- List("Admin", "browser_info", "heaps")) {
         Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
       }
 
       other_isabelle.cleanup()
 
 
       progress.echo_warning("Creating distribution archive " + release.isabelle_archive)
 
       def execute_dist_name(script: String): Unit =
         Isabelle_System.bash(script, cwd = release.dist_dir.file,
           env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check
 
       execute_dist_name("""
 set -e
 
 chmod -R a+r "$DIST_NAME"
 chmod -R u+w "$DIST_NAME"
 chmod -R g=o "$DIST_NAME"
 find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
 """)
 
       execute_tar(release.dist_dir, "-czf " +
         File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
 
       execute_dist_name("""
 set -e
 
 mv "$DIST_NAME" "${DIST_NAME}-old"
 mkdir "$DIST_NAME"
 
 mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \
   "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME"
 mkdir "$DIST_NAME/doc"
 mv "${DIST_NAME}-old/doc/"*.pdf \
   "${DIST_NAME}-old/doc/"*.html \
   "${DIST_NAME}-old/doc/"*.css \
   "${DIST_NAME}-old/doc/fonts" \
   "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
 
 rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
 
 rm -rf "${DIST_NAME}-old"
 """)
     }
 
 
     /* make application bundles */
 
     val bundle_infos = platform_families.map(release.bundle_info)
 
     for (bundle_info <- bundle_infos) {
       val isabelle_name = release.dist_name
       val platform = bundle_info.platform
 
       progress.echo("\nApplication bundle for " + platform)
 
       Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
       {
         // release archive
 
         execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
         val other_isabelle = release.other_isabelle(tmp_dir)
         val isabelle_target = other_isabelle.isabelle_home
 
 
         // bundled components
 
         progress.echo("Bundled components:")
 
         val contrib_dir = Components.contrib(isabelle_target)
 
         val (bundled_components, jdk_component) =
           get_bundled_components(isabelle_target, platform)
 
         Components.resolve(components_base, bundled_components,
           target_dir = Some(contrib_dir),
           copy_dir = Some(release.dist_dir + Path.explode("contrib")),
           progress = progress)
 
         val more_components_names =
           more_components.map(Components.unpack(contrib_dir, _, progress = progress))
 
         Components.purge(contrib_dir, platform)
 
         activate_components(isabelle_target, platform, more_components_names)
 
 
         // Java parameters
 
         val java_options: List[String] =
           (for {
             variable <-
               List(
                 "ISABELLE_JAVA_SYSTEM_OPTIONS",
                 "JEDIT_JAVA_SYSTEM_OPTIONS",
                 "JEDIT_JAVA_OPTIONS")
             opt <- Word.explode(other_isabelle.getenv(variable))
           }
           yield {
             val s = "-Dapple.awt.application.name="
             if (opt.startsWith(s)) s + isabelle_name else opt
           }) ::: List("-Disabelle.jedit_server=" + isabelle_name)
 
         val classpath: List[Path] =
         {
           val base = isabelle_target.absolute
           Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
           {
             val abs_path = path.absolute
             File.relative_path(base, abs_path) match {
               case Some(rel_path) => rel_path
               case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
             }
           }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
         }
 
         val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
         val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
 
 
         // build heaps
 
         if (build_sessions.nonEmpty) {
           progress.echo("Building heaps ...")
           remote_build_heaps(options, platform, build_sessions, isabelle_target)
         }
 
 
         // application bundling
 
         platform match {
           case Platform.Family.linux =>
             File.change(isabelle_target + jedit_options,
               _.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24"))
 
             File.change(isabelle_target + jedit_props,
               _.replaceAll("console.fontsize=.*", "console.fontsize=18")
                .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18")
                .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18")
                .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18")
                .replaceAll("view.fontsize=.*", "view.fontsize=24")
                .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16"))
 
             make_isabelle_options(
               isabelle_target + Path.explode("Isabelle.options"), java_options)
 
             make_isabelle_app(
               isabelle_target + Path.explode("lib/scripts/Isabelle_app"),
               "../..", jdk_component, classpath)
 
             val linux_app = isabelle_target + Path.explode("contrib/linux_app")
             File.move(linux_app + Path.explode("Isabelle"),
               isabelle_target + Path.explode(isabelle_name))
             Isabelle_System.rm_tree(linux_app)
 
             val archive_name = isabelle_name + "_linux.tar.gz"
             progress.echo("Packaging " + archive_name + " ...")
             execute_tar(tmp_dir,
               "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
               Bash.string(isabelle_name))
 
 
           case Platform.Family.macos =>
             File.change(isabelle_target + jedit_props,
               _.replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
                .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
                .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
 
 
             // MacOS application bundle
 
             File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
 
             val isabelle_app = Path.explode(isabelle_name + ".app")
             val app_dir = tmp_dir + isabelle_app
             File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir)
 
             val app_contents = app_dir + Path.explode("Contents")
             val app_resources = app_contents + Path.explode("Resources")
             File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
 
             val isabelle_home = Path.explode("Contents/Resources/" + isabelle_name)
             val isabelle_options = Path.explode("Isabelle.options")
 
             File.link(
               isabelle_home, app_dir + Path.explode("Isabelle"), force = true)
             File.link(
               isabelle_home + isabelle_options, app_dir + isabelle_options, force = true)
 
             make_isabelle_app(
               app_dir + Path.explode(isabelle_name),
               isabelle_home.implode, jdk_component, classpath)
 
             make_isabelle_options(
               app_dir + isabelle_options,
               java_options ::: List("-Disabelle.app=true"))
 
             make_isabelle_plist(app_contents + Path.explode("Info.plist"), isabelle_name)
 
 
             // application archive
 
             val archive_name = isabelle_name + "_macos.tar.gz"
             progress.echo("Packaging " + archive_name + " ...")
             execute_tar(tmp_dir,
               "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
               File.bash_path(isabelle_app))
 
 
           case Platform.Family.windows =>
             File.change(isabelle_target + jedit_props,
               _.replaceAll("lookAndFeel=.*",
                   "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
                .replaceAll("foldPainter=.*", "foldPainter=Square"))
 
 
             // application launcher
 
             File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
 
             val app_template = Path.explode("~~/Admin/Windows/launch4j")
 
             make_isabelle_options(
               isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
               java_options, line_ending = "\r\n")
 
             val isabelle_xml = Path.explode("isabelle.xml")
             val isabelle_exe = Path.explode(isabelle_name + ".exe")
 
             File.write(tmp_dir + isabelle_xml,
               File.read(app_template + isabelle_xml)
                 .replace("{ISABELLE_NAME}", isabelle_name)
                 .replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe))
                 .replace("{ICON}",
                   File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
                 .replace("{SPLASH}",
                   File.platform_path(app_template + Path.explode("isabelle.bmp")))
                 .replace("{CLASSPATH}",
                   cat_lines(classpath.map(cp =>
                     "    <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>")))
                 .replace("\\jdk\\", "\\" + jdk_component + "\\"))
 
             execute(tmp_dir,
               "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
 
             File.copy(app_template + Path.explode("manifest.xml"),
               isabelle_target + isabelle_exe.ext("manifest"))
 
 
             // Cygwin setup
 
             val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
 
             File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
 
             val cygwin_mirror =
               File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
 
             val cygwin_bat = Path.explode("Cygwin-Setup.bat")
             File.write(isabelle_target + cygwin_bat,
               File.read(cygwin_template + cygwin_bat).replace("{MIRROR}", cygwin_mirror))
             File.set_executable(isabelle_target + cygwin_bat, true)
 
             for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
               val path = Path.explode(name)
               File.copy(cygwin_template + path,
                 isabelle_target + Path.explode("contrib/cygwin") + path)
             }
 
             execute(isabelle_target,
               """find . -type f -not -name "*.exe" -not -name "*.dll" """ +
               (if (Platform.is_macos) "-perm +100" else "-executable") +
               " -print0 > contrib/cygwin/isabelle/executables")
 
             execute(isabelle_target,
               """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
               """> contrib/cygwin/isabelle/symlinks""")
 
             execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
 
             File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
 
 
             // executable archive (self-extracting 7z)
 
             val archive_name = isabelle_name + ".7z"
             val exe_archive = tmp_dir + Path.explode(archive_name)
             exe_archive.file.delete
 
             progress.echo("Packaging " + archive_name + " ...")
             execute(tmp_dir,
               "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
             if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
 
             val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
             val sfx_txt =
               File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt"))
                 .replace("{ISABELLE_NAME}", isabelle_name)
 
             Bytes.write(release.dist_dir + isabelle_exe,
               Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
             File.set_executable(release.dist_dir + isabelle_exe, true)
         }
       })
       progress.echo("DONE")
     }
 
 
     /* minimal website */
 
     for (dir <- website) {
       val website_platform_bundles =
         for {
           bundle_info <- bundle_infos
           if (release.dist_dir + bundle_info.path).is_file
         } yield (bundle_info.name, bundle_info)
 
       val isabelle_link =
         HTML.link(Isabelle_Cronjob.isabelle_repos_source + "/rev/" + release.ident,
           HTML.text("Isabelle/" + release.ident))
       val afp_link =
         HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev))
 
       HTML.write_document(dir, "index.html",
         List(HTML.title(release.dist_name)),
         List(
           HTML.section(release.dist_name),
           HTML.subsection("Platforms"),
           HTML.itemize(
             website_platform_bundles.map({ case (bundle, bundle_info) =>
               List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) })),
           HTML.subsection("Repositories"),
           HTML.itemize(
             List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
 
       for ((bundle, _) <- website_platform_bundles)
         File.copy(release.dist_dir + Path.explode(bundle), dir)
     }
 
 
     /* HTML library */
 
     if (build_library) {
       if (release.isabelle_library_archive.is_file) {
         progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive)
       }
       else {
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
           {
             val bundle =
               release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz")
             execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
 
             val other_isabelle = release.other_isabelle(tmp_dir)
 
             Isabelle_System.make_directory(other_isabelle.etc)
             File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
 
             other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
               " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
               " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
             other_isabelle.isabelle_home_user.file.delete
 
             execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
             execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
             execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) +
               " " + Bash.string(release.dist_name + "/browser_info"))
           })
       }
     }
 
     release
   }
 
 
 
   /** command line entry point **/
 
   def main(args: Array[String])
   {
     Command_Line.tool {
       var afp_rev = ""
       var components_base: Path = Components.default_components_base
       var official_release = false
       var proper_release_name: Option[String] = None
       var website: Option[Path] = None
       var build_sessions: List[String] = Nil
       var more_components: List[Path] = Nil
       var parallel_jobs = 1
       var build_library = false
       var options = Options.init()
       var platform_families = default_platform_families
       var rev = ""
 
       val getopts = Getopts("""
 Usage: Admin/build_release [OPTIONS] BASE_DIR
 
   Options are:
     -A REV       corresponding AFP changeset id
     -C DIR       base directory for Isabelle components (default: """ +
         Components.default_components_base + """)
     -O           official release (not release-candidate)
     -R RELEASE   proper release with name
     -W WEBSITE   produce minimal website in given directory
     -b SESSIONS  build platform-specific session images (separated by commas)
     -c ARCHIVE   clean bundling with additional component .tar.gz archive
     -j INT       maximum number of parallel jobs (default 1)
     -l           build library
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p NAMES     platform families (default: """ + default_platform_families.mkString(",") + """)
     -r REV       Mercurial changeset id (default: RELEASE or tip)
 
   Build Isabelle release in base directory, using the local repository clone.
 """,
         "A:" -> (arg => afp_rev = arg),
         "C:" -> (arg => components_base = Path.explode(arg)),
         "O" -> (_ => official_release = true),
         "R:" -> (arg => proper_release_name = Some(arg)),
         "W:" -> (arg => website = Some(Path.explode(arg))),
         "b:" -> (arg => build_sessions = space_explode(',', arg)),
         "c:" -> (arg =>
           {
             val path = Path.explode(arg)
             Components.Archive.get_name(path.file_name)
             more_components = more_components ::: List(path)
           }),
         "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
         "l" -> (_ => build_library = true),
         "o:" -> (arg => options = options + arg),
         "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)),
         "r:" -> (arg => rev = arg))
 
       val more_args = getopts(args)
       val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() }
 
       val progress = new Console_Progress()
 
       if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
         error("Building for windows requires 7z")
 
       build_release(Path.explode(base_dir), options, components_base = components_base,
         progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release,
         proper_release_name = proper_release_name, website = website,
         platform_families =
           if (platform_families.isEmpty) default_platform_families
           else platform_families,
         more_components = more_components, build_sessions = build_sessions,
         build_library = build_library, parallel_jobs = parallel_jobs)
     }
   }
 }
diff --git a/src/Pure/GUI/gui.scala b/src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala
+++ b/src/Pure/GUI/gui.scala
@@ -1,344 +1,359 @@
 /*  Title:      Pure/GUI/gui.scala
     Author:     Makarius
 
 Basic GUI tools (for AWT/Swing).
 */
 
 package isabelle
 
 import java.awt.{Component, Container, Font, Image, Insets, KeyboardFocusManager, Window, Point,
   Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit}
 import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
 import java.awt.geom.AffineTransform
 import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
   JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities}
 import scala.swing.{ComboBox, ScrollPane, TextArea}
 import scala.swing.event.SelectionChanged
 
 
 object GUI
 {
   /* Swing look-and-feel */
 
   def find_laf(name: String): Option[String] =
     UIManager.getInstalledLookAndFeels().
       find(c => c.getName == name || c.getClassName == name).
       map(_.getClassName)
 
   def get_laf(): String =
     find_laf(System.getProperty("isabelle.laf")) getOrElse {
       if (Platform.is_windows || Platform.is_macos)
         UIManager.getSystemLookAndFeelClassName()
       else
         UIManager.getCrossPlatformLookAndFeelClassName()
     }
 
   def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
 
   def current_laf(): String = UIManager.getLookAndFeel.getClass.getName()
 
   def is_macos_laf(): Boolean =
     Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf()
 
   def is_windows_laf(): Boolean =
     Platform.is_windows && UIManager.getSystemLookAndFeelClassName() == current_laf()
 
 
   /* plain focus traversal, notably for text fields */
 
   def plain_focus_traversal(component: Component)
   {
     val dummy_button = new JButton
     def apply(id: Int): Unit =
       component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id))
     apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS)
     apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS)
   }
 
 
   /* simple dialogs */
 
   def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
     : ScrollPane =
   {
     val txt = Output.clean_yxml(raw_txt)
     val text = new TextArea(txt)
     if (width > 0) text.columns = width
     if (height > 0 && split_lines(txt).length > height) text.rows = height
     text.editable = editable
     new ScrollPane(text)
   }
 
   private def simple_dialog(kind: Int, default_title: String,
     parent: Component, title: String, message: Iterable[Any])
   {
     GUI_Thread.now {
       val java_message =
         message.iterator.map({ case x: scala.swing.Component => x.peer case x => x }).
           toArray.asInstanceOf[Array[AnyRef]]
       JOptionPane.showMessageDialog(parent, java_message,
         if (title == null) default_title else title, kind)
     }
   }
 
   def dialog(parent: Component, title: String, message: Any*): Unit =
     simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
 
   def warning_dialog(parent: Component, title: String, message: Any*): Unit =
     simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
 
   def error_dialog(parent: Component, title: String, message: Any*): Unit =
     simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
 
   def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
     GUI_Thread.now {
       val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
       JOptionPane.showConfirmDialog(parent,
         java_message.toArray.asInstanceOf[Array[AnyRef]], title,
           option_type, JOptionPane.QUESTION_MESSAGE)
     }
 
 
   /* zoom box */
 
   private val Zoom_Factor = "([0-9]+)%?".r
 
   abstract class Zoom_Box extends ComboBox[String](
     List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
   {
     def changed: Unit
     def factor: Int = parse(selection.item)
 
     private def parse(text: String): Int =
       text match {
         case Zoom_Factor(s) =>
           val i = Integer.parseInt(s)
           if (10 <= i && i < 1000) i else 100
         case _ => 100
       }
 
     private def print(i: Int): String = i.toString + "%"
 
     def set_item(i: Int) {
       peer.getEditor match {
         case null =>
         case editor => editor.setItem(print(i))
       }
     }
 
     makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
     peer.getEditor.getEditorComponent match {
       case text: JTextField => text.setColumns(4)
       case _ =>
     }
 
     selection.index = 3
 
     listenTo(selection)
     reactions += { case SelectionChanged(_) => changed }
   }
 
 
   /* tooltip with multi-line support */
 
   def tooltip_lines(text: String): String =
     if (text == null || text == "") null
     else "<html>" + HTML.output(text) + "</html>"
 
 
   /* icon */
 
   def isabelle_icon(): ImageIcon =
     new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle_transparent-32.gif"))
 
   def isabelle_icons(): List[ImageIcon] =
     for (icon <- List("isabelle/isabelle_transparent-32.gif", "isabelle/isabelle_transparent.gif"))
       yield new ImageIcon(getClass.getClassLoader.getResource(icon))
 
   def isabelle_image(): Image = isabelle_icon().getImage
 
+  def isabelle_image_large(): Image =
+    Toolkit.getDefaultToolkit.getImage(
+      File.platform_path(Path.explode("~~/lib/logo/isabelle_transparent-128.png")))
+
+  def set_application_icon()
+  {
+    if (Platform.is_macos) {
+      val image = isabelle_image_large()
+      val app =
+        Class.forName("com.apple.eawt.Application")
+          .getDeclaredMethod("getApplication").invoke(null)
+      app.getClass.getDeclaredMethod("setDockIconImage", classOf[Image]).invoke(app, image)
+    }
+  }
+
 
   /* location within multi-screen environment */
 
   final case class Screen_Location(point: Point, bounds: Rectangle)
   {
     def relative(parent: Component, size: Dimension): Point =
     {
       val w = size.width
       val h = size.height
 
       val x0 = parent.getLocationOnScreen.x
       val y0 = parent.getLocationOnScreen.y
       val x1 = x0 + parent.getWidth - w
       val y1 = y0 + parent.getHeight - h
       val x2 = point.x min (bounds.x + bounds.width - w)
       val y2 = point.y min (bounds.y + bounds.height - h)
 
       val location = new Point((x2 min x1) max x0, (y2 min y1) max y0)
       SwingUtilities.convertPointFromScreen(location, parent)
       location
     }
   }
 
   def screen_location(component: Component, point: Point): Screen_Location =
   {
     val screen_point = new Point(point.x, point.y)
     if (component != null) SwingUtilities.convertPointToScreen(screen_point, component)
 
     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
     val screen_bounds =
       (for {
         device <- ge.getScreenDevices.iterator
         config <- device.getConfigurations.iterator
         bounds = config.getBounds
       } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
 
     Screen_Location(screen_point, screen_bounds)
   }
 
   def mouse_location(): Screen_Location =
     screen_location(null, MouseInfo.getPointerInfo.getLocation)
 
 
   /* screen size */
 
   sealed case class Screen_Size(bounds: Rectangle, insets: Insets)
   {
     def full_screen_bounds: Rectangle =
       if (Platform.is_linux) {
         // avoid menu bar and docking areas
         new Rectangle(
           bounds.x + insets.left,
           bounds.y + insets.top,
           bounds.width - insets.left - insets.right,
           bounds.height - insets.top - insets.bottom)
       }
       else if (Platform.is_macos) {
         // avoid menu bar, but ignore docking areas
         new Rectangle(
           bounds.x,
           bounds.y + insets.top,
           bounds.width,
           bounds.height - insets.top)
       }
       else bounds
   }
 
   def screen_size(component: Component): Screen_Size =
   {
     val config = component.getGraphicsConfiguration
     val bounds = config.getBounds
     val insets = Toolkit.getDefaultToolkit.getScreenInsets(config)
     Screen_Size(bounds, insets)
   }
 
 
   /* component hierachy */
 
   def get_parent(component: Component): Option[Container] =
     component.getParent match {
       case null => None
       case parent => Some(parent)
     }
 
   def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
     private var next_elem = get_parent(component)
     def hasNext(): Boolean = next_elem.isDefined
     def next(): Container =
       next_elem match {
         case Some(parent) =>
           next_elem = get_parent(parent)
           parent
         case None => Iterator.empty.next()
       }
   }
 
   def parent_window(component: Component): Option[Window] =
     ancestors(component).collectFirst({ case x: Window => x })
 
   def layered_pane(component: Component): Option[JLayeredPane] =
     parent_window(component) match {
       case Some(w: JWindow) => Some(w.getLayeredPane)
       case Some(w: JFrame) => Some(w.getLayeredPane)
       case Some(w: JDialog) => Some(w.getLayeredPane)
       case _ => None
     }
 
   def traverse_components(component: Component, apply: Component => Unit)
   {
     def traverse(comp: Component)
     {
       apply(comp)
       comp match {
         case cont: Container =>
           for (i <- 0 until cont.getComponentCount)
             traverse(cont.getComponent(i))
         case _ =>
       }
     }
     traverse(component)
   }
 
 
   /* font operations */
 
   def copy_font(font: Font): Font =
     if (font == null) null
     else new Font(font.getFamily, font.getStyle, font.getSize)
 
   def line_metrics(font: Font): LineMetrics =
     font.getLineMetrics("", new FontRenderContext(null, false, false))
 
   def transform_font(font: Font, transform: AffineTransform): Font =
     font.deriveFont(java.util.Map.of(TextAttribute.TRANSFORM, new TransformAttribute(transform)))
 
   def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
     new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
 
   def label_font(): Font = (new JLabel).getFont
 
 
   /* Isabelle fonts */
 
   def imitate_font(font: Font,
     family: String = Isabelle_Fonts.sans,
     scale: Double = 1.0): Font =
   {
     val font1 = new Font(family, font.getStyle, font.getSize)
     val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
     new Font(family, font.getStyle, (scale * rel_size * font.getSize).toInt)
   }
 
   def imitate_font_css(font: Font,
     family: String = Isabelle_Fonts.sans,
     scale: Double = 1.0): String =
   {
     val font1 = new Font(family, font.getStyle, font.getSize)
     val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
     "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;"
   }
 
   def use_isabelle_fonts()
   {
     val default_font = label_font()
     val ui = UIManager.getDefaults
     for (prop <- List(
       "ToggleButton.font",
       "CheckBoxMenuItem.font",
       "Label.font",
       "Menu.font",
       "MenuItem.font",
       "PopupMenu.font",
       "Table.font",
       "TableHeader.font",
       "TextArea.font",
       "TextField.font",
       "TextPane.font",
       "ToolTip.font",
       "Tree.font"))
     {
       val font = ui.get(prop) match { case font: Font => font case _ => default_font }
       ui.put(prop, GUI.imitate_font(font))
     }
   }
 }
diff --git a/src/Tools/jEdit/src-base/plugin.scala b/src/Tools/jEdit/src-base/plugin.scala
--- a/src/Tools/jEdit/src-base/plugin.scala
+++ b/src/Tools/jEdit/src-base/plugin.scala
@@ -1,33 +1,35 @@
 /*  Title:      Tools/jEdit/src-base/plugin.scala
     Author:     Makarius
 
 Isabelle base environment for jEdit.
 */
 
 package isabelle.jedit_base
 
 
 import isabelle._
 
 import org.gjt.sp.jedit.{EBMessage, Debug, EBPlugin}
 import org.gjt.sp.util.SyntaxUtilities
 
 
 class Plugin extends EBPlugin
 {
   override def start()
   {
     Isabelle_System.init()
 
+    GUI.set_application_icon()
+
     Debug.DISABLE_SEARCH_DIALOG_POOL = true
 
     Syntax_Style.dummy_style_extender()
   }
 
   override def stop()
   {
     Syntax_Style.set_style_extender(new SyntaxUtilities.StyleExtender)
   }
 
   override def handleMessage(message: EBMessage) { }
 }