| Mon, 12 Apr 2021 18:29:34 +0200 | wenzelm | clarified signature: avoid tmp file; | changeset | files |
| Mon, 12 Apr 2021 18:10:13 +0200 | wenzelm | clarified signature for Scala functions; | changeset | files |
| Mon, 12 Apr 2021 15:00:03 +0200 | wenzelm | clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9); | changeset | files |
| Mon, 12 Apr 2021 14:14:47 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 12 Apr 2021 12:32:09 +0200 | wenzelm | clarified cache; | changeset | files |
| Mon, 12 Apr 2021 12:16:49 +0200 | wenzelm | clarified signature: Bytes extends CharSequence already (see d201996f72a8); | changeset | files |
| Mon, 12 Apr 2021 11:45:16 +0200 | wenzelm | clarified exceptions; | changeset | files |