Protocol.IDE

(source)

Messages exchanged during the IDE protocol

Reexports

import public Libraries.Data.Span
import public Protocol.IDE.Command as Protocol.IDE
import public Protocol.IDE.Decoration as Protocol.IDE
import public Protocol.IDE.Formatting as Protocol.IDE
import public Protocol.IDE.FileContext as Protocol.IDE
import public Protocol.IDE.Holes as Protocol.IDE
import public Protocol.IDE.Result as Protocol.IDE
import public Protocol.IDE.Highlight as Protocol.IDE

Definitions

Highlighting : Type

Totality: total
Visibility: public export

data ReplyPayload : Type

Totality: total
Visibility: public export
Constructors:

OK : Result -> Highlighting -> ReplyPayload
HighlightSource : List SourceHighlight -> ReplyPayload
Error : String -> Highlighting -> ReplyPayload

Hints:

FromSExpable ReplyPayload
SExpable ReplyPayload

data Reply : Type

Totality: total
Visibility: public export
Constructors:

ProtocolVersion : Int -> Int -> Reply
Immediate : ReplyPayload -> Integer -> Reply
Intermediate : ReplyPayload -> Integer -> Reply
WriteString : String -> Integer -> Reply
SetPrompt : String -> Integer -> Reply
Warning : FileContext -> String -> Highlighting -> Integer -> Reply

Hints:

FromSExpable Reply
SExpable Reply

data Request : Type

Totality: total
Visibility: public export
Constructor:

Cmd : IDECommand -> Request

Hints:

FromSExpable Request
SExpable Request