Hoogle Search
Within LTS Haskell 24.41 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
oldInteractionScopes :: CommandState -> !OldInteractionScopesAgda Agda.Interaction.Base We remember (the scope of) old interaction points to make it possible to parse and compute highlighting information for the expression that it got replaced by.
theInteractionPoints :: CommandState -> [InteractionId]Agda Agda.Interaction.Base The interaction points of the buffer, in the order in which they appear in the buffer. The interaction points are recorded in theTCState, but when new interaction points are added by give or refine Agda does not ensure that the ranges of later interaction points are updated.
getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]Agda Agda.Interaction.BasicOps getSolvedInteractionPoints True returns all solutions, even if just solved by another, non-interaction meta. getSolvedInteractionPoints False only returns metas that are solved by a non-meta.
runInteractionLoop :: Maybe AbsolutePath -> TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM ()Agda Agda.Interaction.CommandLine No documentation available.
getOldInteractionScope :: InteractionId -> CommandM ScopeInfoAgda Agda.Interaction.InteractionTop No documentation available.
insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()Agda Agda.Interaction.InteractionTop No documentation available.
modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()Agda Agda.Interaction.InteractionTop A Lens for oldInteractionScopes.
modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> CommandM ()Agda Agda.Interaction.InteractionTop A Lens for theInteractionPoints.
removeOldInteractionScope :: InteractionId -> CommandM ()Agda Agda.Interaction.InteractionTop No documentation available.
runInteraction :: IOTCM -> CommandM ()Agda Agda.Interaction.InteractionTop Run an IOTCM value, catch the exceptions, emit output If an error happens the state of CommandM does not change, but stPersistent may change (which contains successfully loaded interfaces for example).