| Fri, 12 Aug 2022 15:48:47 +0200 | wenzelm | clarified output; | changeset | files |
| Fri, 12 Aug 2022 15:40:38 +0200 | wenzelm | clarified signature: support different document_session, e.g. within running PIDE session; | changeset | files |
| Fri, 12 Aug 2022 14:39:37 +0200 | wenzelm | unused (despite cf52379c0776); | changeset | files |
| Fri, 12 Aug 2022 14:33:50 +0200 | wenzelm | tuned, following hints by IntelliJ IDEA; | changeset | files |