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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
