Documentation

Lean.Widget.UserWidget

A widget module is a unit of source code that can execute in the infoview.

Every module definition must either be annotated with @[widget_module], or use a value of javascript identical to that of another definition annotated with @[widget_module]. This makes it possible for the infoview to load the module.

See the manual entry for more information on how to use the widgets system.

  • javascript : String

    A JS module intended for use in user widgets.

    The JS environment in which modules execute provides a fixed set of libraries accessible via direct import, notably @leanprover/infoview and react.

    To initialize this field from an external JS file, you may use include_str "path"/"to"/"file.js". However beware that this does not register a dependency with Lake, so your Lean module will not automatically be rebuilt when the .js file changes.

  • javascriptHash : { x : UInt64 // x = hash self.javascript }

    The hash is cached to avoid recomputing it whenever the Module is used.

Instances For
    @[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.

                    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
                          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
                                            Equations
                                            @[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

                                                Get the panel widgets present around a particular position.

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