Jean-Marc Lasgouttes da57154f94 Rework display of numbers in margins of hull insets
This requires the introduction of the booleans selected_left and
selected_right in PainterInfo. These tell whether the selection
continues at the left/right of the inset.

This information allows to

1/ paint equation number in the right color: either current text color
   or selection text color.

2/ before that, paint a small background rectangle of the correct color.

This allows to avoid painting a large rectangle of an arbitrary color
that was the cause of the bug.

Fixes bug #12319.
2021-07-09 23:46:16 +02:00
..
2020-11-01 22:24:48 +02:00
2020-12-05 17:17:02 -05:00
2020-12-05 17:17:02 -05:00
2020-01-14 21:59:05 +01:00
2020-10-25 09:28:34 +02:00
2020-10-25 09:28:34 +02:00
2021-04-09 18:15:31 +02:00
2020-12-06 18:26:41 +02:00
2020-12-06 18:26:41 +02:00
2020-10-13 09:57:36 +03:00
2020-12-05 17:17:02 -05:00
2020-10-19 17:33:51 +03:00
2020-10-19 17:33:51 +03:00
2020-10-19 17:33:51 +03:00
2020-12-01 00:46:21 +02:00
2020-12-01 00:46:21 +02:00
2021-06-14 18:01:35 +02:00
2020-12-05 17:17:02 -05:00
2020-10-19 17:33:51 +03:00
2020-11-20 15:57:26 +02:00
2020-10-29 15:52:38 +02:00
2020-11-30 13:04:58 +02:00
2020-11-30 13:04:58 +02:00
2020-12-05 17:17:02 -05:00
2020-10-23 15:00:23 +02:00
2020-10-05 14:55:00 +02:00
2020-11-01 22:23:26 +02:00
2020-11-26 06:22:27 +01:00
2020-11-24 15:19:56 +01:00
2020-11-26 11:09:17 +01:00
2020-07-28 18:01:38 +02:00
2020-11-12 14:22:00 +02:00
2020-03-16 02:18:19 -04:00
2021-01-10 00:43:01 -05:00
2020-12-01 00:46:21 +02:00
2020-12-05 17:17:02 -05:00
2020-12-05 17:17:02 -05:00
2020-05-05 11:19:21 -04:00
2020-02-29 00:21:02 -05:00
2020-11-21 20:32:16 +02:00
2020-11-30 13:04:54 +02:00
2020-10-23 15:00:23 +02:00
2021-02-27 20:34:29 -05:00
2020-11-30 11:32:35 +01:00
2020-11-01 22:25:08 +02:00
2020-11-01 22:25:08 +02:00
2020-11-29 15:27:28 +02:00
2020-12-05 17:17:02 -05:00
2020-05-03 02:46:11 -04:00
2020-12-05 17:17:02 -05:00
2020-11-21 19:54:43 +01:00
2020-11-21 20:32:16 +02:00
2021-04-07 17:13:43 +02:00
2021-04-07 16:19:20 +02:00
2020-12-19 18:29:10 +01:00
2020-12-18 14:30:21 -05:00
2020-12-05 17:17:02 -05:00
2020-12-05 17:17:02 -05:00
2020-12-05 17:17:02 -05:00
2020-12-05 17:17:02 -05:00
2020-12-05 17:17:02 -05:00
2020-12-05 17:17:02 -05:00
2020-12-01 00:46:21 +02:00
2021-04-07 17:17:05 +02:00
2020-11-01 22:23:26 +02:00
2020-12-01 00:46:21 +02:00
2021-02-16 12:29:40 +01:00
2020-12-20 12:42:04 +01:00
2021-01-14 01:15:19 -05:00
2020-11-01 22:23:26 +02:00
2020-10-25 09:28:34 +02:00
2021-03-09 12:46:23 +01:00
2020-12-18 17:35:58 -05:00
2020-11-30 13:05:03 +02:00
2021-01-02 19:52:23 +01:00