diff --git a/Admin/components/components.sha1 b/Admin/components/components.sha1
--- a/Admin/components/components.sha1
+++ b/Admin/components/components.sha1
@@ -1,469 +1,470 @@
59a71e08c34ff01f3f5c4af00db5e16369527eb7 Haskabelle-2013.tar.gz
23a96ff4951d72f4024b6e8843262eda988bc151 Haskabelle-2014.tar.gz
eccff31931fb128c1dd522cfc85495c9b66e67af Haskabelle-2015.tar.gz
ed740867925dcf58692c8d3e350c28e3b4d4a60f Isabelle_app-20210126.tar.gz
8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz
51e1e0f399e934020565b2301358452c0bcc8a5e ProofGeneral-4.2-2.tar.gz
8472221c876a430cde325841ce52893328302712 ProofGeneral-4.2.tar.gz
fbe83b522cb37748ac1b3c943ad71704fdde2f82 bash_process-1.1.1.tar.gz
bb9ef498cd594b4289221b96146d529c899da209 bash_process-1.1.tar.gz
81250148f8b89ac3587908fb20645081d7f53207 bash_process-1.2.1.tar.gz
97b2491382130a841b3bbaebdcf8720c4d4fb227 bash_process-1.2.2.tar.gz
5c5b7c18cc1dc2a4d22b997dac196da09eaca868 bash_process-1.2.3-1.tar.gz
48b01bd9436e243ffcb7297f08b498d0c0875ed9 bash_process-1.2.3.tar.gz
11815d5f3af0de9022e903ed8702c136591f06fe bash_process-1.2.4-1.tar.gz
729486311833e4eff0fbf2d8041dddad520ca88c bash_process-1.2.4-2.tar.gz
7ae9ec8aab2d8a811842d9dc67d8bf6c179e11ee bash_process-1.2.4.tar.gz
9e21f447bfa0431ae5097301d553dd6df3c58218 bash_process-1.2.tar.gz
a65ce644b6094d41e9f991ef851cf05eff5dd0a9 bib2xhtml-20171221.tar.gz
4085dd6060a32d7e0d2e3f874c463a9964fd409b bib2xhtml-20190409.tar.gz
f92cff635dfba5d4d77f469307369226c868542c cakeml-2.0.tar.gz
e7ffe4238b61a3c1ee87aca4421e7a612e09b836 ci-extras-1.tar.gz
e880f31f59bd403fb72fcd3b5afb413c3831a21c csdp-6.1-1.tar.gz
2659100ba8e28e7cb0ecb554178ee5315d4a87f5 csdp-6.1.1.tar.gz
a2bd94f4f9281dc70dfda66cf28016c2ffef7ed7 csdp-6.1.tar.gz
ec17080269737e4a97b4424a379924c09b338ca2 csdp-6.2.0.tar.gz
70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz
2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz
d70bfbe63590153c07709dea7084fbc39c669841 cvc4-1.5-1.tar.gz
541eac340464c5d34b70bb163ae277cc8829c40f cvc4-1.5-2.tar.gz
1a44895d2a440091a15cc92d7f77a06a2e432507 cvc4-1.5-3.tar.gz
c0d8d5929b00e113752d8bf5d11241cd3bccafce cvc4-1.5-4.tar.gz
ffb0d4739c10eb098eb092baef13eccf94a79bad cvc4-1.5-5.tar.gz
3682476dc5e915cf260764fa5b86f1ebdab57507 cvc4-1.5.tar.gz
a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz
4d9658fd2688ae8ac78da8fdfcbf85960f871b71 cvc4-1.5pre-2.tar.gz
b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9 cvc4-1.5pre-3.tar.gz
76ff6103b8560f0e2778bbfbdb05f5fa18f850b7 cvc4-1.5pre-4.tar.gz
03aec2ec5757301c9df149f115d1f4f1d2cafd9e cvc4-1.5pre.tar.gz
e99560d0b7cb9bafde2b0ec1a3a95af315918a25 cvc4-1.8.tar.gz
842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz
cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz
3b44cca04855016d5f8cfb5101b2e0579ab80197 cygwin-20130117.tar.gz
1fde9ddf0fa4f398965113d0c0c4f0e97c78d008 cygwin-20130716.tar.gz
a03735a53c2963eb0b453f6a7282d3419f28bf38 cygwin-20130916.tar.gz
7470125fc46e24ee188bdaacc6d560e01b6fa839 cygwin-20140520.tar.gz
db4dedae026981c5f001be283180abc1962b79ad cygwin-20140521.tar.gz
acbc4bf161ad21e96ecfe506266ccdbd288f8a6f cygwin-20140530.tar.gz
3dc680d9eb85276e8c3e9f6057dad0efe2d5aa41 cygwin-20140626.tar.gz
8e562dfe57a2f894f9461f4addedb88afa108152 cygwin-20140725.tar.gz
238d8e30e8e22495b7ea3f5ec36e852e97fe8bbf cygwin-20140813.tar.gz
629b8fbe35952d1551cd2a7ff08db697f6dff870 cygwin-20141024.tar.gz
ce93d0b3b2743c4f4e5bba30c2889b3b7bc22f2c cygwin-20150410.tar.gz
fa712dd5ec66ad16add1779d68aa171ff5694064 cygwin-20151210.tar.gz
056b843d5a3b69ecf8a52c06f2ce6e696dd275f9 cygwin-20151221.tar.gz
44f3a530f727e43a9413226c2423c9ca3e4c0cf5 cygwin-20161002.tar.gz
dd56dd16d861fc6e1a008bf5e9da6f33ed6eb820 cygwin-20161022.tar.gz
d9ad7aae99d54e3b9813151712eb88a441613f04 cygwin-20161024.tar.gz
f8eb6a0f722e3cfe3775d1204c5c7063ee1f008e cygwin-20170828.tar.gz
c22048912b010a5a0b4f2a3eb4d318d6953761e4 cygwin-20170930.tar.gz
5a3919e665947b820fd7f57787280c7512be3782 cygwin-20180604.tar.gz
2aa049170e8088de59bd70eed8220f552093932d cygwin-20190320.tar.gz
fb898e263fcf6f847d97f564fe49ea0760bb453f cygwin-20190322.tar.gz
cd01fac0ab4fdb50a2bbb6416da3f15a4d540da1 cygwin-20190524.tar.gz
caa616fbab14c1fce790a87db5c4758c1322cf28 cygwin-20200116.tar.gz
f053a9ab01f0be9cb456560f7eff66a8e7ba2fd2 cygwin-20200323.tar.gz
0107343cd2562618629f73b2581168f0045c3234 cygwin-20201002.tar.gz
a3d481401b633c0ee6abf1da07d75da94076574c cygwin-20201130.tar.gz
5b1820b87b25d8f2d237515d9854e3ce54ee331b cygwin-20211002.tar.gz
5dff30be394d88dd83ea584fa6f8063bdcdc21fd cygwin-20211004.tar.gz
fffaae24da4d274d34b8dc79a76b478b87ec31dd cygwin-20211007.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
b98a98025d1f7e560ca6864a53296137dae736b4 e-1.6.tar.gz
c11b25c919e2ec44fe2b6ac2086337b456344e97 e-1.8.tar.gz
a895a96ec7e6fcc275114bb9b4c92b20fac73dba e-2.0-1.tar.gz
2ebd7e3067a2cdae3cb8b073345827013978d74b e-2.0-2.tar.gz
fac44556dd16f666a2c186be30aa6d8c67228bb9 e-2.0-3.tar.gz
5d36fb62912cfcff7f3b99a6266c578aafc288b7 e-2.0-4.tar.gz
3223c51c0b16fe00ced4ae903041fff858e61742 e-2.0-5.tar.gz
6b962a6b4539b7ca4199977973c61a8c98a492e8 e-2.0.tar.gz
66449a7b68b7d85a7189e10735a81069356123b6 e-2.5-1.tar.gz
813b66ca151d7a39b5cacb39ab52acabc2a54845 e-2.5.tar.gz
6e63f9f354b8c06035952845b987080699a12d55 e-2.6-1.tar.gz
a3bebab5df4294dac2dd7fd2065a94df00e0b3ff e-2.6.tar.gz
6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz
8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz
e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz
ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz
7a4b46752aa60c1ee6c53a2c128dedc8255a4568 flatlaf-0.46-1.tar.gz
ed5cbc216389b655dac21a19e770a02a96867b85 flatlaf-0.46.tar.gz
d37b38b9a27a6541c644e22eeebe9a339282173d flatlaf-1.0-rc1.tar.gz
dac46ce81cee10fb36a9d39b414dec7b7b671545 flatlaf-1.0-rc2.tar.gz
d94e6da7299004890c04a7b395a3f2d381a3281e flatlaf-1.0-rc3.tar.gz
7ca3e6a8c9bd837990e64d89e7fa07a7e7cf78ff flatlaf-1.0.tar.gz
9908e5ab721f1c0035c0ab04dc7ad0bd00a8db27 flatlaf-1.2.tar.gz
212a0f1f867511722024cc60156fd71872a16f92 flatlaf-1.6.tar.gz
f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz
71259aa46134e6cf2c6473b4fc408051b3336490 gnu-utils-20211030.tar.gz
683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
989234b3799fe8750f3c24825d1f717c24fb0214 idea-icons-20210508.tar.gz
20b53cfc3ffc5b15c1eabc91846915b49b4c0367 isabelle_fonts-20151021.tar.gz
736844204b2ef83974cd9f0a215738b767958c41 isabelle_fonts-20151104.tar.gz
9502c1aea938021f154adadff254c5c55da344bd isabelle_fonts-20151106.tar.gz
f5c63689a394b974ac0d365debda577c6fa31c07 isabelle_fonts-20151107.tar.gz
812101680b75f7fa9ee8e138ea6314fa4824ea2d isabelle_fonts-20151229.tar.gz
2730e1475c7d655655882e75743e0b451725a274 isabelle_fonts-20151231.tar.gz
1f004a6bf20088a7e8f1b3d4153aa85de6fc1091 isabelle_fonts-20160101.tar.gz
379d51ef3b71452dac34ba905def3daa8b590f2e isabelle_fonts-20160102.tar.gz
878536aab1eaf1a52da560c20bb41ab942971fa3 isabelle_fonts-20160227.tar.gz
8ff0eedf0191d808ecc58c6b3149a4697f29ab21 isabelle_fonts-20160812-1.tar.gz
9283e3b0b4c7239f57b18e076ec8bb21021832cb isabelle_fonts-20160812.tar.gz
620cffeb125e198b91a716da116f754d6cc8174b isabelle_fonts-20160830.tar.gz
b70690c85c05d0ca5bc29287abd20142f6ddcfb0 isabelle_fonts-20171222.tar.gz
c17c482e411bbaf992498041a3e1dea80336aaa6 isabelle_fonts-20171230.tar.gz
3affbb306baff37c360319b21cbaa2cc96ebb282 isabelle_fonts-20180113.tar.gz
bee32019e5d7cf096ef2ea1d836c732e9a7628cc isabelle_fonts-20181124.tar.gz
f249bc2c85bd2af9eee509de17187a766b74ab86 isabelle_fonts-20181129.tar.gz
928b5320073d04d93bcc5bc4347b6d01632b9d45 isabelle_fonts-20190210.tar.gz
dfcdf9a757b9dc36cee87f82533b43c58ba84abe isabelle_fonts-20190309.tar.gz
95e3acf038df7fdeeacd8b4769930e6f57bf3692 isabelle_fonts-20190406.tar.gz
dabcf5085d67c99159007007ff0e9bf775e423d1 isabelle_fonts-20190409.tar.gz
76827987c70051719e117138858930d42041f57d isabelle_fonts-20190717.tar.gz
abc8aea3ae471f9313917008ac90e5c1c99e17da isabelle_fonts-20210317.tar.gz
3ff9195aab574fc75ca3b77af0adb33f9b6d7b74 isabelle_fonts-20210318.tar.gz
b166b4bd583b6442a5d75eab06f7adbb66919d6d isabelle_fonts-20210319.tar.gz
9467ad54a9ac10a6e7e8db5458d8d2a5516eba96 isabelle_fonts-20210321.tar.gz
1f7a0b9829ecac6552b21e995ad0f0ac168634f3 isabelle_fonts-20210322.tar.gz
667000ce6dd6ea3c2d11601a41c206060468807d isabelle_fonts-20211004.tar.gz
916adccd2f40c55116b68b92ce1eccb24d4dd9a2 isabelle_setup-20210630.tar.gz
c611e363287fcc9bdd93c33bef85fa4e66cd3f37 isabelle_setup-20210701.tar.gz
a0e7527448ef0f7ce164a38a50dc26e98de3cad6 isabelle_setup-20210709.tar.gz
e413706694b0968245ee15183af2d464814ce0a4 isabelle_setup-20210711.tar.gz
d2c9fd7b73457a460111edd6eb93a133272935fb isabelle_setup-20210715.tar.gz
a5f478ba1088f67c2c86dc2fa7764b6d884e5ae5 isabelle_setup-20210716-1.tar.gz
79fad009cb22aa5e7cb4aed3c810ad5f61790293 isabelle_setup-20210716.tar.gz
692a39f716998e556ec9559c9ca362fc8fc9d5b6 isabelle_setup-20210717-1.tar.gz
7322d6d84d75c486a58ed36630431db4499e3232 isabelle_setup-20210717-2.tar.gz
14f8508bcae9140815bb23e430e26d2cbc504b81 isabelle_setup-20210717.tar.gz
ca801d5c380ea896ee32b309ff19ae5f34538963 isabelle_setup-20210718.tar.gz
ac9739e38e4fbbfce1a71a0987a57b22f83922d3 isabelle_setup-20210724-1.tar.gz
4554679cc8ea31e539655810a14d14216b383d0e isabelle_setup-20210724-2.tar.gz
127a75ae33e97480d352087fcb9b47a632d77169 isabelle_setup-20210724.tar.gz
309909ec6d43ae460338e9af54c1b2a48adcb1ec isabelle_setup-20210726.tar.gz
a14ce46c62c64c3413f3cc9239242e33570d0f3d isabelle_setup-20210922.tar.gz
b22066a9dcde6f813352dcf6404ac184440a22df isabelle_setup-20211109.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
06ac8993b5bebd02c70f1bd18ce13075f01115f3 jdk-11.0.3+7.tar.gz
e7e3cc9b0550c1e5d71197ad8c30f92b622d7183 jdk-11.0.4+11.tar.gz
49007a84a2643a204ce4406770dfd574b97880d9 jdk-11.0.5+10.tar.gz
3c250e98eb82f98afc6744ddc9170d293f0677e1 jdk-11.0.6+10.tar.gz
76cf7a141e15db30bd975089c65c833b58092aa7 jdk-11.0.9+11.tar.gz
71d19df63816e9be1c4c5eb44aea7a44cfadb319 jdk-11.tar.gz
72455a2fdb6cced9cd563f4d5d6134f7a6c34913 jdk-15.0.1+9.tar.gz
e8ae300e61b0b121018456d50010b555bc96ce10 jdk-15.0.2+7.tar.gz
a426a32ad34014953c0f7d4cc6f44199572e1c38 jdk-17+35.tar.gz
85707cfe369d0d32accbe3d96a0730c87e8639b5 jdk-17.0.1+12.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz
13a265e4b706ece26fdfa6fc9f4a3dd1366016d2 jdk-7u21.tar.gz
5080274f8721a18111a7f614793afe6c88726739 jdk-7u25.tar.gz
dd24d63afd6d17b29ec9cb2b2464d4ff2e02de2c jdk-7u40.tar.gz
ec740ee9ffd43551ddf1e5b91641405116af6291 jdk-7u6.tar.gz
71b629b2ce83dbb69967c4785530afce1bec3809 jdk-7u60.tar.gz
e119f4cbfa2a39a53b9578d165d0dc44b59527b7 jdk-7u65.tar.gz
d6d1c42989433839fe64f34eb77298ef6627aed4 jdk-7u67.tar.gz
b66039bc6dc2bdb2992133743005e1e4fc58ae24 jdk-7u72.tar.gz
d980055694ddfae430ee001c7ee877d535e97252 jdk-7u76.tar.gz
baa6de37bb6f7a104ce5fe6506bca3d2572d601a jdk-7u80.tar.gz
7d5b152ac70f720bb9e783fa45ecadcf95069584 jdk-7u9.tar.gz
baf275a68d3f799a841932e4e9a95a1a604058ae jdk-8u102.tar.gz
5442f1015a0657259be0590b04572cd933431df7 jdk-8u11.tar.gz
741de6a4a805a0f9fb917d1845409e99346c2747 jdk-8u112.tar.gz
ae7df8bd0c18eb40237cf54cc28933f4893b9c92 jdk-8u121.tar.gz
51531a3a0c16e180ed95cb7d2bd680c2ec0aa553 jdk-8u131.tar.gz
e45edcf184f608d6f4a7b966d65a5d3289462693 jdk-8u144.tar.gz
264e806b9300a4fb3b6e15ba0e2c664d4ea698c8 jdk-8u152.tar.gz
84b04d877a2ea3a4e2082297b540e14f76722bc5 jdk-8u162.tar.gz
87303a0de3fd595aa3857c8f7cececa036d6ed18 jdk-8u172.tar.gz
9ae0338a5277d8749b4b4c7e65fc627319d98b27 jdk-8u181.tar.gz
cfecb1383faaf027ffbabfcd77a0b6a6521e0969 jdk-8u20.tar.gz
44ffeeae219782d40ce6822b580e608e72fd4c76 jdk-8u31.tar.gz
c95ebf7777beb3e7ef10c0cf3f734cb78f9828e4 jdk-8u5.tar.gz
4132cf52d5025bf330d53b96a5c6466fef432377 jdk-8u51.tar.gz
74df343671deba03be7caa49de217d78b693f817 jdk-8u60.tar.gz
dfb087bd64c3e5da79430e0ba706b9abc559c090 jdk-8u66.tar.gz
2ac389babd15aa5ddd1a424c1509e1c459e6fbb1 jdk-8u72.tar.gz
caa0cf65481b6207f66437576643f41dabae3c83 jdk-8u92.tar.gz
778fd85c827ec49d2d658a832d20e63916186b0d jedit-20210715.tar.gz
beb99f2cb0bd4e595c5c597d3970c46aa21616e4 jedit-20210717.tar.gz
33dd96cd83f2c6a26c035b7a0ee57624655224c5 jedit-20210724.tar.gz
0e4fd4d66388ddc760fa5fbd8d4a9a3b77cf59c7 jedit-20210802.tar.gz
258d527819583d740a3aa52dfef630eed389f8c6 jedit-20211019.tar.gz
f4f3fcbd54488297a5d2fcd23a2595912d5ba80b jedit-20211103.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
9c221fe71af8a063fcffcce21672a97aea0a8d5b jedit_build-20120313.tar.gz
ed72630f307729df08fdedb095f0af8725f81b9c jedit_build-20120327.tar.gz
6425f622625024c1de27f3730d6811f6370a19cd jedit_build-20120414.tar.gz
7b012f725ec1cc102dc259df178d511cc7890bba jedit_build-20120813.tar.gz
8e1d36f5071e3def2cb281f7fefe9f52352cb88f jedit_build-20120903.tar.gz
8fa0c67f59beba369ab836562eed4e56382f672a jedit_build-20121201.tar.gz
06e9be2627ebb95c45a9bcfa025d2eeef086b408 jedit_build-20130104.tar.gz
c85c0829b8170f25aa65ec6852f505ce2a50639b jedit_build-20130628.tar.gz
5de3e399be2507f684b49dfd13da45228214bbe4 jedit_build-20130905.tar.gz
87136818fd5528d97288f5b06bd30c787229eb0d jedit_build-20130910.tar.gz
c63189cbe39eb8104235a0928f579d9523de78a9 jedit_build-20130925.tar.gz
65cc13054be20d3a60474d406797c32a976d7db7 jedit_build-20130926.tar.gz
30ca171f745adf12b65c798c660ac77f9c0f9b4b jedit_build-20131106.tar.gz
054c1300128f8abd0f46a3e92c756ccdb96ff2af jedit_build-20140405.tar.gz
4a963665537ea66c69de4d761846541ebdbf69f2 jedit_build-20140511.tar.gz
a9d637a30f6a87a3583f265da51e63e3619cff52 jedit_build-20140722.tar.gz
f29391c53d85715f8454e1aaa304fbccc352928f jedit_build-20141018.tar.gz
d7206d4c9d14d3f4c8115422b7391ffbcc6e80b4 jedit_build-20141026.tar.gz
f15d36abc1780875a46b6dbd4568e43b776d5db6 jedit_build-20141104.tar.gz
14ce124c897abfa23713928dc034d6ef0e1c5031 jedit_build-20150228.tar.gz
b5f7115384c167559211768eb5fe98138864473b jedit_build-20151023.tar.gz
8ba7b6791be788f316427cdcd805daeaa6935190 jedit_build-20151124.tar.gz
c70c5a6c565d435a09a8639f8afd3de360708e1c jedit_build-20160330.tar.gz
d4e1496c257659cf15458d718f4663cdd95a404e jedit_build-20161024.tar.gz
d806c1c26b571b5b4ef05ea11e8b9cf936518e06 jedit_build-20170319.tar.gz
7bcb202e13358dd750e964b2f747664428b5d8b3 jedit_build-20180417.tar.gz
23c8a05687d05a6937f7d600ac3aa19e3ce59c9c jedit_build-20180504.tar.gz
9c64ee0705e5284b507ca527196081979d689519 jedit_build-20181025.tar.gz
cfa65bf8720b9b798ffa0986bafbc8437f44f758 jedit_build-20181026.tar.gz
847492b75b38468268f9ea424d27d53f2d95cef4 jedit_build-20181203.tar.gz
536a38ed527115b4bf2545a2137ec57b6ffad718 jedit_build-20190120.tar.gz
58b9f03e5ec0b85f8123c31f5d8092dae5803773 jedit_build-20190130.tar.gz
ec0aded5f2655e2de8bc4427106729e797584f2f jedit_build-20190224.tar.gz
1e53598a02ec8d8736b15f480cbe2c84767a7827 jedit_build-20190508.tar.gz
b9c6f49d3f6ebe2e85a50595ce7412d01a4314ac jedit_build-20190717.tar.gz
1c753beb93e92e95e99e8ead23a68346bd1af44a jedit_build-20200610.tar.gz
533b1ee6459f59bcbe4f09e214ad2cb990fb6952 jedit_build-20200908.tar.gz
f9966b5ed26740bb5b8bddbfe947fcefaea43d4d jedit_build-20201223.tar.gz
0bdbd36eda5992396e9c6b66aa24259d4dd7559c jedit_build-20210201.tar.gz
a0744f1948abdde4bfb51dd4769b619e7444baf1 jedit_build-20210510-1.tar.gz
837d6c8f72ecb21ad59a2544c69aadc9f05684c6 jedit_build-20210510.tar.gz
7bdae3d24b10261f6cb277446cf9ecab6062bd6f jedit_build-20210708.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz
d84b7d8ef273afec55284327fca7dd20f5ecb77a jfreechart-1.5.1.tar.gz
6fa0c221ef55919b684449f0111a8112358e94ff jfreechart-1.5.3.tar.gz
c8a19a36adf6cefa779d85f22ded2f4654e68ea5 jortho-1.0-1.tar.gz
2155e0bdbd29cd3d2905454de2e7203b9661d239 jortho-1.0-2.tar.gz
ffe179867cf5ffaabbb6bb096db9bdc0d7110065 jortho-1.0.tar.gz
6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
afb04f4048a87bb888fe7b05b0139cb060c7925b kodkodi-1.5.2-1.tar.gz
5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz
0634a946b216f7f07f1a0f7e28cf345daa28828f kodkodi-1.5.3.tar.gz
52e95b3493d71902f9df89d0bb59d0046a5f0c63 kodkodi-1.5.4-1.tar.gz
267189c637de26cf304d699cfa95389da002b250 kodkodi-1.5.4.tar.gz
3ecdade953bb455ed2907952be287d7e5cf6533b kodkodi-1.5.5.tar.gz
8aa939f5127290eb9a99952d375be9ffbf90c43b kodkodi-1.5.6-1.tar.gz
6b12bf3f40b16fae8ff22aa39171fa018d107cb3 kodkodi-1.5.6.tar.gz
c8b2e632f3ab959a4e037833a45e6360c8b72a99 kodkodi-1.5.7.tar.gz
377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz
759848095e2ad506083d92b5646947e3c32f27a0 linux_app-20191223.tar.gz
1a449ce69ac874e21804595d16aaaf5a0d0d0c10 linux_app-20200110.tar.gz
0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz
ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz
400af57ec5cd51f96928d9de00d077524a6fe316 macos_app-20181205.tar.gz
3bc42b8e22f0be5ec5614f1914066164c83498f8 macos_app-20181208.tar.gz
5fb1a2d21b220d0e588790c0203ac87c10ed0870 minisat-2.2.1-1.tar.gz
ae76bfaade3bf72ff6b2d3aafcd52fa45609fcd1 minisat-2.2.1.tar.gz
eda10c62da927a842c0a8881f726eac85e1cb4f7 naproche-20210122.tar.gz
edcb517b7578db4eec1b6573b624f291776e11f6 naproche-20210124.tar.gz
d858eb0ede6aea6b8cc40de63bd3a17f8f9f5300 naproche-20210129.tar.gz
810ee0f35adada9bf970c33fd80b986ab2255bf3 naproche-20210201.tar.gz
4a4e56fd03b7ba4edd38046f853873a90cf55d1a naproche-4ad61140062f.tar.gz
77252e0b40f89825b9b5935f9f0c4cd5d4e7012a naproche-6d0d76ce2f2a.tar.gz
9c02ecf93863c3289002c5e5ac45a83e2505984c naproche-755224402e36.tar.gz
e1b34e8f54e7e5844873612635444fed434718a1 naproche-7d0947a91dd5.tar.gz
26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz
e573f2cbb57eb7b813ed5908753cfe2cb41033ca nunchaku-0.5.tar.gz
3d7b7690dfd09e25ad56e64b519f61f06e3ab706 old_vampire-4.2.2.tar.gz
fe57793aca175336deea4f5e9c0d949a197850ac opam-1.2.2.tar.gz
eb499a18e7040ca0fe1ca824c9dcb2087c47c9ba opam-2.0.3-1.tar.gz
002f74c9e65e650de2638bf54d7b012b8de76c28 opam-2.0.3.tar.gz
ddb3b438430d9565adbf5e3d913bd52af8337511 opam-2.0.6.tar.gz
fc66802c169f44511d3be30435eb89a11e635742 opam-2.0.7.tar.gz
108e947d17e9aa6170872614492d8f647802f483 opam-2.1.0.tar.gz
1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz
a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56 polyml-5.5.0-1.tar.gz
7d604a99355efbfc1459d80db3279ffa7ade3e39 polyml-5.5.0-2.tar.gz
b3d776e6744f0cd2773d467bc2cfe1de3d1ca2fd polyml-5.5.0-3.tar.gz
1812e9fa6d163f63edb93e37d1217640a166cf3e polyml-5.5.0.tar.gz
36f5b8224f484721749682a3655c796a55a2718d polyml-5.5.1-1.tar.gz
36f78f27291a9ceb13bf1120b62a45625afd44a6 polyml-5.5.1.tar.gz
a588640dbf5da9ae15455b02ef709764a48637dc polyml-5.5.2-1.tar.gz
4b690390946f7bfb777b89eb16d6f08987cca12f polyml-5.5.2-2.tar.gz
5b31ad8556e41dfd6d5e85f407818be399aa3d2a polyml-5.5.2-3.tar.gz
532f6e8814752aeb406c62fabcfd2cc05f8a7ca8 polyml-5.5.2.tar.gz
1c53f699d35c0db6c7cf4ea51f2310adbd1d0dc5 polyml-5.5.3-20150820.tar.gz
b4b624fb5f34d1dc814fb4fb469fafd7d7ea018a polyml-5.5.3-20150908.tar.gz
b668e1f43a41608a8eb365c5e19db6c54c72748a polyml-5.5.3-20150911.tar.gz
1f5cd9b1390dab13861f90dfc06d4180cc107587 polyml-5.5.3-20150916.tar.gz
f78896e588e8ebb4da57bf0c95210b0f0fa9e551 polyml-5.6-1.tar.gz
21fa0592b7dfd23269063f42604438165630c0f0 polyml-5.6-2.tar.gz
03ba81e595fa6d6df069532d67ad3195c37d9046 polyml-5.6-20151123.tar.gz
822f489c18e38ce5ef979ec21dccce4473e09be6 polyml-5.6-20151206.tar.gz
bd6a448f0e0d5787747f4f30ca661f9c1868e4a7 polyml-5.6-20151223.tar.gz
5b70c12c95a90d858f90c1945011289944ea8e17 polyml-5.6-20160118.tar.gz
5b19dc93082803b82aa553a5cfb3e914606c0ffd polyml-5.6.tar.gz
80b923fca3533bf291ff9da991f2262a98b68cc4 polyml-5.7-20170217.tar.gz
381a70cecf0fdee47f6842e2bdb5107ed52adab6 polyml-5.7.1-1.tar.gz
39dac33b569ac66f76126b8f4edc6d9227bd8a63 polyml-5.7.1-2.tar.gz
0b896ccc35bd3f2541cd55e6f0ed14637ed9fc68 polyml-5.7.1-4.tar.gz
262450ac9966abebae2e1d4f9ae703cfe0f5d8d9 polyml-5.7.1-5.tar.gz
1aeb57877d694db7fe4d4395287cddf3bc77710b polyml-5.7.1-6.tar.gz
e3e7e20b1e0e5d5d68df4cd4caa1e1a7410d46b6 polyml-5.7.1-7.tar.gz
1430533c09b17f8be73798a47a5f409d43a04cf4 polyml-5.7.1-8.tar.gz
171b5783b88522a35e4822b19ef8ba838c04f494 polyml-5.7.1.tar.gz
5fbcab1da2b5eb97f24da2590ece189d55b3a105 polyml-5.7.tar.gz
51e024225b460900da5279f0b91b217085f98cf9 polyml-5.8-20190220.tar.gz
20a83fa58d497b533150defe39bcd4540529b25f polyml-5.8-20190306.tar.gz
9f0e9cd10df4c3383b063eb076e8b698ca50c3d0 polyml-5.8.1-20191101.tar.gz
f46deb909d645ac8c140968e4d32b5763beb9add polyml-5.8.1-20191113.tar.gz
36a40a981b57daae0463d14940a8edf6fa1af179 polyml-5.8.1-20191114.tar.gz
525b05536b08c11a1eae943fe6818a8622326084 polyml-5.8.1-20191124.tar.gz
9043828803483ca14df64488dff014ad050a6d34 polyml-5.8.1-20200228.tar.gz
1186607e2c43b77db86731f12fbedb531ca50a21 polyml-5.8.1-20200708.tar.gz
22ae16bf7850e73b903d2ca8eb506da05b441cf3 polyml-5.8.1.tar.gz
cb8e85387315f62dcfc6b21ec378186e58068f76 polyml-5.8.2.tar.gz
d1fd6eced69dc1df7226432fcb824568e0994ff2 polyml-5.8.tar.gz
fb40145228f84513a9b083b54678a7d61b9c34c4 polyml-5.9-5d4caa8f7148.tar.gz
5f00a47b8f5180b33e68fcc6c343b061957a0a98 polyml-5.9-960de0cd0795.tar.gz
+7056b285af67902b32f5049349a064f073f05860 polyml-5.9-cc80e2b43c38.tar.gz
49f1adfacdd6d29fa9f72035d94a31eaac411a97 polyml-test-0a6ebca445fc.tar.gz
2a8c4421e0a03c0d6ad556b3c36c34eb11568adb polyml-test-1236652ebd55.tar.gz
8e83fb5088cf265902b8da753a8eac5fe3f6a14b polyml-test-159dc81efc3b.tar.gz
a0064c157a59e2706e18512a49a6dca914fa17fc polyml-test-1b2dcf8f5202.tar.gz
4e6543dbbb2b2aa402fd61428e1c045c48f18b47 polyml-test-79534495ee94.tar.gz
853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz
85bfda83d138e936fdafd68ed3627b1058e5c2c3 polyml-test-7e49fce62e3d.tar.gz
c629cd499a724bbe37b962f727e4ff340c50299d polyml-test-8529546198aa.tar.gz
7df4857d73dbc9edda25a6ad329e47639e70fadf polyml-test-8fda4fd22441.tar.gz
2b7c02b67feb2f44dda6938a7244f4257e7c580c polyml-test-905dae2ebfda.tar.gz
3dfdc58e5d9b28f038a725e05c9c2f2ce0bb2632 polyml-test-a3cfdf648da-1.tar.gz
e2f075b0cc709f4f7f6492b725362f9010b2c6d1 polyml-test-a3cfdf648da-2.tar.gz
33568f69ce813b7405386ddbefa14ad0342bb8f0 polyml-test-a3cfdf648da.tar.gz
4bedaac4f1fb9a9199aa63695735063c47059003 polyml-test-a444f281ccec.tar.gz
f3031692edcc5d8028a42861e4e40779f0f9d3e1 polyml-test-b68438d33c69.tar.gz
cb2318cff6ea9293cd16a4435a4fe28ad9dbe0b8 polyml-test-cf46747fee61.tar.gz
67ffed2f98864721bdb1e87f0ef250e4c69e6160 polyml-test-d68c6736402e.tar.gz
b4ceeaac47f3baae41c2491a8368b03217946166 polyml-test-e7a662f8f9c4.tar.gz
609c7d09d3ed01156ff91261e801e2403ff93729 polyml-test-e8d82343b692.tar.gz
b6d87466e9b44e8ef4a2fac74c96b139080a506a polyml-test-f54aa41240d0.tar.gz
d365f3fc11c2427cafc62b3c79951880a1476ebb polyml-test-f86ae3dc1686.tar.gz
a619177143fea42a464f49bb864665407c07a16c polyml-test-fb4f42af00fa.tar.gz
53123dc011b2d4b4e8fe307f3c9fa355718ad01a postgresql-42.1.1.tar.gz
3a5d31377ec07a5069957f5477a4848cfc89a594 postgresql-42.1.4.tar.gz
7d6ef4320d5163ceb052eb83c1cb3968f099a422 postgresql-42.2.18.tar.gz
e7cd5c7955e9eb5ce8cd07feb97230b23d2eec40 postgresql-42.2.2.tar.gz
1aaa38429dc9aa7b1095394d9a7ba3465f8d6e04 postgresql-42.2.24.tar.gz
231b33c9c3c27d47e3ba01b399103d70509e0731 postgresql-42.2.5.tar.gz
6335fbc0658e447b5b9bc48c9ad36e33a05bb72b postgresql-42.2.9.tar.gz
f132329ca1045858ef456cc08b197c9eeea6881b postgresql-9.4.1212.tar.gz
0885e1f1d8feaca78d2f204b6487e6eec6dfab4b scala-2.10.0.tar.gz
f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc scala-2.10.1.tar.gz
207e4916336335386589c918c5e3f3dcc14698f2 scala-2.10.2.tar.gz
21c8ee274ffa471ab54d4196ecd827bf3d43e591 scala-2.10.3.tar.gz
d4688ddaf83037ca43b5bf271325fc53ae70e3aa scala-2.10.4.tar.gz
44d12297a78988ffd34363535e6a8e0d94c1d8b5 scala-2.11.0.tar.gz
14f20de82b25215a5e055631fb147356400625e6 scala-2.11.1.tar.gz
4fe9590d08e55760b86755d3fab750e90ac6c380 scala-2.11.2.tar.gz
27a296495b2167148de06314ed9a942f2dbe23fe scala-2.11.4.tar.gz
4b24326541161ce65424293ca9da3e7c2c6ab452 scala-2.11.5.tar.gz
e7cf20e3b27c894c6127c7a37042c1667f57385e scala-2.11.6.tar.gz
4810c1b00719115df235be1c5991aa6ea7186134 scala-2.11.7.tar.gz
3eca4b80710996fff87ed1340dcea2c5f6ebf4f7 scala-2.11.8.tar.gz
0004e53f885fb165b50c95686dec40d99ab0bdbd scala-2.12.0.tar.gz
059cbdc58d36e3ac1fffcccd9139ecd34f271882 scala-2.12.10.tar.gz
82056106aa6fd37c159ea76d16096c20a749cccd scala-2.12.11.tar.gz
fe7ff585acffaad7f0dd4a1d079134d15c26ed0d scala-2.12.12.tar.gz
74a8c3dab3a25a87357996ab3e95d825dc820fd0 scala-2.12.2.tar.gz
d66796a68ec3254b46b17b1f8ee5bcc56a93aacf scala-2.12.3.tar.gz
1636556167dff2c191baf502c23f12e09181ef78 scala-2.12.4.tar.gz
8171f494bba54fb0d01c887f889ab8fde7171c2a scala-2.12.5.tar.gz
54c1b06fa2c5f6c2ab3d391ef342c0532cd7f392 scala-2.12.6.tar.gz
02358f00acc138371324b6248fdb62eed791c6bd scala-2.12.7.tar.gz
201c05ae9cc382ee6c08af49430e426f6bbe0d5a scala-2.12.8.tar.gz
a0622fe75c3482ba7dc3ce74d58583b648a1ff0d scala-2.13.4-1.tar.gz
ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz
f51981baf34c020ad103b262f81796c37abcaa4a scala-2.13.5.tar.gz
0a7cab09dec357dab7819273f2542ff1c3ea0968 scala-2.13.6.tar.gz
1f8532dba290c6b2ef364632f3f92e71da93baba scala-2.13.7.tar.gz
b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz
cbd491c0feba1d21019d05564e76dd04f592ccb4 spass-3.8ds-1.tar.gz
edaa1268d82203067657aabcf0371ce7d4b579b9 spass-3.8ds-2.tar.gz
43b5afbcad575ab6817d2289756ca22fd2ef43a9 spass-3.8ds.tar.gz
b016a785f1f78855c00d351ff598355c3b87450f sqlite-jdbc-3.18.0-1.tar.gz
b85b5bc071a59ef2a8326ceb1617d5a9a5be41cf sqlite-jdbc-3.18.0.tar.gz
e56117a67ab01fb24c7fc054ede3160cefdac5f8 sqlite-jdbc-3.20.0.tar.gz
27aeac6a91353d69f0438837798ac4ae6f9ff8c5 sqlite-jdbc-3.23.1.tar.gz
4d17611857fa3a93944c1f159c0fd2a161967aaf sqlite-jdbc-3.27.2.1.tar.gz
806be457eb79408fcc5a72aeca3f64b2d89a6b63 sqlite-jdbc-3.30.1.tar.gz
cba2b194114216b226d75d49a70d1bd12b141ac8 sqlite-jdbc-3.32.3.2.tar.gz
29306acd6ce9f4c87032b2c271c6df035fe7d4d3 sqlite-jdbc-3.34.0.tar.gz
8a2ca4d02cfedbfe4dad4490f1ed3ddba33a009a sqlite-jdbc-3.36.0.3.tar.gz
8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz
2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz
a2335d28b5b95d8d26500a53f1a9303fc5beaf36 ssh-java-20190323.tar.gz
fdc415284e031ee3eb2f65828cbc6945736fe995 stack-1.9.1.tar.gz
6e19948ff4a821e2052fc9b3ddd9ae343f4fcdbb stack-1.9.3.tar.gz
f969443705aa8619e93af5b34ea98d15cd7efaf1 stack-2.1.3.tar.gz
ebd0221d038966aa8bde075f1b0189ff867b02ca stack-2.5.1.tar.gz
fa2d882ec45cbc8c7d2f3838b705a8316696dc66 stack-2.7.3.tar.gz
1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd sumatra_pdf-2.1.1.tar.gz
601e08d048d8e50b0729429c8928b667d9b6bde9 sumatra_pdf-2.3.2.tar.gz
14d46c2eb1a34821703da59d543433f581e91df3 sumatra_pdf-2.4.tar.gz
44d67b6742919ce59a42368fc60e2afa210a3e42 sumatra_pdf-2.5.2.tar.gz
89719a13bc92810730a430973684629426ed1b2a sumatra_pdf-3.0.tar.gz
f5afcc82f8e734665d38867e99475d3ad0d5ed15 sumatra_pdf-3.1.1.tar.gz
a45eca5c1277f42f87bb8dc12a3074ccf5488221 sumatra_pdf-3.1.2-1.tar.gz
3b3239b2e6f8062b90d819f3703e30a50f4fa1e7 sumatra_pdf-3.1.2-2.tar.gz
8486387f61557147ec06b1f637117c017c8f0528 sumatra_pdf-3.1.2.tar.gz
e8648878f908e93d64a393231ab21fdac976a9c2 sumatra_pdf-3.3.3.tar.gz
869ea6d8ea35c8ba68d7fcb028f16b2b7064c5fd vampire-1.0.tar.gz
399f687b56575b93e730f68c91c989cb48aa34d8 vampire-4.2.2.tar.gz
0402978ca952f08eea73e483b694928ac402a304 vampire-4.5.1-1.tar.gz
26d9d171e169c6420a08aa99eda03ef5abb9c545 vampire-4.5.1.tar.gz
4571c042efd6fc3097e105a528826959acd888a3 vampire-4.6.tar.gz
98c5c79fef7256db9f64c8feea2edef0a789ce46 verit-2016post.tar.gz
52ba18a6c96b53c5ae9b179d5a805a0c08f1da6d verit-2020.10-rmx-1.tar.gz
b6706e74e20e14038e9b38f0acdb5639a134246a verit-2020.10-rmx.tar.gz
d33e1e36139e86b9e9a48d8b46a6f90d7863a51c verit-2021.06-rmx-1.tar.gz
c11d1120fcefaec79f099fe2be05b03cd2aed8b9 verit-2021.06-rmx.tar.gz
b576fd5d89767c1067541d4839fb749c6a68d22c verit-2021.06.1-rmx.tar.gz
81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz
fe15e1079cf5ad86f3cbab4553722a0d20002d11 windows_app-20130905.tar.gz
e6a43b7b3b21295853bd2a63b27ea20bd6102f5f windows_app-20130906.tar.gz
8fe004aead867d4c82425afac481142bd3f01fb0 windows_app-20130908.tar.gz
d273abdc7387462f77a127fa43095eed78332b5c windows_app-20130909.tar.gz
c368908584e2bca38b3bcb20431d0c69399fc2f0 windows_app-20131130.tar.gz
c3f5285481a95fde3c1961595b4dd0311ee7ac1f windows_app-20131201.tar.gz
14807afcf69e50d49663d5b48f4b103f30ae842b windows_app-20150821.tar.gz
ed106181510e825bf959025d8e0a2fc3f78e7a3f windows_app-20180417.tar.gz
e809e4ab0d33cb413a7c47dd947e7dbdfcca1c24 windows_app-20181002.tar.gz
9e96ba128a0617a9020a178781df49d48c997e19 windows_app-20181006.tar.gz
1c36a840320dfa9bac8af25fc289a4df5ea3eccb xz-java-1.2-1.tar.gz
2ae13aa17d0dc95ce254a52f1dba10929763a10d xz-java-1.2.tar.gz
c22196148fcace5443a933238216cff5112948df xz-java-1.5.tar.gz
4368ee09154dff42666a8c87e072261745619e51 xz-java-1.6.tar.gz
63f5fa09e92a895cb9aea27d7142abc86c487d25 xz-java-1.8.tar.gz
a06875bdadd653627a68d2083c5178c1264d8fc6 xz-java-1.9.tar.gz
4530a1aa6f4498ee3d78d6000fa71a3f63bd077f yices-1.0.28.tar.gz
3a8f77822278fe9250890e357248bc678d8fac95 z3-3.2-1.tar.gz
12ae71acde43bd7bed1e005c43034b208c0cba4c z3-3.2.tar.gz
d94a716502c8503d63952bcb4d4176fac8b28704 z3-4.0.tar.gz
86e721296c400ada440e4a9ce11b9e845eec9e25 z3-4.3.0.tar.gz
a8917c31b31c182edeec0aaa48870844960c8a61 z3-4.3.2pre-1.tar.gz
06b30757ff23aefbc30479785c212685ffd39f4d z3-4.3.2pre.tar.gz
93e7e4bddc6afcf87fe2b6656cfcb1b1acd0a4f8 z3-4.4.0pre-1.tar.gz
b1bc411c2083fc01577070b56b94514676f53854 z3-4.4.0pre-2.tar.gz
4c366ab255d2e9343fb635d44d4d55ddd24c76d0 z3-4.4.0pre-3.tar.gz
517ba7b94c1985416c5b411c8ae84456367eb231 z3-4.4.0pre.tar.gz
aa20745f0b03e606b1a4149598e0c7572b63c657 z3-4.8.3.tar.gz
9dfeb39c87393af7b6a34118507637aa53aca05e zipperposition-2.0-1.tar.gz
b884c60653002a7811e3b652ae0515e825d98667 zipperposition-2.0.tar.gz
b129ec4f8a4474953ec107536298ee08a01fbebc zipperposition-2.1-1.tar.gz
5f53a77efb5cbe9d0c95d74a1588cc923bd711a7 zipperposition-2.1.tar.gz
diff --git a/Admin/components/main b/Admin/components/main
--- a/Admin/components/main
+++ b/Admin/components/main
@@ -1,32 +1,32 @@
#main components for repository clones or release bundles
gnu-utils-20211030
bash_process-1.2.4-2
bib2xhtml-20190409
csdp-6.1.1
cvc4-1.8
e-2.6-1
flatlaf-1.6
idea-icons-20210508
isabelle_fonts-20211004
isabelle_setup-20211109
jdk-17.0.1+12
jedit-20211103
jfreechart-1.5.3
jortho-1.0-2
kodkodi-1.5.7
minisat-2.2.1-1
nunchaku-0.5
opam-2.0.7
-polyml-5.9-5d4caa8f7148
+polyml-5.9-cc80e2b43c38
postgresql-42.2.24
scala-2.13.5
smbc-0.4.1
spass-3.8ds-2
sqlite-jdbc-3.36.0.3
ssh-java-20190323
stack-2.7.3
vampire-4.6
verit-2021.06.1-rmx
xz-java-1.9
z3-4.4.0pre-3
zipperposition-2.1-1
diff --git a/Admin/polyml/README b/Admin/polyml/README
--- a/Admin/polyml/README
+++ b/Admin/polyml/README
@@ -1,58 +1,58 @@
Poly/ML for Isabelle
====================
This compilation of Poly/ML (https://www.polyml.org) is based on the
source distribution from
-https://github.com/polyml/polyml/commit/5d4caa8f7148 (shortly before
+https://github.com/polyml/polyml/commit/cc80e2b43c38 (shortly before
official version 5.9).
The Isabelle repository provides an administrative tool "isabelle
build_polyml", which can be used in the polyml component directory as
follows.
* Linux:
$ isabelle build_polyml -m32 -s sha1 src
$ isabelle build_polyml -m64 -s sha1 src
* macOS:
$ isabelle build_polyml -m32 -s sha1 src
$ isabelle build_polyml -m64 -s sha1 src
* Windows (Cygwin shell)
$ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src
$ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src
Building libgmp on macOS
========================
The build_polyml invocations above implicitly use the GNU Multiple Precision
Arithmetic Library (libgmp), but that is not available on macOS by default.
Appending "--without-gmp" to the command-line omits this library. Building
libgmp properly from sources works as follows (library headers and binaries
will be placed in /usr/local).
* Download:
$ curl https://gmplib.org/download/gmp/gmp-6.2.1.tar.bz2 | tar xjf -
$ cd gmp-6.2.1
* build:
$ make distclean
#Intel
$ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
#ARM
$ ./configure --enable-cxx --build=aarch64-apple-darwin"$(uname -r)"
$ make && make check
$ sudo make install
Makarius
- 07-Nov-2021
+ 12-Nov-2021
diff --git a/src/Pure/General/name_space.ML b/src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML
+++ b/src/Pure/General/name_space.ML
@@ -1,649 +1,649 @@
(* Title: Pure/General/name_space.ML
Author: Markus Wenzel, TU Muenchen
Generic name spaces with declared and hidden entries; no support for
absolute addressing.
*)
type xstring = string; (*external names*)
signature NAME_SPACE =
sig
type entry =
{concealed: bool,
group: serial option,
theory_long_name: string,
pos: Position.T,
serial: serial}
type T
val empty: string -> T
val kind_of: T -> string
val markup: T -> string -> Markup.T
val markup_def: T -> string -> Markup.T
val get_names: T -> string list
val the_entry: T -> string -> entry
val the_entry_theory_name: T -> string -> string
val entry_ord: T -> string ord
val is_concealed: T -> string -> bool
val intern: T -> xstring -> string
val names_long: bool Config.T
val names_short: bool Config.T
val names_unique: bool Config.T
val extern: Proof.context -> T -> string -> xstring
val extern_ord: Proof.context -> T -> string ord
val extern_shortest: Proof.context -> T -> string -> xstring
val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
val pretty: Proof.context -> T -> string -> Pretty.T
val completion: Context.generic -> T -> (string -> bool) -> xstring * Position.T -> Completion.T
val merge: T * T -> T
type naming
val get_scopes: naming -> Binding.scope list
val get_scope: naming -> Binding.scope option
val new_scope: naming -> Binding.scope * naming
val restricted: bool -> Position.T -> naming -> naming
val private_scope: Binding.scope -> naming -> naming
val private: Position.T -> naming -> naming
val qualified_scope: Binding.scope -> naming -> naming
val qualified: Position.T -> naming -> naming
val concealed: naming -> naming
val get_group: naming -> serial option
val set_group: serial option -> naming -> naming
val set_theory_long_name: string -> naming -> naming
val new_group: naming -> naming
val reset_group: naming -> naming
val add_path: string -> naming -> naming
val root_path: naming -> naming
val parent_path: naming -> naming
val mandatory_path: string -> naming -> naming
val qualified_path: bool -> binding -> naming -> naming
val global_naming: naming
val local_naming: naming
val transform_naming: naming -> naming -> naming
val transform_binding: naming -> binding -> binding
val full_name: naming -> binding -> string
val base_name: binding -> string
val hide: bool -> string -> T -> T
val alias: naming -> binding -> string -> T -> T
val naming_of: Context.generic -> naming
val map_naming: (naming -> naming) -> Context.generic -> Context.generic
val declared: T -> string -> bool
val declare: Context.generic -> bool -> binding -> T -> string * T
type 'a table
val change_base: bool -> 'a table -> 'a table
val change_ignore: 'a table -> 'a table
val space_of_table: 'a table -> T
val check_reports: Context.generic -> 'a table ->
xstring * Position.T list -> (string * Position.report list) * 'a
val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
val defined: 'a table -> string -> bool
val lookup: 'a table -> string -> 'a option
val lookup_key: 'a table -> string -> (string * 'a) option
val get: 'a table -> string -> 'a
val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
val alias_table: naming -> binding -> string -> 'a table -> 'a table
val hide_table: bool -> string -> 'a table -> 'a table
val del_table: string -> 'a table -> 'a table
val map_table_entry: string -> ('a -> 'a) -> 'a table -> 'a table
val fold_table: (string * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
val dest_table: 'a table -> (string * 'a) list
val empty_table: string -> 'a table
val merge_tables: 'a table * 'a table -> 'a table
val join_tables: (string -> 'a * 'a -> 'a) (*exception Change_Table.SAME*) ->
'a table * 'a table -> 'a table
val extern_entries: bool -> Proof.context -> T -> (string * 'a) list ->
((string * xstring) * 'a) list
val markup_entries: bool -> Proof.context -> T -> (string * 'a) list ->
((Markup.T * xstring) * 'a) list
val extern_table: bool -> Proof.context -> 'a table -> ((string * xstring) * 'a) list
val markup_table: bool -> Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
end;
structure Name_Space: NAME_SPACE =
struct
(** name spaces **)
(* datatype entry *)
type entry =
{concealed: bool,
group: serial option,
theory_long_name: string,
pos: Position.T,
serial: serial};
fun entry_markup def kind (name, {pos, theory_long_name, serial, ...}: entry) =
Position.make_entity_markup def serial kind (name, pos)
- ||> not (#def def) ? cons (Markup.def_theoryN, theory_long_name);
+ ||> not (#def def orelse theory_long_name = "") ? cons (Markup.def_theoryN, theory_long_name);
fun print_entry_ref kind (name, entry) =
quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name);
fun err_dup kind entry1 entry2 pos =
error ("Duplicate " ^ plain_words kind ^ " declaration " ^
print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos);
(* internal names *)
type internals = (string list * string list) Change_Table.T; (*xname -> visible, hidden*)
fun map_internals f xname : internals -> internals =
Change_Table.map_default (xname, ([], [])) f;
val del_name = map_internals o apfst o remove (op =);
fun del_name_extra name =
map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
val add_name = map_internals o apfst o update (op =);
fun hide_name name = map_internals (apsnd (update (op =) name)) name;
(* external accesses *)
type accesses = (xstring list * xstring list); (*input / output fragments*)
type entries = (accesses * entry) Change_Table.T; (*name -> accesses, entry*)
(* datatype T *)
datatype T = Name_Space of {kind: string, internals: internals, entries: entries};
fun make_name_space (kind, internals, entries) =
Name_Space {kind = kind, internals = internals, entries = entries};
fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
make_name_space (f (kind, internals, entries));
fun change_base_space begin = map_name_space (fn (kind, internals, entries) =>
(kind, Change_Table.change_base begin internals, Change_Table.change_base begin entries));
val change_ignore_space = map_name_space (fn (kind, internals, entries) =>
(kind, Change_Table.change_ignore internals, Change_Table.change_ignore entries));
fun empty kind = make_name_space (kind, Change_Table.empty, Change_Table.empty);
fun kind_of (Name_Space {kind, ...}) = kind;
fun gen_markup def (Name_Space {kind, entries, ...}) name =
(case Change_Table.lookup entries name of
NONE => Markup.intensify
| SOME (_, entry) => entry_markup def kind (name, entry));
val markup = gen_markup {def = false};
val markup_def = gen_markup {def = true};
fun undefined (space as Name_Space {kind, entries, ...}) bad =
let
val (prfx, sfx) =
(case Long_Name.dest_hidden bad of
SOME name =>
if Change_Table.defined entries name
then ("Inaccessible", Markup.markup (markup space name) (quote name))
else ("Undefined", quote name)
| NONE => ("Undefined", quote bad));
in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end;
fun get_names (Name_Space {entries, ...}) =
Change_Table.fold (cons o #1) entries [];
fun the_entry (space as Name_Space {entries, ...}) name =
(case Change_Table.lookup entries name of
NONE => error (undefined space name)
| SOME (_, entry) => entry);
fun the_entry_theory_name space name =
Long_Name.base_name (#theory_long_name (the_entry space name));
fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
fun is_concealed space name =
#concealed (the_entry space name) handle ERROR _ => false;
(* intern *)
fun intern' (Name_Space {internals, ...}) xname =
(case the_default ([], []) (Change_Table.lookup internals xname) of
([name], _) => (name, true)
| (name :: _, _) => (name, false)
| ([], []) => (Long_Name.hidden xname, true)
| ([], name' :: _) => (Long_Name.hidden name', true));
val intern = #1 oo intern';
fun get_accesses (Name_Space {entries, ...}) name =
(case Change_Table.lookup entries name of
NONE => ([], [])
| SOME (accesses, _) => accesses);
fun is_valid_access (Name_Space {internals, ...}) name xname =
(case Change_Table.lookup internals xname of
SOME (name' :: _, _) => name = name'
| _ => false);
(* extern *)
val names_long = Config.declare_option_bool ("names_long", \<^here>);
val names_short = Config.declare_option_bool ("names_short", \<^here>);
val names_unique = Config.declare_option_bool ("names_unique", \<^here>);
fun extern ctxt space name =
let
val names_long = Config.get ctxt names_long;
val names_short = Config.get ctxt names_short;
val names_unique = Config.get ctxt names_unique;
fun valid require_unique xname =
let val (name', is_unique) = intern' space xname
in name = name' andalso (not require_unique orelse is_unique) end;
fun ext [] = if valid false name then name else Long_Name.hidden name
| ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
in
if names_long then name
else if names_short then Long_Name.base_name name
else ext (#2 (get_accesses space name))
end;
fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space);
fun extern_shortest ctxt =
extern
(ctxt
|> Config.put names_long false
|> Config.put names_short false
|> Config.put names_unique false);
fun markup_extern ctxt space name = (markup space name, extern ctxt space name);
fun pretty ctxt space name = Pretty.mark_str (markup_extern ctxt space name);
(* completion *)
fun completion context space pred (xname, pos) =
Completion.make (xname, pos) (fn completed =>
let
fun result_ord ((pri1, (xname1, (_, name1))), (pri2, (xname2, (_, name2)))) =
(case int_ord (pri2, pri1) of
EQUAL =>
(case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of
EQUAL =>
(case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of
EQUAL => string_ord (xname1, xname2)
| ord => ord)
| ord => ord)
| ord => ord);
val Name_Space {kind, internals, ...} = space;
val ext = extern_shortest (Context.proof_of context) space;
val full = Name.clean xname = "";
fun complete xname' name =
if (completed xname' orelse exists completed (Long_Name.explode xname')) andalso
not (is_concealed space name) andalso pred name
then
let
val xname'' = ext name;
val pri = (if xname' = xname'' then 1 else 0) + (if completed xname' then 1 else 0);
in
if xname' <> xname'' andalso full then I
else cons (pri, (xname', (kind, name)))
end
else I;
in
Change_Table.fold (fn (xname', (name :: _, _)) => complete xname' name | _ => I) internals []
|> sort_distinct result_ord
|> map #2
end);
(* merge *)
fun merge
(Name_Space {kind = kind1, internals = internals1, entries = entries1},
Name_Space {kind = kind2, internals = internals2, entries = entries2}) =
let
val kind' =
if kind1 = kind2 then kind1
else error ("Attempt to merge different kinds of name spaces " ^
quote kind1 ^ " vs. " ^ quote kind2);
val internals' = (internals1, internals2) |> Change_Table.join
(K (fn ((names1, names1'), (names2, names2')) =>
if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
then raise Change_Table.SAME
else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
val entries' = (entries1, entries2) |> Change_Table.join
(fn name => fn ((_, entry1), (_, entry2)) =>
if #serial entry1 = #serial entry2 then raise Change_Table.SAME
else err_dup kind' (name, entry1) (name, entry2) Position.none);
in make_name_space (kind', internals', entries') end;
(** naming context **)
(* datatype naming *)
datatype naming = Naming of
{scopes: Binding.scope list,
restricted: (bool * Binding.scope) option,
concealed: bool,
group: serial option,
theory_long_name: string,
path: (string * bool) list};
fun make_naming (scopes, restricted, concealed, group, theory_long_name, path) =
Naming {scopes = scopes, restricted = restricted, concealed = concealed,
group = group, theory_long_name = theory_long_name, path = path};
fun map_naming f (Naming {scopes, restricted, concealed, group, theory_long_name, path}) =
make_naming (f (scopes, restricted, concealed, group, theory_long_name, path));
(* scope and access restriction *)
fun get_scopes (Naming {scopes, ...}) = scopes;
val get_scope = try hd o get_scopes;
fun new_scope naming =
let
val scope = Binding.new_scope ();
val naming' =
naming |> map_naming (fn (scopes, restricted, concealed, group, theory_long_name, path) =>
(scope :: scopes, restricted, concealed, group, theory_long_name, path));
in (scope, naming') end;
fun restricted_scope strict scope =
map_naming (fn (scopes, _, concealed, group, theory_long_name, path) =>
(scopes, SOME (strict, scope), concealed, group, theory_long_name, path));
fun restricted strict pos naming =
(case get_scope naming of
SOME scope => restricted_scope strict scope naming
| NONE => error ("Missing local scope -- cannot restrict name space accesses" ^ Position.here pos));
val private_scope = restricted_scope true;
val private = restricted true;
val qualified_scope = restricted_scope false;
val qualified = restricted false;
val concealed = map_naming (fn (scopes, restricted, _, group, theory_long_name, path) =>
(scopes, restricted, true, group, theory_long_name, path));
(* additional structural info *)
fun set_theory_long_name theory_long_name =
map_naming (fn (scopes, restricted, concealed, group, _, path) =>
(scopes, restricted, concealed, group, theory_long_name, path));
fun get_group (Naming {group, ...}) = group;
fun set_group group =
map_naming (fn (scopes, restricted, concealed, _, theory_long_name, path) =>
(scopes, restricted, concealed, group, theory_long_name, path));
fun new_group naming = set_group (SOME (serial ())) naming;
val reset_group = set_group NONE;
(* name entry path *)
fun get_path (Naming {path, ...}) = path;
fun map_path f =
map_naming (fn (scopes, restricted, concealed, group, theory_long_name, path) =>
(scopes, restricted, concealed, group, theory_long_name, f path));
fun add_path elems = map_path (fn path => path @ [(elems, false)]);
val root_path = map_path (fn _ => []);
val parent_path = map_path (perhaps (try (#1 o split_last)));
fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
fun qualified_path mandatory binding = map_path (fn path =>
path @ Binding.path_of (Binding.qualify_name mandatory binding ""));
val global_naming = make_naming ([], NONE, false, NONE, "", []);
val local_naming = global_naming |> add_path Long_Name.localN;
(* transform *)
fun transform_naming (Naming {restricted = restricted', concealed = concealed', ...}) =
(case restricted' of
SOME (strict, scope) => restricted_scope strict scope
| NONE => I) #>
concealed' ? concealed;
fun transform_binding (Naming {restricted, concealed, ...}) =
Binding.restricted restricted #>
concealed ? Binding.concealed;
(* full name *)
fun name_spec naming binding =
Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);
fun full_name naming =
name_spec naming #> #spec #> map #1 #> Long_Name.implode;
val base_name = full_name global_naming #> Long_Name.base_name;
(* accesses *)
fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
and mandatory_prefixes1 [] = []
| mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
| mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
fun make_accesses naming binding =
(case name_spec naming binding of
{restriction = SOME true, ...} => ([], [])
| {restriction, spec, ...} =>
let
val restrict = is_some restriction ? filter (fn [_] => false | _ => true);
val sfxs = restrict (mandatory_suffixes spec);
val pfxs = restrict (mandatory_prefixes spec);
in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
(* hide *)
fun hide fully name space =
space |> map_name_space (fn (kind, internals, entries) =>
let
val _ = the_entry space name;
val (accs, accs') = get_accesses space name;
val xnames = filter (is_valid_access space name) accs;
val internals' = internals
|> hide_name name
|> fold (del_name name)
(if fully then xnames else inter (op =) [Long_Name.base_name name] xnames)
|> fold (del_name_extra name) accs';
in (kind, internals', entries) end);
(* alias *)
fun alias naming binding name space =
space |> map_name_space (fn (kind, internals, entries) =>
let
val _ = the_entry space name;
val (more_accs, more_accs') = make_accesses naming binding;
val internals' = internals |> fold (add_name name) more_accs;
val entries' = entries
|> Change_Table.map_entry name (apfst (fn (accs, accs') =>
(fold_rev (update op =) more_accs accs,
fold_rev (update op =) more_accs' accs')))
in (kind, internals', entries') end);
(** context naming **)
structure Data_Args =
struct
type T = naming;
val empty = global_naming;
fun init _ = local_naming;
val merge = #1;
end;
structure Global_Naming = Theory_Data(Data_Args);
structure Local_Naming = Proof_Data(Data_Args);
fun naming_of (Context.Theory thy) = Global_Naming.get thy
| naming_of (Context.Proof ctxt) = Local_Naming.get ctxt;
fun map_naming f (Context.Theory thy) = Context.Theory (Global_Naming.map f thy)
| map_naming f (Context.Proof ctxt) = Context.Proof (Local_Naming.map f ctxt);
(** entry definition **)
(* declaration *)
fun declared (Name_Space {entries, ...}) = Change_Table.defined entries;
fun declare context strict binding space =
let
val naming = naming_of context;
val Naming {group, theory_long_name, ...} = naming;
val {concealed, spec, ...} = name_spec naming binding;
val accesses = make_accesses naming binding;
val name = Long_Name.implode (map fst spec);
val _ = name = "" andalso error (Binding.bad binding);
val (proper_pos, pos) = Position.default (Binding.pos_of binding);
val entry =
{concealed = concealed,
group = group,
theory_long_name = theory_long_name,
pos = pos,
serial = serial ()};
val space' =
space |> map_name_space (fn (kind, internals, entries) =>
let
val internals' = internals |> fold (add_name name) (#1 accesses);
val entries' =
(if strict then Change_Table.update_new else Change_Table.update)
(name, (accesses, entry)) entries
handle Change_Table.DUP dup =>
err_dup kind (dup, #2 (the (Change_Table.lookup entries dup)))
(name, entry) (#pos entry);
in (kind, internals', entries') end);
val _ =
if proper_pos andalso Context_Position.is_reported_generic context pos then
Position.report pos (entry_markup {def = true} (kind_of space) (name, entry))
else ();
in (name, space') end;
(* definition in symbol table *)
datatype 'a table = Table of T * 'a Change_Table.T;
fun change_base begin (Table (space, tab)) =
Table (change_base_space begin space, Change_Table.change_base begin tab);
fun change_ignore (Table (space, tab)) =
Table (change_ignore_space space, Change_Table.change_ignore tab);
fun space_of_table (Table (space, _)) = space;
fun check_reports context (Table (space, tab)) (xname, ps) =
let val name = intern space xname in
(case Change_Table.lookup tab name of
SOME x =>
let
val reports =
filter (Context_Position.is_reported_generic context) ps
|> map (fn pos => (pos, markup space name));
in ((name, reports), x) end
| NONE =>
error (undefined space name ^ Position.here_list ps ^
Completion.markup_report
(map (fn pos => completion context space (K true) (xname, pos)) ps)))
end;
fun check context table (xname, pos) =
let
val ((name, reports), x) = check_reports context table (xname, [pos]);
val _ = Context_Position.reports_generic context reports;
in (name, x) end;
fun defined (Table (_, tab)) name = Change_Table.defined tab name;
fun lookup (Table (_, tab)) name = Change_Table.lookup tab name;
fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name;
fun get table name =
(case lookup_key table name of
SOME (_, x) => x
| NONE => error (undefined (space_of_table table) name));
fun define context strict (binding, x) (Table (space, tab)) =
let
val (name, space') = declare context strict binding space;
val tab' = Change_Table.update (name, x) tab;
in (name, Table (space', tab')) end;
(* derived table operations *)
fun alias_table naming binding name (Table (space, tab)) =
Table (alias naming binding name space, tab);
fun hide_table fully name (Table (space, tab)) =
Table (hide fully name space, tab);
fun del_table name (Table (space, tab)) =
let
val space' = hide true name space handle ERROR _ => space;
val tab' = Change_Table.delete_safe name tab;
in Table (space', tab') end;
fun map_table_entry name f (Table (space, tab)) =
Table (space, Change_Table.map_entry name f tab);
fun fold_table f (Table (_, tab)) = Change_Table.fold f tab;
fun dest_table (Table (_, tab)) = Change_Table.dest tab;
fun empty_table kind = Table (empty kind, Change_Table.empty);
fun merge_tables (Table (space1, tab1), Table (space2, tab2)) =
Table (merge (space1, space2), Change_Table.merge (K true) (tab1, tab2));
fun join_tables f (Table (space1, tab1), Table (space2, tab2)) =
Table (merge (space1, space2), Change_Table.join f (tab1, tab2));
(* present table content *)
fun extern_entries verbose ctxt space entries =
fold (fn (name, x) =>
(verbose orelse not (is_concealed space name)) ?
cons ((name, extern ctxt space name), x)) entries []
|> sort_by (#2 o #1);
fun markup_entries verbose ctxt space entries =
extern_entries verbose ctxt space entries
|> map (fn ((name, xname), x) => ((markup space name, xname), x));
fun extern_table verbose ctxt (Table (space, tab)) =
extern_entries verbose ctxt space (Change_Table.dest tab);
fun markup_table verbose ctxt (Table (space, tab)) =
markup_entries verbose ctxt space (Change_Table.dest tab);
end;
diff --git a/src/Pure/Thy/presentation.scala b/src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala
+++ b/src/Pure/Thy/presentation.scala
@@ -1,636 +1,667 @@
/* Title: Pure/Thy/presentation.scala
Author: Makarius
HTML presentation of PIDE document content.
*/
package isabelle
import scala.annotation.tailrec
import scala.collection.immutable.SortedMap
import scala.collection.mutable
object Presentation
{
/** HTML documents **/
/* HTML context */
sealed case class HTML_Document(title: String, content: String)
- def html_context(cache: Term.Cache = Term.Cache.make()): HTML_Context =
- new HTML_Context(cache)
+ abstract class HTML_Context
+ {
+ /* directory structure */
- final class HTML_Context private[Presentation](val cache: Term.Cache)
- {
+ def root_dir: Path
+ def theory_session(name: Document.Node.Name): Sessions.Info
+
+ def session_dir(info: Sessions.Info): Path =
+ root_dir + Path.explode(info.chapter_session)
+ def theory_path(name: Document.Node.Name): Path =
+ session_dir(theory_session(name)) + Path.explode(name.theory_base_name).html
+ def files_path(name: Document.Node.Name, path: Path): Path =
+ theory_path(name).dir + Path.explode("files") + path.squash.html
+
+
+ /* cached theory exports */
+
+ val cache: Term.Cache = Term.Cache.make()
+
private val already_presented = Synchronized(Set.empty[String])
def register_presented(nodes: List[Document.Node.Name]): List[Document.Node.Name] =
already_presented.change_result(presented =>
(nodes.filterNot(name => presented.contains(name.theory)),
presented ++ nodes.iterator.map(_.theory)))
private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory])
def cache_theory(thy_name: String, make_thy: => Export_Theory.Theory): Export_Theory.Theory =
{
theory_cache.change_result(thys =>
{
thys.get(thy_name) match {
case Some(thy) => (thy, thys)
case None =>
val thy = make_thy
(thy, thys + (thy_name -> thy))
}
})
}
+
+ /* HTML content */
+
def head(title: String, rest: XML.Body = Nil): XML.Tree =
HTML.div("head", HTML.chapter(title) :: rest)
def source(body: XML.Body): XML.Tree = HTML.pre("source", body)
def contents(heading: String, items: List[XML.Body], css_class: String = "contents")
: List[XML.Elem] =
{
if (items.isEmpty) Nil
else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items))))
}
+ val isabelle_css: String = File.read(HTML.isabelle_css)
+
def html_document(title: String, body: XML.Body, fonts_css: String): HTML_Document =
{
val content =
HTML.output_document(
List(
- HTML.style(fonts_css + "\n\n" + File.read(HTML.isabelle_css)),
+ HTML.style(fonts_css + "\n\n" + isabelle_css),
HTML.title(title)),
List(HTML.source(body)), css = "", structural = false)
HTML_Document(title, content)
}
}
/* presentation elements */
sealed case class Elements(
html: Markup.Elements = Markup.Elements.empty,
entity: Markup.Elements = Markup.Elements.empty,
language: Markup.Elements = Markup.Elements.empty)
val elements1: Elements =
Elements(
html = Rendering.foreground_elements ++ Rendering.text_color_elements +
Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE,
entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,
Markup.CLASS, Markup.LOCALE, Markup.FREE))
val elements2: Elements =
Elements(
html = elements1.html ++ Rendering.markdown_elements,
language = Markup.Elements(Markup.Language.DOCUMENT))
/* formal entities */
type Entity = Export_Theory.Entity[Export_Theory.No_Content]
object Entity_Context
{
+ object Theory_Ref
+ {
+ def unapply(props: Properties.T): Option[Document.Node.Name] =
+ (props, props, props) match {
+ case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file)) =>
+ Some(Resources.file_node(Path.explode(thy_file), theory = theory))
+ case _ => None
+ }
+ }
+
+ object Entity_Ref
+ {
+ def unapply(props: Properties.T): Option[(Path, Option[String], String, String)] =
+ (props, props, props, props) match {
+ case (Markup.Ref(_), Position.Def_File(def_file), Markup.Kind(kind), Markup.Name(name)) =>
+ val def_theory = Position.Def_Theory.unapply(props)
+ Some((Path.explode(def_file), def_theory, kind, name))
+ case _ => None
+ }
+ }
+
val empty: Entity_Context = new Entity_Context
def make(
session: String,
deps: Sessions.Deps,
node: Document.Node.Name,
theory_exports: Map[String, Export_Theory.Theory]): Entity_Context =
new Entity_Context {
private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
override def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] =
{
body match {
case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
case _ =>
Some {
val entities =
theory_exports.get(node.theory).flatMap(_.entity_by_range.get(range))
.getOrElse(Nil)
val body1 =
if (seen_ranges.contains(range)) {
HTML.entity_def(HTML.span(HTML.id(offset_id(range)), body))
}
else HTML.span(body)
entities.map(_.kname).foldLeft(body1) {
case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
}
}
}
}
private def offset_id(range: Text.Range): String =
"offset_" + range.start + ".." + range.stop
private def physical_ref(thy_name: String, props: Properties.T): Option[String] =
{
for {
range <- Position.Def_Range.unapply(props)
if thy_name == node.theory
} yield {
seen_ranges += range
offset_id(range)
}
}
private def logical_ref(thy_name: String, kind: String, name: String): Option[String] =
for {
thy <- theory_exports.get(thy_name)
entity <- thy.entity_by_kind_name.get((kind, name))
} yield entity.kname
override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
{
- (props, props, props, props, props) match {
- case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _, _) =>
- val node_name = Resources.file_node(Path.explode(thy_file), theory = theory)
+ props match {
+ case Theory_Ref(node_name) =>
node_relative(deps, session, node_name).map(html_dir =>
HTML.link(html_dir + html_name(node_name), body))
- case (Markup.Ref(_), Position.Def_File(def_file), Position.Def_Theory(def_theory),
- Markup.Kind(kind), Markup.Name(name)) =>
- val file_path = Path.explode(def_file)
- val proper_thy_name =
- proper_string(def_theory) orElse
- (if (File.eq(node.path, file_path)) Some(node.theory) else None)
+ case Entity_Ref(file_path, def_theory, kind, name) =>
for {
- thy_name <- proper_thy_name
+ thy_name <-
+ def_theory orElse (if (File.eq(node.path, file_path)) Some(node.theory) else None)
node_name = Resources.file_node(file_path, theory = thy_name)
html_dir <- node_relative(deps, session, node_name)
html_file = node_file(node_name)
html_ref <-
logical_ref(thy_name, kind, name) orElse physical_ref(thy_name, props)
} yield {
HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body))
}
case _ => None
}
}
}
}
class Entity_Context
{
def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] = None
def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = None
}
/* HTML output */
private val div_elements =
Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
HTML.descr.name)
def make_html(
entity_context: Entity_Context,
elements: Elements,
xml: XML.Body): XML.Body =
{
def html_div(html: XML.Body): Boolean =
html exists {
case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
case XML.Text(_) => false
}
def html_class(c: String, html: XML.Body): XML.Body =
if (c == "") html
else if (html_div(html)) List(HTML.div(c, html))
else List(HTML.span(c, html))
def html_body(xml_body: XML.Body, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
xml_body.foldRight((List.empty[XML.Tree], end_offset)) { case (tree, (res, end_offset1)) =>
val (res1, offset) = html_body_single(tree, end_offset1)
(res1 ++ res, offset)
}
@tailrec
def html_body_single(xml_tree: XML.Tree, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
xml_tree match {
case XML.Wrapped_Elem(markup, _, body) => html_body_single(XML.Elem(markup, body), end_offset)
case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) =>
val (body1, offset) = html_body(body, end_offset)
if (elements.entity(kind)) {
entity_context.make_ref(props, body1) match {
case Some(link) => (List(link), offset)
case None => (body1, offset)
}
}
else (body1, offset)
case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(name)), body) =>
val (body1, offset) = html_body(body, end_offset)
(html_class(if (elements.language(name)) name else "", body1), offset)
case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) =>
val (body1, offset) = html_body(body, end_offset)
(List(HTML.par(body1)), offset)
case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) =>
val (body1, offset) = html_body(body, end_offset)
(List(HTML.item(body1)), offset)
case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), text) =>
(Nil, end_offset - XML.symbol_length(text))
case XML.Elem(Markup.Markdown_List(kind), body) =>
val (body1, offset) = html_body(body, end_offset)
if (kind == Markup.ENUMERATE) (List(HTML.enum(body1)), offset)
else (List(HTML.list(body1)), offset)
case XML.Elem(markup, body) =>
val name = markup.name
val (body1, offset) = html_body(body, end_offset)
val html =
markup.properties match {
case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
html_class(kind, body1)
case _ =>
body1
}
Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
case Some(c) => (html_class(c.toString, html), offset)
case None => (html_class(name, html), offset)
}
case XML.Text(text) =>
val offset = end_offset - Symbol.length(text)
val body = HTML.text(Symbol.decode(text))
entity_context.make_def(Text.Range(offset, end_offset), body) match {
case Some(body1) => (List(body1), offset)
case None => (body, offset)
}
}
html_body(xml, XML.symbol_length(xml) + 1)._1
}
/* PIDE HTML document */
def html_document(
snapshot: Document.Snapshot,
html_context: HTML_Context,
elements: Elements,
plain_text: Boolean = false,
fonts_css: String = HTML.fonts_css()): HTML_Document =
{
require(!snapshot.is_outdated, "document snapshot outdated")
val name = snapshot.node_name
if (plain_text) {
val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
val body = HTML.text(snapshot.node.source)
html_context.html_document(title, body, fonts_css)
}
else {
Resources.html_document(snapshot) getOrElse {
val title =
if (name.is_theory) "Theory " + quote(name.theory_base_name)
else "File " + Symbol.cartouche_decoded(name.path.file_name)
val xml = snapshot.xml_markup(elements = elements.html)
val body = make_html(Entity_Context.empty, elements, xml)
html_context.html_document(title, body, fonts_css)
}
}
}
/** HTML presentation **/
/* presentation context */
object Context
{
val none: Context = new Context { def enabled: Boolean = false }
val standard: Context = new Context { def enabled: Boolean = true }
def dir(path: Path): Context =
new Context {
def enabled: Boolean = true
override def dir(store: Sessions.Store): Path = path
}
def make(s: String): Context =
if (s == ":") standard else dir(Path.explode(s))
}
abstract class Context private
{
def enabled: Boolean
def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info
def dir(store: Sessions.Store): Path = store.presentation_dir
def dir(store: Sessions.Store, info: Sessions.Info): Path =
dir(store) + Path.explode(info.chapter_session)
}
/* maintain chapter index */
private val sessions_path = Path.basic(".sessions")
private def read_sessions(dir: Path): List[(String, String)] =
{
val path = dir + sessions_path
if (path.is_file) {
import XML.Decode._
list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
}
else Nil
}
def update_chapter(
presentation_dir: Path, chapter: String, new_sessions: List[(String, String)]): Unit =
{
val dir = Isabelle_System.make_directory(presentation_dir + Path.basic(chapter))
val sessions0 =
try { read_sessions(dir) }
catch { case _: XML.Error => Nil }
val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
File.write(dir + sessions_path,
{
import XML.Encode._
YXML.string_of_body(list(pair(string, string))(sessions))
})
val title = "Isabelle/" + chapter + " sessions"
HTML.write_document(dir, "index.html",
List(HTML.title(title + Isabelle_System.isabelle_heading())),
HTML.chapter(title) ::
(if (sessions.isEmpty) Nil
else
List(HTML.div("sessions",
List(HTML.description(
sessions.map({ case (name, description) =>
val descr = Symbol.trim_blank_lines(description)
(List(HTML.link(name + "/index.html", HTML.text(name))),
if (descr == "") Nil
else HTML.break ::: List(HTML.pre(HTML.text(descr)))) })))))),
base = Some(presentation_dir))
}
def update_root(presentation_dir: Path): Unit =
{
Isabelle_System.make_directory(presentation_dir)
HTML.init_fonts(presentation_dir)
Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"),
presentation_dir + Path.explode("isabelle.gif"))
val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library"
File.write(presentation_dir + Path.explode("index.html"),
HTML.header +
"""
""" + HTML.head_meta + """
""" + title + """
""" + File.read(Path.explode("~~/lib/html/library_index_content.template")) +
"""
""" + HTML.footer)
}
/* present session */
val session_graph_path = Path.explode("session_graph.pdf")
val readme_path = Path.explode("README.html")
- val files_path = Path.explode("files")
def html_name(name: Document.Node.Name): String = Path.explode(name.theory_base_name).html.implode
- def html_path(path: Path): String = (files_path + path.squash.html).implode
+ def files_path(src_path: Path): String = (Path.explode("files") + src_path.squash.html).implode
- private def node_file(node: Document.Node.Name): String =
- if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node))
+ private def node_file(name: Document.Node.Name): String =
+ if (name.node.endsWith(".thy")) html_name(name) else files_path(name.path)
private def session_relative(deps: Sessions.Deps, session0: String, session1: String): Option[String] =
{
for {
info0 <- deps.sessions_structure.get(session0)
info1 <- deps.sessions_structure.get(session1)
} yield info0.relative_path(info1)
}
def node_relative(
deps: Sessions.Deps,
session0: String,
node_name: Document.Node.Name): Option[String] =
{
val session1 = deps(session0).theory_qualifier(node_name)
session_relative(deps, session0, session1)
}
def theory_link(deps: Sessions.Deps, session0: String,
name: Document.Node.Name, body: XML.Body, anchor: Option[String] = None): Option[XML.Tree] =
{
val session1 = deps(session0).theory_qualifier(name)
val info0 = deps.sessions_structure.get(session0)
val info1 = deps.sessions_structure.get(session1)
val fragment = if (anchor.isDefined) "#" + anchor.get else ""
if (info0.isDefined && info1.isDefined) {
Some(HTML.link(info0.get.relative_path(info1.get) + html_name(name) + fragment, body))
}
else None
}
def session_html(
session: String,
deps: Sessions.Deps,
db_context: Sessions.Database_Context,
progress: Progress = new Progress,
verbose: Boolean = false,
html_context: HTML_Context,
- session_elements: Elements,
- presentation: Context): Unit =
+ session_elements: Elements): Unit =
{
val hierarchy = deps.sessions_structure.hierarchy(session)
val info = deps.sessions_structure(session)
val options = info.options
val base = deps(session)
- def make_session_dir(name: String): Path =
- Isabelle_System.make_directory(
- presentation.dir(db_context.store, deps.sessions_structure(name)))
-
- val session_dir = make_session_dir(session)
- val presentation_dir = presentation.dir(db_context.store)
+ val session_dir = Isabelle_System.make_directory(html_context.session_dir(info))
Bytes.write(session_dir + session_graph_path,
graphview.Graph_File.make_pdf(options, base.session_graph_display))
val documents =
for {
doc <- info.document_variants
document <- db_context.input_database(session)(Document_Build.read_document(_, _, doc.name))
} yield {
val doc_path = (session_dir + doc.path.pdf).expand
if (verbose) progress.echo("Presenting document " + session + "/" + doc.name)
if (options.bool("document_echo")) progress.echo("Document at " + doc_path)
Bytes.write(doc_path, document.pdf)
doc
}
val view_links =
{
val deps_link =
HTML.link(session_graph_path, HTML.text("theory dependencies"))
val readme_links =
if ((info.dir + readme_path).is_file) {
Isabelle_System.copy_file(info.dir + readme_path, session_dir + readme_path)
List(HTML.link(readme_path, HTML.text("README")))
}
else Nil
val document_links =
documents.map(doc => HTML.link(doc.path.pdf, HTML.text(doc.name)))
Library.separate(HTML.break ::: HTML.nl,
(deps_link :: readme_links ::: document_links).
map(link => HTML.text("View ") ::: List(link))).flatten
}
val all_used_theories = hierarchy.reverse.flatMap(a => deps(a).used_theories.map(_._1))
val present_theories = html_context.register_presented(all_used_theories)
val theory_exports: Map[String, Export_Theory.Theory] =
(for (node <- all_used_theories.iterator) yield {
val thy_name = node.theory
val theory =
if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
else {
html_context.cache_theory(thy_name,
{
val provider = Export.Provider.database_context(db_context, hierarchy, thy_name)
if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
Export_Theory.read_theory(
provider, session, thy_name, cache = html_context.cache)
}
else Export_Theory.no_theory
})
}
thy_name -> theory
}).toMap
def entity_context(name: Document.Node.Name): Entity_Context =
Entity_Context.make(session, deps, name, theory_exports)
val theories: List[XML.Body] =
{
sealed case class Seen_File(
- src_path: Path, file_name: String, thy_session: String, thy_name: Document.Node.Name)
+ src_path: Path, thy_name: Document.Node.Name, thy_session: String)
{
- def check(src_path1: Path, file_name1: String, thy_session1: String): Boolean =
- (src_path == src_path1 || file_name == file_name1) && thy_session == thy_session1
+ val files_path: Path = html_context.files_path(thy_name, src_path)
+
+ def check(src_path1: Path, thy_name1: Document.Node.Name, thy_session1: String): Boolean =
+ {
+ val files_path1 = html_context.files_path(thy_name1, src_path1)
+ (src_path == src_path1 || files_path == files_path1) && thy_session == thy_session1
+ }
}
var seen_files = List.empty[Seen_File]
sealed case class Theory(
name: Document.Node.Name,
command: Command,
files_html: List[(Path, XML.Tree)],
html: XML.Tree)
def read_theory(name: Document.Node.Name): Option[Theory] =
{
progress.expose_interrupt()
for (command <- Build_Job.read_theory(db_context, hierarchy, name.theory))
yield {
if (verbose) progress.echo("Presenting theory " + name)
val snapshot = Document.State.init.snippet(command)
val thy_elements =
session_elements.copy(entity =
theory_exports(name.theory).others.keySet.foldLeft(session_elements.entity)(_ + _))
val files_html =
for {
(src_path, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html)
if xml.nonEmpty
}
yield {
progress.expose_interrupt()
if (verbose) progress.echo("Presenting file " + src_path)
(src_path, html_context.source(
make_html(entity_context(name), thy_elements, xml)))
}
val html =
html_context.source(
make_html(entity_context(name), thy_elements,
snapshot.xml_markup(elements = thy_elements.html)))
Theory(name, command, files_html, html)
}
}
(for (thy <- Par_List.map(read_theory, present_theories).flatten) yield {
- val thy_session = base.theory_qualifier(thy.name)
- val thy_dir = make_session_dir(thy_session)
+ val thy_session = html_context.theory_session(thy.name)
+ val thy_dir = Isabelle_System.make_directory(html_context.session_dir(thy_session))
val files =
for { (src_path, file_html) <- thy.files_html }
yield {
- val file_name = html_path(src_path)
-
- seen_files.find(_.check(src_path, file_name, thy_session)) match {
- case None => seen_files ::= Seen_File(src_path, file_name, thy_session, thy.name)
+ seen_files.find(_.check(src_path, thy.name, thy_session.name)) match {
+ case None => seen_files ::= Seen_File(src_path, thy.name, thy_session.name)
case Some(seen_file) =>
- error("Incoherent use of file name " + src_path + " as " + quote(file_name) +
+ error("Incoherent use of file name " + src_path + " as " + files_path(src_path) +
" in theory " + seen_file.thy_name + " vs. " + thy.name)
}
- val file_path = thy_dir + Path.explode(file_name)
+ val file_path = html_context.files_path(thy.name, src_path)
val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
HTML.write_document(file_path.dir, file_path.file_name,
List(HTML.title(file_title)), List(html_context.head(file_title), file_html),
- base = Some(presentation_dir))
+ base = Some(html_context.root_dir))
- List(HTML.link(file_name, HTML.text(file_title)))
+ List(HTML.link(files_path(src_path), HTML.text(file_title)))
}
val thy_title = "Theory " + thy.name.theory_base_name
HTML.write_document(thy_dir, html_name(thy.name),
List(HTML.title(thy_title)), List(html_context.head(thy_title), thy.html),
- base = Some(presentation_dir))
+ base = Some(html_context.root_dir))
- if (thy_session == session) {
+ if (thy_session.name == session) {
Some(
List(HTML.link(html_name(thy.name),
HTML.text(thy.name.theory_base_name) :::
(if (files.isEmpty) Nil else List(HTML.itemize(files))))))
}
else None
}).flatten
}
val title = "Session " + session
HTML.write_document(session_dir, "index.html",
List(HTML.title(title + Isabelle_System.isabelle_heading())),
html_context.head(title, List(HTML.par(view_links))) ::
html_context.contents("Theories", theories),
- base = Some(presentation_dir))
+ base = Some(html_context.root_dir))
}
}
diff --git a/src/Pure/Tools/build.scala b/src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala
+++ b/src/Pure/Tools/build.scala
@@ -1,684 +1,690 @@
/* Title: Pure/Tools/build.scala
Author: Makarius
Options: :folding=explicit:
Build and manage Isabelle sessions.
*/
package isabelle
import scala.collection.immutable.SortedSet
import scala.annotation.tailrec
object Build
{
/** auxiliary **/
/* persistent build info */
sealed case class Session_Info(
sources: String,
input_heaps: List[String],
output_heap: Option[String],
return_code: Int)
{
def ok: Boolean = return_code == 0
}
/* queue with scheduling information */
private object Queue
{
type Timings = (List[Properties.T], Double)
def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings =
{
val no_timings: Timings = (Nil, 0.0)
store.try_open_database(session_name) match {
case None => no_timings
case Some(db) =>
def ignore_error(msg: String) =
{
progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
no_timings
}
try {
val command_timings = store.read_command_timings(db, session_name)
val session_timing =
store.read_session_timing(db, session_name) match {
case Markup.Elapsed(t) => t
case _ => 0.0
}
(command_timings, session_timing)
}
catch {
case ERROR(msg) => ignore_error(msg)
case exn: java.lang.Error => ignore_error(Exn.message(exn))
case _: XML.Error => ignore_error("")
}
finally { db.close() }
}
}
def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
: Map[String, Double] =
{
val maximals = sessions_structure.build_graph.maximals.toSet
def desc_timing(session_name: String): Double =
{
if (maximals.contains(session_name)) timing(session_name)
else {
val descendants = sessions_structure.build_descendants(List(session_name)).toSet
val g = sessions_structure.build_graph.restrict(descendants)
(0.0 :: g.maximals.flatMap(desc => {
val ps = g.all_preds(List(desc))
if (ps.exists(p => !timing.isDefinedAt(p))) None
else Some(ps.map(timing(_)).sum)
})).max
}
}
timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
}
def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
: Queue =
{
val graph = sessions_structure.build_graph
val names = graph.keys
val timings = names.map(name => (name, load_timings(progress, store, name)))
val command_timings =
timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
val session_timing =
make_session_timing(sessions_structure,
timings.map({ case (name, (_, t)) => (name, t) }).toMap)
object Ordering extends scala.math.Ordering[String]
{
def compare(name1: String, name2: String): Int =
session_timing(name2) compare session_timing(name1) match {
case 0 =>
sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
case 0 => name1 compare name2
case ord => ord
}
case ord => ord
}
}
new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
}
}
private class Queue(
graph: Graph[String, Sessions.Info],
order: SortedSet[String],
val command_timings: String => List[Properties.T])
{
def is_inner(name: String): Boolean = !graph.is_maximal(name)
def is_empty: Boolean = graph.is_empty
def - (name: String): Queue =
new Queue(graph.del_node(name), order - name, command_timings)
def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
{
val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
if (it.hasNext) { val name = it.next(); Some((name, graph.get_node(name))) }
else None
}
}
/** build with results **/
class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
{
def sessions: Set[String] = results.keySet
def infos: List[Sessions.Info] = results.values.map(_._2).toList
def cancelled(name: String): Boolean = results(name)._1.isEmpty
def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
def get_info(name: String): Option[Sessions.Info] = results.get(name).map(_._2)
def info(name: String): Sessions.Info = get_info(name).get
val rc: Int =
results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
foldLeft(Process_Result.RC.ok)(_ max _)
def ok: Boolean = rc == Process_Result.RC.ok
override def toString: String = rc.toString
}
def session_finished(session_name: String, process_result: Process_Result): String =
"Finished " + session_name + " (" + process_result.timing.message_resources + ")"
def session_timing(session_name: String, build_log: Build_Log.Session_Info): String =
{
val props = build_log.session_timing
val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
val timing = Markup.Timing_Properties.parse(props)
"Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
}
def build(
options: Options,
selection: Sessions.Selection = Sessions.Selection.empty,
presentation: Presentation.Context = Presentation.Context.none,
progress: Progress = new Progress,
check_unknown_files: Boolean = false,
build_heap: Boolean = false,
clean_build: Boolean = false,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
infos: List[Sessions.Info] = Nil,
numa_shuffling: Boolean = false,
max_jobs: Int = 1,
list_files: Boolean = false,
check_keywords: Set[String] = Set.empty,
fresh_build: Boolean = false,
no_build: Boolean = false,
soft_build: Boolean = false,
verbose: Boolean = false,
export_files: Boolean = false,
session_setup: (String, Session) => Unit = (_, _) => ()): Results =
{
val build_options =
options +
"completion_limit=0" +
"editor_tracing_messages=0" +
"kodkod_scala=false" +
("pide_reports=" + options.bool("build_pide_reports"))
val store = Sessions.store(build_options)
Isabelle_Fonts.init()
/* session selection and dependencies */
val full_sessions =
Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
val full_sessions_selection = full_sessions.imports_selection(selection)
def sources_stamp(deps: Sessions.Deps, session_name: String): String =
{
val digests =
full_sessions(session_name).meta_digest ::
deps.sources(session_name) :::
deps.imported_sources(session_name)
SHA1.digest_set(digests).toString
}
val deps =
{
val deps0 =
Sessions.deps(full_sessions.selection(selection),
progress = progress, inlined_files = true, verbose = verbose,
list_files = list_files, check_keywords = check_keywords).check_errors
if (soft_build && !fresh_build) {
val outdated =
deps0.sessions_structure.build_topological_order.flatMap(name =>
store.try_open_database(name) match {
case Some(db) =>
using(db)(store.read_build(_, name)) match {
case Some(build)
if build.ok && build.sources == sources_stamp(deps0, name) => None
case _ => Some(name)
}
case None => Some(name)
})
Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
progress = progress, inlined_files = true).check_errors
}
else deps0
}
/* check unknown files */
if (check_unknown_files) {
val source_files =
(for {
(_, base) <- deps.session_bases.iterator
(path, _) <- base.sources.iterator
} yield path).toList
val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
val unknown_files =
Mercurial.check_files(source_files)._2.
filterNot(path => exclude_files.contains(path.canonical_file))
if (unknown_files.nonEmpty) {
progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", ""))
}
}
/* main build process */
val queue = Queue(progress, deps.sessions_structure, store)
store.prepare_output_dir()
if (clean_build) {
for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
val (relevant, ok) = store.clean_output(name)
if (relevant) {
if (ok) progress.echo("Cleaned " + name)
else progress.echo(name + " FAILED to clean")
}
}
}
// scheduler loop
case class Result(
current: Boolean,
heap_digest: Option[String],
process: Option[Process_Result],
info: Sessions.Info)
{
def ok: Boolean =
process match {
case None => false
case Some(res) => res.ok
}
}
def sleep(): Unit =
Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep() }
val log =
build_options.string("system_log") match {
case "" => No_Logger
case "true" => Logger.make(progress)
case log_file => Logger.make(Some(Path.explode(log_file)))
}
val numa_nodes = new NUMA.Nodes(numa_shuffling)
@tailrec def loop(
pending: Queue,
running: Map[String, (List[String], Build_Job)],
results: Map[String, Result]): Map[String, Result] =
{
def used_node(i: Int): Boolean =
running.iterator.exists(
{ case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
if (pending.is_empty) results
else {
if (progress.stopped) {
for ((_, (_, job)) <- running) job.terminate()
}
running.find({ case (_, (_, job)) => job.is_finished }) match {
case Some((session_name, (input_heaps, job))) =>
//{{{ finish job
val (process_result, heap_digest) = job.join
val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
val process_result_tail =
{
val tail = job.info.options.int("process_output_tail")
process_result.copy(
out_lines =
"(see also " + store.output_log(session_name).file.toString + ")" ::
(if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
}
val build_log =
Build_Log.Log_File(session_name, process_result.out_lines).
parse_session_info(
command_timings = true,
theory_timings = true,
ml_statistics = true,
task_statistics = true)
// write log file
if (process_result.ok) {
File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines))
}
else File.write(store.output_log(session_name), terminate_lines(log_lines))
// write database
using(store.open_database(session_name, output = true))(db =>
store.write_session_info(db, session_name,
build_log =
if (process_result.timeout) build_log.error("Timeout") else build_log,
build =
Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest,
process_result.rc)))
// messages
process_result.err_lines.foreach(progress.echo)
if (process_result.ok) {
if (verbose) progress.echo(session_timing(session_name, build_log))
progress.echo(session_finished(session_name, process_result))
}
else {
progress.echo(session_name + " FAILED")
if (!process_result.interrupted) progress.echo(process_result_tail.out)
}
loop(pending - session_name, running - session_name,
results +
(session_name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
//}}}
case None if running.size < (max_jobs max 1) =>
//{{{ check/start next job
pending.dequeue(running.isDefinedAt) match {
case Some((session_name, info)) =>
val ancestor_results =
deps.sessions_structure.build_requirements(List(session_name)).
filterNot(_ == session_name).map(results(_))
val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
val do_store =
build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
val (current, heap_digest) =
{
store.try_open_database(session_name) match {
case Some(db) =>
using(db)(store.read_build(_, session_name)) match {
case Some(build) =>
val heap_digest = store.find_heap_digest(session_name)
val current =
!fresh_build &&
build.ok &&
build.sources == sources_stamp(deps, session_name) &&
build.input_heaps == ancestor_heaps &&
build.output_heap == heap_digest &&
!(do_store && heap_digest.isEmpty)
(current, heap_digest)
case None => (false, None)
}
case None => (false, None)
}
}
val all_current = current && ancestor_results.forall(_.current)
if (all_current)
loop(pending - session_name, running,
results +
(session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
else if (no_build) {
progress.echo_if(verbose, "Skipping " + session_name + " ...")
loop(pending - session_name, running,
results +
(session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
}
else if (ancestor_results.forall(_.ok) && !progress.stopped) {
progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
store.clean_output(session_name)
using(store.open_database(session_name, output = true))(
store.init_session_info(_, session_name))
val numa_node = numa_nodes.next(used_node)
val job =
new Build_Job(progress, session_name, info, deps, store, do_store,
log, session_setup, numa_node, queue.command_timings(session_name))
loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
}
else {
progress.echo(session_name + " CANCELLED")
loop(pending - session_name, running,
results + (session_name -> Result(false, heap_digest, None, info)))
}
case None => sleep(); loop(pending, running, results)
}
///}}}
case None => sleep(); loop(pending, running, results)
}
}
}
/* build results */
val results =
{
val results0 =
if (deps.is_empty) {
progress.echo_warning("Nothing to build")
Map.empty[String, Result]
}
else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
new Results(
(for ((name, result) <- results0.iterator)
yield (name, (result.process, result.info))).toMap)
}
if (export_files) {
for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) {
val info = results.info(name)
if (info.export_files.nonEmpty) {
progress.echo("Exporting " + info.name + " ...")
for ((dir, prune, pats) <- info.export_files) {
Export.export_files(store, name, info.dir + dir,
progress = if (verbose) progress else new Progress,
export_prune = prune,
export_patterns = pats)
}
}
}
}
if (results.rc != Process_Result.RC.ok && (verbose || !no_build)) {
val unfinished =
(for {
name <- results.sessions.iterator
if !results(name).ok
} yield name).toList.sorted
progress.echo("Unfinished session(s): " + commas(unfinished))
}
/* PDF/HTML presentation */
if (!no_build && !progress.stopped && results.ok) {
val selected = full_sessions_selection.toSet
val presentation_sessions =
(for {
session_name <- deps.sessions_structure.imports_topological_order.iterator
info <- results.get_info(session_name)
if selected(session_name) && presentation.enabled(info) && results(session_name).ok }
yield info).toList
if (presentation_sessions.nonEmpty) {
val presentation_dir = presentation.dir(store)
progress.echo("Presentation in " + presentation_dir.absolute)
Presentation.update_root(presentation_dir)
for ((chapter, infos) <- presentation_sessions.groupBy(_.chapter).iterator) {
val entries = infos.map(info => (info.name, info.description))
Presentation.update_chapter(presentation_dir, chapter, entries)
}
- val html_context = Presentation.html_context(cache = store.cache)
-
using(store.open_database_context())(db_context =>
- for (info <- presentation_sessions) {
+ for (session <- presentation_sessions.map(_.name)) {
progress.expose_interrupt()
- progress.echo("Presenting " + info.name + " ...")
+ progress.echo("Presenting " + session + " ...")
+
+ val html_context =
+ new Presentation.HTML_Context {
+ override val cache: Term.Cache = store.cache
+ override def root_dir: Path = presentation_dir
+ override def theory_session(name: Document.Node.Name): Sessions.Info =
+ deps.sessions_structure(deps(session).theory_qualifier(name))
+ }
Presentation.session_html(
- info.name, deps, db_context, progress = progress,
+ session, deps, db_context, progress = progress,
verbose = verbose, html_context = html_context,
- Presentation.elements1, presentation = presentation)
+ Presentation.elements1)
})
}
}
results
}
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions",
Scala_Project.here, args =>
{
val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
var numa_shuffling = false
var presentation = Presentation.Context.none
var requirements = false
var soft_build = false
var exclude_session_groups: List[String] = Nil
var all_sessions = false
var build_heap = false
var clean_build = false
var dirs: List[Path] = Nil
var export_files = false
var fresh_build = false
var session_groups: List[String] = Nil
var max_jobs = 1
var check_keywords: Set[String] = Set.empty
var list_files = false
var no_build = false
var options = Options.init(opts = build_options)
var verbose = false
var exclude_sessions: List[String] = Nil
val getopts = Getopts("""
Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-N cyclic shuffling of NUMA CPU nodes (performance tuning)
-P DIR enable HTML/PDF presentation in directory (":" for default)
-R refer to requirements of selected sessions
-S soft build: only observe changes of sources, not heap images
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-b build heap images
-c clean build
-d DIR include session directory
-e export files from session specification into file-system
-f fresh build
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
-k KEYWORD check theory sources for conflicts with proposed keywords
-l list session source files
-n no build -- test dependencies only
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v verbose
-x NAME exclude session NAME and all descendants
Build and manage Isabelle sessions, depending on implicit settings:
""" + Library.indent_lines(2, Build_Log.Settings.show()) + "\n",
"B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"N" -> (_ => numa_shuffling = true),
"P:" -> (arg => presentation = Presentation.Context.make(arg)),
"R" -> (_ => requirements = true),
"S" -> (_ => soft_build = true),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
"a" -> (_ => all_sessions = true),
"b" -> (_ => build_heap = true),
"c" -> (_ => clean_build = true),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"e" -> (_ => export_files = true),
"f" -> (_ => fresh_build = true),
"g:" -> (arg => session_groups = session_groups ::: List(arg)),
"j:" -> (arg => max_jobs = Value.Int.parse(arg)),
"k:" -> (arg => check_keywords = check_keywords + arg),
"l" -> (_ => list_files = true),
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
val sessions = getopts(args)
val progress = new Console_Progress(verbose = verbose)
val start_date = Date.now()
if (verbose) {
progress.echo(
"Started at " + Build_Log.print_date(start_date) +
" (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
progress.echo(Build_Log.Settings.show() + "\n")
}
val results =
progress.interrupt_handler {
build(options,
selection = Sessions.Selection(
requirements = requirements,
all_sessions = all_sessions,
base_sessions = base_sessions,
exclude_session_groups = exclude_session_groups,
exclude_sessions = exclude_sessions,
session_groups = session_groups,
sessions = sessions),
presentation = presentation,
progress = progress,
check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME),
build_heap = build_heap,
clean_build = clean_build,
dirs = dirs,
select_dirs = select_dirs,
numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
max_jobs = max_jobs,
list_files = list_files,
check_keywords = check_keywords,
fresh_build = fresh_build,
no_build = no_build,
soft_build = soft_build,
verbose = verbose,
export_files = export_files)
}
val end_date = Date.now()
val elapsed_time = end_date.time - start_date.time
if (verbose) {
progress.echo("\nFinished at " + Build_Log.print_date(end_date))
}
val total_timing =
results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
copy(elapsed = elapsed_time)
progress.echo(total_timing.message_resources)
sys.exit(results.rc)
})
/* build logic image */
def build_logic(options: Options, logic: String,
progress: Progress = new Progress,
build_heap: Boolean = false,
dirs: List[Path] = Nil,
fresh: Boolean = false,
strict: Boolean = false): Int =
{
val selection = Sessions.Selection.session(logic)
val rc =
if (!fresh && build(options, selection = selection,
build_heap = build_heap, no_build = true, dirs = dirs).ok) Process_Result.RC.ok
else {
progress.echo("Build started for Isabelle/" + logic + " ...")
Build.build(options, selection = selection, progress = progress,
build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc
}
if (strict && rc != Process_Result.RC.ok) error("Failed to build Isabelle/" + logic) else rc
}
}
diff --git a/src/Tools/VSCode/src/preview_panel.scala b/src/Tools/VSCode/src/preview_panel.scala
--- a/src/Tools/VSCode/src/preview_panel.scala
+++ b/src/Tools/VSCode/src/preview_panel.scala
@@ -1,46 +1,51 @@
/* Title: Tools/VSCode/src/preview_panel.scala
Author: Makarius
HTML document preview.
*/
package isabelle.vscode
import isabelle._
import java.io.{File => JFile}
class Preview_Panel(resources: VSCode_Resources)
{
private val pending = Synchronized(Map.empty[JFile, Int])
def request(file: JFile, column: Int): Unit =
pending.change(map => map + (file -> column))
def flush(channel: Channel): Boolean =
{
pending.change_result(map =>
{
val map1 =
map.iterator.foldLeft(map) {
case (m, (file, column)) =>
resources.get_model(file) match {
case Some(model) =>
val snapshot = model.snapshot()
if (snapshot.is_outdated) m
else {
- val html_context = Presentation.html_context()
+ val html_context =
+ new Presentation.HTML_Context {
+ override def root_dir: Path = Path.current
+ override def theory_session(name: Document.Node.Name): Sessions.Info =
+ resources.sessions_structure(resources.session_base.theory_qualifier(name))
+ }
val document =
Presentation.html_document(snapshot, html_context, Presentation.elements2)
channel.write(LSP.Preview_Response(file, column, document.title, document.content))
m - file
}
case None => m - file
}
}
(map1.nonEmpty, map1)
})
}
}
diff --git a/src/Tools/jEdit/src/document_model.scala b/src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala
+++ b/src/Tools/jEdit/src/document_model.scala
@@ -1,703 +1,709 @@
/* Title: Tools/jEdit/src/document_model.scala
Author: Fabian Immler, TU Munich
Author: Makarius
Document model connected to jEdit buffer or external file: content of theory
node or auxiliary file (blob).
*/
package isabelle.jedit
import isabelle._
import java.io.{File => JFile}
import scala.collection.mutable
import scala.annotation.tailrec
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.Buffer
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
object Document_Model
{
/* document models */
sealed case class State(
models: Map[Document.Node.Name, Document_Model] = Map.empty,
buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty,
overlays: Document.Overlays = Document.Overlays.empty)
{
def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
for {
(node_name, model) <- models.iterator
if model.isInstanceOf[File_Model]
} yield (node_name, model.asInstanceOf[File_Model])
def document_blobs: Document.Blobs =
Document.Blobs(
(for {
(node_name, model) <- models.iterator
blob <- model.get_blob
} yield (node_name -> blob)).toMap)
def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer)
: (Buffer_Model, State) =
{
val old_model =
models.get(node_name) match {
case Some(file_model: File_Model) => Some(file_model)
case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
case _ => None
}
val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model)
(buffer_model,
copy(models = models + (node_name -> buffer_model),
buffer_models = buffer_models + (buffer -> buffer_model)))
}
def close_buffer(buffer: JEditBuffer): State =
{
buffer_models.get(buffer) match {
case None => this
case Some(buffer_model) =>
val file_model = buffer_model.exit()
copy(models = models + (file_model.node_name -> file_model),
buffer_models = buffer_models - buffer)
}
}
def provide_file(session: Session, node_name: Document.Node.Name, text: String): State =
if (models.isDefinedAt(node_name)) this
else {
val edit = Text.Edit.insert(0, text)
val model = File_Model.init(session, node_name, text, pending_edits = List(edit))
copy(models = models + (node_name -> model))
}
}
private val state = Synchronized(State()) // owned by GUI thread
def reset(): Unit = state.change(_ => State())
def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
def document_blobs(): Document.Blobs = state.value.document_blobs
/* bibtex */
def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
Bibtex.entries_iterator(state.value.models)
def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
: Option[Completion.Result] =
Bibtex.completion(history, rendering, caret, state.value.models)
/* overlays */
def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
state.value.overlays(name)
def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args)))
def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args)))
/* sync external files */
def sync_files(changed_files: Set[JFile]): Boolean =
{
state.change_result(st =>
{
val changed_models =
(for {
(node_name, model) <- st.file_models_iterator
file <- model.file if changed_files(file)
text <- PIDE.resources.read_file_content(node_name)
if model.content.text != text
} yield {
val content = Document_Model.File_Content(text)
val edits = Text.Edit.replace(0, model.content.text, text)
(node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
}).toList
if (changed_models.isEmpty) (false, st)
else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _)))
})
}
/* syntax */
def syntax_changed(names: List[Document.Node.Name]): Unit =
{
GUI_Thread.require {}
val models = state.value.models
for (name <- names.iterator; model <- models.get(name)) {
model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => }
}
}
/* init and exit */
def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model =
{
GUI_Thread.require {}
state.change_result(st =>
st.buffer_models.get(buffer) match {
case Some(buffer_model) if buffer_model.node_name == node_name =>
buffer_model.init_token_marker()
(buffer_model, st)
case _ =>
val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer)
buffer.propertiesChanged()
res
})
}
def exit(buffer: Buffer): Unit =
{
GUI_Thread.require {}
state.change(st =>
if (st.buffer_models.isDefinedAt(buffer)) {
val res = st.close_buffer(buffer)
buffer.propertiesChanged()
res
}
else st)
}
def provide_files(session: Session, files: List[(Document.Node.Name, String)]): Unit =
{
GUI_Thread.require {}
state.change(st =>
files.foldLeft(st) {
case (st1, (node_name, text)) => st1.provide_file(session, node_name, text)
})
}
/* required nodes */
def required_nodes(): Set[Document.Node.Name] =
(for {
(node_name, model) <- state.value.models.iterator
if model.node_required
} yield node_name).toSet
def node_required(
name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false): Unit =
{
GUI_Thread.require {}
val changed =
state.change_result(st =>
st.models.get(name) match {
case None => (false, st)
case Some(model) =>
val required = if (toggle) !model.node_required else set
model match {
case model1: File_Model if required != model1.node_required =>
(true, st.copy(models = st.models + (name -> model1.copy(node_required = required))))
case model1: Buffer_Model if required != model1.node_required =>
model1.set_node_required(required); (true, st)
case _ => (false, st)
}
})
if (changed) {
PIDE.plugin.options_changed()
PIDE.editor.flush()
}
}
def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit =
Document_Model.get(view.getBuffer).foreach(model =>
node_required(model.node_name, toggle = toggle, set = set))
/* flushed edits */
def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
{
GUI_Thread.require {}
state.change_result(st =>
{
val doc_blobs = st.document_blobs
val buffer_edits =
(for {
(_, model) <- st.buffer_models.iterator
edit <- model.flush_edits(doc_blobs, hidden).iterator
} yield edit).toList
val file_edits =
(for {
(node_name, model) <- st.file_models_iterator
(edits, model1) <- model.flush_edits(doc_blobs, hidden)
} yield (edits, node_name -> model1)).toList
val model_edits = buffer_edits ::: file_edits.flatMap(_._1)
val purge_edits =
if (purge) {
val purged =
(for ((node_name, model) <- st.file_models_iterator)
yield (node_name -> model.purge_edits(doc_blobs))).toList
val imports =
{
val open_nodes =
(for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList
val touched_nodes = model_edits.map(_._1)
val pending_nodes = for ((node_name, None) <- purged) yield node_name
(open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
}
val retain = PIDE.resources.dependencies(imports).theories.toSet
for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits)
yield edit
}
else Nil
val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1))
PIDE.plugin.file_watcher.purge(
(for {
(_, model) <- st1.file_models_iterator
file <- model.file
} yield file.getParentFile).toSet)
((doc_blobs, model_edits ::: purge_edits), st1)
})
}
/* file content */
sealed case class File_Content(text: String)
{
lazy val bytes: Bytes = Bytes(Symbol.encode(text))
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
lazy val bibtex_entries: List[Text.Info[String]] =
try { Bibtex.entries(text) }
catch { case ERROR(_) => Nil }
}
/* HTTP preview */
private val plain_text_prefix = "plain_text="
def open_preview(view: View, plain_text: Boolean): Unit =
{
Document_Model.get(view.getBuffer) match {
case Some(model) =>
val name = model.node_name
val url =
PIDE.plugin.http_server.url + PIDE.plugin.http_root + "/preview?" +
(if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
PIDE.editor.hyperlink_url(url).follow(view)
case _ =>
}
}
def http_handlers(http_root: String): List[HTTP.Handler] =
{
val fonts_root = http_root + "/fonts"
val preview_root = http_root + "/preview"
val html =
HTTP.Handler.get(preview_root, arg =>
for {
query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode)
name = Library.perhaps_unprefix(plain_text_prefix, query)
model <- get(PIDE.resources.node_name(name))
}
yield {
val snapshot = model.await_stable_snapshot()
- val html_context = Presentation.html_context()
+ val html_context =
+ new Presentation.HTML_Context {
+ override def root_dir: Path = Path.current
+ override def theory_session(name: Document.Node.Name): Sessions.Info =
+ PIDE.resources.sessions_structure(
+ PIDE.resources.session_base.theory_qualifier(name))
+ }
val document =
Presentation.html_document(
snapshot, html_context, Presentation.elements2,
plain_text = query.startsWith(plain_text_prefix),
fonts_css = HTML.fonts_css_dir(http_root))
HTTP.Response.html(document.content)
})
List(HTTP.welcome(http_root), HTTP.fonts(fonts_root), html)
}
}
sealed abstract class Document_Model extends Document.Model
{
/* perspective */
def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
def node_perspective(
doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) =
{
GUI_Thread.require {}
if (Isabelle.continuous_checking && is_theory) {
val snapshot = this.snapshot()
val reparse = snapshot.node.load_commands_changed(doc_blobs)
val perspective =
if (hidden) Text.Perspective.empty
else {
val view_ranges = document_view_ranges(snapshot)
val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node)
Text.Perspective(view_ranges ::: load_ranges)
}
val overlays = PIDE.editor.node_overlays(node_name)
(reparse, Document.Node.Perspective(node_required, perspective, overlays))
}
else (false, Document.Node.no_perspective_text)
}
/* snapshot */
@tailrec final def await_stable_snapshot(): Document.Snapshot =
{
val snapshot = this.snapshot()
if (snapshot.is_outdated) {
PIDE.options.seconds("editor_output_delay").sleep()
await_stable_snapshot()
}
else snapshot
}
}
object File_Model
{
def empty(session: Session): File_Model =
File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
false, Document.Node.no_perspective_text, Nil)
def init(session: Session,
node_name: Document.Node.Name,
text: String,
node_required: Boolean = false,
last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
pending_edits: List[Text.Edit] = Nil): File_Model =
{
val file = JEdit_Lib.check_file(node_name.node)
file.foreach(PIDE.plugin.file_watcher.register_parent(_))
val content = Document_Model.File_Content(text)
val node_required1 = node_required || File_Format.registry.is_theory(node_name)
File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
}
}
case class File_Model(
session: Session,
node_name: Document.Node.Name,
file: Option[JFile],
content: Document_Model.File_Content,
node_required: Boolean,
last_perspective: Document.Node.Perspective_Text,
pending_edits: List[Text.Edit]) extends Document_Model
{
/* text */
def get_text(range: Text.Range): Option[String] =
range.try_substring(content.text)
/* header */
def node_header: Document.Node.Header =
PIDE.resources.special_header(node_name) getOrElse
PIDE.resources.check_thy(node_name, Scan.char_reader(content.text), strict = false)
/* content */
def node_position(offset: Text.Offset): Line.Node_Position =
Line.Node_Position(node_name.node,
Line.Position.zero.advance(content.text.substring(0, offset)))
def get_blob: Option[Document.Blob] =
if (is_theory) None
else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
def bibtex_entries: List[Text.Info[String]] =
if (Bibtex.is_bibtex(node_name.node)) content.bibtex_entries else Nil
/* edits */
def update_text(text: String): Option[File_Model] =
Text.Edit.replace(0, content.text, text) match {
case Nil => None
case edits =>
val content1 = Document_Model.File_Content(text)
val pending_edits1 = pending_edits ::: edits
Some(copy(content = content1, pending_edits = pending_edits1))
}
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean)
: Option[(List[Document.Edit_Text], File_Model)] =
{
val (reparse, perspective) = node_perspective(doc_blobs, hidden)
if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
val edits = node_edits(node_header, pending_edits, perspective)
Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
}
else None
}
def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
if (pending_edits.nonEmpty ||
!File_Format.registry.is_theory(node_name) &&
(node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
else {
val text_edits = List(Text.Edit.remove(0, content.text))
Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text))
}
/* snapshot */
def is_stable: Boolean = pending_edits.isEmpty
def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
}
case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
extends Document_Model
{
/* text */
def get_text(range: Text.Range): Option[String] =
JEdit_Lib.get_text(buffer, range)
/* header */
def node_header(): Document.Node.Header =
{
GUI_Thread.require {}
PIDE.resources.special_header(node_name) getOrElse
JEdit_Lib.buffer_lock(buffer) {
PIDE.resources.check_thy(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
}
}
/* perspective */
// owned by GUI thread
private var _node_required = false
def node_required: Boolean = _node_required
def set_node_required(b: Boolean): Unit = GUI_Thread.require { _node_required = b }
def document_view_iterator: Iterator[Document_View] =
for {
text_area <- JEdit_Lib.jedit_text_areas(buffer)
doc_view <- Document_View.get(text_area)
} yield doc_view
override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
{
GUI_Thread.require {}
(for {
doc_view <- document_view_iterator
range <- doc_view.perspective(snapshot).ranges.iterator
} yield range).toList
}
/* blob */
// owned by GUI thread
private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None
private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
def get_blob: Option[Document.Blob] =
GUI_Thread.require {
if (is_theory) None
else {
val (bytes, text, chunk) =
_blob match {
case Some(x) => x
case None =>
val bytes = PIDE.resources.make_file_content(buffer)
val text = buffer.getText(0, buffer.getLength)
val chunk = Symbol.Text_Chunk(text)
val x = (bytes, text, chunk)
_blob = Some(x)
x
}
val changed = pending_edits.nonEmpty
Some(Document.Blob(bytes, text, chunk, changed))
}
}
/* bibtex entries */
// owned by GUI thread
private var _bibtex_entries: Option[List[Text.Info[String]]] = None
private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
def bibtex_entries: List[Text.Info[String]] =
GUI_Thread.require {
if (Bibtex.is_bibtex(node_name.node)) {
_bibtex_entries match {
case Some(entries) => entries
case None =>
val text = JEdit_Lib.buffer_text(buffer)
val entries =
try { Bibtex.entries(text) }
catch { case ERROR(msg) => Output.warning(msg); Nil }
_bibtex_entries = Some(entries)
entries
}
}
else Nil
}
/* pending edits */
private object pending_edits
{
private val pending = new mutable.ListBuffer[Text.Edit]
private var last_perspective = Document.Node.no_perspective_text
def nonEmpty: Boolean = synchronized { pending.nonEmpty }
def get_edits: List[Text.Edit] = synchronized { pending.toList }
def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
synchronized { last_perspective = perspective }
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
synchronized {
GUI_Thread.require {}
val edits = get_edits
val (reparse, perspective) = node_perspective(doc_blobs, hidden)
if (reparse || edits.nonEmpty || last_perspective != perspective) {
pending.clear()
last_perspective = perspective
node_edits(node_header(), edits, perspective)
}
else Nil
}
def edit(edits: List[Text.Edit]): Unit = synchronized
{
GUI_Thread.require {}
reset_blob()
reset_bibtex_entries()
for (doc_view <- document_view_iterator)
doc_view.rich_text_area.active_reset()
pending ++= edits
PIDE.editor.invoke()
}
}
def is_stable: Boolean = !pending_edits.nonEmpty
def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
pending_edits.flush_edits(doc_blobs, hidden)
/* buffer listener */
private val buffer_listener: BufferListener = new BufferAdapter
{
override def contentInserted(buffer: JEditBuffer,
start_line: Int, offset: Int, num_lines: Int, length: Int): Unit =
{
pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
}
override def preContentRemoved(buffer: JEditBuffer,
start_line: Int, offset: Int, num_lines: Int, removed_length: Int): Unit =
{
pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
}
}
/* syntax */
def syntax_changed(): Unit =
{
JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
invoke(text_area)
buffer.invalidateCachedFoldLevels()
}
def init_token_marker(): Unit =
{
Isabelle.buffer_token_marker(buffer) match {
case Some(marker) if marker != buffer.getTokenMarker =>
buffer.setTokenMarker(marker)
syntax_changed()
case _ =>
}
}
/* init */
def init(old_model: Option[File_Model]): Buffer_Model =
{
GUI_Thread.require {}
old_model match {
case None =>
pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
case Some(file_model) =>
set_node_required(file_model.node_required)
pending_edits.set_last_perspective(file_model.last_perspective)
pending_edits.edit(
file_model.pending_edits :::
Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
}
buffer.addBufferListener(buffer_listener)
init_token_marker()
this
}
/* exit */
def exit(): File_Model =
{
GUI_Thread.require {}
buffer.removeBufferListener(buffer_listener)
init_token_marker()
File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required,
pending_edits.get_last_perspective, pending_edits.get_edits)
}
}