-
Notifications
You must be signed in to change notification settings - Fork 22
/
Basic.lean
75 lines (59 loc) · 3.21 KB
/
Basic.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
import Lean.Widget.InteractiveCode
import Lean.Widget.UserWidget
import ProofWidgets.Compat
namespace ProofWidgets
open Lean
/-- A component is a widget module with a `default` or named export which is a
[React component](https://react.dev/learn/your-first-component). Every component definition must
be annotated with `@[widget_module]`. This makes it possible for the infoview to load the component.
## Execution environment
The JS environment in which components execute provides a fixed set of libraries accessible via
direct `import`, notably
[`@leanprover/infoview`](https://www.npmjs.com/package/@leanprover/infoview).
All [React contexts](https://react.dev/learn/passing-data-deeply-with-context) exported from
`@leanprover/infoview` are usable from components.
## Lean encoding of props
`Props` is the Lean representation of the type `JsProps` of
[React props](https://react.dev/learn/passing-props-to-a-component)
that the component expects.
The export of the module specified in `«export»` should then have type
`(props: JsProps & { pos: DocumentPosition }): React.ReactNode`
where `DocumentPosition` is defined in `@leanprover/infoview`.
`Props` is expected to have a `Lean.Server.RpcEncodable` instance
specifying how to encode props as JSON.
Note that by defining a `Component Props` with a specific JS implementation,
you are *asserting* that `Props` is a correct representation of `JsProps`. -/
structure Component (Props : Type) extends Widget.Module where
/-- Which export of the module to use as the component function. -/
«export» : String := "default"
instance : Widget.ToModule (Component Props) := ⟨Component.toModule⟩
structure InteractiveCodeProps where
fmt : Widget.CodeWithInfos
deriving Server.RpcEncodable
/-- Present pretty-printed code as interactive text.
The most common use case is to instantiate this component from a `Lean.Expr`. To do so, you must
eagerly pretty-print the `Expr` using `Widget.ppExprTagged`. See also `InteractiveExpr`. -/
@[widget_module]
def InteractiveCode : Component InteractiveCodeProps where
javascript := "
import { InteractiveCode } from '@leanprover/infoview'
import * as React from 'react'
export default function(props) {
return React.createElement(InteractiveCode, props)
}"
structure InteractiveExprProps where
expr : Server.WithRpcRef ExprWithCtx
deriving Server.RpcEncodable
@[server_rpc_method]
def ppExprTagged : InteractiveExprProps → Server.RequestM (Server.RequestTask Widget.CodeWithInfos)
| ⟨⟨expr⟩⟩ => Server.RequestM.asTask <| expr.runMetaM Widget.ppExprTagged
/-- Lazily pretty-print and present a `Lean.Expr` as interactive text.
This component is preferrable over `InteractiveCode` when the `Expr` will not necessarily be
displayed in the UI (e.g. it may be hidden by default), in which case laziness saves some work.
On the other hand if the `Expr` will likely be shown and you are in a `MetaM` context, it is
preferrable to use the eager `InteractiveCode` in order to avoid the extra client-server roundtrip
needed for the pretty-printing RPC call. -/
@[widget_module]
def InteractiveExpr : Component InteractiveExprProps where
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "interactiveExpr.js"
end ProofWidgets