Documentation

Lean.Data.Lsp.Communication

Reading/writing LSP messages from/to IO handles.

source
def IO.FS.Stream.readLspMessage (h : IO.FS.Stream) :
IO Lean.JsonRpc.Message
Instances For
    source
    def IO.FS.Stream.readLspRequestAs (h : IO.FS.Stream) (expectedMethod : String) (α : Type) [Lean.FromJson α] :
    IO (Lean.JsonRpc.Request α)
    Instances For
      source
      def IO.FS.Stream.readLspNotificationAs (h : IO.FS.Stream) (expectedMethod : String) (α : Type) [Lean.FromJson α] :
      IO (Lean.JsonRpc.Notification α)
      Instances For
        source
        def IO.FS.Stream.readLspResponseAs (h : IO.FS.Stream) (expectedID : Lean.JsonRpc.RequestID) (α : Type) [Lean.FromJson α] :
        IO (Lean.JsonRpc.Response α)
        Instances For
          source
          def IO.FS.Stream.writeLspMessage (h : IO.FS.Stream) (msg : Lean.JsonRpc.Message) :
          IO Unit
          Instances For
            source
            def IO.FS.Stream.writeLspRequest {α : Type u_1} [Lean.ToJson α] (h : IO.FS.Stream) (r : Lean.JsonRpc.Request α) :
            IO Unit
            Instances For
              source
              def IO.FS.Stream.writeLspNotification {α : Type u_1} [Lean.ToJson α] (h : IO.FS.Stream) (n : Lean.JsonRpc.Notification α) :
              IO Unit
              Instances For
                source
                def IO.FS.Stream.writeLspResponse {α : Type u_1} [Lean.ToJson α] (h : IO.FS.Stream) (r : Lean.JsonRpc.Response α) :
                IO Unit
                Instances For
                  source
                  def IO.FS.Stream.writeLspResponseError (h : IO.FS.Stream) (e : Lean.JsonRpc.ResponseError Unit) :
                  IO Unit
                  Instances For
                    source
                    def IO.FS.Stream.writeLspResponseErrorWithData {α : Type u_1} [Lean.ToJson α] (h : IO.FS.Stream) (e : Lean.JsonRpc.ResponseError α) :
                    IO Unit
                    Instances For