The RefreshComponent widget

This file defines RefreshComponent, which allows you to have an HTML widget that updates incrementally as more results are computed by a Lean computation.

Known limitations

Cancellation is a bit hard to get right, and there is one limitation.

1. When using a RefreshComponent that comes directly from a command/tactic (no shift-clicking), then we pass the cancel token used by elaboration to the refresh component computation. Unfortunately there is an edge case where the cancel token gets set while the corresponding command does not get re-elaborated. In particular, if you have three command in a row, e.g.

#html countToTen
#html countToTen
#html countToTen

Then commenting out the third command will cancel the widget of the first command. It refreshes the second command, and doesn't affect commands before the first command - only the first command gets badly affected.

structure ProofWidgets.RefreshComponent.VersionedHtml : Type

A HTML tree together with a version number. We use this to check whether the tree currently on display is up to date.

• html : Html
• idx : Nat

@[implicit_reducible]

instance ProofWidgets.RefreshComponent.instRpcEncodableVersionedHtml : Lean.Server.RpcEncodable VersionedHtml

Equations

• One or more equations did not get rendered due to their size.

structure ProofWidgets.RefreshComponent.RefreshState : Type

The server-side state of a RefreshComponent.

• curr : Thunk Html

  The HTML tree to display, stored as a delayed computation.

  We only force the thunk when the client requests it. This means that if several updates arrive in quick succession, only the ones that the client actually sees will be computed.

• idx : Nat

  Version of the current HTML tree. It should increase by 1 with each state update.

• next : Task (Option Unit)

  A task that resolves when this state has become out-of-date. It resolves with some () if a new state is available, and with none if the display will never be updated again.

  It is implemented using RefreshToken.promise.result?, but we don't store the Promise here in order to make sure it can reach a refcount of 0.

@[implicit_reducible]

instance ProofWidgets.RefreshComponent.instInhabitedRefreshState : Inhabited RefreshState

Equations

• ProofWidgets.RefreshComponent.instInhabitedRefreshState = { default := ProofWidgets.RefreshComponent.instInhabitedRefreshState.default }

structure ProofWidgets.RefreshComponent.RefreshRef : Type

A reference to a RefreshState. Only exists because TypeName is not derivable for compound types.

• ref : IO.Ref RefreshState

@[implicit_reducible]

instance ProofWidgets.RefreshComponent.instTypeNameRefreshRef : TypeName RefreshRef

Equations

• ProofWidgets.RefreshComponent.instTypeNameRefreshRef = ProofWidgets.RefreshComponent.inst✝

structure ProofWidgets.RefreshComponent.AwaitRefreshParams : Type

The data used to call awaitRefresh, for updating the HTML display.

• state : Lean.Server.WithRpcRef RefreshRef
• oldIdx : Nat

  The index of the HTML tree that is currently on display.

@[implicit_reducible]

instance ProofWidgets.RefreshComponent.instRpcEncodableAwaitRefreshParams : Lean.Server.RpcEncodable AwaitRefreshParams

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.RefreshComponent.awaitRefresh (ps : AwaitRefreshParams) : Lean.Server.RequestM (Lean.Server.RequestTask (Option VersionedHtml))

If any updates are available (i.e., the server-side state is more recent than the client's), immediately return the most recent version of the HTML tree. Otherwise await the next update. Returns none if the client's state is the last one that should be shown.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ProofWidgets.RefreshComponent.instTypeNameCancelToken_proofWidgets : TypeName IO.CancelToken

Equations

• ProofWidgets.RefreshComponent.instTypeNameCancelToken_proofWidgets = ProofWidgets.RefreshComponent.inst✝

structure ProofWidgets.RefreshComponent.Props : Type

• state : Lean.Server.WithRpcRef RefreshRef

  Initial state of the component.

• cancelTk : Lean.Server.WithRpcRef IO.CancelToken

  Will be cancelled whenever the widget is rendered with a new state, or unmounted, or when the whole infoview is closed.

@[implicit_reducible]

instance ProofWidgets.RefreshComponent.instRpcEncodableProps : Lean.Server.RpcEncodable Props

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.RefreshComponent.monitor (p : Props) : Lean.Server.RequestM (Lean.Server.RequestTask Unit)

HACK: We cancel background threads driving RefreshComponents when they are no longer needed. However, there is currently no good way to do this when the infoview closes, as in that case React effect cleanup functions are never executed. Instead, RefreshComponent calls this persistent monitor task during creation. The call is auto-cancelled when the infoview closes, setting cancelTk.

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.RefreshComponent : Component RefreshComponent.Props

Displays a HTML tree, refreshing the display when the tree is updated.

Use mkRefreshComponentM to conveniently spawn a dedicated thread from which you can update the display.

The component resets its state when rendered with a new props.state. Conversely, reusing props.state preserves the client-side state.

Equations

• One or more equations did not get rendered due to their size.

API for creating a RefreshComponent

structure ProofWidgets.RefreshToken : Type

A RefreshToken allows you to manage a RefreshComponent instance.

Use RefreshToken.update to update the HTML currently on display. Use RefreshToken.cancelTk to check if the instance has been discarded.

• state : IO.Ref RefreshComponent.RefreshState
• cancelTk : IO.CancelToken

  If set, the RefreshComponent is no longer displayed in the UI. The RefreshToken should be discarded, and any associated thread should exit.

• promise : IO.Ref (IO.Promise Unit)

def ProofWidgets.RefreshToken.updateLazy (token : RefreshToken) (html : Thunk Html) : BaseIO Unit

Update the current HTML tree to be html.

The html thunk is only forced when the client requests it; if another update is made before that, it will never be forced.

This function is thread-safe: each update is made atomically.

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.RefreshToken.update (token : RefreshToken) (html : Html) : BaseIO Unit

Update the current HTML tree to be html. See also updateLazy.

Equations

• token.update html = token.updateLazy (Thunk.pure html)

def ProofWidgets.mkRefreshComponent (initial : Html := Html.text "") : BaseIO (Html × RefreshToken)

Create a RefreshComponent instance together with a token to manage it.

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.mkRefreshComponentM {m : Type → Type} [Monad m] [MonadLiftT BaseIO m] [MonadSaveCtx m (EIO Lean.Exception)] [MonadWithReaderOf Lean.Core.Context m] (initial : Html) (k : RefreshToken → m Unit) : m Html

Create a RefreshComponent together with a dedicated thread that drives it by running k.

The typeclass assumptions essentially require m to extend CoreM. For early cooperative cancellation of CoreM computations, we automatically pass RefreshToken.cancelTk to Core.Context.

Equations

• One or more equations did not get rendered due to their size.