Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

doc: fix documentation for widgets #1412

Closed
wants to merge 1 commit into from
Closed

doc: fix documentation for widgets #1412

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions doc/widgets.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ dependent on JavaScript. However the primary use case is the web-based infoview

## How to write your own user-widgets

You can write your own user-widgets using the `@[widgetSource]` attribute:
You can write your own user-widgets using the `@[widget]` attribute:

```lean
import Lean
Expand All @@ -28,10 +28,10 @@ def widget1 : UserWidgetDefinition := {
This JavaScript text must include `import * as React from "react"` in the imports and may not use JSX.
The default export of the sourcetext must be a React component whose props are an RPC encoding.
The React component may accept a props argument whose value will be determined for each particular widget instance (below).
Widget sources may import the `@lean4/infoview` package ([todo] publish on NPM) in order to use
Widget sources may import the `@lean4/infoview` package in order to use
components such as `InteractiveMessage` to display `MessageData` interactively.

## Using Lake to build your widgets

For larger projects, you can use Lake to create files that will be used as `widgetSource`.
To learn how to do this, please view the readme of the [WidgetsMinimal sample](https://github.com/leanprover/lean4-samples/tree/main/WidgetsMinimal) ([todo] merge sample).
To learn how to do this, please view the readme of the [RubiksCube sample](https://github.com/leanprover/lean4-samples/tree/main/RubiksCube).