On 07/03/2019 00:48, Fabian Immler wrote:
>
> 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).
There is some complexity in overlapping markup, and it all stems from a
time when there was mostly outer and inner syntax only, without further
nesting of embedded sub-languages.
I have now reworked various aspects of PIDE markup in
Isabelle/4e98239aa083 (and before). We still have some months left
before the Isabelle2019 for sorting out inevitable problems coming from
that.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
