| Tue, 27 Nov 2018 23:20:58 +0100 | wenzelm | adjusted to Isabelle DejaVu fonts (see also 8bd8750a2f9b, b3c665940d62); | changeset | files |
| Tue, 27 Nov 2018 21:07:39 +0100 | wenzelm | more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups; | changeset | files |
| Tue, 27 Nov 2018 16:22:12 +0100 | wenzelm | more robust (amending 76979adf0b96); | changeset | files |