[isabelle-dev] syntax highlighting of inner comments

Fabian Immler 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 
July/August/November, e.g.:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-July/msg00124.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-August/msg00146.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-November/msg00002.html

Fabian

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.
> 
> Peter
> 
> 
> -------- Original Message --------
> Subject: [isabelle-dev] syntax highlighting of inner comments
> From: Fabian Immler
> To: isabelle-dev at mailbroy.informatik.tu-muenchen.de
> CC:
> 
> 
>     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
> 
>     _______________________________________________
>     isabelle-dev mailing list
>     isabelle-dev at in.tum.de
>     https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- 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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190306/5b4832cc/attachment.bin>


More information about the isabelle-dev mailing list