Re: [isabelle] 2014-RC1 issues



On 30.07.2014 22:02, Makarius wrote:
> On Wed, 30 Jul 2014, Lars Noschinski wrote:
>
>> On 30.07.2014 10:26, Peter Lammich wrote:
>>> Here is a list of issues that I encountered with RC1:
>> And a completion-related one: In a string context in a ML-context,
>> symbol completion is enabled.
>
> 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.

  -- Lars




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