Re: [isabelle] 2014-RC1 issues

On Thu, 31 Jul 2014, Lars Noschinski wrote:

Why is that an issue? The language context switches symbols on for ML strings and comments, since both might use them.
Take it as a data point for the long-term considerations about symbol completion.

But there is also something not totally smooth outside of strings: Yesterday, I occasionally had symbols complete in normal ML-code (outside of strings; in a ML-block in a theory file). Typically, this seemed to occur when I was typing pretty fast and changing the structure of the code. It seemed unrelated to string literals.

One way to trigger this is placing the cursor directly after the closing
} of an antiquotation and typing a symbol fast. I can even type a few
  spaces before typing the symbol and it will still get completed.

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.


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