[isabelle-dev] syntax highlighting of inner comments

[Makarius]

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