Re: [isabelle-dev] Whole word search

2016-06-08 Thread Makarius
On 07/06/16 10:10, Fabian Immler wrote:
> 
>> Am 06.06.2016 um 21:29 schrieb Makarius :
>>
>> 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.)
> 
> Have you noticed that (in isabelle/f59fd6cc935e) this individual selection 
> via double-click works only in the main text area?
> In the panels for State, Output, and Query, a double-click selects the long 
> identifier. This also applies to popups when e.g., hovering over a constant.

Thanks for keeping an eye on such details.

See now:

changeset:   63261:90a44d271683
tag: tip
user:wenzelm
date:Wed Jun 08 19:36:45 2016 +0200
files:   src/Tools/jEdit/src/pretty_text_area.scala
description:
proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Whole word search

2016-06-06 Thread Makarius
On 06/06/16 22:40, Lawrence Paulson wrote:
>> On 6 Jun 2016, at 20:29, Makarius  wrote:
>>
>>
>> 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

> But what is the scope of this selection? The entire file or some local scope?

It is the true scope of the lambda term -- assuming that it has been
formally checked by the prover.


Makarius


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Whole word search

2016-06-06 Thread Lawrence Paulson
But what is the scope of this selection? The entire file or some local scope?
Larry

> On 6 Jun 2016, at 20:29, Makarius  wrote:
> 
> 
> 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
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Whole word search

2016-06-06 Thread 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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev