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 glitch.


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.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.