Documentation

Lean.Widget.UserWidget

@[implemented_by _private.Lean.Widget.UserWidget.0.Lean.Widget.evalModuleUnsafe]
@[implemented_by _private.Lean.Widget.UserWidget.0.Lean.Widget.evalWidgetInstanceUnsafe]

Storage of widget modules #

class Lean.Widget.ToModule (α : Type u) :
Instances

    Registers a widget module. Its type must implement Lean.Widget.ToModule.

    Retrieval of widget modules #

    Instances For
      • sourcetext : String

        Sourcetext of the JS module to run.

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

          Storage of panel widget instances #

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

                Construct a widget instance by finding a widget module in the current environment.

                hash must be hash (toModule c).javascript where c is some global constant annotated with @[widget_module], or the name of a builtin widget module.

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

                  Save the data of a panel widget which will be displayed whenever the text cursor is on stx.

                  hash must be as in WidgetInstance.ofHash.

                  For panel widgets, the Lean infoview appends additional fields to the props object: see https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/userWidget.tsx#L145.

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

                    show_panel_widgets command #

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Lean.Widget.elabWidgetInstanceSpec :
                        TSyntax `Lean.Widget.widgetInstanceSpecElab.TermElabM Expr
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                Use show_panel_widgets [<widget>] to mark that <widget> should always be displayed, including in downstream modules.

                                The type of <widget> must implement Widget.ToModule, and the type of <props> must implement Server.RpcEncodable. In particular, <props> : Json works.

                                Use show_panel_widgets [<widget> with <props>] to specify the <props> that the widget should be given as arguments.

                                Use show_panel_widgets [local <widget> (with <props>)?] to mark it for display in the current section, namespace, or file only.

                                Use show_panel_widgets [scoped <widget> (with <props>)?] to mark it for display only when the current namespace is open.

                                Use show_panel_widgets [-<widget>] to temporarily hide a previously shown widget in the current section, namespace, or file. Note that persistent erasure is not possible, i.e., -<widget> has no effect on downstream modules.

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

                                    #widget command #

                                    Use #widget <widget> to display a panel widget, and #widget <widget> with <props> to display it with the given props. Useful for debugging widgets.

                                    The type of <widget> must implement Widget.ToModule, and the type of <props> must implement Server.RpcEncodable. In particular, <props> : Json works.

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

                                        Deprecated definitions #

                                        Use this structure and the @[widget] attribute to define your own widgets.

                                        @[widget]
                                        def rubiks : UserWidgetDefinition :=
                                          { name := "Rubiks cube app"
                                            javascript := include_str ...
                                          }
                                        
                                        • name : String

                                          Pretty name of user widget to display to the user.

                                        • javascript : String

                                          An ESmodule that exports a react component to render.

                                        Instances For
                                          @[implemented_by _private.Lean.Widget.UserWidget.0.Lean.Widget.evalUserWidgetDefinitionUnsafe]

                                          Retrieving panel widget instances #

                                          Retrieve all the UserWidgetInfos that intersect a given line.

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

                                              Output of getWidgets RPC.

                                              Instances For

                                                Get the panel widgets present around a particular position.

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