[isabelle-dev] syntax highlighting of inner comments
immler at in.tum.de
Thu Mar 7 04:12:32 CET 2019
Oh, you are right - there was a thread about that on isabelle-users in
On 3/6/2019 7:32 PM, Peter Lammich wrote:
> Hi Fabian
> I already pointed out the missing highlighting of cancel a few months
> ago ... I am still strongly in favor of having a highlighting that can
> easily be distinguished, eg the legacy red, or perhaps gray ...
> Right now, when using Isabelle 2018, I do not use cancel, but (**),
> getting a warning, but having highlighting at least.
> -------- Original Message --------
> Subject: [isabelle-dev] syntax highlighting of inner comments
> From: Fabian Immler
> To: isabelle-dev at mailbroy.informatik.tu-muenchen.de
> Up until Isabelle2018, I used (* ... *) to comment out parts of
> lemmas/definitions, mostly for debugging larger expressions.
> Highlighted in red, (* ... *) was nicely set apart from the rest of the
> Now (e.g., isabelle/b58a575d211e) we can use \<^cancel>, but its
> "highlighting" in black makes it very hard to keep an overview.
> Note that e.g., with a type error in a lemma statement, canceled
> text is
> highlighted red (like in the attached screenshot).
> Best regards,
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev