Re: [isabelle] (inner?) syntax highlighting of ― ‹...› and ⌦‹...›
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] (inner?) syntax highlighting of ― ‹...› and ⌦‹...›
- From: Peter Lammich <lammich at in.tum.de>
- Date: Mon, 05 Nov 2018 14:21:08 +0100
- In-reply-to: <20181105124346.GK5388@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>
- References: <firstname.lastname@example.org> <20180730124406.GA1555@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f> <email@example.com> <firstname.lastname@example.org> <20181105124346.GK5388@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>
> > 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.
So +1 from me to have the next release with a usable mechanism for ad-
hoc commenting-out of parts of inner syntax. At least for my style of
Isabelle development and proof exploration this is essential to have.
The \cancel\open ...\close syntax is slightly more annoying to type
than (* ... *) was, but would be OK if properly highlighted as
This archive was generated by a fusion of
Pipermail (Mailman edition) and