Re: [isabelle] 2014-RC1 issues
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.
The examples shown here are about embedded ML code, which is not really
the normal use of strings.
In general, the "guess what I mean" functionality of the system will
occasionally guess wrong. It is sometimes hard to get the defaults right,
but so far I don't see an indication to change them in this case.
This archive was generated by a fusion of
Pipermail (Mailman edition) and