[isabelle-dev] Whole word search
makarius at sketis.net
Mon Jun 6 21:29:59 CEST 2016
On 27/05/16 17:53, Lawrence Paulson wrote:
> There appear to have been some changes in policy concerning the meaning of “whole word” in jEdit find and replace. Let’s suppose that we want to rename the variable x in the expression λx. if P x then 1 else 0. For quite some time, the occurrence of x in “λx.” was not regarded as a “whole word”, but for a week or two recently, it was. I prefer the latter behaviour as being more consistent, even though I can see issues connected with compound identifiers. Is this topic worth discussing?
I have now studied jEdit/org/gjt/sp/jedit/search/SearchMatcher.java a
bit. I've always thought that jEdit search would just use hardwired
regexps with \b delimiters, but it is more sophisticated. In particular,
the noWordSep property of the editor mode is taken into account.
That has changed here:
date: Thu Apr 07 20:54:20 2016 +0200
clarified word syntax: "." is separator or delimiter;
It means that the parts of long identifiers can be selected individually
(e.g. via double-clicked). It also has an effect on searching "x" in
"x.", but note that the lambda in "λx." is still a word character.
(Maybe that should be changed as well.)
Anyway, for the described application to rename the "x" within a lambda
expression, you can now use isabelle.select-entity as described in
More information about the isabelle-dev