Documentation

Lean.Data.Lsp.Ipc

Provides an IpcM monad for interacting with an external LSP process. Used for testing the Lean server.

source
def Lean.Lsp.Ipc.ipcStdioConfig :
IO.Process.StdioConfig
Instances For
    source
    @[inline, reducible]
    abbrev Lean.Lsp.Ipc.IpcM (α : Type) :
    Type
    Instances For
      source
      def Lean.Lsp.Ipc.stdin :
      Lean.Lsp.Ipc.IpcM IO.FS.Stream
      Instances For
        source
        def Lean.Lsp.Ipc.stdout :
        Lean.Lsp.Ipc.IpcM IO.FS.Stream
        Instances For
          source
          def Lean.Lsp.Ipc.writeRequest {α : Type u_1} [Lean.ToJson α] (r : Lean.JsonRpc.Request α) :
          Lean.Lsp.Ipc.IpcM Unit
          Instances For
            source
            def Lean.Lsp.Ipc.writeNotification {α : Type u_1} [Lean.ToJson α] (n : Lean.JsonRpc.Notification α) :
            Lean.Lsp.Ipc.IpcM Unit
            Instances For
              source
              def Lean.Lsp.Ipc.shutdown (requestNo : Nat) :
              Lean.Lsp.Ipc.IpcM Unit
              Instances For
                source
                def Lean.Lsp.Ipc.readMessage :
                Lean.Lsp.Ipc.IpcM Lean.JsonRpc.Message
                Instances For
                  source
                  def Lean.Lsp.Ipc.readRequestAs (expectedMethod : String) (α : Type) [Lean.FromJson α] :
                  Lean.Lsp.Ipc.IpcM (Lean.JsonRpc.Request α)
                  Instances For
                    source
                    def Lean.Lsp.Ipc.readResponseAs (expectedID : Lean.JsonRpc.RequestID) (α : Type) [Lean.FromJson α] :
                    Lean.Lsp.Ipc.IpcM (Lean.JsonRpc.Response α)
                    Instances For
                      source
                      def Lean.Lsp.Ipc.waitForExit :
                      Lean.Lsp.Ipc.IpcM UInt32
                      Instances For
                        source
                        def Lean.Lsp.Ipc.collectDiagnostics (waitForDiagnosticsId : optParam Lean.JsonRpc.RequestID 0) (target : Lean.Lsp.DocumentUri) (version : Nat) :
                        Lean.Lsp.Ipc.IpcM (List (Lean.JsonRpc.Notification Lean.Lsp.PublishDiagnosticsParams))

                        Waits for the worker to emit all diagnostics for the current document version and returns them as a list.

                        Instances For
                          source
                          partial def Lean.Lsp.Ipc.collectDiagnostics.loop (waitForDiagnosticsId : optParam Lean.JsonRpc.RequestID 0) :
                          Lean.Lsp.Ipc.IpcM (List (Lean.JsonRpc.Notification Lean.Lsp.PublishDiagnosticsParams))
                          source
                          def Lean.Lsp.Ipc.runWith {α : Type} (lean : Lake.FilePath) (args : optParam (Array String) #[]) (test : Lean.Lsp.Ipc.IpcM α) :
                          IO α
                          Instances For