| Wed, 06 Nov 2024 16:07:30 +0100 | wenzelm | clarified signature; | changeset | files |
| Wed, 06 Nov 2024 15:52:31 +0100 | wenzelm | clarified signature, with subtle change of semantics: proper non-null result; | changeset | files |
| Wed, 06 Nov 2024 15:38:45 +0100 | wenzelm | clarified modules; | changeset | files |
| Wed, 06 Nov 2024 15:17:39 +0100 | wenzelm | more robust and uniform metric, still with special treatment motivated by jEdit (see also 0cdfce0bf956); | changeset | files |
| Wed, 06 Nov 2024 11:05:18 +0100 | wenzelm | misc tuning; | changeset | files |
| Fri, 08 Nov 2024 18:13:55 +0100 | Fabian Huch | try0: avoid mapping background theory -- should be handled by Context_Position visibility; | changeset | files |
| Thu, 31 Oct 2024 11:35:24 +0100 | Fabian Huch | try0: stop early if more subgoals are created; | changeset | files |