[isabelle-dev] syntax highlighting of inner comments

Fabian Immler immler at in.tum.de
Thu Mar 7 00:48:55 CET 2019


Hi,

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 
expression.

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,
Fabian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: highlighting_cancel.PNG
Type: image/png
Size: 9022 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20190306/9b04c5ee/attachment-0001.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20190306/9b04c5ee/attachment-0001.p7s>


More information about the isabelle-dev mailing list