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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to