[isabelle-dev] Whole word search

[Makarius]

On 07/06/16 10:10, Fabian Immler wrote:
> 
>> Am 06.06.2016 um 21:29 schrieb Makarius <makarius at sketis.net>:
>>
>> 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