Re: [isabelle] 2014-RC1 issues

On 02.08.2014 13:31, Makarius wrote:
> On Fri, 1 Aug 2014, Lars Noschinski wrote:
>> Makarius <makarius at> schrieb:
>>> Semantic completion (i.e. the language context) works via the
>>> asynchronous document model, so typing fast means the physical
>>> editor state and the document markup range may disagree.
>>> These delays are system options that may be adjusted as usual: most
>>> notably editor_input_delay and editor_output_delay.  Maybe you want
>>> to try these by a factor of 5 or 10 faster -- results also depend on
>>> the amount of CPU cycles you can spend on interactive document
>>> processing and GUI rendering.
>> As a side note: Shouldn't the position directly after the closing
>> brace belong to the ML context again?
> It does, but only after convergence according to
> 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).

Attachment: antiquotation-completion.mp4
Description: video/mp4

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