[isabelle-dev] Whole word search

[Makarius]

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:

changeset:   62909:5024d0c48e02
user:        wenzelm
date:        Thu Apr 07 20:54:20 2016 +0200
files:       src/Tools/jEdit/src/modes/isabelle-ml.xml
src/Tools/jEdit/src/modes/isabelle-news.xml
src/Tools/jEdit/src/modes/isabelle-options.xml
src/Tools/jEdit/src/modes/isabelle-root.xml
src/Tools/jEdit/src/modes/isabelle.xml src/Tools/jEdit/src/modes/sml.xml
description:
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
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-June/006879.html


	Makarius