On 07/06/16 10:10, Fabian Immler wrote:
>
>> Am 06.06.2016 um 21:29 schrieb Makarius <makar...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
