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

[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
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





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

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.

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