Documentation

Lean.Server.FileWorker.InlayHints

source
def Lean.Elab.InlayHintLinkLocation.toLspLocation (text : FileMap) (l : InlayHintLinkLocation) :
IO (Option Lsp.Location)
Equations
    Instances For
      source
      def Lean.Elab.InlayHintLabelPart.toLspInlayHintLabelPart (text : FileMap) (p : InlayHintLabelPart) :
      IO Lsp.InlayHintLabelPart
      Equations
        Instances For
          source
          def Lean.Elab.InlayHintLabel.toLspInlayHintLabel (text : FileMap) :
          InlayHintLabel → IO Lsp.InlayHintLabel
          Equations
            Instances For
              source
              def Lean.Elab.InlayHintKind.toLspInlayHintKind :
              InlayHintKind → Lsp.InlayHintKind
              Equations
                Instances For
                  source
                  def Lean.Elab.InlayHintTextEdit.toLspTextEdit (text : FileMap) (e : InlayHintTextEdit) :
                  Lsp.TextEdit
                  Equations
                    Instances For
                      source
                      def Lean.Elab.InlayHintInfo.toLspInlayHint (text : FileMap) (i : InlayHintInfo) :
                      IO Lsp.InlayHint
                      Equations
                        Instances For
                          source
                          def Lean.Server.FileWorker.applyEditToHint? (hintMod : Name) (ihi : Elab.InlayHintInfo) (range : Syntax.Range) (newText : String) :
                          Option Elab.InlayHintInfo
                          Equations
                            Instances For
                              source
                              structure Lean.Server.FileWorker.InlayHintState :
                              Type
                              Instances For
                                source
                                instance Lean.Server.FileWorker.instTypeNameInlayHintState :
                                TypeName InlayHintState
                                Equations
                                  source
                                  def Lean.Server.FileWorker.instInhabitedInlayHintState.default :
                                  InlayHintState
                                  Equations
                                    Instances For
                                      source
                                      instance Lean.Server.FileWorker.instInhabitedInlayHintState :
                                      Inhabited InlayHintState
                                      Equations
                                        source
                                        def Lean.Server.FileWorker.InlayHintState.init :
                                        InlayHintState
                                        Equations
                                          Instances For
                                            source
                                            def Lean.Server.FileWorker.handleInlayHints (p : Lsp.InlayHintParams) (s : InlayHintState) :
                                            RequestM (LspResponse (Array Lsp.InlayHint) × InlayHintState)
                                            Equations
                                              Instances For
                                                source
                                                def Lean.Server.FileWorker.handleInlayHintsDidChange (p : Lsp.DidChangeTextDocumentParams) :
                                                StateT InlayHintState RequestM Unit
                                                Equations
                                                  Instances For