wenzelm [Fri, 15 Nov 2024 13:31:36 +0100] rev 81448
more rebust mechanics of refresh (see also 82110cbcf9a1 and 2d9b6e32632d): painter.getFontRenderContext might be in undefined state (notably on macOS due to display scaling);
wenzelm [Fri, 15 Nov 2024 13:08:48 +0100] rev 81447
less ambitious selection;
nipkow [Fri, 15 Nov 2024 21:37:26 +0100] rev 81446
mv Discrete to Discrete_Cpo to avoid theory name clashes
wenzelm [Thu, 14 Nov 2024 11:33:51 +0100] rev 81445
disable 2d9b6e32632d for now: unknown problems on macOS;
wenzelm [Thu, 14 Nov 2024 11:12:11 +0100] rev 81444
clarified mouse selection, avoid conflict of double-click with single-click (follow hyperlink);
wenzelm [Thu, 14 Nov 2024 10:50:49 +0100] rev 81443
more careful isConsumed() / consume() for key and mouse events;
nipkow [Wed, 13 Nov 2024 23:11:06 +0100] rev 81442
merged
nipkow [Wed, 13 Nov 2024 23:10:58 +0100] rev 81441
added field input_eqns to record the list of equations (the specification)
given to the function command.
wenzelm [Wed, 13 Nov 2024 20:14:24 +0100] rev 81440
merged
wenzelm [Wed, 13 Nov 2024 20:14:17 +0100] rev 81439
more NEWS;
wenzelm [Wed, 13 Nov 2024 20:10:34 +0100] rev 81438
tuned proofs;
wenzelm [Wed, 13 Nov 2024 15:14:48 +0100] rev 81437
more ambitious mouse handler: double-click selects highlight_area;
wenzelm [Wed, 13 Nov 2024 14:54:08 +0100] rev 81436
more accurate mouse handler: only for single clicks, consume accepted event;
wenzelm [Wed, 13 Nov 2024 11:53:02 +0100] rev 81435
more ambitious scrolling: retain original scroll position if possible;
wenzelm [Wed, 13 Nov 2024 10:56:17 +0100] rev 81434
more ambitious scrolling: retain bottom position after output;
wenzelm [Tue, 12 Nov 2024 22:30:45 +0100] rev 81433
performance tuning: cache for Rich_Text.format, notably for incremental tracing;