Agda.Interaction.InteractionTop
data CommandState
type OldInteractionScopes
initCommandState
type CommandM
revLift
commandMToIO
liftCommandMT
putResponse
modifyTheInteractionPoints
oldInteractionScopes
modifyOldInteractionScopes
insertOldInteractionScope
removeOldInteractionScope
getOldInteractionScope
handleCommand_
handleCommand
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
searchAbout
whyInScope
setCommandLineOpts
status
displayStatus
display_info
refreshStr
nameModifiers
lowerMeta
parseAndDoAtToplevel
maybeTimed
tellToUpdateHighlighting
tellEmacsToJumpToError