## Stream: general

### Topic: katex

#### Kevin Buzzard (Aug 29 2020 at 18:43):

For me shaking on the goal is fine, but if I start shaking over the entire local context then I get problems

#### Alex Peattie (Aug 30 2020 at 08:40):

Ah OK I see the problem (although not new as far as I can see). It's to do with how handle_widget_event handles multithreading/receiving requests faster than the Lean server can handle - which it looks like you flagged already @Edward Ayers : https://github.com/leanprover-community/lean/blob/v3.19.0/src/shell/server.cpp#L630-L632 . It seems that for complicated tactic states, the onMouseEnter/onMouseLeave events start taking a while and they start "stacking up" quite quickly.

#### Alex Peattie (Aug 30 2020 at 08:40):

I guess there are a few ways to handle this - one would be changing the behaviour of handle_widget_event on the server-side. We could also have VSCode be smarter about how it dispatches widget events. E.g. if it's waiting for a widget rerender from the server, instead of dispatching another widget event request right away, enqueue it in memory. Then once the widget's rerendered, prune the queue to get rid of duplicate onMouseEnter events etc. :thinking:

#### Edward Ayers (Aug 30 2020 at 08:52):

I can't get this lagginess to happen on Scott's file. :/

#### Edward Ayers (Aug 30 2020 at 08:52):

I agree that indenting is a huge issue

#### Edward Ayers (Aug 30 2020 at 08:57):

But the lagging thing is certainly caused by a queue of events. So the fix is to have lean only keep the latest widget_event in the queue. Maybe @Gabriel Ebner will know how difficult that is. But it still doesn't explain why the issues would have started over the last few days.

#### Alex Peattie (Aug 30 2020 at 09:01):

Not to complicate things further, but I was thinking about it and I actually wonder if keeping only the latest widget_event will cause strange behaviour. Like if you hovered and quickly clicked an expression, Lean might throw away either the onMouseEnter or the onClick event, and so the UI only registers either the hover or the click (but not both)...

#### Alex Peattie (Aug 30 2020 at 09:02):

Ideally maybe Lean should keep only the latest of each kind of widget_event?

#### Edward Ayers (Aug 30 2020 at 09:02):

Yeah that's a good idea

#### Edward Ayers (Aug 30 2020 at 11:26):

Indenting fix is on the way thanks to CSS wizardry of @Daniel Fabian and @Gabriel Ebner #3764

#### Edward Ayers (Aug 30 2020 at 12:07):

Patrick Massot said:

Wouldn't be easier to work on "jump to definition" in the info view?

#3982

#### Kevin Buzzard (Aug 30 2020 at 12:26):

As I've been using widgets more and more I've been realising I'm missing this.

#### Scott Morrison (Aug 30 2020 at 12:57):

I don't think it's (laggy highlighting) started in the last few days; I think I've had it all along.

#### Patrick Massot (Aug 30 2020 at 14:45):

I'd love to have this merged! I'll give a propaganda talk tomorrow morning, I could certainly use it.

#### Gabriel Ebner (Aug 30 2020 at 15:00):

Re: lagging and event queue. Maybe it would help to handle some events directly in the info view instead of sending them back to Lean? For example, we could offload the highlighting like here: https://gebner.github.io/mathlib_docs/geometry/euclidean/circumcenter.html#euclidean_geometry.exists_unique_dist_eq_of_insert

Oh, is this new?

#### Gabriel Ebner (Aug 30 2020 at 15:04):

The flashy highlighting? I've been toying around with the idea for a while, but this is not the official documentation page.

#### Patrick Massot (Aug 30 2020 at 15:04):

Yes, the flashy highlighting. Maybe the color gradient is a bit too much, but some highlighting is nice.

#### Rob Lewis (Sep 24 2020 at 08:33):

I forgot about @Gabriel Ebner 's highlighting to the docs, sorry! Do people feel like it's too much? I like it and it adds functionality.

#### Sebastien Gouezel (Sep 24 2020 at 08:44):

I like the idea of highlighting a lot. If we have to choose between the two color schemes, I prefer the first one (one color, with a gradient) over the second one (random rainbow colors, too much "flower power" for my taste)

#### Rob Lewis (Sep 24 2020 at 08:45):

But how else will we capture Lean's hippie spirit? :peace:

#### Rob Lewis (Sep 24 2020 at 08:46):

It matches Kevin's pants!

#### Johan Commelin (Sep 24 2020 at 09:02):

I can totally see a footnote at the bottom of the docs page

UI design by Kevin's pants, Inc.

#### Rob Lewis (Sep 24 2020 at 09:32):

Here's an alternative color scheme: https://github.com/leanprover-community/doc-gen/pull/73

Last updated: May 09 2021 at 19:11 UTC