Re: [isabelle] 2014-RC1 issues
On Mon, 4 Aug 2014, Lars Noschinski wrote:
It does, but only after convergence according to
http://www4.in.tum.de/~wenzelm/papers/itp-pide.pdf section 2, figure 2.
The Δt corresponds to the delays mentioned above (plus some internal
processing in Scala and ML).
What I meant is that I can place the cursor directly after the closing
brace, wait for an arbitrary amount of time (to give the system time to
converge), and still get symbol completion if I type fast at that point
(see attached video).
That is still within the convergence model sketched here, but there is an
additional coincidence: completion sits right in the input event loop.
When you type something there is always an edit-distance, and the language
context of the closing delimiter is stretched into the new space. Unless
there is a completion delay, the semantic information needs to be
retrieved on the spot, but it can never be accurate.
You can see the same effect when you insert new material quickly at the
end of some semantically marked up token (e.g. a free or bound variable).
It does not matter so much there, since it is only a transient visual
In the next round of completion refinement (not for this release), one
could try to mark only the interior with the specific language context,
not the delimiters.
This archive was generated by a fusion of
Pipermail (Mailman edition) and