Agda.Interaction.InteractionTop
data CommandState
type OldInteractionScopes
initCommandState
type CommandM
revLift
commandMToIO
liftCommandMT
putResponse
modifyTheInteractionPoints
oldInteractionScopes
modifyOldInteractionScopes
insertOldInteractionScope
removeOldInteractionScope
getOldInteractionScope
runInteraction
type Interaction
data Interaction' range
type IOTCM
data IOTCM' range
type Parse a
readsToParse
parseToReadsPrec
exact
readParse
parens'
independent
interpret
showOpenMetas
cmd_load'
withCurrentFile
data Backend
data GiveRefine
give_gen
highlightExpr
sortInteractionPoints
prettyTypeOfMeta
prettyContext
cmd_helper_function
cmd_goal_type_context_and
showModuleContents
whyInScope
setCommandLineOptions'
status
displayStatus
display_info
refreshStr
nameModifiers
lowerMeta
parseAndDoAtToplevel
tellToUpdateHighlighting
tellEmacsToJumpToError