Fri, 15 Nov 2024 13:31:36 +0100 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: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);
Fri, 15 Nov 2024 13:08:48 +0100 less ambitious selection;
wenzelm [Fri, 15 Nov 2024 13:08:48 +0100] rev 81447
less ambitious selection;
Fri, 15 Nov 2024 21:37:26 +0100 mv Discrete to Discrete_Cpo to avoid theory name clashes
nipkow [Fri, 15 Nov 2024 21:37:26 +0100] rev 81446
mv Discrete to Discrete_Cpo to avoid theory name clashes
Thu, 14 Nov 2024 11:33:51 +0100 disable 2d9b6e32632d for now: unknown problems on macOS;
wenzelm [Thu, 14 Nov 2024 11:33:51 +0100] rev 81445
disable 2d9b6e32632d for now: unknown problems on macOS;
Thu, 14 Nov 2024 11:12:11 +0100 clarified mouse selection, avoid conflict of double-click with single-click (follow hyperlink);
wenzelm [Thu, 14 Nov 2024 11:12:11 +0100] rev 81444
clarified mouse selection, avoid conflict of double-click with single-click (follow hyperlink);
Thu, 14 Nov 2024 10:50:49 +0100 more careful isConsumed() / consume() for key and mouse events;
wenzelm [Thu, 14 Nov 2024 10:50:49 +0100] rev 81443
more careful isConsumed() / consume() for key and mouse events;
Wed, 13 Nov 2024 23:11:06 +0100 merged
nipkow [Wed, 13 Nov 2024 23:11:06 +0100] rev 81442
merged
Wed, 13 Nov 2024 23:10:58 +0100 added field input_eqns to record the list of equations (the specification)
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.
Wed, 13 Nov 2024 20:14:24 +0100 merged
wenzelm [Wed, 13 Nov 2024 20:14:24 +0100] rev 81440
merged
Wed, 13 Nov 2024 20:14:17 +0100 more NEWS;
wenzelm [Wed, 13 Nov 2024 20:14:17 +0100] rev 81439
more NEWS;
Wed, 13 Nov 2024 20:10:34 +0100 tuned proofs;
wenzelm [Wed, 13 Nov 2024 20:10:34 +0100] rev 81438
tuned proofs;
Wed, 13 Nov 2024 15:14:48 +0100 more ambitious mouse handler: double-click selects highlight_area;
wenzelm [Wed, 13 Nov 2024 15:14:48 +0100] rev 81437
more ambitious mouse handler: double-click selects highlight_area;
Wed, 13 Nov 2024 14:54:08 +0100 more accurate mouse handler: only for single clicks, consume accepted event;
wenzelm [Wed, 13 Nov 2024 14:54:08 +0100] rev 81436
more accurate mouse handler: only for single clicks, consume accepted event;
Wed, 13 Nov 2024 11:53:02 +0100 more ambitious scrolling: retain original scroll position if possible;
wenzelm [Wed, 13 Nov 2024 11:53:02 +0100] rev 81435
more ambitious scrolling: retain original scroll position if possible;
Wed, 13 Nov 2024 10:56:17 +0100 more ambitious scrolling: retain bottom position after output;
wenzelm [Wed, 13 Nov 2024 10:56:17 +0100] rev 81434
more ambitious scrolling: retain bottom position after output;
Tue, 12 Nov 2024 22:30:45 +0100 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm [Tue, 12 Nov 2024 22:30:45 +0100] rev 81433
performance tuning: cache for Rich_Text.format, notably for incremental tracing;
(0) -30000 -10000 -3000 -1000 -300 -100 -16 +16 +100 +300 tip