Re: [isabelle] Highlight sorry in jEdit

On Fri, 9 Nov 2012, Lars Noschinski wrote:

On 09.11.2012 09:09, Joachim Breitner wrote:
Dear List,

I often use sorry when doing my proofs top-down; and then I later need
to find them again. I found out about Ctrl-, to search, but it would be
more convenient if sorry were prominently highlighted, e.g. in red. This
would give me continuous feedback about how far I am with my proof.

Can I easily configure that myself? Also, please consider making that
the default, I’d say others profit from that as well.

There is the highlighter plugin which you can use to highlight arbitrary text in colors of your choosing.

I also want to add something productive here: the Highlighter (and Hypersearch) are big assets of jEdit. I use them all the time for many things.

The regex language accepted here is that of Java, see

This allows very nice things like word context \b. So for 'sorry' the pattern would be like this:



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.