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.


	Makarius





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