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
