feat: RefreshComponent

[JovanGerb]

This PR defines RefreshComponent, which allows you to have a refreshing HTML display, which updates whenever the given RefreshTask returns a new HTML.

For cancellation, we store an Option IO.CancelToken. This could be generalized to storing an arbitrary IO Unit function, but I don't think that would be very useful.

[dranov]

In Veil, we have a need for widgets where the data is provided incrementally. Do you intend to merge this (or a similar solution) in the near future?

[JovanGerb]

I just opened the demo file from this PR, and did the countToTen demo, and as you can see whenever I reopen the infoview, the numbers flicker a bit. This is what I mean with the glitching.

WidgetGlitch.mp4

[Vtec234]

I am seeing this in the countToTen demo. To reproduce, uncomment line 33, then check that the counter on line 30 is running, then uncomment line 36. Now line 30 is cancelled. It seems worrying since no shared cancel token is explicitly created here.

[JovanGerb]

Aha interesting! Although it's true that no cancel token is created explicitly, we are implicitly passing around the cancel token that was given to the command in question.

Apparently this cancel token from line 30 gets set when (un)commenting line 36. I find this a bit surprising. I'd have to look more carefully into how/where the cancel tokens usually get passed around.

[Vtec234]

Could this just be From/ToJson? We usually don't impl RpcEncodable directly for types that don't do something with RPC.

[JovanGerb]

The reason for this is that I want to be able to have an RPC method that doesn't return anything, called from JavaScript. And the @[server_rpc_method] attribute requires the RpcEncodable instance. Alternatively I'd have to return a String or something else, and then throw it away.

[Vtec234]

Wdym by 'reloaded/unloaded' here? Is the situation just that a tactic that saves this widget (and launches the thread) is elaborated, then we make an edit, and it gets re-elaborated while leaving the previous thread alive? If so, is it not possible to reuse the standard tactic cancellation mechanism? E.g. what happens if you pass the CoreM cancel token instead of one created manually?

[JovanGerb]

I've updated the description to be more clear. The issue is when clicking on expressions in the goal, every shift-click generates a call to mkGoalRefreshComponent. When shift-clicking as fast as possible, there is not enough time for each of the intermediate widgets to load.

[Vtec234]

The issue is when clicking on expressions in the goal, every shift-click generates a call to mkGoalRefreshComponent.

Ah, if doing that you could also create/cancel cancellation tokens in the outer function (e.g. in cycleSelections). Then you probably wouldn't need the global cancel token map.

[Vtec234]

E.g. what happens if you pass the CoreM cancel token instead of one created manually?

I'm still wondering about this. In particular w.r.t. to "when the infoview gets closed, cancelRefresh isn't run, and I don't know how to fix this." Using the CoreM token wouldn't cause anything to happen when the infoview is closed, of course, but I think we don't care about that. Mainly, we should ensure that no more than one RefreshComponent thread chain is alive at any given time.

[JovanGerb]

Well, my solution with storing the cancel token in a IO.Ref ensures exactly that: whenever a new RefreshComponent thread is started, it cancels the previous one. So there can be at most one alive at any given time.

[JovanGerb]

you could also create/cancel cancellation tokens in the outer function (e.g. in cycleSelections).

The function cycleSelections is not the outer function. It is called every time when the props : PanelWidgetProps is updated. In particular when selecting something, props.selectedLocations is updated.

Instead, the outer function is the one generated by

@[widget_module]
def cycleComponent : Component PanelWidgetProps :=
  mk_rpc_widget% cycleSelections

But I haven't looked at the code implementing widget_module and mk_rpc_widget%.

[Vtec234]

Instead, the outer function is the one generated

Right, but your RPC method gets called every time the props change; so you can put an IO.Ref in the props (by extending PanelWidgetProps) and modify it as needed. I'm just suggesting this to avoid the situation where all widgets corresponding to the given declaration get cancelled globally.

[JovanGerb]

Ah I see. This would allow multiple copies of the same widget to co-exist, because each of them can have its own canceltoken.

Though I don't see how the current approach would ever have all widgets corresponding to the given declaration get cancelled globally.

[Vtec234]

Did I misunderstand

If the same widget is loaded again, we set the previous cancel token.
As a result, there can be at most one instance of that particular widget
running at a time, and any other instances will say This component was cancelled.

? You use decl_name% as the key.

[JovanGerb]

Every new widget cancels the previous one, so for any given key there can be at most 1 computation running.

But that one computation wouldn't get cancelled, unless the corresponding widget is unloaded.

[JovanGerb]

For the flickering that can be seen in the video, when the message disappears, this is actually the <></> that is the initial/default value for the HTML (which can be seen at the end of the RefreshComponent implementation in TypeScript).

In an earlier version of this widget, instead of disappearing for a bit, the message would change into whatever the initial HTML was set to, which gave a more jarring effect.