Re: [isabelle] 2014-RC1 issues



On 02.08.2014 13:31, Makarius wrote:
> On Fri, 1 Aug 2014, Lars Noschinski wrote:
>
>> Makarius <makarius at sketis.net> 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
> 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).

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



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