diff --git a/.hgignore b/.hgignore --- a/.hgignore +++ b/.hgignore @@ -1,22 +1,21 @@ syntax: glob *~ *.class *.jar *.marks *.orig *.rej .DS_Store .swp syntax: regexp ^contrib ^heaps/ ^browser_info/ ^doc/.*\.pdf -^lib/classes/ ^src/Tools/VSCode/out/ ^src/Tools/VSCode/extension/node_modules/ ^Admin/jenkins/ci-extras/target/ diff --git a/Admin/build b/Admin/build deleted file mode 100755 --- a/Admin/build +++ /dev/null @@ -1,88 +0,0 @@ -#!/usr/bin/env bash -# -# Administrative build for Isabelle source distribution. - -## directory layout - -if [ -z "$ISABELLE_HOME" ]; then - unset CDPATH - ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" - ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" -fi - - -## diagnostics - -PRG="$(basename "$0")" - -function usage() -{ - cat <&2 - exit 2 -} - - -## process command line - -[ "$#" -eq 0 ] && usage - -MODULES="$@"; shift "$#" - - -## modules - -function build_all () -{ - build_browser - build_setup build -} - - -function build_browser () -{ - pushd "$ISABELLE_HOME/lib/browser" >/dev/null - "$ISABELLE_TOOL" env ./build || exit $? - popd >/dev/null -} - - -function build_setup () -{ - rm -rf \ - "$ISABELLE_HOME/lib/classes/Pure.jar" \ - "$ISABELLE_HOME/lib/classes/Pure.shasum" \ - "$ISABELLE_HOME/src/Tools/jEdit/dist" - env ISABELLE_SETUP_CLASSPATH_SKIP=true "$ISABELLE_TOOL" java isabelle.setup.Setup "$@" -} - - -## main - -for MODULE in $MODULES -do - case $MODULE in - all) build_all;; - browser) build_browser;; - jars) build_setup build;; - jars_fresh) build_setup build_fresh;; - *) fail "Bad module $MODULE" - esac -done diff --git a/Admin/build_history b/Admin/build_history --- a/Admin/build_history +++ b/Admin/build_history @@ -1,9 +1,9 @@ #!/usr/bin/env bash # # DESCRIPTION: build history versions from another repository clone unset CDPATH THIS="$(cd "$(dirname "$0")"; pwd)" -"$THIS/build" jars > /dev/null || exit $? +env ISABELLE_SETUP_CLASSPATH_SKIP=true "$THIS/../bin/isabelle" java isabelle.setup.Setup build > /dev/null || exit $? exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@" diff --git a/Admin/build_release b/Admin/build_release --- a/Admin/build_release +++ b/Admin/build_release @@ -1,9 +1,9 @@ #!/usr/bin/env bash # # DESCRIPTION: build full Isabelle distribution from repository unset CDPATH THIS="$(cd "$(dirname "$0")"; pwd)" -"$THIS/build" jars || exit $? +env ISABELLE_SETUP_CLASSPATH_SKIP=true "$THIS/../bin/isabelle" java isabelle.setup.Setup build > /dev/null || exit $? exec "$THIS/../bin/isabelle_java" isabelle.Build_Release "$@" diff --git a/Admin/components/components.sha1 b/Admin/components/components.sha1 --- a/Admin/components/components.sha1 +++ b/Admin/components/components.sha1 @@ -1,421 +1,423 @@ 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 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 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 f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.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 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 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 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 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 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 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 0fbc826e4fcb95bb9e1814642f7fce788e7fe1c3 naproche-20210122-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 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 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 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 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 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 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 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 869ea6d8ea35c8ba68d7fcb028f16b2b7064c5fd vampire-1.0.tar.gz 399f687b56575b93e730f68c91c989cb48aa34d8 vampire-4.2.2.tar.gz 98c5c79fef7256db9f64c8feea2edef0a789ce46 verit-2016post.tar.gz 52ba18a6c96b53c5ae9b179d5a805a0c08f1da6d verit-2020.10-rmx-1.tar.gz b6706e74e20e14038e9b38f0acdb5639a134246a verit-2020.10-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 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 diff --git a/Admin/components/main b/Admin/components/main --- a/Admin/components/main +++ b/Admin/components/main @@ -1,31 +1,31 @@ #main components for repository clones or release bundles gnu-utils-20210414 bash_process-1.2.4-2 bib2xhtml-20190409 csdp-6.1.1 cvc4-1.8 e-2.5-1 flatlaf-1.2 idea-icons-20210508 isabelle_fonts-20210322 -isabelle_setup-20210715 +isabelle_setup-20210716-1 jdk-15.0.2+7 jedit-20210715 jfreechart-1.5.1 jortho-1.0-2 kodkodi-1.5.6-1 nunchaku-0.5 opam-2.0.7 polyml-5.8.2 postgresql-42.2.18 scala-2.13.5 smbc-0.4.1 spass-3.8ds-2 sqlite-jdbc-3.34.0 ssh-java-20190323 stack-2.5.1 vampire-4.2.2 verit-2020.10-rmx-1 xz-java-1.8 z3-4.4.0pre-3 zipperposition-2.0-1 diff --git a/bin/isabelle b/bin/isabelle --- a/bin/isabelle +++ b/bin/isabelle @@ -1,51 +1,51 @@ #!/usr/bin/env bash # # Author: Markus Wenzel, TU Muenchen # # Isabelle tool wrapper. unset CDPATH if [ -L "$0" ]; then TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" fi ## settings PRG="$(basename "$0")" ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 ## external tool (shell script) if [ "$#" -ge 1 -a "$1" != "-?" ] then TOOL_NAME="$1" splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}") for DIR in "${TOOLS[@]}" do TOOL="$DIR/$TOOL_NAME" case "$TOOL" in *~ | *.orig) ;; *) if [ -f "$TOOL" -a -x "$TOOL" ]; then shift exec "$TOOL" "$@" fi ;; esac done fi ## internal tool or usage (Scala) -isabelle_admin_build jars || exit $? +isabelle_scala_build || exit $? eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)" exec isabelle java "${JAVA_ARGS[@]}" isabelle.Isabelle_Tool "$@" diff --git a/etc/components b/etc/components --- a/etc/components +++ b/etc/components @@ -1,9 +1,10 @@ #built-in components src/Tools/jEdit +src/Tools/GraphBrowser src/Tools/Graphview src/Tools/VSCode src/HOL/Mutabelle src/HOL/Library/Sum_of_Squares src/HOL/SPARK src/HOL/Tools src/HOL/TPTP diff --git a/lib/Tools/components b/lib/Tools/components --- a/lib/Tools/components +++ b/lib/Tools/components @@ -1,166 +1,166 @@ #!/usr/bin/env bash # # Author: Makarius # # DESCRIPTION: resolve Isabelle components ## diagnostics PRG="$(basename "$0")" function usage() { echo echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]" echo echo " Options are:" echo " -I init user settings" echo " -R URL component repository (default \$ISABELLE_COMPONENT_REPOSITORY)" echo " -a resolve all missing components" echo " -l list status" echo " -u DIR update \$ISABELLE_HOME_USER/etc/components: add directory" echo " -x DIR update \$ISABELLE_HOME_USER/etc/components: remove directory" echo echo " Resolve Isabelle components via download and installation: given COMPONENTS" echo " are identified via base name. Further operations manage etc/settings and" echo " etc/components in \$ISABELLE_HOME_USER." echo echo " ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\"" echo " ISABELLE_HOME_USER=\"$ISABELLE_HOME_USER\"" echo exit 1 } function fail() { echo "$1" >&2 exit 2 } ## process command line #options INIT_SETTINGS="" COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY" ALL_MISSING="" LIST_ONLY="" declare -a UPDATE_COMPONENTS=() while getopts "IR:alu:x:" OPT do case "$OPT" in I) INIT_SETTINGS="true" ;; R) COMPONENT_REPOSITORY="$OPTARG" ;; a) ALL_MISSING="true" ;; l) LIST_ONLY="true" ;; u) UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="+$OPTARG" ;; x) UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="-$OPTARG" ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args [ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" -a "${#UPDATE_COMPONENTS[@]}" -eq 0 ] && usage if [ -z "$ALL_MISSING" ]; then splitarray ":" "$@" else splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@" fi declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}") ## main splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}") splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}") if [ -n "$INIT_SETTINGS" ]; then SETTINGS="$ISABELLE_HOME_USER/etc/settings" SETTINGS_CONTENT='init_components "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}" "$ISABELLE_HOME/Admin/components/main"' if [ ! -e "$SETTINGS" ]; then echo "Initializing \"$SETTINGS\"" mkdir -p "$(dirname "$SETTINGS")" { echo "#-*- shell-script -*- :mode=shellscript:" echo echo "$SETTINGS_CONTENT" } > "$SETTINGS" elif grep "init_components.*components/main" "$SETTINGS" >/dev/null 2>/dev/null then : else echo "User settings file already exists!" echo echo "Edit \"$SETTINGS\" manually" echo "and add the following line near its start:" echo echo " $SETTINGS_CONTENT" echo fi elif [ -n "$LIST_ONLY" ]; then echo echo "Available components:" for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo " $NAME"; done echo echo "Missing components:" for NAME in "${MISSING_COMPONENTS[@]}"; do echo " $NAME"; done elif [ "${#UPDATE_COMPONENTS[@]}" -ne 0 ]; then - isabelle_admin_build jars || exit $? + isabelle_scala_build || exit $? exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}" else for NAME in "${SELECTED_COMPONENTS[@]}" do BASE_NAME="$(basename "$NAME")" FULL_NAME="" for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}" do [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X" done if [ -z "$FULL_NAME" ]; then echo "Ignoring irrelevant component \"$NAME\"" elif [ -d "$FULL_NAME" ]; then echo "Skipping existing component \"$FULL_NAME\"" else if [ ! -e "${FULL_NAME}.tar.gz" ]; then REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz" type -p curl > /dev/null || fail "Cannot download files: missing curl" echo "Getting \"$REMOTE\"" mkdir -p "$(dirname "$FULL_NAME")" if curl --fail --silent --location "$REMOTE" > "${FULL_NAME}.tar.gz.part" then mv -f "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz" else rm -f "${FULL_NAME}.tar.gz.part" fail "Failed to download \"$REMOTE\"" fi fi if [ -e "${FULL_NAME}.tar.gz" ]; then echo "Unpacking \"${FULL_NAME}.tar.gz\"" tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2 fi fi done fi diff --git a/lib/Tools/console b/lib/Tools/console --- a/lib/Tools/console +++ b/lib/Tools/console @@ -1,19 +1,19 @@ #!/usr/bin/env bash # # Author: Makarius # # DESCRIPTION: raw ML process (interactive mode) -isabelle_admin_build jars || exit $? +isabelle_scala_build || exit $? eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)" mkdir -p "$ISABELLE_TMP_PREFIX" || exit $? if type -p "$ISABELLE_LINE_EDITOR" > /dev/null then exec "$ISABELLE_LINE_EDITOR" isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" else echo >&2 "### No line editor: \"$ISABELLE_LINE_EDITOR\"" exec isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" fi diff --git a/lib/Tools/scala b/lib/Tools/scala --- a/lib/Tools/scala +++ b/lib/Tools/scala @@ -1,21 +1,21 @@ #!/usr/bin/env bash # # Author: Makarius # # DESCRIPTION: invoke Scala within the Isabelle environment -isabelle_admin_build jars || exit $? +isabelle_scala_build || exit $? eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)" declare -a SCALA_ARGS=() for ARG in "${JAVA_ARGS[@]}" do SCALA_ARGS["${#SCALA_ARGS[@]}"]="-J$ARG" done classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH classpath "$CLASSPATH"; unset CLASSPATH isabelle_scala scala "${SCALA_ARGS[@]}" \ -classpath "$(platform_path "$ISABELLE_CLASSPATH")" \ -Disabelle.scala.classpath="$(platform_path "$ISABELLE_CLASSPATH")" "$@" diff --git a/lib/Tools/scalac b/lib/Tools/scalac --- a/lib/Tools/scalac +++ b/lib/Tools/scalac @@ -1,13 +1,13 @@ #!/usr/bin/env bash # # Author: Makarius # # DESCRIPTION: invoke Scala compiler within the Isabelle environment -isabelle_admin_build jars || exit $? +isabelle_scala_build || exit $? classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH classpath "$CLASSPATH"; unset CLASSPATH isabelle_scala scalac -Dfile.encoding=UTF-8 \ -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@" diff --git a/lib/browser/build b/lib/browser/build deleted file mode 100755 --- a/lib/browser/build +++ /dev/null @@ -1,72 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Makarius -# -# mk - build graph browser -# -# Requires proper Isabelle settings environment. - - -## diagnostics - -function fail() -{ - echo "$1" >&2 - exit 2 -} - -[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment" - - -## dependencies - -declare -a SOURCES=( - GraphBrowser/AWTFontMetrics.java - GraphBrowser/AbstractFontMetrics.java - GraphBrowser/Box.java - GraphBrowser/Console.java - GraphBrowser/DefaultFontMetrics.java - GraphBrowser/Directory.java - GraphBrowser/DummyVertex.java - GraphBrowser/Graph.java - GraphBrowser/GraphBrowser.java - GraphBrowser/GraphBrowserFrame.java - GraphBrowser/GraphView.java - GraphBrowser/NormalVertex.java - GraphBrowser/ParseError.java - GraphBrowser/Region.java - GraphBrowser/Spline.java - GraphBrowser/TreeBrowser.java - GraphBrowser/TreeNode.java - GraphBrowser/Vertex.java - awtUtilities/Border.java - awtUtilities/MessageDialog.java - awtUtilities/TextFrame.java -) - -TARGET="$ISABELLE_HOME/lib/browser/GraphBrowser.jar" - - -## main - -OUTDATED=false - -for SOURCE in "${SOURCES[@]}" -do - [ ! -e "$SOURCE" ] && fail "Missing source file: $SOURCE" - [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true -done - -if [ "$OUTDATED" = true ] -then - echo >&2 "### Building graph browser ..." - - rm -rf classes && mkdir classes - - isabelle_jdk javac -d classes -Xlint:-options -source 7 -target 7 "${SOURCES[@]}" || \ - fail "Failed to compile sources" - isabelle_jdk jar cf "$(platform_path "$TARGET")" -C classes . || - fail "Failed to produce $TARGET" - - rm -rf classes -fi diff --git a/lib/scripts/getfunctions b/lib/scripts/getfunctions --- a/lib/scripts/getfunctions +++ b/lib/scripts/getfunctions @@ -1,309 +1,316 @@ # -*- shell-script -*- :mode=shellscript: # # Author: Makarius # # Isabelle shell functions, with on-demand re-initialization for # non-interactive bash processess. NB: bash shell functions are not portable # and may be dropped by aggressively POSIX-conformant versions of /bin/sh. unset CDPATH if type splitarray >/dev/null 2>/dev/null then : else if [ "$OSTYPE" = cygwin ]; then function platform_path() { cygpath -i -C UTF8 -w -p "$@"; } function standard_path() { cygpath -i -u -p "$@" | tr -d '\r'; } else function platform_path() { echo "$@"; } function standard_path() { echo "$@"; } fi export -f platform_path standard_path #GNU tar (notably on macOS) function tar() { if [ -f "$ISABELLE_TAR" ]; then "$ISABELLE_TAR" "$@" else "$(type -P tar)" "$@" fi } export -f tar #OCaml management via OPAM function isabelle_opam () { if [ -z "$ISABELLE_OPAM" ]; then echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2 return 127 else env OPAMROOT="$ISABELLE_OPAM_ROOT" OPAMCOLOR="never" "$ISABELLE_OPAM" "$@" fi } export -f isabelle_opam #GHC management via Stack function isabelle_stack () { if [ -z "$ISABELLE_STACK" ]; then echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2 return 127 else env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" --resolver "$ISABELLE_STACK_RESOLVER" --compiler "$ISABELLE_GHC_VERSION" "$@" fi } export -f isabelle_stack #robust invocation via ISABELLE_JDK_HOME function isabelle_jdk () { if [ -z "$ISABELLE_JDK_HOME" ]; then echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2 return 127 else local PRG="$1"; shift "$ISABELLE_JDK_HOME/bin/$PRG" "$@" fi } export -f isabelle_jdk #robust invocation via JAVA_HOME function isabelle_java () { if [ -z "$JAVA_HOME" ]; then echo "Unknown JAVA_HOME -- Java unavailable" >&2 return 127 else local PRG="$1"; shift "$JAVA_HOME/bin/$PRG" "$@" fi } export -f isabelle_java #robust invocation via SCALA_HOME function isabelle_scala () { if [ -z "$JAVA_HOME" ]; then echo "Unknown JAVA_HOME -- Java unavailable" >&2 return 127 elif [ -z "$SCALA_HOME" ]; then echo "Unknown SCALA_HOME -- Scala unavailable" >&2 return 127 else local PRG="$1"; shift "$SCALA_HOME/bin/$PRG" "$@" fi } export -f isabelle_scala #classpath function classpath () { local X="" for X in "$@" do if [ -z "$ISABELLE_CLASSPATH" ]; then ISABELLE_CLASSPATH="$X" elif [ -n "$X" ]; then ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X" fi done export ISABELLE_CLASSPATH } export -f classpath #java_library function java_library () { local X="" for X in "$@" do case "$ISABELLE_PLATFORM_FAMILY" in linux) if [ -z "$LD_LIBRARY_PATH" ]; then export LD_LIBRARY_PATH="$X" else export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$X" fi ;; macos) if [ -z "$JAVA_LIBRARY_PATH" ]; then export JAVA_LIBRARY_PATH="$X" else export JAVA_LIBRARY_PATH="$JAVA_LIBRARY_PATH:$X" fi ;; windows) if [ -z "$PATH" ]; then export PATH="$X" else export PATH="$PATH:$X" fi ;; esac done export ISABELLE_CLASSPATH } export -f java_library #Isabelle fonts function isabelle_fonts () { local X="" for X in "$@" do if [ -z "$ISABELLE_FONTS" ]; then ISABELLE_FONTS="$X" else ISABELLE_FONTS="$ISABELLE_FONTS:$X" fi done export ISABELLE_FONTS } export -f isabelle_fonts function isabelle_fonts_hidden () { local X="" for X in "$@" do if [ -z "$ISABELLE_FONTS_HIDDEN" ]; then ISABELLE_FONTS_HIDDEN="$X" else ISABELLE_FONTS_HIDDEN="$ISABELLE_FONTS_HIDDEN:$X" fi done export ISABELLE_FONTS_HIDDEN } export -f isabelle_fonts_hidden #Isabelle/Scala services function isabelle_scala_service () { local X="" for X in "$@" do if [ -z "$ISABELLE_SCALA_SERVICES" ]; then ISABELLE_SCALA_SERVICES="$X" else ISABELLE_SCALA_SERVICES="$ISABELLE_SCALA_SERVICES:$X" fi done export ISABELLE_SCALA_SERVICES } export -f isabelle_scala_service #Special directories function isabelle_directory () { local X="" for X in "$@" do if [ -z "$ISABELLE_DIRECTORIES" ]; then ISABELLE_DIRECTORIES="$X" else ISABELLE_DIRECTORIES="$ISABELLE_DIRECTORIES:$X" fi done export ISABELLE_DIRECTORIES } export -f isabelle_directory -#administrative build -function isabelle_admin_build () +#Isabelle/Scala/Java build +function isabelle_scala_build () { - if [ -e "$ISABELLE_HOME/Admin/build" ]; then - "$ISABELLE_HOME/Admin/build" "$@" + rm -rf \ + "$ISABELLE_HOME/lib/classes/Pure.jar" \ + "$ISABELLE_HOME/lib/classes/Pure.shasum" \ + "$ISABELLE_HOME/src/Tools/jEdit/dist" + if [ "$1" = "fresh" ]; then + CMD="build_fresh" + else + CMD="build" fi + env ISABELLE_SETUP_CLASSPATH_SKIP=true isabelle java isabelle.setup.Setup "$CMD" } -export -f isabelle_admin_build +export -f isabelle_scala_build #arrays function splitarray () { SPLITARRAY=() local IFS="$1"; shift local X="" for X in $* do SPLITARRAY["${#SPLITARRAY[@]}"]="$X" done } export -f splitarray #init component tree function init_component () { local COMPONENT="$1" case "$COMPONENT" in /*) ;; *) echo >&2 "Absolute component path required: \"$COMPONENT\"" exit 2 ;; esac if [ -d "$COMPONENT" ]; then if [ -z "$ISABELLE_COMPONENTS" ]; then ISABELLE_COMPONENTS="$COMPONENT" else ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" fi else echo >&2 "### Missing Isabelle component: \"$COMPONENT\"" if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then ISABELLE_COMPONENTS_MISSING="$COMPONENT" else ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT" fi fi if [ -f "$COMPONENT/etc/settings" ]; then source "$COMPONENT/etc/settings" local RC="$?" if [ "$RC" -ne 0 ]; then echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\"" exit 2 fi fi if [ -f "$COMPONENT/etc/components" ]; then init_components "$COMPONENT" "$COMPONENT/etc/components" fi } export -f init_component #init component forest function init_components () { local REPLY="" local BASE="$1" local CATALOG="$2" local COMPONENT="" local -a COMPONENTS=() if [ ! -f "$CATALOG" ]; then echo >&2 "Bad component catalog file: \"$CATALOG\"" exit 2 fi { while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } do case "$REPLY" in \#* | "") ;; /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;; *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;; esac done } < "$CATALOG" for COMPONENT in "${COMPONENTS[@]}" do init_component "$COMPONENT" done } export -f init_components fi diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala +++ b/src/Pure/Admin/build_release.scala @@ -1,937 +1,936 @@ /* Title: Pure/Admin/build_release.scala Author: Makarius Build full Isabelle distribution from repository. */ package isabelle object Build_Release { /** release context **/ private def execute(dir: Path, script: String): Unit = Isabelle_System.bash(script, cwd = dir.file).check private def execute_tar(dir: Path, args: String, strip: Int = 0): Unit = Isabelle_System.gnutar(args, dir = dir, strip = strip).check object Release_Context { def apply( target_dir: Path, release_name: String = "", components_base: Path = Components.default_components_base, progress: Progress = new Progress): Release_Context = { val date = Date.now() val dist_name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date)) val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute new Release_Context(release_name, dist_name, dist_dir, components_base, progress) } } class Release_Context private[Build_Release]( val release_name: String, val dist_name: String, val dist_dir: Path, val components_base: Path, val progress: Progress) { override def toString: String = dist_name val isabelle: Path = Path.explode(dist_name) val isabelle_dir: Path = dist_dir + isabelle val isabelle_archive: Path = dist_dir + isabelle.tar.gz val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") def other_isabelle(dir: Path): Other_Isabelle = Other_Isabelle(dir + isabelle, isabelle_identifier = dist_name + "-build", progress = progress) def make_announce(id: String): Unit = { if (release_name.isEmpty) { File.write(isabelle_dir + Path.explode("ANNOUNCE"), """ IMPORTANT NOTE ============== This is a snapshot of Isabelle/""" + id + """ from the repository. """) } } def make_contrib(): Unit = { Isabelle_System.make_directory(Components.contrib(isabelle_dir)) File.write(Components.contrib(isabelle_dir, name = "README"), """This directory contains add-on components that contribute to the main Isabelle distribution. Separate licensing conditions apply, see each directory individually. """) } def bundle_info(platform: Platform.Family.Value): Bundle_Info = platform match { case Platform.Family.linux_arm => Bundle_Info(platform, "Linux (ARM)", dist_name + "_linux_arm.tar.gz") case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz") case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz") case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe") } } sealed case class Bundle_Info( platform: Platform.Family.Value, platform_description: String, name: String) { def path: Path = Path.explode(name) } /** release archive **/ val ISABELLE: Path = Path.basic("Isabelle") val ISABELLE_ID: Path = Path.explode("etc/ISABELLE_ID") val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS") val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER") object Release_Archive { def make(bytes: Bytes, rename: String = ""): Release_Archive = { Isabelle_System.with_tmp_dir("tmp")(dir => Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path => { val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE) Bytes.write(archive_path, bytes) execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1) val id = File.read(isabelle_dir + ISABELLE_ID) val tags = File.read(isabelle_dir + ISABELLE_TAGS) val identifier = File.read(isabelle_dir + ISABELLE_IDENTIFIER) val (bytes1, identifier1) = if (rename.isEmpty || rename == identifier) (bytes, identifier) else { File.write(isabelle_dir + ISABELLE_IDENTIFIER, rename) Isabelle_System.move_file(isabelle_dir, dir + Path.basic(rename)) execute_tar(dir, "-czf " + File.bash_path(archive_path) + " " + Bash.string(rename)) (Bytes.read(archive_path), rename) } new Release_Archive(bytes1, id, tags, identifier1) }) ) } def read(path: Path, rename: String = ""): Release_Archive = make(Bytes.read(path), rename = rename) def get(url: String, rename: String = "", progress: Progress = new Progress): Release_Archive = { val bytes = if (Path.is_wellformed(url)) Bytes.read(Path.explode(url)) else Isabelle_System.download(url, progress = progress).bytes make(bytes, rename = rename) } } case class Release_Archive private[Build_Release]( bytes: Bytes, id: String, tags: String, identifier: String) { override def toString: String = identifier } /** generated content **/ /* bundled components */ class Bundled(platform: Option[Platform.Family.Value] = None) { def detect(s: String): Boolean = s.startsWith("#bundled") && !s.startsWith("#bundled ") def apply(name: String): String = "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name private val Pattern1 = ("""^#bundled:(.*)$""").r private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r def unapply(s: String): Option[String] = s match { case Pattern1(name) => Some(name) case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name) case _ => None } } def record_bundled_components(dir: Path): Unit = { val catalogs = List("main", "bundled").map((_, new Bundled())) ::: Platform.Family.list.flatMap(platform => List(platform.toString, "bundled-" + platform.toString). map((_, new Bundled(platform = Some(platform))))) File.append(Components.components(dir), terminate_lines("#bundled components" :: (for { (catalog, bundled) <- catalogs.iterator path = Components.admin(dir) + Path.basic(catalog) if path.is_file line <- split_lines(File.read(path)) if line.nonEmpty && !line.startsWith("#") } yield bundled(line)).toList)) } def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) = { val Bundled = new Bundled(platform = Some(platform)) val components = for { Bundled(name) <- Components.read_components(dir) } yield name val jdk_component = components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component") (components, jdk_component) } def activate_components( dir: Path, platform: Platform.Family.Value, more_names: List[String]): Unit = { def contrib_name(name: String): String = Components.contrib(name = name).implode val Bundled = new Bundled(platform = Some(platform)) Components.write_components(dir, Components.read_components(dir).flatMap(line => line match { case Bundled(name) => if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name)) else None case _ => if (Bundled.detect(line)) None else Some(line) }) ::: more_names.map(contrib_name)) } /** build release **/ /* build heaps */ private def build_heaps( options: Options, platform: Platform.Family.Value, build_sessions: List[String], local_dir: Path): Unit = { val server_option = "build_host_" + platform.toString val ssh = options.string(server_option) match { case "" => if (Platform.family == platform) SSH.Local else error("Undefined option " + server_option + ": cannot build heaps") case SSH.Target(user, host) => SSH.open_session(options, host = host, user = user) case s => error("Malformed option " + server_option + ": " + quote(s)) } try { Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar => { execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .") ssh.with_tmp_dir(remote_dir => { val remote_tmp_tar = remote_dir + Path.basic("tmp.tar") ssh.write_file(remote_tmp_tar, local_tmp_tar) val remote_commands = List( "cd " + File.bash_path(remote_dir), "tar -xf tmp.tar", "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions), "tar -cf tmp.tar heaps") ssh.execute(remote_commands.mkString(" && "), settings = false).check ssh.read_file(remote_tmp_tar, local_tmp_tar) }) execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar)) }) } finally { ssh.close() } } /* Isabelle application */ def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n"): Unit = { val title = "# Java runtime options" File.write(path, (title :: options).map(_ + line_ending).mkString) } def make_isabelle_app( platform: Platform.Family.Value, isabelle_target: Path, isabelle_name: String, jdk_component: String, classpath: List[Path], dock_icon: Boolean = false): Unit = { val script = """#!/usr/bin/env bash # # Author: Makarius # # Main Isabelle application script. # minimal Isabelle environment ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)" source "$ISABELLE_HOME/lib/scripts/isabelle-platform" #paranoia settings -- avoid intrusion of alien options unset "_JAVA_OPTIONS" unset "JAVA_TOOL_OPTIONS" #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc. unset XMODIFIERS COMPONENT="$ISABELLE_HOME/contrib/""" + jdk_component + """" source "$COMPONENT/etc/settings" # main declare -a JAVA_OPTIONS=($(grep -v '^#' "$ISABELLE_HOME/Isabelle.options")) "$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup" exec "$ISABELLE_JDK_HOME/bin/java" \ "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \ -classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \ "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \ """ + (if (dock_icon) """"-Xdock:icon=$ISABELLE_HOME/lib/logo/isabelle_transparent-128.png" \ """ else "") + """isabelle.jedit.Main "$@" """ val script_path = isabelle_target + Path.explode("lib/scripts/Isabelle_app") File.write(script_path, script) File.set_executable(script_path, true) val component_dir = isabelle_target + Path.explode("contrib/Isabelle_app") Isabelle_System.move_file( component_dir + Path.explode(Platform.Family.standard(platform)) + Path.explode("Isabelle"), isabelle_target + Path.explode(isabelle_name)) Isabelle_System.rm_tree(component_dir) } def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String): Unit = { File.write(path, """ CFBundleDevelopmentRegion English CFBundleIconFile isabelle.icns CFBundleIdentifier de.tum.in.isabelle CFBundleDisplayName """ + isabelle_name + """ CFBundleInfoDictionaryVersion 6.0 CFBundleName """ + isabelle_name + """ CFBundlePackageType APPL CFBundleShortVersionString """ + isabelle_name + """ CFBundleSignature ???? CFBundleVersion """ + isabelle_rev + """ NSHumanReadableCopyright LSMinimumSystemVersion 10.11 LSApplicationCategoryType public.app-category.developer-tools NSHighResolutionCapable true NSSupportsAutomaticGraphicsSwitching true CFBundleDocumentTypes CFBundleTypeExtensions thy CFBundleTypeIconFile theory.icns CFBundleTypeName Isabelle theory file CFBundleTypeRole Editor LSTypeIsPackage """) } /* main */ def use_release_archive( context: Release_Context, archive: Release_Archive, id: String = ""): Unit = { if (id.nonEmpty && id != archive.id) { error("Mismatch of release identification " + id + " vs. archive " + archive.id) } if (!context.isabelle_archive.is_file || Bytes.read(context.isabelle_archive) != archive.bytes) { Bytes.write(context.isabelle_archive, archive.bytes) } } def build_release_archive( context: Release_Context, version: String, parallel_jobs: Int = 1): Unit = { val progress = context.progress val hg = Mercurial.repository(Path.ISABELLE_HOME) val id = try { hg.id(version) } catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) } if (context.isabelle_archive.is_file) { progress.echo_warning("Found existing release archive: " + context.isabelle_archive) use_release_archive(context, Release_Archive.read(context.isabelle_archive), id = id) } else { progress.echo_warning("Preparing release " + context.dist_name + " ...") Isabelle_System.new_directory(context.dist_dir) hg.archive(context.isabelle_dir.expand.implode, rev = id, options = "--type files") for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) { (context.isabelle_dir + Path.explode(name)).file.delete } File.write(context.isabelle_dir + ISABELLE_ID, id) File.write(context.isabelle_dir + ISABELLE_TAGS, hg.tags(rev = id)) File.write(context.isabelle_dir + ISABELLE_IDENTIFIER, context.dist_name) context.make_announce(id) context.make_contrib() execute(context.isabelle_dir, """find . -print | xargs chmod -f u+rw""") record_bundled_components(context.isabelle_dir) /* build tools and documentation */ val other_isabelle = context.other_isabelle(context.dist_dir) other_isabelle.init_settings( other_isabelle.init_components( components_base = context.components_base, catalogs = List("main"))) other_isabelle.resolve_components(echo = true) try { - val export_classpath = - "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" - other_isabelle.bash(export_classpath + "Admin/build all", echo = true).check - other_isabelle.bash(export_classpath + "bin/isabelle jedit -b", echo = true).check + other_isabelle.bash( + "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" + + "bin/isabelle jedit -b", echo = true).check } catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) } try { other_isabelle.bash( "bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check } catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) } other_isabelle.make_news() for (name <- List("Admin", "browser_info", "heaps")) { Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name)) } other_isabelle.cleanup() progress.echo_warning("Creating release archive " + context.isabelle_archive + " ...") execute(context.dist_dir, """chmod -R a+r . && chmod -R u+w . && chmod -R g=o .""") execute(context.dist_dir, """find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""") execute_tar(context.dist_dir, "-czf " + File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name)) } } def default_platform_families: List[Platform.Family.Value] = Platform.Family.list0 def build_release( options: Options, context: Release_Context, afp_rev: String = "", platform_families: List[Platform.Family.Value] = default_platform_families, more_components: List[Path] = Nil, website: Option[Path] = None, build_sessions: List[String] = Nil, build_library: Boolean = false, parallel_jobs: Int = 1): Unit = { val progress = context.progress /* release directory */ val archive = Release_Archive.read(context.isabelle_archive) for (path <- List(context.isabelle, ISABELLE)) { Isabelle_System.rm_tree(context.dist_dir + path) } Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path => { Bytes.write(archive_path, archive.bytes) val extract = List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc"). map(name => context.dist_name + "/" + name) execute_tar(context.dist_dir, "-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract)) }) Isabelle_System.symlink(Path.explode(context.dist_name), context.dist_dir + ISABELLE) /* make application bundles */ val bundle_infos = platform_families.map(context.bundle_info) for (bundle_info <- bundle_infos) { val isabelle_name = context.dist_name val platform = bundle_info.platform progress.echo("\nApplication bundle for " + platform) Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { // release archive execute_tar(tmp_dir, "-xzf " + File.bash_path(context.isabelle_archive)) val other_isabelle = context.other_isabelle(tmp_dir) val isabelle_target = other_isabelle.isabelle_home // bundled components progress.echo("Bundled components:") val contrib_dir = Components.contrib(isabelle_target) val (bundled_components, jdk_component) = get_bundled_components(isabelle_target, platform) Components.resolve(context.components_base, bundled_components, target_dir = Some(contrib_dir), copy_dir = Some(context.dist_dir + Path.explode("contrib")), progress = progress) val more_components_names = more_components.map(Components.unpack(contrib_dir, _, progress = progress)) activate_components(isabelle_target, platform, more_components_names) // Java parameters val java_options: List[String] = (for { variable <- List( "ISABELLE_JAVA_SYSTEM_OPTIONS", "JEDIT_JAVA_SYSTEM_OPTIONS", "JEDIT_JAVA_OPTIONS") opt <- Word.explode(other_isabelle.getenv(variable)) } yield { val s = "-Dapple.awt.application.name=" if (opt.startsWith(s)) s + isabelle_name else opt }) ::: List("-Disabelle.jedit_server=" + isabelle_name) val classpath: List[Path] = { val base = isabelle_target.absolute val classpath1 = Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")) val classpath2 = Path.split(other_isabelle.getenv("ISABELLE_SETUP_CLASSPATH")) (classpath1 ::: classpath2).map(path => { val abs_path = path.absolute File.relative_path(base, abs_path) match { case Some(rel_path) => rel_path case None => error("Bad classpath element: " + abs_path) } }) } val jedit_options = Path.explode("src/Tools/jEdit/etc/options") val jedit_props = Path.explode(other_isabelle.getenv("JEDIT_HOME") + "/properties/jEdit.props") // build heaps if (build_sessions.nonEmpty) { progress.echo("Building heaps " + commas_quote(build_sessions) + " ...") build_heaps(options, platform, build_sessions, isabelle_target) } // application bundling Components.purge(contrib_dir, platform) platform match { case Platform.Family.linux_arm | Platform.Family.linux => File.change(isabelle_target + jedit_options, _.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24")) File.change(isabelle_target + jedit_props, _.replaceAll("console.fontsize=.*", "console.fontsize=18") .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18") .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18") .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18") .replaceAll("view.fontsize=.*", "view.fontsize=24") .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16")) make_isabelle_options( isabelle_target + Path.explode("Isabelle.options"), java_options) make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath) progress.echo("Packaging " + bundle_info.name + " ...") execute_tar(tmp_dir, "-czf " + File.bash_path(context.dist_dir + bundle_info.path) + " " + Bash.string(isabelle_name)) case Platform.Family.macos => File.change(isabelle_target + jedit_props, _.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d") .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")) // macOS application bundle val app_contents = isabelle_target + Path.explode("Contents") for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) { Isabelle_System.copy_file(isabelle_target + Path.explode(icon), Isabelle_System.make_directory(app_contents + Path.explode("Resources"))) } make_isabelle_plist( app_contents + Path.explode("Info.plist"), isabelle_name, archive.id) make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath, dock_icon = true) val isabelle_options = Path.explode("Isabelle.options") make_isabelle_options( isabelle_target + isabelle_options, java_options ::: List("-Disabelle.app=true")) // application archive progress.echo("Packaging " + bundle_info.name + " ...") val isabelle_app = Path.explode(isabelle_name + ".app") Isabelle_System.move_file(tmp_dir + Path.explode(isabelle_name), tmp_dir + isabelle_app) execute_tar(tmp_dir, "-czf " + File.bash_path(context.dist_dir + bundle_info.path) + " " + File.bash_path(isabelle_app)) case Platform.Family.windows => File.change(isabelle_target + jedit_props, _.replaceAll("foldPainter=.*", "foldPainter=Square")) // application launcher Isabelle_System.move_file(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir) val app_template = Path.explode("~~/Admin/Windows/launch4j") make_isabelle_options( isabelle_target + Path.explode(isabelle_name + ".l4j.ini"), java_options, line_ending = "\r\n") val isabelle_xml = Path.explode("isabelle.xml") val isabelle_exe = bundle_info.path File.write(tmp_dir + isabelle_xml, File.read(app_template + isabelle_xml) .replace("{ISABELLE_NAME}", isabelle_name) .replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe)) .replace("{ICON}", File.platform_path(app_template + Path.explode("isabelle_transparent.ico"))) .replace("{SPLASH}", File.platform_path(app_template + Path.explode("isabelle.bmp"))) .replace("{CLASSPATH}", cat_lines(classpath.map(cp => " %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + ""))) .replace("\\jdk\\", "\\" + jdk_component + "\\")) execute(tmp_dir, "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml") Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"), isabelle_target + isabelle_exe.ext("manifest")) // Cygwin setup val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin") Isabelle_System.copy_file(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target) val cygwin_mirror = File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror")) val cygwin_bat = Path.explode("Cygwin-Setup.bat") File.write(isabelle_target + cygwin_bat, File.read(cygwin_template + cygwin_bat).replace("{MIRROR}", cygwin_mirror)) File.set_executable(isabelle_target + cygwin_bat, true) for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) { val path = Path.explode(name) Isabelle_System.copy_file(cygwin_template + path, isabelle_target + Path.explode("contrib/cygwin") + path) } execute(isabelle_target, """find . -type f -not -name "*.exe" -not -name "*.dll" """ + (if (Platform.is_macos) "-perm +100" else "-executable") + " -print0 > contrib/cygwin/isabelle/executables") execute(isabelle_target, """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ + """> contrib/cygwin/isabelle/symlinks""") execute(isabelle_target, """find . -type l -exec rm "{}" ";" """) File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "") // executable archive (self-extracting 7z) val archive_name = isabelle_name + ".7z" val exe_archive = tmp_dir + Path.explode(archive_name) exe_archive.file.delete progress.echo("Packaging " + archive_name + " ...") execute(tmp_dir, "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name)) if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive) val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx") val sfx_txt = File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")) .replace("{ISABELLE_NAME}", isabelle_name) Bytes.write(context.dist_dir + isabelle_exe, Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive)) File.set_executable(context.dist_dir + isabelle_exe, true) } }) progress.echo("DONE") } /* minimal website */ for (dir <- website) { val website_platform_bundles = for { bundle_info <- bundle_infos if (context.dist_dir + bundle_info.path).is_file } yield (bundle_info.name, bundle_info) val isabelle_link = HTML.link(Isabelle_System.isabelle_repository.changeset(archive.id), HTML.text("Isabelle/" + archive.id)) val afp_link = HTML.link(Isabelle_System.afp_repository.changeset(afp_rev), HTML.text("AFP/" + afp_rev)) HTML.write_document(dir, "index.html", List(HTML.title(context.dist_name)), List( HTML.section(context.dist_name), HTML.subsection("Downloads"), HTML.itemize( List(HTML.link(context.dist_name + ".tar.gz", HTML.text("Source archive"))) :: website_platform_bundles.map({ case (bundle, bundle_info) => List(HTML.link(bundle, HTML.text(bundle_info.platform_description + " bundle"))) })), HTML.subsection("Repositories"), HTML.itemize( List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link)))))) Isabelle_System.copy_file(context.isabelle_archive, dir) for ((bundle, _) <- website_platform_bundles) { Isabelle_System.copy_file(context.dist_dir + Path.explode(bundle), dir) } } /* HTML library */ if (build_library) { if (context.isabelle_library_archive.is_file) { progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive) } else { Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { val bundle = context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz") execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle)) val other_isabelle = context.other_isabelle(tmp_dir) Isabelle_System.make_directory(other_isabelle.etc) File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n") other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs + " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check other_isabelle.isabelle_home_user.file.delete execute(tmp_dir, "chmod -R a+r " + Bash.string(context.dist_name)) execute(tmp_dir, "chmod -R g=o " + Bash.string(context.dist_name)) execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) + " " + Bash.string(context.dist_name + "/browser_info")) }) } } } /** command line entry point **/ def main(args: Array[String]): Unit = { Command_Line.tool { var afp_rev = "" var components_base: Path = Components.default_components_base var target_dir = Path.current var release_name = "" var source_archive = "" var website: Option[Path] = None var build_sessions: List[String] = Nil var more_components: List[Path] = Nil var parallel_jobs = 1 var build_library = false var options = Options.init() var platform_families = default_platform_families var rev = "" val getopts = Getopts(""" Usage: Admin/build_release [OPTIONS] Options are: -A REV corresponding AFP changeset id -C DIR base directory for Isabelle components (default: """ + Components.default_components_base + """) -D DIR target directory (default ".") -R RELEASE explicit release name -S ARCHIVE use existing source archive (file or URL) -W WEBSITE produce minimal website in given directory -b SESSIONS build platform-specific session images (separated by commas) -c ARCHIVE clean bundling with additional component .tar.gz archive -j INT maximum number of parallel jobs (default 1) -l build library -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) -r REV Mercurial changeset id (default: ARCHIVE or RELEASE or tip) Build Isabelle release in base directory, using the local repository clone. """, "A:" -> (arg => afp_rev = arg), "C:" -> (arg => components_base = Path.explode(arg)), "D:" -> (arg => target_dir = Path.explode(arg)), "R:" -> (arg => release_name = arg), "S:" -> (arg => source_archive = arg), "W:" -> (arg => website = Some(Path.explode(arg))), "b:" -> (arg => build_sessions = space_explode(',', arg)), "c:" -> (arg => { val path = Path.explode(arg) Components.Archive.get_name(path.file_name) more_components = more_components ::: List(path) }), "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), "l" -> (_ => build_library = true), "o:" -> (arg => options = options + arg), "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)), "r:" -> (arg => rev = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok) error("Building for windows requires 7z") val progress = new Console_Progress() def make_context(name: String): Release_Context = Release_Context(target_dir, release_name = name, components_base = components_base, progress = progress) val context = if (source_archive.isEmpty) { val context = make_context(release_name) val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip" build_release_archive(context, version, parallel_jobs = parallel_jobs) context } else { val archive = Release_Archive.get(source_archive, rename = release_name, progress = progress) val context = make_context(archive.identifier) Isabelle_System.make_directory(context.dist_dir) use_release_archive(context, archive, id = rev) context } build_release(options, context, afp_rev = afp_rev, platform_families = platform_families, more_components = more_components, build_sessions = build_sessions, build_library = build_library, parallel_jobs = parallel_jobs, website = website) } } } diff --git a/lib/browser/awtUtilities/Border.java b/src/Tools/GraphBrowser/awt/Border.java rename from lib/browser/awtUtilities/Border.java rename to src/Tools/GraphBrowser/awt/Border.java --- a/lib/browser/awtUtilities/Border.java +++ b/src/Tools/GraphBrowser/awt/Border.java @@ -1,39 +1,39 @@ /*************************************************************************** - Title: awtUtilities/Border.java + Title: awt/Border.java Author: Stefan Berghofer, TU Muenchen This class defines a nice 3D border. ***************************************************************************/ -package awtUtilities; +package isabelle.awt; import java.awt.*; public class Border extends Panel { int bs; public Insets getInsets() { return new Insets(bs*3/2,bs*3/2,bs*3/2,bs*3/2); } public Border(Component comp,int s) { setLayout(new GridLayout(1,1)); add(comp); bs=s; } public void paint(Graphics g) { int w = getSize().width; int h = getSize().height; int x1[]={0,bs,w-bs,w}, y1[]={0,bs,bs,0}; int x2[]={w,w-bs,w-bs,w}, y2[]={0,bs,h-bs,h}; int y3[]={h,h-bs,h-bs,h}; g.setColor(new Color(224,224,224)); g.fillPolygon(y1,y2,4); g.fillPolygon(x1,y1,4); g.setColor(Color.gray); g.fillPolygon(x2,y2,4); g.fillPolygon(x1,y3,4); } } diff --git a/lib/browser/awtUtilities/MessageDialog.java b/src/Tools/GraphBrowser/awt/MessageDialog.java rename from lib/browser/awtUtilities/MessageDialog.java rename to src/Tools/GraphBrowser/awt/MessageDialog.java --- a/lib/browser/awtUtilities/MessageDialog.java +++ b/src/Tools/GraphBrowser/awt/MessageDialog.java @@ -1,53 +1,53 @@ /*************************************************************************** - Title: awtUtilities/MessageDialog.java + Title: awt/MessageDialog.java Author: Stefan Berghofer, TU Muenchen This class defines a dialog window for displaying messages and buttons. ***************************************************************************/ -package awtUtilities; +package isabelle.awt; import java.awt.*; import java.awt.event.*; public class MessageDialog extends Dialog implements ActionListener { String txt; public String getText() { return txt; } public void actionPerformed(ActionEvent evt) { txt = evt.getActionCommand(); setVisible(false); } public MessageDialog(Frame parent,String title,String text,String []buttons) { super(parent,title,true); int i; Panel p1=new Panel(),p2=new Panel(); p1.setLayout(new FlowLayout(FlowLayout.CENTER,0,0)); p2.setLayout(new FlowLayout()); setFont(new Font("Helvetica", Font.PLAIN, 14)); setLayout(new GridLayout(2,1)); while (true) { int pos=text.indexOf(' '); if (pos<0) { p1.add(new Label(text)); break; } else { p1.add(new Label(text.substring(0,pos))); if (pos+1==text.length()) break; else text=text.substring(pos+1); } } add(p1);add(p2); for (i=0;i [ + ] "+ "[ < | > ] [ [ ... [ ] ... ] ] ;"); } } public static void main(String[] args) { try { if (args.length <= 1) { System.err.println("Graph and output file expected."); return; } Console console=new Console(args[0]); InputStream is=new FileInputStream(args[0]); console.initBrowser(is); is.close(); try { if (args[1].endsWith(".ps")) console.PS(args[1], true); else if (args[1].endsWith(".eps")) console.PS(args[1], false); else System.err.println("Unknown file type: " + args[1]); } catch (IOException exn) { System.err.println("Unable to write file " + args[1]); } } catch (IOException exn) { System.err.println("Can't open graph file "+args[0]); } } } diff --git a/lib/browser/GraphBrowser/DefaultFontMetrics.java b/src/Tools/GraphBrowser/graphbrowser/DefaultFontMetrics.java rename from lib/browser/GraphBrowser/DefaultFontMetrics.java rename to src/Tools/GraphBrowser/graphbrowser/DefaultFontMetrics.java --- a/lib/browser/GraphBrowser/DefaultFontMetrics.java +++ b/src/Tools/GraphBrowser/graphbrowser/DefaultFontMetrics.java @@ -1,48 +1,48 @@ /*************************************************************************** - Title: GraphBrowser/DefaultFontMetrics.java + Title: graphbrowser/DefaultFontMetrics.java Author: Stefan Berghofer, TU Muenchen Options: :tabSize=2: Default font metrics which is used when no graphics context is available (batch mode). ***************************************************************************/ -package GraphBrowser; +package isabelle.graphbrowser; public class DefaultFontMetrics implements AbstractFontMetrics { private static int[] chars = {13, 13, 17, 27, 27, 43, 32, 11, 16, 16, 19, 28, 13, 28, 13, 13, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 13, 13, 28, 28, 28, 27, 49, 32, 32, 35, 35, 32, 29, 37, 35, 13, 24, 32, 27, 40, 35, 37, 32, 37, 35, 32, 29, 35, 32, 45, 32, 32, 29, 13, 13, 13, 22, 27, 11, 27, 27, 24, 27, 27, 13, 27, 27, 11, 11, 24, 11, 40, 27, 27, 27, 27, 16, 24, 13, 27, 24, 35, 24, 24, 24, 16, 12, 16, 28}; private int size; public DefaultFontMetrics(int size) { this.size = size; } public int getLeading() { return 1; } public int getAscent() { return (int)(Math.round(size * 46.0 / 48.0)); } public int getDescent() { return (int)(Math.round(size * 10.0 / 48.0)); } public int charWidth(char c) { if (c < 32 || c > 126) { return 0; } else { return (int)(Math.round(chars[c - 32] * size / 48.0)); } } public int stringWidth(String s) { int l=0, i; for (i=0; i < s.length(); i++) { l += charWidth(s.charAt(i)); } return l; } } diff --git a/lib/browser/GraphBrowser/Directory.java b/src/Tools/GraphBrowser/graphbrowser/Directory.java rename from lib/browser/GraphBrowser/Directory.java rename to src/Tools/GraphBrowser/graphbrowser/Directory.java --- a/lib/browser/GraphBrowser/Directory.java +++ b/src/Tools/GraphBrowser/graphbrowser/Directory.java @@ -1,21 +1,21 @@ -package GraphBrowser; +package isabelle.graphbrowser; import java.util.Vector; class Directory { TreeNode node; String name; Vector collapsed; public Directory(TreeNode nd,String n,Vector col) { collapsed=col; name=n; node=nd; } public TreeNode getNode() { return node; } public String getName() { return name; } public Vector getCollapsed() { return collapsed; } } diff --git a/lib/browser/GraphBrowser/DummyVertex.java b/src/Tools/GraphBrowser/graphbrowser/DummyVertex.java rename from lib/browser/GraphBrowser/DummyVertex.java rename to src/Tools/GraphBrowser/graphbrowser/DummyVertex.java --- a/lib/browser/GraphBrowser/DummyVertex.java +++ b/src/Tools/GraphBrowser/graphbrowser/DummyVertex.java @@ -1,29 +1,29 @@ /*************************************************************************** - Title: GraphBrowser/DummyVertex.java + Title: graphbrowser/DummyVertex.java Author: Stefan Berghofer, TU Muenchen Options: :tabSize=4: This class represents a dummy vertex, which is used to simplify the layout algorithm. ***************************************************************************/ -package GraphBrowser; +package isabelle.graphbrowser; import java.awt.*; class DummyVertex extends Vertex { public boolean isDummy() {return true;} public Object clone() { Vertex ve=new DummyVertex(); ve.setX(getX());ve.setY(getY()); return ve; } public int leftX() { return getX(); } public int rightX() { return getX(); } public void draw(Graphics g) {} } diff --git a/lib/browser/GraphBrowser/Graph.java b/src/Tools/GraphBrowser/graphbrowser/Graph.java rename from lib/browser/GraphBrowser/Graph.java rename to src/Tools/GraphBrowser/graphbrowser/Graph.java --- a/lib/browser/GraphBrowser/Graph.java +++ b/src/Tools/GraphBrowser/graphbrowser/Graph.java @@ -1,1062 +1,1062 @@ /*************************************************************************** - Title: GraphBrowser/Graph.java + Title: graphbrowser/Graph.java Author: Stefan Berghofer, TU Muenchen Options: :tabSize=4: This class contains the core of the layout algorithm and methods for drawing and PostScript output. ***************************************************************************/ -package GraphBrowser; +package isabelle.graphbrowser; import java.util.*; import java.awt.*; import java.io.*; public class Graph { /**** parameters for layout ****/ public int box_height=0; public int box_height2; public Graphics gfx; Vector vertices=new Vector(10,10); Vector splines=new Vector(10,10); Vector numEdges=new Vector(10,10); Vertex []vertices2; public int min_x=0,min_y=0,max_x=10,max_y=10; /********************************************************************/ /* clone graph object */ /********************************************************************/ public Object clone() { Graph gr=new Graph(); Enumeration e1; int i; gr.splines=(Vector)(splines.clone()); e1=vertices.elements(); while (e1.hasMoreElements()) gr.addVertex((Vertex)(((Vertex)(e1.nextElement())).clone())); for (i=0;i') { children=false; tok.nextToken(); } else children=true; while (tok.ttype!=';') { if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"') throw new ParseError("expected: child vertex identifier or ';'\nfound : "+tok.toString()); ve2=findVertex(tok.sval); if (ve2==null) { ve2=new NormalVertex(""); ve2.setID(tok.sval); ve2.setNumber(index++); addVertex(ve2); } if (children) ve1.addChild(ve2); else ve1.addParent(ve2); tok.nextToken(); } tok.nextToken(); } vertices2 = new Vertex[vertices.size()]; vertices.copyInto(vertices2); } /*** Find vertex with identifier vertexID ***/ public Vertex findVertex(String vertexID) { Enumeration e1=vertices.elements(); Vertex v1; while (e1.hasMoreElements()) { v1=(Vertex)(e1.nextElement()); if ((v1.getID()).equals(vertexID)) return v1; } return null; } public void addVertex(Vertex v) { vertices.addElement(v); v.setGraph(this); } public void removeVertex(Vertex v) { vertices.removeElement(v); } public Enumeration getVertices() { return vertices.elements(); } /********************************************************************/ /* graph layout */ /********************************************************************/ public void layout(Graphics g) { splines.removeAllElements(); hasseDiagram(); Vector layers=min_crossings(insert_dummies((Vector)(sort().elementAt(0)))); setParameters(g); init_coordinates(layers); pendulum(layers); rubberband(layers); calcSplines(layers); calcBoundingBox(); } /********************************************************************/ /* set layout parameters */ /********************************************************************/ public void setParameters(Graphics g) { Enumeration e1=vertices.elements(); int h; h=Integer.MIN_VALUE; while (e1.hasMoreElements()) { Box dim=((Vertex)(e1.nextElement())).getLabelSize(g); h=Math.max(h,dim.height); } box_height=h+4; box_height2=box_height/2; gfx=g; } /********************************************************************/ /* topological sorting */ /********************************************************************/ public Vector sort() { Vector todo=(Vector)(vertices.clone()); Vector layers=new Vector(10,10); Vector todo2; Enumeration e1,e2; Vertex v,v2; e1=vertices.elements(); while (e1.hasMoreElements()) ((Vertex)(e1.nextElement())).setDegree(0); e1=vertices.elements(); while (e1.hasMoreElements()) { v=(Vertex)(e1.nextElement()); e2=v.getChildren(); while (e2.hasMoreElements()) { v2=(Vertex)(e2.nextElement()); todo.removeElement(v2); v2.setDegree(1+v2.getDegree()); } } while (!todo.isEmpty()) { layers.addElement(todo); todo2=new Vector(10,10); e1=todo.elements(); while (e1.hasMoreElements()) { e2=((Vertex)(e1.nextElement())).getChildren(); while (e2.hasMoreElements()) { v=(Vertex)(e2.nextElement()); v.setDegree(v.getDegree()-1); if (v.getDegree()==0) { todo2.addElement(v); v.setDegree(layers.size()); } } } todo=todo2; } return layers; } /********************************************************************/ /* compute hasse diagram */ /********************************************************************/ public void hasseDiagram() { Enumeration e1,e2; Vertex vx1,vx2; /** construct adjacence matrix **/ int vs=vertices.size(); boolean adj[][]=new boolean[vs][vs]; boolean adj2[][]=new boolean[vs][vs]; int i,j,k; e1=getVertices(); for (i=0;i=oldcr) return cr; } } } } } } return cr; } /********************************************************************/ /* calculation of crossings where vertices vx1 and vx2 are involved */ /* vx1 and vx2 must be in same layer and vx1 is left from vx2 */ /********************************************************************/ public int count_crossings_2(Vector layers,Vertex vx1,Vertex vx2,int oldcr) { int i,cr=0,l=vx1.getDegree(); Vertex va,vb; Vector layer; Enumeration e1,e2; if (l>0) { layer=(Vector)(layers.elementAt(l-1)); e1=vx1.getParents(); while (e1.hasMoreElements()) { va=(Vertex)(e1.nextElement()); i=layer.indexOf(va); e2=vx2.getParents(); while (e2.hasMoreElements()) { vb=(Vertex)(e2.nextElement()); if (layer.indexOf(vb)=oldcr) return cr; } } } } if (l=oldcr) return cr; } } } } return cr; } /********************************************************************/ /* reduction of crossings by exchanging adjacent vertices */ /********************************************************************/ public void exchangeVertices(Vector layers,int oldcr) { int i,l,c1,c2; Vertex vx1,vx2; Vector v1; for (l=0;l0) { if (topdown) { /** top-down-traversal **/ layers2=new Vector(10,10); for (l=0;l0) vx1.setWeight(((double)(k))/z); else if (first) vx1.setWeight(Double.MAX_VALUE); for (i=0;i=0;l--) { v1=(Vector)(layers.elementAt(l)); if (l==layers.size()-1) layers2.addElement(v1.clone()); else { v2=new Vector(10,10); layers2.insertElementAt(v2,0); e1=v1.elements(); while (e1.hasMoreElements()) { vx1=(Vertex)(e1.nextElement()); k=0;z=0; e2=vx1.getChildren(); while (e2.hasMoreElements()) { k+=((Vector)(layers2.elementAt(1))).indexOf(e2.nextElement()); z++; } if (z>0) vx1.setWeight(((double)(k))/z); else if (first) vx1.setWeight(Double.MAX_VALUE); for (i=0;i=2) { do { change=false; d1=((Region)(l.firstElement())).pred_deflection(); for (i=0;i 0 && d1 > d2 || d1 > 0 && d2 < 0)) { r1.combine(r2); l.removeElement(r2); change=true; d2=r1.pred_deflection(); } d1=d2; } } while (change); } for (i=0;i0) offset=-Math.min( ((Region)(l.elementAt(i-1))).spaceBetween(r1),-d1); if (d1>=0 && i0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-20 > vx.rightX()+d2)) vx.setX(vx.getX()+d2); } } } } /**** Intersection point of two lines (auxiliary function for calcSplines) ****/ /**** Calculate intersection point of line which is parallel to line (p1,p2) ****/ /**** and leads through p5, with line (p3,p4) ****/ Point intersect(Point p1,Point p2,Point p3,Point p4,Point p5) { float x=0,y=0,s1=0,s2=0; if (p1.x!=p2.x) s1=((float)(p2.y-p1.y))/(p2.x-p1.x); if (p3.x!=p4.x) s2=((float)(p4.y-p3.y))/(p4.x-p3.x); if (p1.x==p2.x) { x=p5.x; y=s2*(p5.x-p3.x)+p3.y; } else if (p3.x==p4.x) { x=p3.x; y=s1*(p3.x-p5.x)+p5.y; } else { x=(p5.x*s1-p3.x*s2+p3.y-p5.y)/(s1-s2); y=s2*(x-p3.x)+p3.y; } return new Point(Math.round(x),Math.round(y)); } /**** Calculate control points (auxiliary function for calcSplines) ****/ Points calcPoint(Point p1,Point p2,Point p3,int lboxx,int rboxx,int boxy) { /*** Points p1 , p2 , p3 define a triangle which encloses the spline. ***/ /*** Check if adjacent boxes (specified by lboxx,rboxx and boxy) ***/ /*** collide with the spline. In this case p1 and p3 are shifted by an ***/ /*** appropriate offset before they are returned ***/ int xh1,xh2,bx=0,by=0; boolean pt1 = boxy >= p1.y && boxy <= p3.y || boxy >= p3.y && boxy <= p1.y; boolean pt2 = boxy+box_height >= p1.y && boxy+box_height <= p3.y || boxy+box_height >= p3.y && boxy+box_height <= p1.y; boolean move = false; Point b; xh1 = p1.x+(boxy-p1.y)*(p3.x-p1.x)/(p3.y-p1.y); xh2 = p1.x+(boxy+box_height-p1.y)*(p3.x-p1.x)/(p3.y-p1.y); if (xh1 <= lboxx && pt1 && xh2 <= lboxx && pt2) { move = true; bx = lboxx; by = boxy + (xh1 < xh2 ? 0 : box_height ) ; } else if (xh1 >= rboxx && pt1 && xh2 >= rboxx && pt2) { move = true; bx = rboxx; by = boxy + (xh1 > xh2 ? 0 : box_height ) ; } else if ( (xh1 <= lboxx || xh1 >= rboxx) && pt1) { move = true; bx = (xh1 <= lboxx ? lboxx : rboxx ) ; by = boxy; } else if ( (xh2 <= lboxx || xh2 >= rboxx) && pt2) { move = true; bx = (xh2 <= lboxx ? lboxx : rboxx ) ; by = boxy+box_height; } b=new Point(bx,by); if (move) return new Points(intersect(p1,p3,p1,p2,b),intersect(p1,p3,p2,p3,b)); else return new Points(p1,p3); } /********************************************************************/ /* calculate splines */ /********************************************************************/ public void calcSplines(Vector layers) { Enumeration e2,e1=vertices.elements(); Vertex vx1,vx2,vx3; Vector pos,layer; int x1,y1,x2,y2,x3,y3,xh,k,leftx,rightx,spc; while (e1.hasMoreElements()) { vx1=(Vertex)(e1.nextElement()); if (!vx1.isDummy()) { e2=vx1.getChildren(); while (e2.hasMoreElements()) { vx2=(Vertex)(e2.nextElement()); if (vx2.isDummy()) { vx3=vx2; /**** convert edge to spline ****/ pos=new Vector(10,10); x1=vx1.getX(); y1=vx1.getY()+box_height; do { /*** calculate position of control points ***/ x2=vx2.getX(); y2=vx2.getY(); layer=(Vector)(layers.elementAt(vx2.getDegree())); k=layer.indexOf(vx2); vx2=(Vertex)((vx2.getChildren()).nextElement()); x3=vx2.getX(); y3=vx2.getY(); spc=0; leftx = k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ? Integer.MIN_VALUE: ((Vertex)(layer.elementAt(k-1))).rightX()+spc; rightx = k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ? Integer.MAX_VALUE: ((Vertex)(layer.elementAt(k+1))).leftX()-spc; xh=x2+box_height*(x3-x2)/(y3-y2); if (!(x2<=x3 && xh>=rightx || x2>x3 && xh<=leftx)) { /* top control point */ - pos.addElement(new Integer(1)); + pos.addElement(Integer.valueOf(1)); y1=y2; } else { xh=x1+(y2-y1)*(x2-x1)/(y2+box_height-y1); if (!(x2<=x1 && xh>=rightx || x2>x1 && xh<=leftx)) /* bottom control point */ - pos.addElement(new Integer(2)); + pos.addElement(Integer.valueOf(2)); else /* two control points needed */ - pos.addElement(new Integer(3)); + pos.addElement(Integer.valueOf(3)); y1=y2+box_height; } x1=x2; } while (vx2.isDummy()); - pos.addElement(new Integer(1)); + pos.addElement(Integer.valueOf(1)); /**** calculate triangles ****/ vx2=vx3; int pos1,pos2,i=0; Vector pts=new Vector(10,10); int lboxx,rboxx,boxy; x1=vx1.getX(); y1=vx1.getY()+box_height; pts.addElement(new Point(x1,y1)); /** edge starting point **/ do { x2=vx2.getX(); y2=vx2.getY(); pos1=((Integer)(pos.elementAt(i))).intValue(); pos2=((Integer)(pos.elementAt(i+1))).intValue(); i++; layer=(Vector)(layers.elementAt(vx2.getDegree())); k=layer.indexOf(vx2); boxy=vx2.getY(); vx2=(Vertex)((vx2.getChildren()).nextElement()); x3=vx2.getX(); y3=vx2.getY(); if (pos1==2) y2+=box_height; if (pos2==2) y3+=box_height; lboxx = (k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ) ? Integer.MIN_VALUE : ((Vertex)(layer.elementAt(k-1))).rightX(); rboxx = (k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ) ? Integer.MAX_VALUE : ((Vertex)(layer.elementAt(k+1))).leftX(); Point p1,p2,p3; Points ps; p1 = new Point((x1+x2)/2,(y1+y2)/2); if (pos1<=2) { /** one control point **/ p2 = new Point(x2,y2); ps = calcPoint(p1,p2,new Point((x2+x3)/2,(y2+y3)/2),lboxx,rboxx,boxy); pts.addElement(ps.p); pts.addElement(p2); pts.addElement(ps.q); } else { /** two control points **/ p2 = new Point(x2,y2-box_height); p3 = new Point(x2,y2+box_height2); ps = calcPoint(p1,p2,p3,lboxx,rboxx,boxy); pts.addElement(ps.p); pts.addElement(p2); pts.addElement(ps.q); p2 = new Point(x2,y2+box_height*2); ps = calcPoint(p3,p2,new Point((p2.x+x3)/2,(p2.y+y3)/2), lboxx,rboxx,boxy); pts.addElement(ps.p); pts.addElement(p2); pts.addElement(ps.q); } x1=p2.x; y1=p2.y; } while (vx2.isDummy()); pts.addElement(new Point(vx2.getX(),vx2.getY())); /** edge end point **/ splines.addElement(new Spline(pts)); } } } } } /********************************************************************/ /* calculate bounding box */ /********************************************************************/ public void calcBoundingBox() { min_y=min_x=Integer.MAX_VALUE; max_y=max_x=Integer.MIN_VALUE; Enumeration e1=vertices.elements(); Vertex v; while (e1.hasMoreElements()) { v=(Vertex)(e1.nextElement()); min_x=Math.min(min_x,v.leftX()); max_x=Math.max(max_x,v.rightX()); min_y=Math.min(min_y,v.getY()); max_y=Math.max(max_y,v.getY()+box_height); } min_x-=20; min_y-=20; max_x+=20; max_y+=20; } /********************************************************************/ /* draw graph */ /********************************************************************/ public void draw(Graphics g) { if (box_height==0) layout(g); g.translate(-min_x,-min_y); Enumeration e1=vertices.elements(); while (e1.hasMoreElements()) ((Vertex)(e1.nextElement())).draw(g); e1=splines.elements(); while (e1.hasMoreElements()) ((Spline)(e1.nextElement())).draw(g); } /********************************************************************/ /* return vertex at position (x,y) */ /********************************************************************/ public Vertex vertexAt(int x,int y) { Enumeration e1=vertices.elements(); while (e1.hasMoreElements()) { Vertex v=(Vertex)(e1.nextElement()); if (v.contains(x,y)) return v; } return null; } /********************************************************************/ /* encode list of vertices (as array of vertice numbers) */ /********************************************************************/ public Vector encode(Vector v) { Vector code=new Vector(10,10); Enumeration e1=v.elements(); while (e1.hasMoreElements()) { Vertex vx=(Vertex)(e1.nextElement()); if (vx.getNumber()>=0) - code.addElement(new Integer(vx.getNumber())); + code.addElement(Integer.valueOf(vx.getNumber())); } return code; } /********************************************************************/ /* get vertex with number n */ /********************************************************************/ public Vertex getVertexByNum(int x) { Enumeration e1=vertices.elements(); while (e1.hasMoreElements()) { Vertex vx=(Vertex)(e1.nextElement()); if (vx.getNumber()==x) return vx; } return null; } /********************************************************************/ /* decode list of vertices */ /********************************************************************/ public Vector decode(Vector code) { Enumeration e1=code.elements(); Vector vec=new Vector(10,10); while (e1.hasMoreElements()) { int i=((Integer)(e1.nextElement())).intValue(); //Vertex vx=getVertexByNum(i); //if (vx!=null) vec.addElement(vx); vec.addElement(vertices2[i]); } return vec; } /********************************************************************/ /* collapse vertices */ /********************************************************************/ public void collapse(Vector vs,String name,Vector inflate) { Enumeration e1,e2,e3; boolean nonempty=false; Vertex vx3,vx2,vx1; e1=vertices.elements(); vx1=new NormalVertex(name); vx1.setInflate(inflate); while (e1.hasMoreElements()) { vx2=(Vertex)(e1.nextElement()); if (vs.indexOf(vx2)<0) { e2=vx2.getParents(); while (e2.hasMoreElements()) { vx3=(Vertex)(e2.nextElement()); if (vs.indexOf(vx3)>=0) { if (!vx1.isChild(vx2)) vx1.addChild(vx2); vx3.removeChild(vx2); } } e2=vx2.getChildren(); while (e2.hasMoreElements()) { vx3=(Vertex)(e2.nextElement()); if (vs.indexOf(vx3)>=0) { if (!vx2.isChild(vx1)) vx2.addChild(vx1); vx2.removeChild(vx3); } } } else { nonempty=true; } } e1=vs.elements(); while (e1.hasMoreElements()) try { removeVertex((Vertex)(e1.nextElement())); } catch (NoSuchElementException exn) {} if (nonempty) addVertex(vx1); } /********************************************************************/ /* PostScript output */ /********************************************************************/ public void PS(String fname,boolean printable) throws IOException { FileOutputStream f = new FileOutputStream(fname); PrintWriter p = new PrintWriter(f, true); if (printable) p.println("%!PS-Adobe-2.0\n\n%%BeginProlog"); else { p.println("%!PS-Adobe-2.0 EPSF-2.0\n%%Orientation: Portrait"); p.println("%%BoundingBox: "+min_x+" "+min_y+" "+max_x+" "+max_y); p.println("%%EndComments\n\n%%BeginProlog"); } p.println("/m { moveto } def /l { lineto } def /n { newpath } def"); p.println("/s { stroke } def /c { curveto } def"); p.println("/b { n 0 0 m dup true charpath pathbbox 1 index 4 index sub"); p.println("7 index exch sub 2 div 9 index add 1 index 4 index sub 7 index exch sub"); p.println("2 div 9 index add 2 index add m pop pop pop pop"); p.println("1 -1 scale show 1 -1 scale n 3 index 3 index m 1 index 0 rlineto"); p.println("0 exch rlineto neg 0 rlineto closepath s pop pop } def"); p.println("%%EndProlog\n"); if (printable) { int hsize=max_x-min_x; int vsize=max_y-min_y; if (hsize>vsize) { // Landscape output double scale=Math.min(1,Math.min(750.0/hsize,500.0/vsize)); double trans_x=50+max_y*scale+(500-scale*vsize)/2.0; double trans_y=50+max_x*scale+(750-scale*hsize)/2.0; p.println(trans_x+" "+trans_y+" translate"); p.println("-90 rotate"); p.println(scale+" "+(-scale)+" scale"); } else { // Portrait output double scale=Math.min(1,Math.min(500.0/hsize,750.0/vsize)); double trans_x=50-min_x*scale+(500-scale*hsize)/2.0; double trans_y=50+max_y*scale+(750-scale*vsize)/2.0; p.println(trans_x+" "+trans_y+" translate"); p.println(scale+" "+(-scale)+" scale"); } } else p.println("0 "+(max_y+min_y)+" translate\n1 -1 scale"); p.println("/Helvetica findfont 12 scalefont setfont"); p.println("0.5 setlinewidth"); Enumeration e1=vertices.elements(); while (e1.hasMoreElements()) ((Vertex)(e1.nextElement())).PS(p); e1=splines.elements(); while (e1.hasMoreElements()) ((Spline)(e1.nextElement())).PS(p); if (printable) p.println("showpage"); f.close(); } } /**** Return value of function calcPoint ****/ class Points { public Point p,q; public Points(Point p1,Point p2) { p=p1;q=p2; } } diff --git a/lib/browser/GraphBrowser/GraphBrowser.java b/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java rename from lib/browser/GraphBrowser/GraphBrowser.java rename to src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java --- a/lib/browser/GraphBrowser/GraphBrowser.java +++ b/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java @@ -1,215 +1,215 @@ /*************************************************************************** - Title: GraphBrowser/GraphBrowser.java + Title: graphbrowser/GraphBrowser.java Author: Stefan Berghofer, TU Muenchen Options: :tabSize=4: This is the graph browser's main class. It contains the "main(...)" method, which is used for the stand-alone version, as well as "init(...)", "start(...)" and "stop(...)" methods which are used for the applet version. Note: GraphBrowser is designed for the 1.1.x version of the JDK. ***************************************************************************/ -package GraphBrowser; +package isabelle.graphbrowser; import java.awt.*; import java.applet.*; import java.io.*; import java.util.*; import java.net.*; -import awtUtilities.*; +import isabelle.awt.*; public class GraphBrowser extends Applet { GraphView gv; TreeBrowser tb=null; String gfname; static boolean isApplet; static Frame f; public GraphBrowser(String name) { gfname=name; } public GraphBrowser() {} public void showWaitMessage() { if (isApplet) getAppletContext().showStatus("calculating layout, please wait ..."); else { f.setCursor(new Cursor(Cursor.WAIT_CURSOR)); } } public void showReadyMessage() { if (isApplet) getAppletContext().showStatus("ready !"); else { f.setCursor(new Cursor(Cursor.DEFAULT_CURSOR)); } } public void viewFile(String fname) { try { if (isApplet) getAppletContext().showDocument(new URL(getDocumentBase(), fname), "_blank"); else { String path = gfname.substring(0, gfname.lastIndexOf('/') + 1); Reader rd; BufferedReader br; String line, text = ""; try { rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream())); } catch (Exception exn) { rd = new FileReader(path + fname); } br = new BufferedReader(rd); while ((line = br.readLine()) != null) text += line + "\n"; if (fname.endsWith(".html")) { /**** convert HTML to text (just a quick hack) ****/ String buf=""; char[] text2,text3; int i,j=0; boolean special=false, html=false; char ctrl; text2 = text.toCharArray(); text3 = new char[text.length()]; for (i = 0; i < text.length(); i++) { char c = text2[i]; if (c == '&') { special = true; buf = ""; } else if (special) { if (c == ';') { special = false; if (buf.equals("lt")) text3[j++] = '<'; else if (buf.equals("gt")) text3[j++] = '>'; else if (buf.equals("amp")) text3[j++] = '&'; } else buf += c; } else if (c == '<') { html = true; ctrl = text2[i+1]; } else if (c == '>') html = false; else if (!html) text3[j++] = c; } text = String.valueOf(text3); } Frame f=new TextFrame(fname.substring(fname.lastIndexOf('/')+1),text); f.setSize(500,600); - f.show(); + f.setVisible(true); } } catch (Exception exn) { System.err.println("Can't read file "+fname); } } public void PS(String fname,boolean printable) throws IOException { gv.PS(fname,printable); } public boolean isEmpty() { return tb==null; } public void initBrowser(InputStream is, boolean noAWT) { try { Font font = noAWT ? null : new Font("Helvetica", Font.PLAIN, 12); TreeNode tn = new TreeNode("Root", "", -1, true); gv = new GraphView(new Graph(is, tn), this, font); tb = new TreeBrowser(tn, gv, font); gv.setTreeBrowser(tb); Vector v = new Vector(10,10); tn.collapsedDirectories(v); gv.collapseDir(v); ScrollPane scrollp1 = new ScrollPane(); ScrollPane scrollp2 = new ScrollPane(); scrollp1.add(gv); scrollp2.add(tb); scrollp1.getHAdjustable().setUnitIncrement(20); scrollp1.getVAdjustable().setUnitIncrement(20); scrollp2.getHAdjustable().setUnitIncrement(20); scrollp2.getVAdjustable().setUnitIncrement(20); Component gv2 = new Border(scrollp1, 3); Component tb2 = new Border(scrollp2, 3); GridBagLayout gridbag = new GridBagLayout(); GridBagConstraints cnstr = new GridBagConstraints(); setLayout(gridbag); cnstr.fill = GridBagConstraints.BOTH; cnstr.insets = new Insets(5,5,5,5); cnstr.weightx = 1; cnstr.weighty = 1; cnstr.gridwidth = 1; gridbag.setConstraints(tb2,cnstr); add(tb2); cnstr.weightx = 2.5; cnstr.gridwidth = GridBagConstraints.REMAINDER; gridbag.setConstraints(gv2,cnstr); add(gv2); } catch (IOException exn) { System.err.println("\nI/O error while reading graph file."); } catch (ParseError exn) { System.err.println("\nParse error in graph file:"); System.err.println(exn.getMessage()); System.err.println("\nSyntax:\n [ + ] [ < | > ] [ [ ... [ ] ... ] ] ;"); } } public void init() { isApplet=true; gfname=getParameter("graphfile"); try { InputStream is=(new URL(getDocumentBase(), gfname)).openConnection().getInputStream(); initBrowser(is, false); is.close(); } catch (MalformedURLException exn) { System.err.println("Invalid URL: "+gfname); } catch (IOException exn) { System.err.println("I/O error while reading "+gfname+"."); } } public static void main(String[] args) { isApplet=false; try { GraphBrowser gb=new GraphBrowser(args.length > 0 ? args[0] : ""); if (args.length > 0) { InputStream is=new FileInputStream(args[0]); gb.initBrowser(is, args.length > 1); is.close(); } if (args.length > 1) { try { if (args[1].endsWith(".ps")) gb.gv.PS(args[1], true); else if (args[1].endsWith(".eps")) gb.gv.PS(args[1], false); else System.err.println("Unknown file type: " + args[1]); } catch (IOException exn) { System.err.println("Unable to write file " + args[1]); } } else { f=new GraphBrowserFrame(gb); f.setSize(700,500); - f.show(); + f.setVisible(true); } } catch (IOException exn) { System.err.println("Can't open graph file "+args[0]); } } } diff --git a/lib/browser/GraphBrowser/GraphBrowserFrame.java b/src/Tools/GraphBrowser/graphbrowser/GraphBrowserFrame.java rename from lib/browser/GraphBrowser/GraphBrowserFrame.java rename to src/Tools/GraphBrowser/graphbrowser/GraphBrowserFrame.java --- a/lib/browser/GraphBrowser/GraphBrowserFrame.java +++ b/src/Tools/GraphBrowser/graphbrowser/GraphBrowserFrame.java @@ -1,125 +1,125 @@ /*************************************************************************** - Title: GraphBrowser/GraphBrowserFrame.java + Title: graphbrowser/GraphBrowserFrame.java Author: Stefan Berghofer, TU Muenchen Options: :tabSize=2: This class is the frame for the stand-alone application. It contains methods for handling menubar events. ***************************************************************************/ -package GraphBrowser; +package isabelle.graphbrowser; import java.awt.*; import java.awt.event.*; import java.io.*; -import awtUtilities.*; +import isabelle.awt.*; public class GraphBrowserFrame extends Frame implements ActionListener { GraphBrowser gb; MenuItem i1, i2; String graphDir, psDir; public void checkMenuItems() { if (gb.isEmpty()) { i1.setEnabled(false); i2.setEnabled(false); } else { i1.setEnabled(true); i2.setEnabled(true); } } public void actionPerformed(ActionEvent evt) { String label = evt.getActionCommand(); if (label.equals("Quit")) System.exit(0); else if (label.equals("Export to PostScript")) { PS(true, label); return; } else if (label.equals("Export to EPS")) { PS(false, label); return; } else if (label.equals("Open ...")) { FileDialog fd = new FileDialog(this, "Open graph file", FileDialog.LOAD); if (graphDir != null) fd.setDirectory(graphDir); fd.setVisible(true); if (fd.getFile() == null) return; graphDir = fd.getDirectory(); String fname = graphDir + fd.getFile(); GraphBrowser gb2 = new GraphBrowser(fname); try { InputStream is = new FileInputStream(fname); gb2.initBrowser(is, false); is.close(); } catch (IOException exn) { String button[] = {"OK"}; MessageDialog md = new MessageDialog(this, "Error", "Can't open file " + fname + ".", button); md.setSize(350, 200); md.setVisible(true); return; } remove(gb); add("Center", gb2); gb = gb2; checkMenuItems(); validate(); } } public void PS(boolean printable,String label) { FileDialog fd=new FileDialog(this,label,FileDialog.SAVE); if (psDir!=null) fd.setDirectory(psDir); fd.setVisible(true); if (fd.getFile()==null) return; psDir=fd.getDirectory(); String fname=psDir+fd.getFile(); if ((new File(fname)).exists()) { String buttons[]={"Overwrite","Cancel"}; MessageDialog md=new MessageDialog(this,"Warning", "Warning: File "+fname+" already exists. Overwrite?", buttons); md.setSize(350,200); md.setVisible(true); if (md.getText().equals("Cancel")) return; } try { gb.PS(fname,printable); } catch (IOException exn) { String button[]={"OK"}; MessageDialog md=new MessageDialog(this,"Error", "Unable to write file "+fname+".",button); md.setSize(350,200); md.setVisible(true); } } public GraphBrowserFrame(GraphBrowser br) { super("GraphBrowser"); MenuItem i3, i4; gb = br; MenuBar mb = new MenuBar(); Menu m1 = new Menu("File"); m1.add(i3 = new MenuItem("Open ...")); m1.add(i1 = new MenuItem("Export to PostScript")); m1.add(i2 = new MenuItem("Export to EPS")); m1.add(i4 = new MenuItem("Quit")); i1.addActionListener(this); i2.addActionListener(this); i3.addActionListener(this); i4.addActionListener(this); checkMenuItems(); mb.add(m1); setMenuBar(mb); add("Center", br); addWindowListener( new WindowAdapter() { public void windowClosing(WindowEvent e) { System.exit(0); } }); } } diff --git a/lib/browser/GraphBrowser/GraphView.java b/src/Tools/GraphBrowser/graphbrowser/GraphView.java rename from lib/browser/GraphBrowser/GraphView.java rename to src/Tools/GraphBrowser/graphbrowser/GraphView.java --- a/lib/browser/GraphBrowser/GraphView.java +++ b/src/Tools/GraphBrowser/graphbrowser/GraphView.java @@ -1,276 +1,276 @@ /*************************************************************************** - Title: GraphBrowser/GraphView.java + Title: graphbrowser/GraphView.java Author: Stefan Berghofer, TU Muenchen Options: :tabSize=4: This class defines the window in which the graph is displayed. It contains methods for handling events such as collapsing / uncollapsing nodes of the graph. ***************************************************************************/ -package GraphBrowser; +package isabelle.graphbrowser; import java.awt.*; import java.awt.event.*; import java.io.*; import java.util.*; public class GraphView extends Canvas implements MouseListener, MouseMotionListener { Graph gra, gra2; GraphBrowser browser; Vertex v = null; Vector collapsed = new Vector(10,10); Vector collapsedDirs = new Vector(10,10); TreeBrowser tb; long timestamp; Vertex highlighted = null; Dimension size; boolean parent_needs_layout; Font font; public void setTreeBrowser(TreeBrowser br) { tb=br; } public GraphBrowser getBrowser() { return browser; } public Graph getGraph() { return gra; } public Graph getOriginalGraph() { return gra2; } public GraphView(Graph gr, GraphBrowser br, Font f) { gra2=gr; browser=br; gra=(Graph)(gra2.clone()); parent_needs_layout = true; size = new Dimension(0, 0); font = f; addMouseListener(this); addMouseMotionListener(this); } public void PS(String fname,boolean printable) throws IOException { Graph gra3 = (Graph)gra.clone(); gra3.layout(null); gra3.PS(fname,printable); } public void paint(Graphics g) { g.setFont(font); gra.draw(g); if (highlighted!=null) highlighted.drawBox(g,Color.white); size = new Dimension(gra.max_x-gra.min_x, gra.max_y-gra.min_y); if (parent_needs_layout) { parent_needs_layout = false; getParent().doLayout(); } } public Dimension getPreferredSize() { return size; } public void mouseMoved(MouseEvent evt) { int x = evt.getX() + gra.min_x; int y = evt.getY() + gra.min_y; Vertex v2=gra.vertexAt(x,y); Graphics g=getGraphics(); g.setFont(font); g.translate(-gra.min_x,-gra.min_y); if (highlighted!=null) { highlighted.drawBox(g,Color.lightGray); highlighted=null; } if (v2!=v) { if (v!=null) v.removeButtons(g); if (v2!=null) v2.drawButtons(g); v=v2; } } public void mouseDragged(MouseEvent evt) {} /*****************************************************************/ /* This method is called if successor / predecessor nodes (whose */ /* numbers are stored in Vector c) of a certain node should be */ /* displayed again */ /*****************************************************************/ void uncollapse(Vector c) { collapsed.removeElement(c); collapseNodes(); } /*****************************************************************/ /* This method is called by class TreeBrowser when directories */ /* are collapsed / uncollapsed by the user */ /*****************************************************************/ public void collapseDir(Vector v) { collapsedDirs=v; collapseNodes(); } /*****************************************************************/ /* Inflate node again */ /*****************************************************************/ public void inflateNode(Vector c) { Enumeration e1; e1=collapsedDirs.elements(); while (e1.hasMoreElements()) { Directory d=(Directory)(e1.nextElement()); if (d.collapsed==c) { tb.selectNode(d.getNode()); return; } } collapsed.removeElement(c); e1=gra2.getVertices(); while (e1.hasMoreElements()) { Vertex vx=(Vertex)(e1.nextElement()); if (vx.getUp()==c) vx.setUp(null); if (vx.getDown()==c) vx.setDown(null); } collapseNodes(); relayout(); } public void relayout() { Graphics g = getGraphics(); g.setFont(font); browser.showWaitMessage(); highlighted=null; gra.layout(g); v=null; parent_needs_layout = true; update(g); browser.showReadyMessage(); } public void focusToVertex(int n) { Vertex vx=gra.getVertexByNum(n); if (vx!=null) { ScrollPane scrollp = (ScrollPane)(getParent()); Dimension vpsize = scrollp.getViewportSize(); int x = vx.getX()-gra.min_x; int y = vx.getY()-gra.min_y; int offset_x = Math.min(scrollp.getHAdjustable().getMaximum(), Math.max(0,x-vpsize.width/2)); int offset_y = Math.min(scrollp.getVAdjustable().getMaximum(), Math.max(0,y-vpsize.height/2)); Graphics g=getGraphics(); g.setFont(font); g.translate(-gra.min_x,-gra.min_y); if (highlighted!=null) highlighted.drawBox(g,Color.lightGray); vx.drawBox(g,Color.white); highlighted=vx; scrollp.setScrollPosition(offset_x, offset_y); } } /*****************************************************************/ /* Create new graph with collapsed nodes */ /*****************************************************************/ public void collapseNodes() { Enumeration e1=collapsed.elements(); gra=(Graph)(gra2.clone()); while (e1.hasMoreElements()) { Vector v1=(Vector)(e1.nextElement()); Vector v2=gra.decode(v1); if (!v2.isEmpty()) gra.collapse(v2,"[. . . .]",v1); } e1=collapsedDirs.elements(); while (e1.hasMoreElements()) { Directory d=(Directory)(e1.nextElement()); Vector v=gra.decode(d.getCollapsed()); if (!v.isEmpty()) gra.collapse(v,"["+d.getName()+"]",d.getCollapsed()); } } public void mouseClicked(MouseEvent evt) { Vector code = null; Vertex v2; int x = evt.getX() + gra.min_x; int y = evt.getY() + gra.min_y; if (v!=null) { int num=v.getNumber(); v2=gra2.getVertexByNum(num); if (v.leftButton(x,y)) { if (v.getUp()!=null) { code=v.getUp(); v2.setUp(null); v=null; uncollapse(code); relayout(); focusToVertex(num); } else { Vector vs=v2.getPreds(); code=gra2.encode(vs); v.setUp(code);v2.setUp(code); v=null; collapsed.insertElementAt(code,0); collapseNodes(); relayout(); focusToVertex(num); } } else if (v.rightButton(x,y)) { if (v.getDown()!=null) { code=v.getDown(); v2.setDown(null); v=null; uncollapse(code); relayout(); focusToVertex(num); } else { Vector vs=v2.getSuccs(); code=gra2.encode(vs); v.setDown(code);v2.setDown(code); v=null; collapsed.insertElementAt(code,0); collapseNodes(); relayout(); focusToVertex(num); } } else if (v.getInflate()!=null) { inflateNode(v.getInflate()); v=null; } else { if (evt.getWhen()-timestamp < 400 && !(v.getPath().equals(""))) browser.viewFile(v.getPath()); timestamp=evt.getWhen(); } } } public void mouseExited(MouseEvent evt) { Graphics g=getGraphics(); g.setFont(font); g.translate(-gra.min_x,-gra.min_y); if (highlighted!=null) { highlighted.drawBox(g,Color.lightGray); highlighted=null; } if (v!=null) v.removeButtons(g); v=null; } public void mouseEntered(MouseEvent evt) {} public void mousePressed(MouseEvent evt) {} public void mouseReleased(MouseEvent evt) {} } diff --git a/lib/browser/GraphBrowser/NormalVertex.java b/src/Tools/GraphBrowser/graphbrowser/NormalVertex.java rename from lib/browser/GraphBrowser/NormalVertex.java rename to src/Tools/GraphBrowser/graphbrowser/NormalVertex.java --- a/lib/browser/GraphBrowser/NormalVertex.java +++ b/src/Tools/GraphBrowser/graphbrowser/NormalVertex.java @@ -1,154 +1,154 @@ /*************************************************************************** - Title: GraphBrowser/NormalVertex.java + Title: graphbrowser/NormalVertex.java Author: Stefan Berghofer, TU Muenchen Options: :tabSize=4: This class represents an ordinary vertex. It contains methods for drawing and PostScript output. ***************************************************************************/ -package GraphBrowser; +package isabelle.graphbrowser; import java.util.*; import java.awt.*; import java.io.*; class NormalVertex extends Vertex { String label="",path="",dir="",ID=""; Vector up,down,inflate=null; public Object clone() { Vertex ve=new NormalVertex(label); ve.setID(ID); ve.setNumber(getNumber()); ve.setUp(getUp());ve.setDown(getDown()); ve.setX(getX());ve.setY(getY()); ve.setPath(getPath()); return ve; } /*** Constructor ***/ public NormalVertex(String s) { label=s; } public void setInflate(Vector v) { inflate=v; } public Vector getInflate() { return inflate; } public Vector getUp() { return up; } public void setUp(Vector v) { up=v; } public Vector getDown() { return down; } public void setDown(Vector v) { down=v; } public String getLabel() {return label;} public void setLabel(String s) {label=s;} public void setID(String s) { ID=s; } public String getID() { return ID; } public String getPath() { return path;} public void setPath(String p) { path=p; } public String getDir() { return dir; } public void setDir(String d) { dir=d; } public int leftX() { return getX()-box_width2(); } public int rightX() { return getX()+box_width2(); } public void drawBox(Graphics g,Color boxColor) { FontMetrics fm = g.getFontMetrics(g.getFont()); int h=fm.getAscent()+fm.getDescent(); g.setColor(boxColor); g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height); g.setColor(Color.black); g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height); if (getNumber()<0) g.setColor(Color.red); g.drawString(label, (int)Math.round((box_width()-fm.stringWidth(label))/2.0)+getX()-box_width2(), fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY()); } public void removeButtons(Graphics g) { drawBox(g,Color.lightGray); } public void draw(Graphics g) { drawBox(g,Color.lightGray); g.setColor(Color.black); Enumeration e1=getChildren(); while (e1.hasMoreElements()) { Vertex v=(Vertex)(e1.nextElement()); if (!v.isDummy()) g.drawLine(getX(),getY()+gra.box_height,v.getX(),v.getY()); } } public boolean contains(int x,int y) { return (x>=leftX() && x<=rightX() && y>=getY() && y<=getY()+gra.box_height); } public boolean leftButton(int x,int y) { return contains(x,y) && x<=leftX()+gra.box_height && getParents().hasMoreElements() && getNumber()>=0; } public boolean rightButton(int x,int y) { return contains(x,y) && x>=rightX()-gra.box_height && getChildren().hasMoreElements() && getNumber()>=0; } public void drawButtons(Graphics g) { if (getNumber()<0) return; int l=gra.box_height*2/3,d=gra.box_height/6; int up_x[] = { leftX()+d , leftX()+d+l/2 , leftX()+d+l }; int up_y[] = { getY()+d+l , getY()+d , getY()+d+l }; int down_x[] = { rightX()-d-l , rightX()-d-l/2 , rightX()-d }; int down_y[] = { getY()+d , getY()+d+l , getY()+d }; if (getParents().hasMoreElements()) { g.setColor(Color.gray); g.fillRect(leftX()+1,getY()+1,gra.box_height-1,gra.box_height-1); g.setColor(getUp()!=null ? Color.red : Color.green); g.fillPolygon(up_x,up_y,3); } if (getChildren().hasMoreElements()) { g.setColor(Color.gray); g.fillRect(rightX()+1-gra.box_height,getY()+1,gra.box_height,gra.box_height-1); g.setColor(getDown()!=null ? Color.red : Color.green); g.fillPolygon(down_x,down_y,3); } g.setColor(Color.black); } public void PS(PrintWriter p) { p.print(leftX()+" "+getY()+" "+box_width()+" "+ gra.box_height+" ("); for (int i=0;i=0) p.print("\\"); p.print(label.charAt(i)); } p.println(") b"); Enumeration e1=getChildren(); while (e1.hasMoreElements()) { Vertex v=(Vertex)(e1.nextElement()); if (!v.isDummy()) p.println("n "+getX()+" "+(getY()+gra.box_height)+ " m "+v.getX()+" "+v.getY()+" l s"); } } } diff --git a/lib/browser/GraphBrowser/ParseError.java b/src/Tools/GraphBrowser/graphbrowser/ParseError.java rename from lib/browser/GraphBrowser/ParseError.java rename to src/Tools/GraphBrowser/graphbrowser/ParseError.java --- a/lib/browser/GraphBrowser/ParseError.java +++ b/src/Tools/GraphBrowser/graphbrowser/ParseError.java @@ -1,5 +1,5 @@ -package GraphBrowser; +package isabelle.graphbrowser; class ParseError extends Exception { public ParseError(String s) { super(s); } } diff --git a/lib/browser/GraphBrowser/Region.java b/src/Tools/GraphBrowser/graphbrowser/Region.java rename from lib/browser/GraphBrowser/Region.java rename to src/Tools/GraphBrowser/graphbrowser/Region.java --- a/lib/browser/GraphBrowser/Region.java +++ b/src/Tools/GraphBrowser/graphbrowser/Region.java @@ -1,89 +1,89 @@ /*************************************************************************** - Title: GraphBrowser/Region.java + Title: graphbrowser/Region.java Author: Stefan Berghofer, TU Muenchen Options: :tabSize=4: This is an auxiliary class which is used by the layout algorithm when calculating coordinates with the "pendulum method". A "region" is a group of nodes which "stick together". ***************************************************************************/ -package GraphBrowser; +package isabelle.graphbrowser; import java.util.*; class Region { Vector vertices=new Vector(10,10); Graph gra; public Region(Graph g) { gra=g; } public void addVertex(Vertex v) { vertices.addElement(v); } public Enumeration getVertices() { return vertices.elements(); } public int pred_deflection() { float d1=0; int n=0; Enumeration e1=vertices.elements(); while (e1.hasMoreElements()) { float d2=0; int p=0; n++; Vertex v=(Vertex)(e1.nextElement()); Enumeration e2=v.getParents(); while (e2.hasMoreElements()) { p++; d2+=((Vertex)(e2.nextElement())).getX()-v.getX(); } if (p>0) d1+=d2/p; } return (int)(Math.round(d1/n)); } public int succ_deflection() { float d1=0; int n=0; Enumeration e1=vertices.elements(); while (e1.hasMoreElements()) { float d2=0; int p=0; n++; Vertex v=(Vertex)(e1.nextElement()); Enumeration e2=v.getChildren(); while (e2.hasMoreElements()) { p++; d2+=((Vertex)(e2.nextElement())).getX()-v.getX(); } if (p>0) d1+=d2/p; } return (int)(Math.round(d1/n)); } public void move(int x) { Enumeration e1=vertices.elements(); while (e1.hasMoreElements()) { Vertex v=(Vertex)(e1.nextElement()); v.setX(v.getX()+x); } } public void combine(Region r2) { Enumeration e1=r2.getVertices(); while (e1.hasMoreElements()) addVertex((Vertex)(e1.nextElement())); } public int spaceBetween(Region r2) { return ((Vertex)(r2.getVertices().nextElement())).leftX()- ((Vertex)(vertices.lastElement())).rightX()- 20; } public boolean touching(Region r2) { return spaceBetween(r2)==0; } } diff --git a/lib/browser/GraphBrowser/Spline.java b/src/Tools/GraphBrowser/graphbrowser/Spline.java rename from lib/browser/GraphBrowser/Spline.java rename to src/Tools/GraphBrowser/graphbrowser/Spline.java --- a/lib/browser/GraphBrowser/Spline.java +++ b/src/Tools/GraphBrowser/graphbrowser/Spline.java @@ -1,120 +1,120 @@ /*************************************************************************** - Title: GraphBrowser/Spline.java + Title: graphbrowser/Spline.java Author: Stefan Berghofer, TU Muenchen Options: :tabSize=4: This class is used for drawing spline curves (which are not yet supported by the Java AWT). ***************************************************************************/ -package GraphBrowser; +package isabelle.graphbrowser; import java.awt.*; import java.util.*; import java.io.*; class SplineSection { /*** Section of a spline function ***/ double x_b,x_c,x_d; double y_b,y_c,y_d; int dx,dy; public SplineSection(double xb,double xc,double xd, double yb,double yc,double yd,int dx2,int dy2) { x_b=xb;x_c=xc;x_d=xd; y_b=yb;y_c=yc;y_d=yd; dx=dx2;dy=dy2; } public Point draw(Graphics g,Point s) { double m; int s_x,s_y,e_x=0,e_y=0; int x,y; s_x=s.x;s_y=s.y; if (dx>=dy) { if (dx==0) return s; m=1/((double)dx); for (x=0;x=starty && y=0) v.addElement(new Integer(number)); + if (number>=0) v.addElement(Integer.valueOf(number)); Enumeration e1=leaves.elements(); while (e1.hasMoreElements()) ((TreeNode)(e1.nextElement())).collapsedNodes(v); } public void collapsedDirectories(Vector v) { if (!unfold) { Vector v2=new Vector(10,10); v.addElement(new Directory(this,name,v2)); collapsedNodes(v2); } else { Enumeration e1=leaves.elements(); while (e1.hasMoreElements()) { TreeNode tn=(TreeNode)(e1.nextElement()); if (!tn.leaves.isEmpty()) tn.collapsedDirectories(v); } } } public Dimension draw(Graphics g,int x,int y,TreeNode t) { FontMetrics fm=g.getFontMetrics(g.getFont()); int h=fm.getHeight(); int e=(int) (h / 10) + 1; int down_x[]={x + e, x + h - e, x + (int)(h / 2)}; int down_y[]={y + e, y + e, y + (int)(3 * h / 4) - e}; int right_x[]={x + e, x + (int)(3 * h / 4) - e, x + e}; int right_y[]={y + e, y + (int)(h / 2), y + h - e}; int dx=0; if (unfold) { g.setColor(Color.green); g.fillPolygon(down_x,down_y,3); g.setColor(Color.black); g.drawString(name,x+h+4,y+fm.getAscent()); starty=y;endy=y+h; dx=Math.max(dx,x+h+4+fm.stringWidth(name)); y+=h+5; for(int i=0;i=0; } public boolean isParent(Vertex v) { return parents.indexOf(v)>=0; } public Enumeration getParents() { return ((Vector)(parents.clone())).elements(); } public void addParent(Vertex v) { parents.addElement(v); v.children.addElement(this); } public void removeParent(Vertex v) { parents.removeElement(v); v.children.removeElement(this); } /********************************************************************/ /* get all predecessor vertices */ /********************************************************************/ public Vector getPreds() { Vector preds=new Vector(10,10); Vector todo=(Vector)(parents.clone()); Vertex vx1,vx2; Enumeration e; while (!todo.isEmpty()) { vx1=(Vertex)(todo.lastElement()); todo.removeElementAt(todo.size()-1); preds.addElement(vx1); e=vx1.parents.elements(); while (e.hasMoreElements()) { vx2=(Vertex)(e.nextElement()); if (preds.indexOf(vx2)<0 && todo.indexOf(vx2)<0) todo.addElement(vx2); } } return preds; } /********************************************************************/ /* get all successor vertices */ /********************************************************************/ public Vector getSuccs() { Vector succs=new Vector(10,10); Vector todo=(Vector)(children.clone()); Vertex vx1,vx2; Enumeration e; while (!todo.isEmpty()) { vx1=(Vertex)(todo.lastElement()); todo.removeElementAt(todo.size()-1); succs.addElement(vx1); e=vx1.children.elements(); while (e.hasMoreElements()) { vx2=(Vertex)(e.nextElement()); if (succs.indexOf(vx2)<0 && todo.indexOf(vx2)<0) todo.addElement(vx2); } } return succs; } public int box_width() { return getLabelSize(gra.gfx).width+8; } public int box_width2() { return box_width()/2; } public void setX(int x) {this.x=x;} public void setY(int y) {this.y=y;} public int getX() {return x;} public int getY() {return y;} public abstract int leftX(); public abstract int rightX(); public abstract void draw(Graphics g); public void drawButtons(Graphics g) {} public void drawBox(Graphics g,Color boxColor) {} public void removeButtons(Graphics g) {} public boolean contains(int x,int y) { return false; } public boolean leftButton(int x,int y) { return false; } public boolean rightButton(int x,int y) { return false; } public void PS(PrintWriter p) {} } diff --git a/lib/Tools/browser b/src/Tools/GraphBrowser/lib/Tools/browser rename from lib/Tools/browser rename to src/Tools/GraphBrowser/lib/Tools/browser --- a/lib/Tools/browser +++ b/src/Tools/GraphBrowser/lib/Tools/browser @@ -1,110 +1,108 @@ #!/usr/bin/env bash # # Author: Markus Wenzel, TU Muenchen # # DESCRIPTION: Isabelle graph browser PRG="$(basename "$0")" function usage() { echo echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]" echo echo " Options are:" echo " -b Admin/build only" echo " -c cleanup -- remove GRAPHFILE after use" echo " -o FILE output to FILE (ps, eps, pdf)" echo exit 1 } function fail() { echo "$1" >&2 exit 2 } ## process command line # options ADMIN_BUILD="" CLEAN="" OUTFILE="" while getopts "bco:" OPT do case "$OPT" in b) ADMIN_BUILD=true ;; c) CLEAN=true ;; o) OUTFILE="$OPTARG" ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args GRAPHFILE="" [ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; } [ "$#" -ne 0 ] && usage ## main -isabelle_admin_build browser || exit $? - -classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar" +isabelle_scala_build || exit $? if [ -n "$GRAPHFILE" ]; then PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE") if [ -n "$CLEAN" ]; then mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE" else cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE" fi PDF="" case "$OUTFILE" in *.pdf) OUTFILE="${OUTFILE%%.pdf}.eps" PDF=true ;; esac if [ -z "$OUTFILE" ]; then - isabelle java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")" + isabelle java isabelle.graphbrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")" else - isabelle java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")" + isabelle java isabelle.graphbrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")" fi RC="$?" if [ -n "$PDF" ]; then ( cd "$(dirname "$OUTFILE")" "$ISABELLE_EPSTOPDF" "$(basename "$OUTFILE")" || fail "Failed to produce pdf output" ) fi rm -f "$PRIVATE_FILE" elif [ -z "$ADMIN_BUILD" ]; then [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" - exec isabelle java GraphBrowser.GraphBrowser + exec isabelle java isabelle.graphbrowser.GraphBrowser else RC=0 fi exit "$RC" diff --git a/src/Tools/Setup/isabelle/setup/Build.java b/src/Tools/Setup/isabelle/setup/Build.java --- a/src/Tools/Setup/isabelle/setup/Build.java +++ b/src/Tools/Setup/isabelle/setup/Build.java @@ -1,498 +1,535 @@ /* Title: Tools/Setup/isabelle/setup/Build.java Author: Makarius Build Isabelle/Scala/Java modules. */ package isabelle.setup; import java.io.BufferedOutputStream; +import java.io.ByteArrayInputStream; +import java.io.ByteArrayOutputStream; +import java.io.CharArrayWriter; import java.io.File; import java.io.IOException; +import java.io.InputStream; +import java.io.PrintStream; import java.math.BigInteger; import java.nio.charset.StandardCharsets; import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.StandardCopyOption; import java.security.MessageDigest; import java.security.NoSuchAlgorithmException; import java.util.ArrayList; import java.util.Comparator; import java.util.LinkedList; import java.util.List; import java.util.Locale; import java.util.Properties; import java.util.TreeMap; import java.util.jar.Attributes; import java.util.jar.JarEntry; import java.util.jar.JarFile; import java.util.jar.JarOutputStream; import java.util.jar.Manifest; import java.util.stream.Stream; import javax.tools.JavaCompiler; import javax.tools.JavaFileObject; import javax.tools.StandardJavaFileManager; import javax.tools.ToolProvider; import scala.tools.nsc.MainClass; public class Build { /** context **/ public static String BUILD_PROPS = "build.props"; public static String COMPONENT_BUILD_PROPS = "etc/build.props"; public static Context directory_context(Path dir) throws IOException { Properties props = new Properties(); props.load(Files.newBufferedReader(dir.resolve(BUILD_PROPS))); return new Context(dir, props); } public static Context component_context(Path dir) throws IOException { Properties props = new Properties(); Path build_props = dir.resolve(COMPONENT_BUILD_PROPS); if (Files.exists(build_props)) { props.load(Files.newBufferedReader(build_props)); } return new Context(dir, props); } public static List component_contexts() throws IOException, InterruptedException { List result = new LinkedList(); for (String p : Environment.getenv("ISABELLE_COMPONENTS").split(":", -1)) { if (!p.isEmpty()) { Path dir = Path.of(Environment.platform_path(p)); if (Files.exists(dir.resolve(COMPONENT_BUILD_PROPS))) { result.add(component_context(dir)); } } } return List.copyOf(result); } private static String sha_digest(MessageDigest sha, String name) { String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest())); return digest + " " + name + "\n"; } public static class Context { private final Path _dir; private final Properties _props; public Context(Path dir, Properties props) { _dir = dir; _props = props; } @Override public String toString() { return _dir.toString(); } public String name() { return _props.getProperty("name", _dir.toFile().getName()); } public String description() { return _props.getProperty("description", name()); } public String lib_name() { return _props.getProperty("lib", "lib") + "/" + name(); } public String jar_name() { return lib_name() + ".jar"; } public String scalac_options() { return _props.getProperty("scalac_options", ""); } public String javac_options() { return _props.getProperty("javac_options", ""); } public String main() { return _props.getProperty("main", ""); } private List get_list(String name) { List list = new LinkedList(); for (String s : _props.getProperty(name, "").split("\\s+")) { if (!s.isEmpty()) { list.add(s); } } return List.copyOf(list); } public List requirements() { return get_list("requirements"); } public List sources() { return get_list("sources"); } public List resources() { return get_list("resources"); } public List services() { return get_list("services"); } public boolean is_vacuous() { return sources().isEmpty() && resources().isEmpty() && services().isEmpty(); } public Path path(String file) throws IOException, InterruptedException { return _dir.resolve(Environment.expand_platform_path(file)); } public boolean exists(String file) throws IOException, InterruptedException { return Files.exists(path(file)); } public String item_name(String s) { int i = s.indexOf(':'); return i > 0 ? s.substring(0, i) : s; } public String item_target(String s) { int i = s.indexOf(':'); return i > 0 ? s.substring(i + 1) : s; } public String shasum(String name, List paths) throws IOException, NoSuchAlgorithmException { MessageDigest sha = MessageDigest.getInstance("SHA"); for (Path file : paths) { if (Files.exists(file)) { sha.update(Files.readAllBytes(file)); } else { throw new RuntimeException( "Missing input file " + Environment.quote(file.toString())); } } return sha_digest(sha, name); } public String shasum(String file) throws IOException, NoSuchAlgorithmException, InterruptedException { return shasum(file, List.of(path(file))); } public String shasum_props() throws NoSuchAlgorithmException { TreeMap sorted = new TreeMap(); for (Object x : _props.entrySet()) { sorted.put(x.toString(), _props.get(x)); } MessageDigest sha = MessageDigest.getInstance("SHA"); sha.update(sorted.toString().getBytes(StandardCharsets.UTF_8)); return sha_digest(sha, ""); } } /** compile sources **/ private static void add_options(List options_list, String options) { if (options != null) { for (String s : options.split("\\s+")) { if (!s.isEmpty()) { options_list.add(s); } } } } + private static void compiler_result(boolean ok, String out, String what) + { + if (ok) { if (!out.isEmpty()) { System.err.println(out); } } + else { + String msg = "Failed to compile " + what + (out.isEmpty() ? "" : ":\n" + out); + throw new RuntimeException(msg); + } + } + public static void compile_scala_sources( Path target_dir, String more_options, List deps, List sources) throws IOException, InterruptedException { ArrayList args = new ArrayList(); add_options(args, Environment.getenv("ISABELLE_SCALAC_OPTIONS")); add_options(args, more_options); args.add("-d"); args.add(target_dir.toString()); args.add("-bootclasspath"); args.add(Environment.join_platform_paths(deps)); args.add("--"); boolean scala_sources = false; for (Path p : sources) { args.add(p.toString()); if (p.toString().endsWith(".scala")) { scala_sources = true; } } if (scala_sources) { - MainClass main = new MainClass(); - boolean ok = main.process(args.toArray(String[]::new)); - if (!ok) throw new RuntimeException("Failed to compile Scala sources"); + boolean ok = false; + + InputStream in_orig = System.in; + PrintStream out_orig = System.out; + PrintStream err_orig = System.err; + ByteArrayInputStream in = new ByteArrayInputStream(new byte[0]); + ByteArrayOutputStream out = new ByteArrayOutputStream(); + + // Single-threaded context! + try { + PrintStream out_stream = new PrintStream(out); + System.setIn(in); + System.setOut(out_stream); + System.setErr(out_stream); + ok = new MainClass().process(args.toArray(String[]::new)); + out_stream.flush(); + } + finally { + System.setIn(in_orig); + System.setOut(out_orig); + System.setErr(err_orig); + } + compiler_result(ok, out.toString(StandardCharsets.UTF_8), "Scala sources"); } } public static void compile_java_sources( Path target_dir, String more_options, List deps, List sources) throws IOException, InterruptedException { JavaCompiler compiler = ToolProvider.getSystemJavaCompiler(); StandardJavaFileManager file_manager = compiler.getStandardFileManager(null, Locale.ROOT, StandardCharsets.UTF_8); List options = new LinkedList(); add_options(options, Environment.getenv("ISABELLE_JAVAC_OPTIONS")); add_options(options, more_options); options.add("-d"); options.add(target_dir.toString()); options.add("-classpath"); options.add(Environment.join_platform_paths(deps)); List java_sources = new LinkedList(); for (Path p : sources) { if (p.toString().endsWith(".java")) { for (JavaFileObject o : file_manager.getJavaFileObjectsFromPaths(List.of(p))) { java_sources.add(o); } } } + if (!java_sources.isEmpty()) { - boolean ok = compiler.getTask(null, file_manager, null, options, null, java_sources).call(); - if (!ok) throw new RuntimeException("Failed to compile Java sources"); + CharArrayWriter out = new CharArrayWriter(); + boolean ok = compiler.getTask(out, file_manager, null, options, null, java_sources).call(); + out.flush(); + compiler_result(ok, out.toString(), "Java sources"); } } /** shasum for jar content **/ private static String SHASUM = "META-INF/isabelle/shasum"; public static String get_shasum(Path jar_path) throws IOException { if (Files.exists(jar_path)) { try (JarFile jar_file = new JarFile(jar_path.toFile())) { JarEntry entry = jar_file.getJarEntry(SHASUM); if (entry != null) { byte[] bytes = jar_file.getInputStream(entry).readAllBytes(); return new String(bytes, StandardCharsets.UTF_8); } else { return ""; } } } else { return ""; } } public static void create_shasum(Path dir, String shasum) throws IOException { Path path = dir.resolve(SHASUM); Files.createDirectories(path.getParent()); Files.writeString(path, shasum); } /** services **/ private static String SERVICES = "META-INF/isabelle/services"; public static List get_services(Path jar_path) throws IOException { if (Files.exists(jar_path)) { try (JarFile jar_file = new JarFile(jar_path.toFile())) { JarEntry entry = jar_file.getJarEntry(SERVICES); if (entry != null) { byte[] bytes = jar_file.getInputStream(entry).readAllBytes(); return Library.split_lines(new String(bytes, StandardCharsets.UTF_8)); } else { return List.of(); } } } else { return List.of(); } } public static void create_services(Path dir, List services) throws IOException { if (!services.isEmpty()) { Path path = dir.resolve(SERVICES); Files.createDirectories(path.getParent()); Files.writeString(path, Library.cat_lines(services)); } } /** create jar **/ public static void create_jar(Path dir, String main, Path jar) throws IOException { Files.createDirectories(dir.resolve(jar).getParent()); Files.deleteIfExists(jar); Manifest manifest = new Manifest(); Attributes attributes = manifest.getMainAttributes(); attributes.put(Attributes.Name.MANIFEST_VERSION, "1.0"); attributes.put(new Attributes.Name("Created-By"), System.getProperty("java.version") + " (" + System.getProperty("java.vendor") + ")"); if (!main.isEmpty()) { attributes.put(Attributes.Name.MAIN_CLASS, main); } try (JarOutputStream out = new JarOutputStream(new BufferedOutputStream(Files.newOutputStream(jar)), manifest)) { for (Path path : Files.walk(dir).sorted().toArray(Path[]::new)) { boolean is_dir = Files.isDirectory(path); boolean is_file = Files.isRegularFile(path); if (is_dir || is_file) { String name = Environment.slashes(dir.relativize(path).toString()); if (!name.isEmpty()) { JarEntry entry = new JarEntry(is_dir ? name + "/" : name); entry.setTime(path.toFile().lastModified()); out.putNextEntry(entry); if (is_file) { out.write(Files.readAllBytes(path)); } out.closeEntry(); } } } } } /** classpath **/ public static List classpath() throws IOException, InterruptedException { List result = new LinkedList(); for (Context context : component_contexts()) { result.add(context.path(context.jar_name())); } return List.copyOf(result); } public static List services() throws IOException, InterruptedException { List result = new LinkedList(); for (Context context : component_contexts()) { for (String s : context.services()) { result.add(s); } } return List.copyOf(result); } /** build **/ public static void build(Context context, boolean fresh) throws IOException, InterruptedException, NoSuchAlgorithmException { String jar_name = context.jar_name(); Path jar_path = context.path(jar_name); List requirements = context.requirements(); List resources = context.resources(); List sources = context.sources(); if (context.is_vacuous()) { Files.deleteIfExists(jar_path); } else { String shasum_old = get_shasum(jar_path); String shasum; List compiler_deps = new LinkedList(); { StringBuilder _shasum = new StringBuilder(); _shasum.append(context.shasum_props()); for (String s : requirements) { if (s.startsWith("env:")) { List paths = new LinkedList(); for (String p : Environment.getenv(s.substring(4)).split(":", -1)) { if (!p.isEmpty()) { Path path = Path.of(Environment.platform_path(p)); compiler_deps.add(path); paths.add(path); } } _shasum.append(context.shasum(s, paths)); } else { compiler_deps.add(context.path(s)); _shasum.append(context.shasum(s)); } } for (String s : resources) { _shasum.append(context.shasum(context.item_name(s))); } for (String s : sources) { _shasum.append(context.shasum(s)); } shasum = _shasum.toString(); } if (fresh || !shasum_old.equals(shasum)) { System.out.print( "### Building " + context.description() + " (" + jar_path + ") ...\n"); String isabelle_class_path = Environment.getenv("ISABELLE_CLASSPATH"); Path build_dir = Files.createTempDirectory("isabelle"); try { /* compile sources */ for (String s : isabelle_class_path.split(":", -1)) { if (!s.isEmpty()) { compiler_deps.add(Path.of(Environment.platform_path(s))); } } List compiler_sources = new LinkedList(); for (String s : sources) { compiler_sources.add(context.path(s)); } compile_scala_sources( build_dir, context.scalac_options(), compiler_deps, compiler_sources); compiler_deps.add(build_dir); compile_java_sources( build_dir, context.javac_options(), compiler_deps, compiler_sources); /* copy resources */ for (String s : context.resources()) { String name = context.item_name(s); String target = context.item_target(s); Path file_name = Path.of(name).normalize().getFileName(); Path target_path = Path.of(target).normalize(); Path target_dir; Path target_file; { if (target.endsWith("/") || target.endsWith("/.")) { target_dir = build_dir.resolve(target_path); target_file = target_dir.resolve(file_name); } else { target_file = build_dir.resolve(target_path); target_dir = target_file.getParent(); } } Files.createDirectories(target_dir); Files.copy(context.path(name), target_file, StandardCopyOption.COPY_ATTRIBUTES); } /* packaging */ create_shasum(build_dir, shasum); create_services(build_dir, context.services()); create_jar(build_dir, context.main(), jar_path); } finally { try (Stream walk = Files.walk(build_dir)) { walk.sorted(Comparator.reverseOrder()) .map(Path::toFile) .forEach(File::delete); } } } } } public static void build_components(boolean fresh) throws IOException, InterruptedException, NoSuchAlgorithmException { for (Context context : component_contexts()) { build(context, fresh); } } } diff --git a/src/Tools/Setup/isabelle/setup/Library.java b/src/Tools/Setup/isabelle/setup/Library.java --- a/src/Tools/Setup/isabelle/setup/Library.java +++ b/src/Tools/Setup/isabelle/setup/Library.java @@ -1,52 +1,48 @@ /* Title: Tools/Setup/isabelle/setup/Library.java Author: Makarius Basic library. */ package isabelle.setup; import java.util.Arrays; import java.util.LinkedList; import java.util.List; public class Library { public static String cat_lines(Iterable lines) { return String.join("\n", lines); } public static List split_lines(String str) { if (str.isEmpty()) { return List.of(); } else { List result = new LinkedList(); result.addAll(Arrays.asList(str.split("\\n"))); return List.copyOf(result); } } public static String prefix_lines(String prfx, String str) { if (str.isEmpty()) { return str; } else { - StringBuilder result = new StringBuilder(); - for (String s : split_lines(str)) { - result.append(prfx); - result.append(s); - result.append('\n'); - } - return result.toString(); + List lines = new LinkedList(); + for (String line : split_lines(str)) { lines.add(prfx + line); } + return cat_lines(lines); } } public static String trim_line(String s) { if (s.endsWith("\r\n")) { return s.substring(0, s.length() - 2); } else if (s.endsWith("\r") || s.endsWith("\n")) { return s.substring(0, s.length() - 1); } else { return s; } } } \ No newline at end of file diff --git a/src/Tools/jEdit/jedit_base/plugin.props b/src/Tools/jEdit/jedit_base/plugin.props --- a/src/Tools/jEdit/jedit_base/plugin.props +++ b/src/Tools/jEdit/jedit_base/plugin.props @@ -1,17 +1,17 @@ ## Isabelle/jEdit plugin properties ## ##:wrap=soft:maxLineLen=100: #identification plugin.isabelle.jedit_base.Plugin.name=Isabelle Base plugin.isabelle.jedit_base.Plugin.author=Makarius Wenzel plugin.isabelle.jedit_base.Plugin.version=1.0 -plugin.isabelle.jedit_base.Plugin.description=Isabelle Base: DO NOT UNLOAD! +plugin.isabelle.jedit_base.Plugin.description=Isabelle/jEdit base plugin: DO NOT UNLOAD! #system parameters plugin.isabelle.jedit_base.Plugin.activate=startup plugin.isabelle.jedit_base.Plugin.usePluginHome=false #dependencies plugin.isabelle.jedit_base.Plugin.depend.0=jdk 11 plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.05.00.00 diff --git a/src/Tools/jEdit/jedit_main/plugin.props b/src/Tools/jEdit/jedit_main/plugin.props --- a/src/Tools/jEdit/jedit_main/plugin.props +++ b/src/Tools/jEdit/jedit_main/plugin.props @@ -1,111 +1,111 @@ ## Isabelle/jEdit plugin properties ## ##:wrap=soft:maxLineLen=100: #identification -plugin.isabelle.jedit_main.Plugin.name=Isabelle +plugin.isabelle.jedit_main.Plugin.name=Isabelle Main plugin.isabelle.jedit_main.Plugin.author=Johannes H\u00F6lzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel plugin.isabelle.jedit_main.Plugin.version=11.2 -plugin.isabelle.jedit_main.Plugin.description=Isabelle Prover IDE +plugin.isabelle.jedit_main.Plugin.description=Isabelle/jEdit main plugin #system parameters plugin.isabelle.jedit_main.Plugin.activate=defer plugin.isabelle.jedit_main.Plugin.usePluginHome=false #dependencies plugin.isabelle.jedit_main.Plugin.depend.0=jdk 11 plugin.isabelle.jedit_main.Plugin.depend.1=jedit 05.05.00.00 plugin.isabelle.jedit_main.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4 plugin.isabelle.jedit_main.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3 plugin.isabelle.jedit_main.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8 plugin.isabelle.jedit_main.Plugin.depend.5=plugin isabelle.jedit_base.Plugin 1.0 #options plugin.isabelle.jedit_main.Plugin.option-group=isabelle-general isabelle-rendering options.isabelle-general.label=General options.isabelle-general.code=new isabelle.jedit.Isabelle_Options1(); options.isabelle-rendering.label=Rendering options.isabelle-rendering.code=new isabelle.jedit.Isabelle_Options2(); #menu actions and dockables plugin.isabelle.jedit_main.Plugin.menu.label=Isabelle plugin.isabelle.jedit_main.Plugin.menu= \ isabelle-export-browser \ isabelle-session-browser \ isabelle.preview \ isabelle.draft \ isabelle.java-monitor \ - \ isabelle-debugger \ isabelle-documentation \ isabelle-monitor \ isabelle-output \ isabelle-protocol \ isabelle-query \ isabelle-raw-output \ isabelle-simplifier-trace \ isabelle-sledgehammer \ isabelle-state \ isabelle-symbols \ isabelle-syslog \ isabelle-theories \ isabelle-timing isabelle-debugger.label=Debugger panel isabelle-debugger.title=Debugger isabelle-documentation.label=Documentation panel isabelle-documentation.title=Documentation isabelle-graphview.label=Graphview panel isabelle-graphview.title=Graphview isabelle-info.label=Info panel isabelle-info.title=Info isabelle-monitor.label=Monitor panel isabelle-monitor.title=Monitor isabelle-output.label=Output panel isabelle-output.title=Output isabelle-protocol.label=Protocol panel isabelle-protocol.title=Protocol isabelle-query.label=Query panel isabelle-query.title=Query isabelle-raw-output.label=Raw Output panel isabelle-raw-output.title=Raw Output isabelle-simplifier-trace.label=Simplifier Trace panel isabelle-simplifier-trace.title=Simplifier Trace isabelle-sledgehammer.label=Sledgehammer panel isabelle-sledgehammer.title=Sledgehammer isabelle-state.label=State panel isabelle-state.title=State isabelle-symbols.label=Symbols panel isabelle-symbols.title=Symbols isabelle-syslog.label=Syslog panel isabelle-syslog.title=Syslog isabelle-theories.label=Theories panel isabelle-theories.title=Theories isabelle-timing.label=Timing panel isabelle-timing.title=Timing #SideKick mode.isabelle-news.folding=sidekick mode.isabelle-news.sidekick.parser=isabelle-news mode.isabelle-options.folding=sidekick mode.isabelle-options.sidekick.parser=isabelle-options mode.isabelle-root.folding=sidekick mode.isabelle-root.sidekick.parser=isabelle-root mode.isabelle.customSettings=true mode.isabelle.folding=isabelle mode.isabelle.sidekick.parser=isabelle mode.isabelle.sidekick.showStatusWindow.label=true mode.isabelle-ml.folding=sidekick mode.isabelle-ml.sidekick.parser=isabelle-ml mode.sml.folding=sidekick mode.sml.sidekick.parser=isabelle-sml mode.bibtex.folding=sidekick mode.bibtex.sidekick.parser=bibtex sidekick.parser.isabelle.label=isabelle sidekick.parser.isabelle-context.label=isabelle-context sidekick.parser.isabelle-markup.label=isabelle-markup sidekick.parser.isabelle-ml.label=isabelle-ml sidekick.parser.isabelle-sml.label=isabelle-sml sidekick.parser.isabelle-news.label=isabelle-news sidekick.parser.isabelle-options.label=isabelle-options sidekick.parser.isabelle-root.label=isabelle-root sidekick.parser.bibtex.label=bibtex diff --git a/src/Tools/jEdit/jedit_main/scala_console.scala b/src/Tools/jEdit/jedit_main/scala_console.scala --- a/src/Tools/jEdit/jedit_main/scala_console.scala +++ b/src/Tools/jEdit/jedit_main/scala_console.scala @@ -1,182 +1,182 @@ /* Title: Tools/jEdit/jedit_main/scala_console.scala Author: Makarius Scala instance of Console plugin. */ package isabelle.jedit_main import isabelle._ import isabelle.jedit._ import console.{Console, ConsolePane, Shell, Output} import org.gjt.sp.jedit.JARClassLoader import java.io.{OutputStream, Writer, PrintWriter} class Scala_Console extends Shell("Scala") { /* global state -- owned by GUI thread */ @volatile private var interpreters = Map.empty[Console, Interpreter] @volatile private var global_console: Console = null @volatile private var global_out: Output = null @volatile private var global_err: Output = null private val console_stream = new OutputStream { val buf = new StringBuilder(100) override def flush(): Unit = { val s = buf.synchronized { val s = buf.toString; buf.clear(); s } val str = UTF8.decode_permissive(s) GUI_Thread.later { - if (global_out == null) System.out.print(str) + if (global_out == null) java.lang.System.out.print(str) else global_out.writeAttrs(null, str) } Time.seconds(0.01).sleep() // FIXME adhoc delay to avoid loosing output } override def close(): Unit = flush() def write(byte: Int): Unit = { val c = byte.toChar buf.synchronized { buf.append(c) } if (c == '\n') flush() } } private val console_writer = new Writer { def flush(): Unit = console_stream.flush() def close(): Unit = console_stream.flush() def write(cbuf: Array[Char], off: Int, len: Int): Unit = { if (len > 0) { UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_)) } } } private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = { global_console = console global_out = out global_err = if (err == null) out else err try { scala.Console.withErr(console_stream) { scala.Console.withOut(console_stream) { e } } } finally { console_stream.flush global_console = null global_out = null global_err = null } } private def report_error(str: String): Unit = { if (global_console == null || global_err == null) isabelle.Output.writeln(str) else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) } } /* interpreter thread */ private abstract class Request private case class Start(console: Console) extends Request private case class Execute(console: Console, out: Output, err: Output, command: String) extends Request private class Interpreter { private val running = Synchronized[Option[Thread]](None) def interrupt(): Unit = running.change(opt => { opt.foreach(_.interrupt()); opt }) private val interp = Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories). interpreter( print_writer = new PrintWriter(console_writer, true), class_loader = new JARClassLoader) val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console") { case Start(console) => interp.bind("view", "org.gjt.sp.jedit.View", console.getView) interp.bind("console", "console.Console", console) interp.interpret("import isabelle._; import isabelle.jedit._") true case Execute(console, out, err, command) => with_console(console, out, err) { try { running.change(_ => Some(Thread.currentThread())) interp.interpret(command) } finally { running.change(_ => None) Exn.Interrupt.dispose() } GUI_Thread.later { if (err != null) err.commandDone() out.commandDone() } true } } } /* jEdit console methods */ override def openConsole(console: Console): Unit = { val interp = new Interpreter interp.thread.send(Start(console)) interpreters += (console -> interp) } override def closeConsole(console: Console): Unit = { interpreters.get(console) match { case Some(interp) => interp.interrupt() interp.thread.shutdown() interpreters -= console case None => } } override def printInfoMessage(out: Output): Unit = { out.print(null, "This shell evaluates Isabelle/Scala expressions.\n\n" + "The contents of package isabelle and isabelle.jedit are imported.\n" + "The following special toplevel bindings are provided:\n" + " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" + " console -- jEdit Console plugin\n" + " PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n") } override def printPrompt(console: Console, out: Output): Unit = { out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>") out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ") } override def execute( console: Console, input: String, out: Output, err: Output, command: String): Unit = { interpreters(console).thread.send(Execute(console, out, err, command)) } override def stop(console: Console): Unit = interpreters.get(console).foreach(_.interrupt()) } diff --git a/src/Tools/jEdit/lib/Tools/jedit b/src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit +++ b/src/Tools/jEdit/lib/Tools/jedit @@ -1,174 +1,172 @@ #!/usr/bin/env bash # # Author: Makarius # # DESCRIPTION: Isabelle/jEdit interface wrapper ## diagnostics PRG="$(basename "$0")" function usage() { echo echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" echo echo " Options are:" echo " -A NAME ancestor session for option -R (default: parent)" echo " -D NAME=X set JVM system property" echo " -J OPTION add JVM runtime option" echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" echo " -R NAME build image with requirements from other sessions" echo " -b build only" echo " -d DIR include session directory" echo " -f fresh build" echo " -i NAME include session in name-space of theories" echo " -j OPTION add jEdit runtime option" echo " (default $JEDIT_OPTIONS)" echo " -l NAME logic session name" echo " -m MODE add print mode for output" echo " -n no build of session image on startup" echo " -p CMD ML process command prefix (process policy)" echo " -s system build mode for session image (system_heaps=true)" echo " -u user build mode for session image (system_heaps=false)" echo echo " Start jEdit with Isabelle plugin setup and open FILES" echo " (default \"$USER_HOME/Scratch.thy\" or \":\" for empty buffer)." echo exit 1 } function fail() { echo "$1" >&2 exit 2 } function failed() { fail "Failed!" } ## process command line # options BUILD_ONLY=false FRESH_BUILD="" ML_PROCESS_POLICY="" JEDIT_LOGIC_ANCESTOR="" JEDIT_LOGIC_REQUIREMENTS="" JEDIT_INCLUDE_SESSIONS="" JEDIT_SESSION_DIRS="-" JEDIT_LOGIC="" JEDIT_PRINT_MODE="" JEDIT_NO_BUILD="" JEDIT_BUILD_MODE="default" function getoptions() { OPTIND=1 while getopts "A:BFD:J:R:bd:fi:j:l:m:np:su" OPT do case "$OPT" in A) JEDIT_LOGIC_ANCESTOR="$OPTARG" ;; D) JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG" ;; J) JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" ;; R) JEDIT_LOGIC="$OPTARG" JEDIT_LOGIC_REQUIREMENTS="true" ;; b) BUILD_ONLY=true ;; d) JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG" ;; i) if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then JEDIT_INCLUDE_SESSIONS="$OPTARG" else JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG" fi ;; f) FRESH_BUILD="true" ;; j) ARGS["${#ARGS[@]}"]="$OPTARG" ;; l) JEDIT_LOGIC="$OPTARG" ;; m) if [ -z "$JEDIT_PRINT_MODE" ]; then JEDIT_PRINT_MODE="$OPTARG" else JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG" fi ;; n) JEDIT_NO_BUILD="true" ;; p) ML_PROCESS_POLICY="$OPTARG" ;; s) JEDIT_BUILD_MODE="system" ;; u) JEDIT_BUILD_MODE="user" ;; \?) usage ;; esac done } eval "declare -a JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" declare -a ARGS=() declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)" getoptions "${OPTIONS[@]}" getoptions "$@" shift $(($OPTIND - 1)) # args while [ "$#" -gt 0 ]; do ARGS["${#ARGS[@]}"]="$(platform_path "$1")" shift done ## main -isabelle_admin_build browser || exit "$?" - if [ -n "$FRESH_BUILD" ]; then - isabelle_admin_build jars_fresh || exit "$?" + isabelle_scala_build fresh || exit "$?" else - isabelle_admin_build jars || exit "$?" + isabelle_scala_build || exit "$?" fi if [ "$BUILD_ONLY" = false ] then "$ISABELLE_HOME/lib/scripts/java-gui-setup" export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \ JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY" exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \ "${JAVA_ARGS[@]}" isabelle.jedit.Main "${ARGS[@]}" fi