diff --git a/lib/logo/theory.icns b/lib/logo/theory.icns
new file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..077996b1e4a193478bef9abd77818fe0fd1b2964
GIT binary patch
literal 41095
zc%1Eg3tUs#x$h1ELLT_QCk-P#b$SKOX|X+_ZSEYZr{lr&Tpg(N^wKhSS_1<V3Nq7~
z!3@gI3lRhZf`H%v8WnsXAZUCbsDMGiL_y>cAv{7h1aS)}8+q)z_70DLFf)#}J?CEb
z{Ibbj-}n8$Z>{yMZ?F7k%>)WUK82vHeSv~c*Fq4q6@q?Q_DkI_(O+V7{R1?<K_2+&
zPk#bI77rOXRM%WvTU~wOG$g?pP;;yHQJwnM*{>im&V-tf_V$*>y33VKkO*f%TBN<L
zQ`dY&bLSic<B?F;Q>6PwiS}M<%F)vhjze8&cgt5-nr_|ER2C7>y;%FP;s=A3jSrfu
ziRXUf#VZBH5A*JnbTkpq&kYqN(jxqf;-<cpl;bU_U*+Gsbo5SN2l4zAM^8%q#22dv
z26|1;FGpK%bk#rW?<bz^K*R9x==jL!@Qc9-1<5#!)1DCDhm1ODn?>&ch@A5AddYi~
z^}mJj+1+jVcHKQb)!ou-T6N0dsqQ{bFSvWzth<?o#U<(2)LK(_dy15KSr`8B*RLkK
zd+W;Hqk6Ax{EiM&ceM#evg9A}_di2S(LX)5_fNm&DPB%@x8-{04Rl6#@lky4?zT#G
zZ=<_c@0-u=jn3LMv)Mfs<d$*k!Sw82eQ$-Gllt-G>|U<&p>A|I)Hyl3l_!2<zszl_
zyR8>4MJ)OyKem6OyJ&Gn%x`~|Gu_>nZB_akGiP_~HM;xh&;JqxK@=Mb#CmrvxPHij
zDC7lwFg66Pmo@L08lWAx>8f)e8=&9dGa9C!@%whrjAxuT>-pz@k7uvx=U))d|JIHe
zOjq+i69HQ=?3R+39o>RL;s0v;T4EfCGC;$1;Ddq>20o+UGY&pD@qxjo419EN`$GlT
z(8TqR^dA^Z6givoB0LT{fLlRzkDD7C;d+|~YIXIEqVwmVSlk+_Z|Uvn?t<HFS{oZ{
zRaZ`5gko?iRM*l0x3OBA8yX)y(A>Rp>S8Ih-_$H>W9hVwjSaP$^33a+<50AzS<=ST
zH8nKW-91@6boU&z&(tbwV`v*1)#ona!}m*}D56oPhdY+Ex3zb4wzo9Z6@PWUpybj;
zNJfYZMsfFI?Y#?+^evCdQo_T&h|f3&Nhc*sPQ}Dl-|c9<r#zjTd*bYA2rOw*1b5r@
z^knTjRZw0~)AaDZx~B4GAtAIUgx%fx?wc7!=bz!j*~czcKW?b6yJZr#_x2fkHED1`
zT@k1$7kZvwzSP$ESUn-^8+g`#J5hN*_3YywJWn~?f2ymct$s>4fP8hd?o@Tj#mm>S
zFJBr=*0vj(CxlPC&!?n!mM2u^WZ+%rk6nA5az@wPHfcGOu0S+#lBhi>j<?5U<=wfi
zdpaq6hUr@F7hH|pzo&T+@Az}v<y)6qpLI<LpO22<Ie8lSv4W;i{7!0Ic1fPWOgN0^
z#UJ?co<@AWCP$r_ocnm-g<(QCI66FjDPsSg{f9Ph%~O|W*BJ(%Vd%sN4U7&C4^<ur
z-Mw$C;KaErr+NpTO$e!k5FTcZzj$<bcX(S#=9!KG_!-qqC>mzG9DDib$@ut_z8C0B
znRIy3*vRnk%a_AL11M@Hh#R&VdOkY+d~leGKQldnZp?TZJNR<?>BY!FY~slhRKQE2
zal5FWHKHJ?4uNVuo#IXZpcF4QPjOMl;;9Tjns@%%j0|tCF03aq{O}jMK98G`;fkoJ
z>Z<uN{HXNAvHTO&&GoNjcxU&GBNvXfkG1bf%(*i=!|xrAIA3?T(|F^P$6d$Ix6jP*
z%D7_9p?&8s=ZB>~&O6jSGsDx5JUDh&5tp!gr}yu(_qKPKW%#*6DV;ZBZz-bt8xr2}
zKIjvwHOugnY~)^4geasD>q%$2?)sS1h)!pC>tppf<rk8Gv-hvbSM&e6c5P$7d4^}5
zz8CY=$+LGa@A=~<pOyUX85yqF7xhWC`cv^f|3Cd8)U)~dj10f<x#Tl({H7KEdyoCP
zrtasnGQ3<C@QLVszW@JO;{9xn46m1e64rJp$fs+L3?F~_uy-8qdp0z8hL4QQnc-u9
zyA1!XMLg$i7ICu-zxYZGe_T^EQNur(Rl`s2kA6_w4Kn=992uS&b^gQE;hOg5xiUQc
z%3kn7|JjGqhpn?RT%ESJpk?c(|G9z<LC)toX4UY7OApWfi`DnpYt~p>?(3aZ!!v60
zyZ6{yFWUV3e_H&PF7q0mmy*_b<5cSndkFgB51p284SsBv;c3T_+JhPAA~ydsbMev@
zzy9No%`;s0xb}K=+}V$;e&)1%`R2eMIyKD5@Z9RIlnV+P)o!)t&p)u=-ZLY^&lH`B
zF?4)PTk@ZOSQoTIJ2S&Cr{<;Po(@^JC1lNyT6$(>I98PoC!Y=8@jK5IAI*{B&+CsK
z+Shr}|086s8a`bAWE@BP=gIKDR}Bv)x388q<c@UKMVWa)tdvtHrmj<m9A+s%%LZ`s
z>)|W~$gXFG9Iv0L@QQqv!mIL`3UkP3D9j}{SC~_7rZBf0KR!87^T@A%gZ%1(d_iuK
z8|RW=o0cPU$*)YwE!S@f448HK{_F>4D`3ux6a@+bz|S{}tuq8T`29rON6Gs*dB;t6
zn7o&fcO7|0$vZ~gN6Gs*dB;t6_`mIa?onG9pE<`TFo5{^yI3p*Z<oWk1*B~j)kF71
z^^|HATy1@;^kTsU97@J*pw`~@_O`Z`W?0K=dQ?|itEnoxTzK{>lmuR`E!}NxKngZM
zjZIDU_wPTbxm{Xx{>*vk5I}6{7PndGv`wN$=plTcR$Y1Z^hsqYlt_wXZItE)xRKfL
zKy$zPX5o<ww@*O{6OyH1_tik`zwX~xUChXAFFyszNzuMGN~>1X$f&ztU6P$<?7Vdf
zI!Frkw=I6$08AdLZ=FhfI?z#m9Ev9eF>Q-m!Je)0LHXIFzR~{9Tj!uSQV`p=SO>O>
zbyWq24TI00c2%7R`$r3?qfgvrukUQvwY9hD^`P604R?!@Wnb=<B^O-02zHYeP*=aS
zdo^M(JZvv6>SzOfzjyU3*%x8E{<<eIO9^(Cgho{NDs5!(!NSh2_O|BQ^8Bxo4kaB*
zKAe@C0QQ)Kf~<RyF*-#Wa$0k?xl7lmxphTUY*lbBC;!Zpf^FZGSomB?`jzCf&Fzot
z;2K)>-HIDmE}xsw5O=eCdU~tnyH8$Ce2R}$9KL$Bx~=)qqlfqJ-LAMep(N_2_q6JJ
zv(8<=m)tGF7d`w#(eY#VTALah9;$0ffYMs1_eFPi57MW|-2dm;mY&qHaeN%FNd@oI
z!^b+n#Mal}Cb9Zn!swFTC#_$c%B;~Ih-pK6F<hMv<Mgq;O+*4bzBj4%?47};tjyT@
zu9(84uG<}8e-T`u$6xMiZfk38YJEsL?R)ubp#SN^$keOtNyQJcTPjYU)tx9RO+-gU
zO(3Uq?UQQ#Z9OH`5sLBR#J1Xd2luwL9Spx-mC}uWDY@3EYeTd^Z7EP2lIMN#MN$9r
zTv&1Qx?eqvFY1JIk374ZSpHRGmyT3h0@Mc8pOh91qsM|}a71{n7`Kf-s<?8n`p)GB
zV;8AJxI~9y@}8kbPv?AjG$AY(9|POcxXj)04K*c~8hW~)nAD!(V25lN$iAp9{P@7$
zkkd_lV<ULNZ_<w!-?)D1VNW;OK@LYh4iCRG^yKr(hK4KK3$Et%bc~JRhobjN(r=Vy
zH}xP>YG9}Ne9zI;vf$$T<tHD5`16iDx)f1zEB$(ZUyqsA%IA^U;)Fk3c-VOR-@nin
z9@bP83u98R4#LkY`lns4d^xZ?Q4$|?SdzQvC+~`n*4?|Fm)-r~x#*b%)?=C{fVF(2
zM7SsQFDaq$uFb9&uiq*!J$v-Upcv>pna~jr+u?ng;lGRAE&tT*1IgLU{2R$NgAy|h
z$?%d9yzlP5za;zbP~VJ7zLu<dE;W<OhHYPtkCsXPT!-T?N;2*}mzfEphgsv;Q?Ne=
zKO;w;_oL>(`-dqnN1}!;K(olKIeD0Z4VpKk3_}?F!eY2<;yHcTV%+rosoD4bZ~RVy
z29Dws1NdeIJ$um>7n2-o6`h3-qF_m9LPfZ#PSQY~tiKN`-CTw8Nt>=sM;6LPvQXZc
zER;mS5w+XBjXGI4Po2D!K3|<oou^JFyjh);bgkBd^4HPUHCZN;q`M;|Nd?7|Wm49?
z3Nh5S7ZrB4wKWq}Qu=vl=%-&M%&3yPFB~Y)8`^cIDw%lbP}1Sd8C6o2Ec!TCovSs>
zS0yh;?KyL8-!ah%ZTsVgb5}{@-T1#Mu86c_J$aJL#dkYit&$EsE&AT{GuLXQ4Z{O3
z(9|tQVh-Qa%~2+^k4E|KYkjh(sdvzDQMeZ$ES09uE|c%{_O<R(q*pgb1zx&wzw{Iw
zHHN)VeWZP*Og4U%vG1W?QV@DI?NZ5^16!okmB&AR{A!u}GU-ZNeBp!rXTA~z9r*AQ
z-ydh3`ah3nm&t2)!;j(T59sdKMEI!g{N>+ce&lrQ%&$JVs-Gy6gxb)7GrPhH2cDnU
zomqD6KX1Oou>0GrIl02$e*WG)L^q{2crUo*{P44*f=J=#yAtrh!QP5r(H(dHI&O#k
zohN365|f;HhNhl8{%LA#K*VFiv#X~!G3~Y;`6JWuZttu@nQ@`|{6~^-|2^k#sB`l^
zV0ryH*xB}-s$Nr}TniQ=r~=rNzmz|$S8h6|l$2bmJbm_ezuWR3ejMiiXfT==N{7MF
z)T9!>BK6Ir{D<oNKl;em{q*y7tIj^3SttiXGrl~q{e11C+dR+Qz~3EwpYflc{p8H>
zD}^%jz@C_o<a-pm|C#oK?eV@0hNSQQi`j+p>Stdh`X~B_2mk92ejmPj%VJvO%jdHT
z<&z_!AME}lCgkV8`c07kzcSZX%~2?;M1BYV^y})<PX+I-yFE0kP>$fE*Y^DB0oZ$%
zd{RC%t5D)t-xyIS$40+hp*%bc{XOdB0kTeJzE+*=1^Y?!IytqWq!JrS__Ye<<#`Ha
z`fG0}kG<}OGI^dtneu9(Y$pok^nNmG=6;eWlt^9MrQ(V0WTq@UEbOyc+es1FPU^eb
z$n9ii@}Z=p<dm7)$*2@@;F*U-9i~DF7h4z2tdy(!uI%4?R>imE=j%bGtf{H4sh(LW
zZHWD3!WXA*y2H?7#*T{Xb)8M1Qa+ebDVG!b$)o44*M>V=K@gR`$?m6zo7&(;%X(9#
zTsc`Ok7q@H9MjVO`}YF>W!Z9jHVn~!k>2_0hEf-PDyyb7$<1on?|!v%^?IOY@o)N9
zH<X!~`|G<Csz0FGQWvwA{q*}bOPBt->y=8`us7vuXWE^<-IlhD#Vf!6C!g=Lmu^B{
z-B1b@c)?fC4IQ6ZT2g605xF?OyTbm9k{OjU?%ZdeUFd&tB30G=2>jTlK#b+fIBV_R
z|I;tj=9N+t0ydQWCj-;c)6+iiUIJMxUA%JTihtSj!J3(sGV0v3fn!(llI~tkS^i^x
z!HVxKU1_%|_V;%0&aRY$iW|mK|C7l=rnT*l*!GK8Z1w(V{qlcO_0HH*Vo&z!dU`AV
z*Ns{`YbMQprNcJf=HG8vy1sE{rR<NmbFKc1vYy6WORVTCmwD`6_oJQb9L~R(St<L!
ztjSV-r0F)ccrK-_@PvQ0<io%I<ot|EDH>ie5OF2Dcz0>`wUj@+YyYnie_Xma_F3&K
zh4O|h{T6&pl64^P=l|j7_pd8il2;4m(`?ZnGm?uB?fmVQKm6h6b}rSk3*}4v$=&F^
z*P}nyl!yI}%c-7SC_xo0jS6eP@!?yat7aF<@gdWWa(u2r`I0D<&;B7h%2z670Lkdm
zZN8cFnd^dn$ou&#m#gKx22d_O$5pvzJ_G2~T>5y!JM$RKqmMVtW}m-7A8(x7!@T<Q
z7|gFfcOSk+A8(wa4_~K0SEs*Le~ys8UjJ1O-=P1Bhi}ryYiQ7G>Er+Yn)?6on)<(9
z&|lDB&|lDB(4R~H{5R=uo2kETH(c}J{yf*i;!k$}V1~ZM*X~9rUoZXIEAX$xzlr$i
z4FX~^)@WR$gPM~YVl*NZrK}8AQu6a*Wd*)ZM{UqG>*5>sYhV=&+O6{Qb8_;PxA1t-
z7!4Yyv~!@coA^QVRzf!`M|lI6gVucjnNe1zR1yH7wG2;~(Fz)~@|C4{;zX+zXa%Zp
z7DZWhoopp=nI_$=tkfJ;SqYw^JJ1j{(M%wurk1Ic*YH%bd67yrp`9wv(WsPHL3`X(
zJJ~F60PR=sw5fJevrI#@U&fDsc9~}Jbh}DN2$c9y;6Mrl1P;-zL`cCU{3{@kXqK2P
zfFK_=NiO2qx|jyBX6Xc$T$Y1Ph>G!J6QZ&*Qj&^Iii+^#KqS)G5LSdp4rA66vJ1EZ
z$Y7HU1R;}&reuZq2~tLz6p5!q1^6jl^rVQ0P%<UT$8&&)uF*`2q*J2vc&=_ADN>b@
zBH5HE4?nGonh=pOMoo#%;pcSH1{)HPknEe1oW=8Wk_Oh4M7GP{Uo5i$X`vzIXYfSC
zLZ?Ggbm9i4DIlU7!d+4R*1LAeb5ttjY5eenST!*TLg6l{KfKFID3qltmAQC20<|QV
zG*qUM1uC*#uuvqUWGQp-uMnHth)$Q|zsg^=PbZoPlz<Y+q(X^|Dwn4!PvJ)qy1zey
z=mdz|DKA<FH!vnfh{&H9nOF|MP7+$H+;1ago=BFgVL#BKPidv@ms<c;Q7R=T{{(&n
zVd`_5^H<6BLatJX!~j*3V<LeQv!F6UWl5HkM$h%s<Z=CV`g|3l(?<b4YeEkw!uhc|
z)>&C#6)3Y5K-(_MX&0iRrXud{adEqv5xr7{$bh~D(1*+RE5-Se97suME^qLs>h+#n
zU6vEoQ-c`%sV=F_dMVJQXuvXxDHAD0`4(V(E5PWjP;v!G8C9mw%K@r_9hyRpyG-9K
z215mFVpL+V!bSOnB2Dk_)PVRqX<&qD@OSIM@gATG8^mDn_iHFMU^T<0B0<Eks2M49
z@<;NiU{G89-NwbZ^>~t-dqz#ONGAh}+@!3)(~w1RLLnmH-qs0qNS&8kj|^vwC+%>F
zQ8nxIdXV5!5Hgh*5Cxu!EGpaONzK<#1<eRj?&;PMjnl_Ucf4QM949R9g?0PE3L`3*
z0#88}>HU%0o@Iz97=k8ux1Ly>Ug&glms_xtu&h@E)_}-V!3bEEJC>7$Ah+}MNQRp+
z2Dcp>iFX0;<C<V6fx4LhhJiK&l;y|@og8@A>k+PJDx%Lv^aygqeQazWP8%N`8Hr!T
z>4d@8&K+)EHFdyrA8D$<A@m?(8|S1!8iaDh$sIwm8bpY7s+$oX!A7JwGzO1Y#INd*
z;#Qhqt{_7r0t-&0fq<n5J%F%Mx&HcHTxyPx>Y3^<Ml3Vjo{r<95g4b8kBWe$%hM>_
zs&pq;pwYvmr2?0rFhW658N$-}uPVzc=DMT1oCJCpu`%e1fcfb7xOfB_6_eJ{IJJ}`
z>m|Ixz%~YzB8+mbK(80BLYkF2U{ojEb;4t8Tr&!fTZ~}!l1ZoIqobU#UNJBP>7~Hq
zP%&cd$t^?5+*M*^alOFZ-D$@dzEd-fYcx3UNF9rJc>wIjMtXsr1lU2q>>$eMMN$1K
zA&LqR5cm>cSkmF|@f1(ejB1iJ<KvPM%Xp5b2BZ>gd~Ad?mVsO%Ol^d69qR91rt=q}
zOX~%mB`Rb3)~Dm0qn$~G_&DgH^;i-&%sswPM2<7HmlM;w57Z_i+IM<|T<R`FPj%m=
z1Q7tYMJ+d*<Y0WplR67=7(~n%i|1CAM|uR8j*W>3Yq&QWWIbU`@AXp2oOGzrvm8d3
z)dzVNsczov$n_Y<$9E=a@KVjV2$&nU?yRb+txEGaCML|odiR6nMVQ+(t8_B1pto5G
zqYfZ&jr!(I6;|YK9LEbw#|yW*xg9f(j2ZphYvC$tc}1+B$sUYPw2soyK+F@pSEKLk
zEzTD@$;2pC;9l1R-*l+a=cWqdJ8`^_Q#u~+wl&G<M?_FtUQrS&ATYLiszd+-0ucLA
z29m$44AuMJmU{}t=u(alGc?tMeyH><{vL&e958IQNp4h5d2MZdeMLzn0b$eY=j47w
zr9%LU0+*q-`i5RqCkMB3r(OO^0MpC$x^xM{T2!i=>iU5&Dz#98vpSP@a3b>ohzW)M
zbnDJYuBU%_FS3t>VaeU~XkDCU*Df8`DOG|lY32%Y(=Xi|zzjE4M!5?oDGImjD0Js~
zz$F$W1fzRvWNlSsn0qmTM3ERwf2tB~cH%m5Z!1%!C{@SxzXYe#FWs!ij4>|M!trR_
zrbn}5D;a}mgl^pGUJC}NJT?;s6_r4smpM80)^WLB?pacF3DS(X3ofO{!1DA<>Ps%1
z(inWv_~;G}X+J_v4_swgtEw!?6eAK7z<`jNht_FOp$7B;i*Y}~1qgD_AUG^t?vxaR
zFB=`}-bx~bjf_3r;ZappUSA8BK$#Lm3=pDFnu^PPj;dt4B<M0=@9$0(UWyUObAtrw
za;^{?iNaTmkB<NlvKxLQBLqgRs;+_nks=}!$bi37Dk_lmiqVx=3|HAy<0-f#4}!gd
zva{vfu(2`hxrD?SnT#gbxPx0;QB_-aT?BAs2n=xcp;kI4_d1<kj4r}roKovm26r$i
z+37G0r_<bn$MLbJBV%A`jl(0037|><6zk_+Ut3#OB>^x|2t@~QqEQP^C!qvofd1sE
zZmOD{1i5fJB|95VXSx8C@o|vr*qBj7qHF~q9F9k=sut^25h(i*$OO{t5BkG0#<(l%
zL5_klOd!}~2YCuy;&HrGG;T3A0zej-Lh%R-19J;fR|+tq5e066VptRk>BQ*wdSl#+
zngE8{;7R2c<))_xas551@#Eu#xOf~IB`}OTII$jS<sic{%T=mL3<#BA7AT6zP-?ML
z*#LZVg-WeTjq}_o$c^!g>1g4C?j$93g6aW{O`vd`(o|JDBO^02%K=KH2_+f>Yt|U&
zR0nrJ_3+J=9hlOS!{uf)sf}I)ghsQob9|hH7}?>z)5$Heid$RdPC`rs5{o$wpy-iR
z@>~?_0BcR9HkPg8#Hm%P761WyGTu2Ig(oOuTsLlQWMoyjxP)368;9;AQR1-G&rh$)
z&dttNV_3b~Smg444l%k$uOwUs%*7+N@gC(w5sTfL20BqLDzU1J_0XVb6louiEk4aT
z0Y)(UQVBL7cj3xA;G0%;17VScxOAK-x{Jq-aWcU=E3c^BnpT@xUJjR7g6uCJfKkXG
zodQ`!fXKaKF4YH7Q;jP4CQVbH7bi>_1v6p~-md@!Ecd#)>m?;yGiz(B%E>iUB1I(=
z5L6-#IGqtBPtO)`RK|J~6hy0fOzpKZNj%ONokXYy0Wh{Y?F7jI5V+<0P|*Z}vnhyN
z0SrFWm|QhBpeDw(L$hj?TjBUPK00!2Yh-zO)oqoigzgdM&h;#>jCC*H56ZF$!Im70
zY`JGlHi#hx&bCouU~&v9ulM0qOuy1j5JMJNX7wsD0LW=5a(9nSs~d<xDaZuE%F~>5
z5Q8TSW+aFs&jte<bIE`y;rDG_R;}8))h&2ySZytal}k!&JWimfMlL8DIDkSElli>?
zxhDuf;FSx9Wy4N{Jsc#sR3GE=K8S$fSK_zzSe2^0uD(K2Lh(2u0)_|Ci98rM;sj@>
z$H=n<z?7SjogEgG>n=}+z2Ns*F00(Gm#c_0P^l_KL;`u7NFof8cx+XZr<1=tJ3Ac=
zJZTps5O{&Fp78rtF4V2pYilJ{5a}<&WO5K&*;3-k-9^|;T4cL}uM?gssxr%gr}A3T
zD9dD&fGsy>aGiqWxw%19U>O#c>oQ^D^}c%*SYcp+WmZ*)ODsTonrseXjC!GylOR3J
zQ=Tn{gDgG4XaWnW7wldR*IH#pX6}rvAo8(tYaC*-Ny3~4N{+aLmxvIc%ZY4)z21M{
z%f*S~wiD!WZ6>!I<X~l`pU{v@S|nrNAHW)l<2;=_cL{Qd86yl<xyw~S9H&T-_~ljC
z!Ar{n?l?^9r(ypzpjUZvL7HWoblue`W<+F8+)VJQ2CvAiGD8Zfnt`zfPJlFv0dWIF
zwHRZf&Hh~XNTB5>G^UbDM={2LLFn$}nH}TgQX|7`P>qo5Ug8HE(nxtGMl)z+p6*WW
zMbVhmK#4Fi&Txd3WMh`7rYtBg2D2RKZ8l=2)+?9^_Znu3_c~@8nKCSq{Cg9VlYehv
z(DQimTLl(J{=JRGl7Fi(tLLCL4Llc{5)*kq6ixD59R_`yzv$oN?-^W0ohEeR@fmc9
z_Eow>qO)$$5&vl8r)B?DD3g>qDU+0xIVqErxha#BxhazrxpYp-1hmgdnSl1WDH9-=
zmokygOPNSh=A}%e^HU}%Qt5n@2@uUknScoAqfCHkKFS1$=BG@g^HL_#c_|aAG}PBu
zEH$T0l8{t0x&(9~JT%JJIy7{GE=d7fEhK50F##ckhlfgi;ZUpaaB0c}W70Z<F##Ci
zvQRi&BqbS>qX423)>-EGvV3PyCMj|eP?boja(Rl0GV%3A5S=$7XP+hXrYIATKQYp2
z%7o=wiInk?Ea^<jBqe3P+ybbIQl=>rZ9Yq`4|i6E&r6xGHF{^h=B%^tx1vngp@@o-
zg1EZMWT9F_ue?1kW#UWG>-o;QEH;I&LArb?>r%AyQzp*dNEt<{Kbr$oz1QZ7X|7Ve
zb}q`qm)(H)vI)wh%a{GIzyBdn6?RQfCU<60CR(J7?Th47z@WDJva7}Y)`noVYuX*{
zE0l>WJRI?MuGEF=kh<;chq8W#A$aY&sN32(DU(n>C0|4F)*{FqKKpibKmBp~TDLl_
zETq6Vn=<i5D*0sy9}Gc*EBj$=KV8f&4P|d&hm;v-Q6{#oBxO>0R*$5yONOHR7c~~1
z+`JArFywAvd)H`Zk|wKkaxF=kIP+5`NRvd@7ccsUWc@Tl$;p$OSu`aKzAD$Ux8JGL
z&Z13ZY!Fbm9AUdo&?YJDlEz-FSJF>uEQC*5Y-Zh-_FLs{aQ04{&6}h+`|3lTDLLU3
zeu}Rcu}ouU8Xkyx;eLvtL<B6?fzh)bO5ft_JtuME%PKot;OvTqvb_o7q)T@J*q2mS
zi+iCGF=-y%Pfe#ujWdZ8XK%eeoP}sj#7Ri#35P;MZV6m%(TkNzNVBMZD?>>MEyOsJ
zIN>{&Au3mbIH~h?b!D%8+`lEax-mERLACfKwQ%#g8W1fQ=v-iE#+(>YRL=@WQE!qt
z0hZU=eH}9UgL6xAgLA8^B_}O6)A+dtF&N;&lcez!a}qAsp}wwVI$sgGw9cD<t-_eh
z%rq!Vl)>W0YS2YyVX!mLb+fp!zn>UtYA!9xI7OWp!<{Lih@RpasstebzZY6d8)Cr-
zRR=4@jWCFrQMlPTBGk)aL;B-F5n(MfPEjYu?J6l-hlcYB>ZDG<zfe(H+OBY@ZmixC
zoZFb5TP*_S@ysm|5weI)4qP!|9%7uLPP8hW)Y;ppC8!e+xu&MH^fq?EHNLu0oNf>^
z*=%n7$-;Pss|=2yhHj)YO!hOV6Qf3NG#2ECv!&o?n73<P16=BGN3Tc;*{p1A6w}fT
zo7v3Zcm@%HEOetC-J8H*@^8<ePD0C2y>F$QA1+3h(!#N>hC0xX3Vo}ugIG)x!(d?q
zvnjMtnXI&QqumMu!zP!(c1^r(&Yc(u?!<_evqOCe?!@T4y{HJoS}Q6_Yw89<C={`z
zpQQ|5OY_PHASM)gCUc9IGvBw|IK`c~>d`uxCNxy%%ubP@OSI13isYiw0j#UE!Wg@b
z797=Yd0Xu2>;T(YkPwW|m|n67FP>|`6nElFQKDM5GuydRnL=<U&b~!(GQFs@4l_or
zqlgXr`sqUtbJsG-AVeqW@l0147@knN-!yr`W*h6AowvJ^<cSt>^)5<|62>MM)fBCx
zrN{IyGL)>Pk@hFa34$XmWjj{b`Aw52;gqukc@nOXpmtc4Yoaqih~*1}A<41q;Qqnr
z{$(YFpD{@c-pRtuwGI&xp`|j|4)U9(Pn?}GR3#0Speq1^uPY^_D9SrlA@EL)bq>LL
z`v;}{D-6{q0Sws{#>tZeicEEUBLOo_p!l*=P;aSGjIP3>oRtlC_})da0^xQ+Mn<eN
z@9|>{8x)g3Cnp2i5Wm)0wlP9>{9O?Mnr2Ygt`iJO6g#D^qRSObO-8a%2q)8AH&i!1
ze%Sj$)DKm|Cl?byD*zCk;aVz_9gmOzm}v%u&kiRTlqlD;6{QtgwzmRKretKm$;@>C
zrMkML_XYL>6t=}=$5zm3GzZxZ8D`u;piD6+T3;i<phUSU>p-f4noJ<rWC-})>ozww
zri-dAUi1QxMW#?3csww{Ac3U-V-|w~FfKFzjG8V!#rc9FIa%QB%cpEMRErzM)ewmh
zzm`UK*c1x#%rA7uj!6tN2Bm;qHUO8dsHmw(k@2^9E28*O?XAwBJHf$9P(+}@2^1Q8
z(~gKOUS58Fp#a6poI#PX>)>{%4lZ5Ujw$&xXXmtr8sl~XA~$!7vbvgtIJwq!3!Ci~
z;Vg@AB_aIG8I(j;tOCW_!HTP>F_y7tvYLvDRsaEdQmvehf)A=0SRFDiuZU2w9d!j=
zHo>5PAHZp>3`Isp4Tja#7%!}I%OM8WxIMUE2CT&=Z8tlF5~YmJ+ywd%DzdX$L3c1G
zP||28zyM|xUBd=q*E!4E;ZiHG_PxZ7QeaOc2AAds)>`Ps70gXCztB+F&JyJR9fCmV
znj%orSOiGy_Nbyd0VTy)0hiJ=b!TPa!6jfq?7^EBpnx@h{P??ec1%B+EFzR#Mc2#-
z6e12dnIVWx&hVzGjCE)O5eZhaeM_*ono%-|PznNIFxgu`ZU6-5J7xrmDF}tP5PT?6
ziW+R7h8Wg%4U5GVS64Tdoa8dSLPH}ecZlrh4k512{LmG2*E?ne3ON=TvHYkE5JME4
zVN-#Dx#_yS-3?|j8R<$8Ll#(Nr8~p`AgAGit1EreOadj1mJDLx3&D&CXt5b!V55q<
zFeU6}yN<<TGT9rLJedr`LM3)K4kUr%J&Qo$g8;m@D}*5#LN;N)N8nvl7q!j}M8IHx
zo^vC1gdQ*5D6ykB%py<{*?TgQqhd3>fvIy^Mn;H0;ToGP+zz|3*0I>{hVCHJV8@OX
zA|ihrrU{e=KHE1oBO@6MJZUHJ_THYHv4;=4S*@cm-<8QE5fJGwZHho?y~cMAC2S@w
zGF*Yhgr|)WexblqsEjl+BT&+u*@9SwLO=nQAt8!&6DHf;TqD2&1MAB#Vx!p30;J~@
zfl?RFW_u@x@MAM#VSyzdj3%(4Zr|e?3d^kgy!^I!Z6xw>1yg25pj=CI1#2ZdL%2Pb
z$R^=-H@EHU*fjPQkjFAV=TMM?D^@T<y37fb0vVsp5A{|MGe#J&T;(bO4J_LTkTCCp
zH<!bnb~6IyHs2YfS%yj1wT2*2q-<wD@WKY~Nv5>Rj6eZt76sx4h&2R(qV;ul^#WRq
za5Dm>E5wz}&xm5LyF(HvA<nLLj6Gdb1WK1i%6DbEULXjRYaw2;E^`7!aF!rYjM~>F
zP|C5n>61GE4MhjA|MKh!WnT8AWiIxFrqyY64Z0R>91#B3I&hLUCwr2XHYa<MmM|xK
zl9rG#7kiSHF!zBI&^{-70@~+hPk>-P_9S8611AZxwE5VR1X;qo>`B`E2Ts!FKX3vf
zoR2*LqWRbpAexswNtpM*Ny5AbP5@lks|QXfU0vn`3h0F}EXv<HEG%L2yop7ZuFH%;
z0bvP+VN!oMj5u?WHo>6um@_B|<e8JOsWT^242u8ynTJl&5+)9vBqXGn9Xbg>5*!Qm
z=^(Ayu@jI*F*0$&B!{w|SBaE)ymIU$Ep2~-1yB{GO>-zM`Rfz(LeAG5J8{(LIUbq<
z&bK>u;uwagC}{|f7Z(@Sg6Nfx=0A2q(d#`px-3VEhX(2Mr)*1WnV&=91R!M;nZ6(g
zs0PrO3>HtOZ<+JhiDLue??`Ycef~@f2(kdGS$z{6%A;8vN()lv=#S)6z_9lCGihST
z+R~26%X`!^=dqIjP9<^dq&bjjA%hr}cC>AZM=f)5C}AE1hZ4|&Aoo3()M$vlVHqu`
zxg~D5a*kssl^$h?2N;4UJf=k~L}xg*hB0j%cbkr#Kuxe2i^4OpC<S^XkGWxWG_=TS
zrM>kw;KCAE1n664vnUBIB#XlFNSk0$4)bbiK3pw>XqLA2_SWlJHZb^VLt_R$YHpc*
z_{5Poe3F1T@+Mf6H0B1YgV;d{M6p^4+gn(#r%E9!rVS?`Z#IjP#_`vOaVR-Liboo8
z`XrBOYv~|52tyQ0TM@9__G1}jy?U7oCt&X5C+o`!lpG!!2D$_zHhsEEU~fyKi4Q`y
zV$wVsqAp|2I(|~Y3DE0>>yZ|cMQPq0c6rT8OQtPMvp9$qN=UOP$jZ{zmX$c`_=yLn
z3@PIgEQ%q3$8)4@fLxd~D<;!{Cbp-pwBGhp5G@#JIxw7d{$#xnMFU6{1z6TT^<QHP
z*)eUIc1#*gVsB~9@?ctu!2qwcCyl4ipCsr|f1c_5i6OwFwtY}Vx3#pfwXtJZ(LfiO
zEA2R3o;AY?f{3A}(pd`g11KCy7^0`}!iWPXz;9(w>yu(ILNq%Yh7}BAW~{X4`1$bH
z*eu(yQbbs1nH@k0RLLB5sL-PVMwb~PJu2H<Tc6gip;^&f?3h-|m^2YEUru-N^9%8N
zZ_P3>VV*dB0HsBxlW_uiTL=~fMBb!tZGD7Q@|M%A7|SdfbS87za{HCbX}l2FkLt6L
zNi*5MdH_Y4FLWdhpak%mpTMmSkM#9vyRB`ktQf3imex$V-EtZcL5R=B)yx0_gYNNY
z28$9#96+f|@E{JLu!LCO69ec+yS~SN4THgAz+hq6F)1vckdVT{jjJ693>!Mlk$3pf
ztP>~+;8x)nW;%hw3Djyatf#%bRc{zdq)-?Vh-G6(WAXC=hzW&mOLyUOJp3!BPM{?4
z^k{ROCM-<HaZHn-OIkPq^(t-a5Z2e)K3KesWfuimQW-qX8hEt@3BmXtogd=I=kk=(
zCr~I#w8fF*$f;DO5iAPFUkj_~+ExQLsMtnfSnh-9t1Xx`IvIq>p1z#U3jxF9!xT)j
zD2|T3%^Xf3k7Q9=5MF>*rN}B)Y4zG|tYtCKBCvp1q`f^kL9m}?$QFmyf+-edNJuF_
zn@vYh>@WrIFb5zMdqid>s)`-$KKw;Aw9Izp_vj=B*M6lfZH=FwPhkkW8WK#iC>#!o
zs$^jVi=yE9^C-Kuih$z!$N*I_XE%26!(T|D6_zx607G_#W^YfRgs4(C5-?LN%8<Wf
z8X7<xLs^9>ILarFJOZ@Eky(L}YIQM(yI}){{z6Ow*-r*!vz*2W+2|LNx=sXurdbq6
zUbBfsQ8=a<+WUB5YSgN%ELdg3v!PjS`0>G-4`B$R!S;&@BnN=Rr11(vLQ?%C0B4#;
z@o*#$q9}L;?XB%Cjsf+cB&*e6%eM`{&}bVD)?hUoL?j9wfUsC=Lbilpy;}&BDH^4P
zJcu%=;3*9tS3yxG5Ny<u9s%2|t*n-bXcjdG0mvd#C~LS}FvB2&r2u30K@<hA@(Gde
zeI67}WxYxj$?^A~SX<H<R$>}tOJFRgv6yS#^8tw_@Y%9u62pu}Q970l!L2LW_3deK
z9xeg(3J=B89uDY^ot+J+BGAeS6qe(ATl`%3e1X6RpzzITl)*U1X80*&fLm8S#grZ_
z4kz!4elU=LU@~27XfzVSp2l-=Wb*wuA$~j(LNG<6458@Z^~Lol_7p6+cKu-4dRCmi
zy}buOfS%B7rlarx<&4ARgz))(KH}9>2d3FU6o8?wSF80HX3!5-ZVSpGMt3mK4w3<L
zvAwPJ8XuyVG3oDtPWXscTRAY-G@0=zhgp}w2&%QU*ii8{PQp{T)v9?Yk<YM_0(&Ae
zmazn2wfSsxpuZO)@bQ6HTY?pEe+WjQz9}B%@OlEII8dQAL{icQ+u>GPlc69^XlDy%
z#2&nB0SZ|4sj2H$uciw^Li~KlbyRD{qY!bxDn?|nN*%yb4H{5T7_AJLKG4NZOk>zi
zA{2rE7<5M$kQ@MkbKi_dF$GZ{kOe*zMZF#y(i7wQv}yf%CWA(^vbA4E=ll5hRc;Zj
zrmsolaXfq+n7sRDJPJ7$>S7Ot8pNQ0)i&)In4G>xfkE(kCT*Dwh#?ECv%)Q60FcvA
z$>TBKYaTM^Q4X_IAO?>tFe8zyVl^08g|-h<!a=s%)~~12nKpE8NC<}cNLJgdxs0Ms
z2?1q8W<1JJf(Hm7Ah13wQJv*T*dK}v&>9rmf<Oce+G-konco(l)WVID)s!`tXYeRP
zhaC^8Rf=MD05Ij`snv;*^}J$LRv;Y2+P0p#&Swje23xi`h=>GQb9stKdE(*dU#wQE
zz`&DskpTgLD)k``ILK-ng}yE%MB)dL{_>`Hl%84-P8eY`X`$u;iwRE~{RBS1lTQd~
zG|i(7=5ZV&i|gwnDZnx@v3}cxNnjAq53De-zyy99#h}oyndVUpLPy5{Ria0+x)_eM
z^Z=s?EU1Bpcs_85m4GjB;cq1J(SdGu5M`+LFb}*-gzBuoVj`Qe0)v7Aw>h$yE+CIX
z1RNibgANX~-F;I$$`IC|jPr2x2n(nuW{fac&r486vK;v!@qPT(fp^!MLr<r8lp*~i
z4-QB(wMiGe0kJ_u=ExC%S2lQ4(q(;9Jj&2zkY)-HH$c=AJW7i{hsOt6G~wVBk22J^
zo9F1ERyb~ZMDQq0yE(kov_pMUJW5}a%!B91tBl61hH7{7<NC~bl*ob@%yOu=W$?8R
zq8yy(7>XqdD$|hUzZH-2SMon(-efcH|9@@a`v3L%rvD~wzUv?D|7}I^-Tl9v0N%j=
zTM6Jz{J)I=-pK!32;j~9zj**}=>LracvJsx8o(R-f5QOY-2a;e@D}{PQ2=kl|C<Ex
zR{Xy~0B^_tcMsq#`Tx!Vye<FVHGsF~|2qco_WXah0N$ei?-an>^#5G~c&q-uLjZ5r
z|LX_vmi@nW0B_s>>jv=F{l8`aZ{Ppx1@JfU|5^e3E&RVu0DlwzuMxoC#{ahu;BVyr
zTL<v}s{d~rz=Hn;{|o*X{4e-l@W0@H!T*B)1^)~F7yK{yU+}-+f5HEP{{{aG{ulf&
z_+Rk9;D5pYg8v2o3;q}UFZf^Zzu<qt|APMo{|o*X{4e-l@W0@H!T*B)|6cyzei*Ok
Mc;Q;O{%+U*1-ZrT6aWAK

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,928 +1,931 @@
 /*  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
 
             val isabelle_app = Path.explode(isabelle_name + ".app")
             val app_dir = tmp_dir + isabelle_app
             val app_contents = app_dir + Path.explode("Contents")
             val app_resources =
               Isabelle_System.make_directory(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)
 
-            File.copy(
-              app_dir + isabelle_home + Path.explode("lib/logo/isabelle.icns"), app_resources)
+            for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) {
+              File.copy(app_dir + isabelle_home + Path.explode(icon), app_resources)
+            }
 
             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)
     }
   }
 }