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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and