Re: [isabelle] (inner?) syntax highlighting of ― ‹...› and ⌦‹...›

Peter Lammich wrote:
> To re-open this thread:
> I also find the missing highlighting of \^cancel comments REALLY
> ANNYOING. In some use-cases, I use commenting out parts of a term a
> lot, and this get's really unreadable now. 
> > RC3 is already too far towards the final version to reconsider this 
> So even if it has been too late for Isabelle2018, please DO consider
> proper highlighting of inner syntax comments.
> For now, I'm back to using the legacy (* ... *) syntax, which, btw, is
> slightly easier to type.

Same here.

However, the legacy syntax has been discontinued in the development
version, so this issue will be important for the next release.



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