Index
| <+> | Render.RichText, Render |
| arrow | Render.RichText, Render |
| Block | Render.RichText, Render |
| braces | Render.RichText, Render |
| braces' | Render.RichText, Render |
| bracesAndSemicolons | Render.Concrete, Render |
| CommandController | Server.CommandController |
| Config | |
| 1 (Type/Class) | Options |
| 2 (Data Constructor) | Options |
| configRawAgdaOptions | Options |
| consumeCommand | Monad |
| createInitEnv | Monad |
| dbraces | Render.RichText, Render |
| destroy | Switchboard |
| dispatch | Server.ResponseController |
| DisplayInfo | Agda.IR |
| DisplayInfoAllGoalsWarnings | Agda.IR |
| DisplayInfoAuto | Agda.IR |
| DisplayInfoCompilationOk | Agda.IR |
| DisplayInfoCurrentGoal | Agda.IR |
| DisplayInfoError | Agda.IR |
| DisplayInfoGeneric | Agda.IR |
| DisplayInfoInferredType | Agda.IR |
| DisplayInfoNormalForm | Agda.IR |
| DisplayInfoTime | Agda.IR |
| emptyIdiomBrkt | Render.RichText, Render |
| Env | |
| 1 (Type/Class) | Monad |
| 2 (Data Constructor) | Monad |
| envCommandController | Monad |
| envConfig | Monad |
| envDevMode | Monad |
| envLogChan | Monad |
| envOptions | Monad |
| envResponseChan | Monad |
| envResponseController | Monad |
| explainWhyInScope | Agda.Convert |
| fcat | Render.RichText, Render |
| forallQ | Render.RichText, Render |
| FromAgda | Agda.IR |
| fromAgda | Agda.IR |
| FromAgdaTCM | Agda.IR |
| fromAgdaTCM | Agda.IR |
| fromDisplayInfo | Agda.Convert |
| fromHighlightingInfo | |
| 1 (Function) | Agda.Convert |
| 2 (Function) | Server.Handler |
| FromOffset | |
| 1 (Type/Class) | Agda.Position |
| 2 (Data Constructor) | Agda.Position |
| fromOffset | Agda.Position |
| fromResponse | Agda.Convert |
| fsep | Render.RichText, Render |
| getCommandLineOptions | Agda |
| getOptionsFromArgv | Options |
| GiveNoParen | Agda.IR |
| GiveParen | Agda.IR |
| GiveResult | Agda.IR |
| GiveString | Agda.IR |
| hcat | Render.RichText, Render |
| Header | Render.RichText, Render |
| HighlightingInfo | |
| 1 (Type/Class) | Agda.IR |
| 2 (Data Constructor) | Agda.IR |
| HighlightingInfos | |
| 1 (Type/Class) | Agda.IR |
| 2 (Data Constructor) | Agda.IR |
| hsep | Render.RichText, Render |
| icon | Render.RichText, Render |
| inferTypeOfText | Server.Handler |
| initConfig | Options |
| initialiseCommandQueue | Server.Handler |
| Inlines | |
| 1 (Type/Class) | Render.RichText, Render |
| 2 (Data Constructor) | Render.RichText, Render |
| isEmptySizedChan | Control.Concurrent.SizedChan |
| Labeled | Render.RichText, Render |
| lambda | Render.RichText, Render |
| leftIdiomBrkt | Render.RichText, Render |
| linkHole | Render.RichText, Render |
| linkRange | Render.RichText, Render |
| lispifyGoalSpecificDisplayInfo | Agda.Convert |
| makeFromOffset | Agda.Position |
| makeToOffset | Agda.Position |
| mparens | Render.RichText, Render |
| new | |
| 1 (Function) | Server.CommandController |
| 2 (Function) | Server.ResponseController |
| 3 (Function) | Switchboard |
| newSizedChan | Control.Concurrent.SizedChan |
| onHover | Server.Handler |
| optHelp | Options |
| Options | |
| 1 (Type/Class) | Options |
| 2 (Data Constructor) | Options |
| optRawAgdaOptions | Options |
| optViaTCP | Options |
| parens | Render.RichText, Render |
| peekSizedChan | Control.Concurrent.SizedChan |
| pHasEta0 | Render.Concrete, Render |
| pRecord | Render.Concrete, Render |
| pRecordDirective | Render.Concrete, Render |
| prefixedThings | Render.Common |
| prettyPositionWithoutFile | Agda.Position |
| prettyResponseContext | Agda.Convert |
| prettyResponseContexts | Agda.Convert |
| prettyTimed | Agda.Convert |
| prettyTypeOfMeta | Agda.Convert |
| provideCommand | Monad |
| punctuate | Render.RichText, Render |
| put | Server.CommandController |
| readSizedChan | Control.Concurrent.SizedChan |
| release | Server.CommandController |
| Render | Render.Class, Render |
| render | Render.Class, Render |
| renderA | Render.Class, Render |
| renderATop | Render.Class, Render |
| renderCohesion | Render.Common |
| renderDom | Render.Internal |
| renderHiding | Render.Common |
| renderM | Render.Class, Render |
| renderOpApp | Render.Concrete, Render |
| renderP | Render.Class, Render |
| renderPrec | Render.Class, Render |
| renderPrecLevelSucs | Render.Internal |
| renderQuantity | Render.Common |
| renderRelevance | Render.Common |
| renderResponseContext | Agda.Convert |
| renderTactic | Render.Concrete, Render |
| renderTactic' | Render.Concrete, Render |
| Response | Agda.IR |
| responseAbbr | Agda.Convert |
| ResponseClearHighlightingNotOnlyTokenBased | Agda.IR |
| ResponseClearHighlightingTokenBased | Agda.IR |
| ResponseClearRunningInfo | Agda.IR |
| ResponseController | Server.ResponseController |
| ResponseDisplayInfo | Agda.IR |
| ResponseDoneAborting | Agda.IR |
| ResponseDoneExiting | Agda.IR |
| ResponseEnd | Agda.IR |
| ResponseGiveAction | Agda.IR |
| ResponseHighlightingInfoDirect | Agda.IR |
| ResponseHighlightingInfoIndirect | Agda.IR |
| ResponseInteractionPoints | Agda.IR |
| ResponseJumpToError | Agda.IR |
| ResponseMakeCaseExtendedLambda | Agda.IR |
| ResponseMakeCaseFunction | Agda.IR |
| ResponseRunningInfo | Agda.IR |
| ResponseSolveAll | Agda.IR |
| ResponseStatus | Agda.IR |
| rightIdiomBrkt | Render.RichText, Render |
| run | Server |
| runAgda | Agda |
| runCommandM | Server.Handler |
| runServerM | Monad |
| sendCommand | Agda |
| sendResponse | Monad |
| sep | Render.RichText, Render |
| serialize | Agda.Convert |
| ServerM | Monad |
| setCheckpointAndWait | Server.ResponseController |
| setupLanguageContextEnv | Switchboard |
| showIndex | Render.RichText, Render |
| showInfoError | Agda.Convert |
| signalCommandFinish | Monad |
| SizedChan | Control.Concurrent.SizedChan |
| smashTel | Render.Concrete, Render |
| space | Render.RichText, Render |
| start | Agda |
| Switchboard | Switchboard |
| take | Server.CommandController |
| text | Render.RichText, Render |
| text' | Render.RichText, Render |
| toAgdaPositionWithoutFile | Agda.Position |
| toAgdaRange | Agda.Position |
| tokenAt | Agda.Parser |
| ToOffset | |
| 1 (Type/Class) | Agda.Position |
| 2 (Data Constructor) | Agda.Position |
| toOffset | Agda.Position |
| tryPeekSizedChan | Control.Concurrent.SizedChan |
| tryReadSizedChan | Control.Concurrent.SizedChan |
| unFromOffset | Agda.Position |
| unInlines | Render.RichText, Render |
| Unlabeled | Render.RichText, Render |
| unToOffset | Agda.Position |
| usageMessage | Options |
| vcat | Render.RichText, Render |
| waitUntilResponsesSent | Monad |
| writeLog | Monad |
| writeLog' | Monad |
| writeSizedChan | Control.Concurrent.SizedChan |