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