Re: [isabelle-dev] syntax highlighting of inner comments
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/msg2.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@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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] syntax highlighting of inner comments
Hi FabianI 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 commentsFrom: Fabian Immler To: isabelle-dev@mailbroy.informatik.tu-muenchen.deCC: 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 listisabelle-...@in.tum.dehttps://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] syntax highlighting of inner comments
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 smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
