Re: [isabelle-dev] syntax highlighting of inner comments

2019-03-06 Thread Fabian Immler
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

Re: [isabelle-dev] syntax highlighting of inner comments

2019-03-06 Thread Peter Lammich
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

[isabelle-dev] syntax highlighting of inner comments

2019-03-06 Thread Fabian Immler
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