Diffusion Isabelle 45b9bbe6e375

avoid redundant SelectionChanged events;
45b9bbe6e375
Actions

Tags

None

Subscribers

None

Description

avoid redundant SelectionChanged events;

Details

Provenance

Authored on

Parents

rISABELLE25dbf5bec91e: more logging;

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rISABELLE45b9bbe6e375: avoid redundant SelectionChanged events;.Feb 3 2023, 4:50 PM

Changes (1)

Path

Size

src/

Tools/

jEdit/

src/

jedit_sessions.scala

rISABELLE45b9bbe6e375

src/Tools/jEdit/src/jedit_sessions.scala

Loading...