Re: [isabelle] Highlight sorry in jEdit
On Fri, 9 Nov 2012, Lars Noschinski wrote:
On 09.11.2012 09:09, Joachim Breitner wrote:
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
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