| Author | Object | Transaction | Date |
|---|
| makarius | rAFP9910accdd127: avoid hardwired documents; | | Mar 17 2023, 10:54 AM |
| makarius | rISABELLEf7174238b5e3: no compression for database server: let PostgreSQL/TOAST do the job; | | Mar 16 2023, 5:42 PM |
| makarius | rISABELLE1db732e6c3d2: back to compression in Isabelle/Scala (in contrast to f7174238b5e3), e.g. | | Mar 16 2023, 5:42 PM |
| makarius | rISABELLE08fcde7c55c0: clarified ML option vs. Scala option (see also caa182bdab7a); | | Mar 16 2023, 5:42 PM |
| makarius | rISABELLEcaa182bdab7a: clarified options: batch-build has pide_reports disabled by default (requires… | | Mar 16 2023, 5:42 PM |
| makarius | rISABELLEa76f49a03448: merged | | Mar 16 2023, 5:12 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPf323a37f60a5: added new files generated by sitegen | | Mar 16 2023, 5:04 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP98e268419ce2: sitegen | | Mar 16 2023, 4:56 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPc2b9a8deb55c: metadata for Expander Graphs | | Mar 16 2023, 4:52 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP528b9fec7472: new entry: Expander Graphs | | Mar 16 2023, 4:49 PM |
| makarius | rISABELLE1db732e6c3d2: back to compression in Isabelle/Scala (in contrast to f7174238b5e3), e.g. | | Mar 16 2023, 4:28 PM |
| makarius | rISABELLEbc8e2fec9650: vacuum everything in the database; | | Mar 16 2023, 4:13 PM |
| makarius | rISABELLEe92000492895: tuned; | | Mar 16 2023, 3:58 PM |
| Fabian Huch <huch@in.tum.de> | rAFPaa0bd4097a74: tuned; | | Mar 16 2023, 3:57 PM |
| makarius | rISABELLEe7d8e990d378: proper vacuum of session_info tables: only once per build process; | | Mar 16 2023, 3:55 PM |
| makarius | rISABELLEdaaaf59375e9: tuned signature; | | Mar 16 2023, 3:46 PM |
| makarius | rISABELLE649708f75c6f: more thorough database checks; | | Mar 16 2023, 3:38 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPf30f86e45086: fix of toml-entries and rerun of sitegen: problem: links where in these quotes… | | Mar 16 2023, 3:33 PM |
| makarius | rISABELLE9e5f8f6e58a0: more thorough treatment of build prefs, guarded by system option… | | Mar 16 2023, 3:16 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPdb530be3d7ca: sitegen (for Binary_Code_Imprimitive and… | | Mar 16 2023, 2:55 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP055662f88f96: metadata for Binary_Code_Imprimitive and Two_Generated_Word_Monoids_Intersection | | Mar 16 2023, 2:49 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP9490f09cf4e6: new entry: Two_Generated_Word_Monoids_Intersection | | Mar 16 2023, 2:47 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP25cfc0d55518: new entry: Binary_Code_Imprimitive | | Mar 16 2023, 2:40 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPb3d3356622c7: running sort on ROOTS | | Mar 16 2023, 2:24 PM |
| nipkow | rISABELLE34176328fc67: merge conflict | | Mar 16 2023, 1:37 PM |
| makarius | rISABELLE488a48453d74: clarified build options; | | Mar 16 2023, 1:18 PM |
| makarius | rISABELLE08fcde7c55c0: clarified ML option vs. Scala option (see also caa182bdab7a); | | Mar 16 2023, 11:44 AM |
| nipkow | rISABELLE8a6a79ed5a83: unified function update and map update syntaxes | | Mar 16 2023, 8:30 AM |
| paulson | rAFP0c1c689ac551: merged | | Mar 15 2023, 10:54 PM |
| paulson <lp15@cam.ac.uk> | rAFPe53c4a724e65: simplified a few proofs | | Mar 15 2023, 10:54 PM |
| Christian Urban <christian.urban@kcl.ac.uk> | rAFPdece9a18f3f5: added character sets to the extension directory of regular expressions | | Mar 15 2023, 3:47 PM |
| blanchette | rISABELLEb9e9b818d7b0: removed accidental junk | | Mar 15 2023, 3:28 PM |
| nipkow | rISABELLE8f96ac621bfd: map update syntax | | Mar 15 2023, 1:01 PM |
| nipkow | rAFPb1c4633dd3f5: more syntax adjustments | | Mar 15 2023, 11:41 AM |
| nipkow | rAFP0b07855e08be: more syntax update for map update syntax | | Mar 15 2023, 11:03 AM |
| nipkow | rAFP1c50c5acb6f3: more map update syntax updates | | Mar 15 2023, 9:33 AM |
| nipkow | rAFP29c1380f84e9: merged | | Mar 15 2023, 6:43 AM |
| nipkow | rAFP2dab1d50e8a7: updated to new map update syntax priorities | | Mar 15 2023, 6:43 AM |
| makarius | rISABELLE5cb7fd36223b: proper sorting of result (amending f458547b4f0f); | | Mar 14 2023, 10:01 PM |
| makarius | rISABELLEf458547b4f0f: clarified signature (again, see also 8c64e51d9dde and 268bf61631ec); | | Mar 14 2023, 10:01 PM |
| makarius | rISABELLE5cb7fd36223b: proper sorting of result (amending f458547b4f0f); | | Mar 14 2023, 10:00 PM |
| makarius | rISABELLEd15ad84d75f7: merged | | Mar 14 2023, 9:01 PM |
| makarius | rISABELLEa84f0b1f607d: enforce rebuild of Isabelle/ML; | | Mar 14 2023, 8:31 PM |
| makarius | rISABELLE74cd42d053bf: more operations; | | Mar 14 2023, 8:31 PM |
| makarius | rISABELLEf5d3ade80d15: more specific vacuum operation, which is also relevant to PostgreSQL; | | Mar 14 2023, 8:25 PM |
| paulson <lp15@cam.ac.uk> | rAFPbe51414bc47e: Some simplifications of proofs | | Mar 14 2023, 8:24 PM |
| makarius | rISABELLEc82d49a56cf9: tuned signature: removed redundant argument; | | Mar 14 2023, 8:06 PM |
| makarius | rISABELLEb45fc98d11ea: tuned signature; | | Mar 14 2023, 8:04 PM |
| makarius | rISABELLE45bd5c26cbcc: proper build_uuid for Build_Process.Task: thus old entries are removed via… | | Mar 14 2023, 8:01 PM |
| makarius | rISABELLE57fdb6c846b0: more informative Build_Process.Snapshot; | | Mar 14 2023, 7:41 PM |
| makarius | rISABELLEd7eb6a4522b8: more explicit snapshot of "_state" and "_database"; | | Mar 14 2023, 7:19 PM |
| makarius | rISABELLE4240e9528586: tuned; | | Mar 14 2023, 6:59 PM |
| makarius | rISABELLEa2a4adc268b8: removed redundant State.workers: directly maintained within the database, using… | | Mar 14 2023, 6:57 PM |
| makarius | rISABELLEfd553b54fce1: more thorough cleanup; | | Mar 14 2023, 6:43 PM |
| makarius | rISABELLE136ab737a36d: tuned signature; | | Mar 14 2023, 6:29 PM |
| nipkow | rISABELLE7edbb16bc60f: Adjusted to new map update priorities | | Mar 14 2023, 6:19 PM |
| makarius | rISABELLE78913f29fc21: tuned signature; | | Mar 14 2023, 5:34 PM |
| makarius | rISABELLE26bb79d17910: tuned signature; | | Mar 14 2023, 5:09 PM |
| makarius | rISABELLE5f706f7c624b: more thorough synchronization of internal "_state" vs. external "_database"; | | Mar 14 2023, 5:05 PM |
| nipkow | rISABELLE48b4e0cd94cd: bring priority in line with ordinary function update notation | | Mar 14 2023, 2:00 PM |
| makarius | rISABELLEb7fe1d822dc1: more database content; | | Mar 14 2023, 11:14 AM |
| makarius | rISABELLEb1ca8975490a: clarified modules; | | Mar 14 2023, 10:35 AM |
| nipkow | rISABELLE4b688b8f1de3: merged | | Mar 14 2023, 10:35 AM |
| nipkow | rISABELLEa28ee8058ea3: use tree (simpler) instead of rbt (exercise) | | Mar 14 2023, 10:34 AM |
| makarius | rISABELLE739cb777cc75: clarified signature; | | Mar 14 2023, 10:27 AM |
| makarius | rISABELLEe79a5ce8a74c: clarified modules; | | Mar 14 2023, 10:16 AM |
| makarius | rISABELLEc14db5d67400: tuned output; | | Mar 14 2023, 10:05 AM |
| makarius | rISABELLEc55443f9fedd: tuned output; | | Mar 14 2023, 9:47 AM |
| makarius | rISABELLE4563db765eb2: enforce rebuild of Isabelle/ML; | | Mar 13 2023, 10:21 PM |
| makarius | rISABELLE9ed8b85e7d67: more direct state update; | | Mar 13 2023, 10:18 PM |
| makarius | rISABELLEf458547b4f0f: clarified signature (again, see also 8c64e51d9dde and 268bf61631ec); | | Mar 13 2023, 10:10 PM |
| makarius | rISABELLE268bf61631ec: more robust options in "prefs" format: avoid odd control character; | | Mar 13 2023, 10:10 PM |
| makarius | rISABELLE8c64e51d9dde: unused (see 268bf61631ec); | | Mar 13 2023, 10:10 PM |
| makarius | rISABELLEd5344cc1fae7: avoid too many synchronized_database; | | Mar 13 2023, 10:08 PM |
| makarius | rISABELLEa4266d54ec35: tuned output; | | Mar 13 2023, 9:43 PM |
| makarius | rISABELLEafb1a19307c4: synchronize progress messages with database; | | Mar 13 2023, 9:12 PM |
| makarius | rISABELLEdc96e6c56369: more robust SQL query for mandatory arguments; | | Mar 13 2023, 8:24 PM |
| makarius | rISABELLEdcd2c3bb4b68: synchronize progress stop/stopped with database; | | Mar 13 2023, 8:14 PM |
| makarius | rISABELLE50fc9143ccfa: more database content; | | Mar 13 2023, 7:04 PM |
| makarius | rISABELLEa65b39fdf8b6: tuned whitespace; | | Mar 13 2023, 6:53 PM |
| makarius | rISABELLEf7208db921c2: tuned signature; | | Mar 13 2023, 5:32 PM |
| makarius | rISABELLE89fffc5f5728: tuned whitespace; | | Mar 13 2023, 5:30 PM |
| makarius | rISABELLE86ef80d13544: clarified signature: avoid confusion due to object-orientation; | | Mar 13 2023, 5:22 PM |
| makarius | rISABELLE979baa91da0f: clarified modules; | | Mar 13 2023, 4:53 PM |
| makarius | rISABELLEa538dab533ef: clarified signature: prefer explicit types; | | Mar 13 2023, 3:53 PM |
| makarius | rISABELLE582a7db1da37: more accurate Sessions.Info.session_prefs: cover relative changes wrt. | | Mar 13 2023, 3:35 PM |
| makarius | rISABELLEaf8ac22d97f0: clarified signature: more explicit type Options.Spec, which incorporates all… | | Mar 13 2023, 3:09 PM |
| makarius | rISABELLE25b7914f488c: tuned output; | | Mar 13 2023, 1:46 PM |
| makarius | rISABELLE809ad223f406: clarified signature: more explicit types; | | Mar 13 2023, 1:43 PM |
| makarius | rISABELLE157ad1f976d2: clarified signature: prefer static types; | | Mar 13 2023, 1:20 PM |
| makarius | rISABELLEf458547b4f0f: clarified signature (again, see also 8c64e51d9dde and 268bf61631ec); | | Mar 13 2023, 11:02 AM |
| makarius | rISABELLE25993910f212: tuned signature; | | Mar 13 2023, 10:51 AM |
| paulson <lp15@cam.ac.uk> | rAFPb8d596202cef: Minor refinements | | Mar 12 2023, 11:05 PM |
| paulson <lp15@cam.ac.uk> | rAFP235abc5dda6c: tiny simplifications | | Mar 12 2023, 5:37 PM |
| paulson <lp15@cam.ac.uk> | rAFPcc1da1318e1d: tidied another file | | Mar 11 2023, 11:51 PM |
| makarius | rISABELLE58576816d304: more operations, thanks to Jsoup; | | Mar 11 2023, 9:36 PM |
| makarius | rISABELLE6d0985955872: discontinued apache-commons in favour of jsoup, which is smaller and more… | | Mar 11 2023, 9:25 PM |
| makarius | rISABELLE3e235fab64db: avoid hard-wired stuff (see also 78f2475aa126); | | Mar 11 2023, 5:01 PM |
| makarius | rISABELLE78f2475aa126: explicit notion of public options, which are shown in the editor options dialog; | | Mar 11 2023, 5:01 PM |
| makarius | rISABELLE8c64e51d9dde: unused (see 268bf61631ec); | | Mar 11 2023, 5:01 PM |