Infoview overhaul #159
Infoview overhaul #159
Conversation
The widget branch of Lean must be used. Also note that many of the goal-view features are currently broken.
I think it makes sense to use tachyons CSS because it is consistent and low level enough that it can do anything without having to change stylesheets in multiple places. I also changed the style on pre to be a class selector `font-code`.
Because none of the events are connected properly.
put widget at top of list
|
Ok I think its starting to look ready for a beta. Hopefully we will get loads of bug reports and be able to prioritise what people want fixing. |
Support get_widget request.
The idea is that it helps the user stop being confused as to why there are two tactic states in the infoview.
|
Will the new info view still work well with older versions of Lean? For instance, I know there's a fix for the "interrupted" issues, in the newer versions of community Lean, but will users of older versions of Lean just have to deal with that by moving the cursor around manually? |
|
It should be backwards compatible. The 'cursor moving around' issues were just because it wouldn't bother to update if the infoview if the lean task status changed (which is fixed now). The only snags I've found are that if you have multiple pinned infos they will not always update properly and you get a "Error updating: interrupted. Try again." message. |
|
Hmm ok there are a few more error updated cases than I thought |
This is so that the update rate is limited if the user drags and moves the cursor around very quickly.
|
I don't quite get what is causing the interruption errors, it seems random to me, but at least now it is not quite so kaleidoscopic when you drag the cursor around. |
|
OK, thanks for looking into it. Hopefully there'll be some solution since it'd be a shame to degrade the experience of looking at projects relying on older versions of Lean. |
|
Yeah you are right it has to still be good for older projects |
It should be easy to add features where the infoview can either reveal or highlight positions in the sourcetext using the 'reveal' and 'hover_position' and 'stop_hover' `FromInfoViewMessage` commands. But how they manifest currently is a bit garish and confusing so I will wait for someone with some design sense to figure out what is best for a good user experience.
This means that getInfo tasks are now marshalled so that only one info request is in flight at a given time. Getting info is fast enough that this might as well be enabled all the time. This hopefully squashes a large category of bugs where multiple inflight getInfos would mess up state.
|
The issues with interupted errors should be behind us now. |
I rewrote the infoview code so that it is a full typescript/react project. It is also 'widget ready'.
There are still some tasks to be done:
filtering hypothesis lists--> should be implemented in leanAnyway the main purpose of this PR is to just be a place where we can discuss what needs to be done here before a merge.