module Agda.Interaction.GhciTop
( module Agda.Interaction.GhciTop
, module Agda.TypeChecker
, module Agda.TypeChecking.MetaVars
, module Agda.TypeChecking.Reduce
, module Agda.TypeChecking.Errors
, module Agda.Syntax.Position
, module Agda.Syntax.Parser
, module Agda.Syntax.Scope.Base
, module Agda.Syntax.Scope.Monad
, module Agda.Syntax.Translation.ConcreteToAbstract
, module Agda.Syntax.Translation.AbstractToConcrete
, module Agda.Syntax.Translation.InternalToAbstract
, module Agda.Syntax.Abstract.Name
, module Agda.Interaction.Exceptions
, mkAbsolute
)
where
import System.Directory
import qualified System.IO as IO
import System.IO.Unsafe
import Data.Char
import Data.Maybe
import Data.IORef
import Data.Function
import Control.Applicative
import Agda.Utils.Fresh
import Agda.Utils.Monad
import Agda.Utils.Pretty as P
import Agda.Utils.String
import Agda.Utils.FileName
import Agda.Utils.Tuple
import qualified Agda.Utils.IO.Locale as LocIO
import qualified Agda.Utils.IO.UTF8 as UTF8
import Control.Monad.Error
import Control.Monad.Reader
import Control.Monad.State hiding (State)
import Control.Exception
import Data.List as List
import qualified Data.Map as Map
import System.Exit
import qualified System.Mem as System
import System.Time
import Text.PrettyPrint
import Agda.TypeChecker
import Agda.TypeChecking.Monad as TM
hiding (initState, setCommandLineOptions)
import qualified Agda.TypeChecking.Monad as TM
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Serialise (encodeFile)
import Agda.Syntax.Position
import Agda.Syntax.Parser
import qualified Agda.Syntax.Parser.Tokens as T
import Agda.Syntax.Concrete as SC
import Agda.Syntax.Common as SCo
import Agda.Syntax.Concrete.Name as CN
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Abstract as SA
import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.Internal as SI
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad hiding (bindName, withCurrentModule)
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Translation.AbstractToConcrete hiding (withScope)
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Abstract.Name
import Agda.Interaction.Exceptions
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import Agda.Interaction.MakeCase
import qualified Agda.Interaction.BasicOps as B
import qualified Agda.Interaction.CommandLine.CommandLine as CL
import Agda.Interaction.Highlighting.Emacs
import Agda.Interaction.Highlighting.Generate
import qualified Agda.Interaction.Imports as Imp
import Agda.Termination.TermCheck
import qualified Agda.Compiler.MAlonzo.Compiler as MAlonzo
import qualified Agda.Auto.Auto as Auto
#include "../undefined.h"
import Agda.Utils.Impossible
data State = State
{ theTCState :: TCState
, theInteractionPoints :: [InteractionId]
, theCurrentFile :: Maybe (AbsolutePath, ClockTime)
}
initState :: State
initState = State
{ theTCState = TM.initState
, theInteractionPoints = []
, theCurrentFile = Nothing
}
theState :: IORef State
theState = unsafePerformIO $ newIORef initState
data Interaction = Interaction
{ isIndependent :: Bool
, command :: TCM (Maybe ModuleName)
}
ioTCM_ :: TCM a -> IO a
ioTCM_ m = do
tcs <- readIORef theState
Right (x, s) <- runTCM $ do
put $ theTCState tcs
x <- withEnv initEnv m
s <- get
return (x, s)
writeIORef theState $ tcs { theTCState = s }
return x
ioTCM :: FilePath
-> Maybe FilePath
-> Interaction
-> IO ()
ioTCM current highlightingFile cmd = infoOnException $ do
#if MIN_VERSION_base(4,2,0)
IO.hSetEncoding IO.stdout IO.utf8
#endif
current <- absolute current
State { theTCState = st
, theCurrentFile = f
} <- readIORef theState
r <- if not (isIndependent cmd) && Just current /= (fst <$> f) then
let s = "Error: First load the file." in
return $ Right $ Left (s, TCErr Nothing $ Exception noRange s)
else
runTCM $ catchError (do
put st
x <- withEnv initEnv $ command cmd
st <- get
return (Right (x, st))
) (\e -> do
s <- prettyError e
return (Left (s, e))
)
case r of
Right (Right (m, st')) ->
modifyIORef theState $ \s ->
s { theTCState = st'
}
_ | isIndependent cmd ->
modifyIORef theState $ \s ->
s { theCurrentFile = Nothing }
_ -> return ()
case highlightingFile of
Nothing -> return ()
Just f -> do
let errHi e s = errHighlighting e
`mplus`
((\h -> (h, Map.empty)) <$>
generateErrorInfo (getRange e) s)
UTF8.writeFile f $
showHighlightingInfo $
case r of
Right (Right (mm, st')) -> do
m <- mm
mi <- Map.lookup (SA.toTopLevelModuleName m)
(stVisitedModules st')
return ( iHighlighting $ miInterface mi
, stModuleToSource st'
)
Right (Left (s, e)) -> errHi e (Just s)
Left e -> errHi e Nothing
let errStatus = Status { sChecked = False
, sShowImplicitArguments =
optShowImplicit $ stPragmaOptions st
}
case r of
Right (Right _) -> return ()
Right (Left (s, e)) -> displayErrorAndExit errStatus (getRange e) s
Left e -> displayErrorAndExit errStatus (getRange e) $
tcErrString e
cmd_load :: FilePath -> [FilePath] -> Interaction
cmd_load m includes =
cmd_load' m includes True (\_ -> command cmd_metas >> return ())
cmd_load' :: FilePath -> [FilePath]
-> Bool
-> ((Interface, Maybe Imp.Warnings) -> TCM ())
-> Interaction
cmd_load' file includes unsolvedOK cmd = Interaction True $ do
liftIO $ modifyIORef theState $ \s ->
s { theInteractionPoints = []
, theCurrentFile = Nothing
}
f <- liftIO $ absolute file
t <- liftIO $ getModificationTime file
oldIncs <- getIncludeDirs
setCommandLineOptions $
defaultOptions { optAllowUnsolved = unsolvedOK
, optIncludeDirs = includes
}
preserveDecodedModules resetState
ok <- Imp.typeCheck file Imp.ProjectRoot (Just oldIncs)
t' <- liftIO $ getModificationTime file
when (t == t') $ do
is <- sortInteractionPoints =<< getInteractionPoints
liftIO $ modifyIORef theState $ \s ->
s { theInteractionPoints = is
, theCurrentFile = Just (f, t)
}
cmd ok
liftIO System.performGC
return $ Just $ iModuleName (fst ok)
cmd_compile :: FilePath -> [FilePath] -> Interaction
cmd_compile file includes =
cmd_load' file includes False (\(i, mw) ->
case mw of
Nothing -> do
MAlonzo.compilerMain i
display_info "*Compilation result*"
"The module was successfully compiled."
Just w ->
display_info errorTitle $ unlines
[ "You can only compile modules without unsolved metavariables"
, "or termination checking problems."
])
cmd_constraints :: Interaction
cmd_constraints = Interaction False $ do
cs <- map show <$> B.getConstraints
display_info "*Constraints*" (unlines cs)
return Nothing
cmd_metas :: Interaction
cmd_metas = Interaction False $ do
ims <- fst <$> B.typeOfMetas B.AsIs
hms <- snd <$> B.typeOfMetas B.Normalised
if not $ null ims && null hms
then do
di <- mapM (\i -> B.withInteractionId (B.outputFormId i) (showA i)) ims
dh <- mapM showA' hms
display_info "*All Goals*" $ unlines $ di ++ dh
return Nothing
else do
cs <- B.getConstraints
if null cs
then display_info "*All Goals*" "" >> return Nothing
else command cmd_constraints
where
metaId (B.OfType i _) = i
metaId (B.JustType i) = i
metaId (B.JustSort i) = i
metaId (B.Assign i e) = i
metaId _ = __IMPOSSIBLE__
showA' m = do
r <- getMetaRange (metaId m)
d <- B.withMetaId (B.outputFormId m) (showA m)
return $ d ++ " [ at " ++ show r ++ " ]"
cmd_reset :: Interaction
cmd_reset = Interaction True $ do
preserveDecodedModules resetState
return Nothing
type GoalCommand = InteractionId -> Range -> String -> Interaction
cmd_give :: GoalCommand
cmd_give = give_gen B.give $ \s ce -> case ce of (SC.Paren _ _)-> "'paren"
_ -> "'no-paren"
cmd_refine :: GoalCommand
cmd_refine = give_gen B.refine $ \s -> quote . show
give_gen give_ref mk_newtxt ii rng s = Interaction False $ do
scope <- getInteractionScope ii
(ae, iis) <- give_ref ii Nothing =<< B.parseExprIn ii rng s
let newtxt = A . mk_newtxt s $ abstractToConcrete (makeEnv scope) ae
iis <- sortInteractionPoints iis
liftIO $ modifyIORef theState $ \s ->
s { theInteractionPoints =
replace ii iis (theInteractionPoints s) }
liftIO $ LocIO.putStrLn $ response $
L [A "agda2-give-action", showNumIId ii, newtxt]
command cmd_metas
return Nothing
where
replace x xs ys = concatMap (\y -> if y == x then xs else [y]) ys
cmd_intro :: GoalCommand
cmd_intro ii rng _ = Interaction False $ do
ss <- B.introTactic ii
B.withInteractionId ii $ case ss of
[] -> do
display_infoD "*Intro*" $ text "No introduction forms found."
return Nothing
[s] -> command $ cmd_refine ii rng s
_:_:_ -> do
display_infoD "*Intro*" $
sep [ text "Don't know which constructor to introduce of"
, let mkOr [] = []
mkOr [x, y] = [text x <+> text "or" <+> text y]
mkOr (x:xs) = text x : mkOr xs
in nest 2 $ fsep $ punctuate comma (mkOr ss)
]
return Nothing
cmd_refine_or_intro :: GoalCommand
cmd_refine_or_intro ii rng s =
(if null s then cmd_intro else cmd_refine) ii rng s
cmd_auto :: GoalCommand
cmd_auto ii rng s = Interaction False $ do
(xs, msg) <- Auto.auto ii rng s
mapM_ (\(ii, s) -> do
liftIO $ modifyIORef theState $ \s ->
s { theInteractionPoints = filter (/= ii) (theInteractionPoints s) }
liftIO $ LocIO.putStrLn $ response $ L [A "agda2-give-action", showNumIId ii, A $ quote s]
) xs
case msg of
Nothing -> command cmd_metas >> return ()
Just msg -> display_info "*Auto*" msg
return Nothing
sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]
sortInteractionPoints is =
map fst . sortBy (compare `on` snd) <$>
mapM (\i -> (,) i <$> getInteractionRange i) is
prettyTypeOfMeta :: B.Rewrite -> InteractionId -> TCM Doc
prettyTypeOfMeta norm ii = do
form <- B.typeOfMeta norm ii
case form of
B.OfType _ e -> prettyA e
_ -> text <$> showA form
prettyContext
:: B.Rewrite
-> InteractionId
-> TCM Doc
prettyContext norm ii = B.withInteractionId ii $ do
ctx <- B.contextOfMeta ii norm
es <- mapM (prettyA . B.ofExpr) ctx
ns <- mapM (showA . B.ofName) ctx
let maxLen = maximum $ 0 : filter (< longNameLength) (map length ns)
return $ vcat $
map (\(n, e) -> text n $$ nest (maxLen + 1) (text ":") <+> e) $
zip ns es
longNameLength = 10
cmd_context :: B.Rewrite -> GoalCommand
cmd_context norm ii _ _ = Interaction False $ do
display_infoD "*Context*" =<< prettyContext norm ii
return Nothing
cmd_infer :: B.Rewrite -> GoalCommand
cmd_infer norm ii rng s = Interaction False $ do
display_infoD "*Inferred Type*"
=<< B.withInteractionId ii
(prettyA =<< B.typeInMeta ii norm =<< B.parseExprIn ii rng s)
return Nothing
cmd_goal_type :: B.Rewrite -> GoalCommand
cmd_goal_type norm ii _ _ = Interaction False $ do
s <- B.withInteractionId ii $ prettyTypeOfMeta norm ii
display_infoD "*Current Goal*" s
return Nothing
cmd_goal_type_context_and doc norm ii _ _ = do
goal <- B.withInteractionId ii $ prettyTypeOfMeta norm ii
ctx <- prettyContext norm ii
display_infoD "*Goal type etc.*"
(ctx $+$
text (replicate 60 '\x2014') $+$
text "Goal:" <+> goal $+$
doc)
return Nothing
cmd_goal_type_context :: B.Rewrite -> GoalCommand
cmd_goal_type_context norm ii rng s = Interaction False $
cmd_goal_type_context_and P.empty norm ii rng s
cmd_goal_type_context_infer :: B.Rewrite -> GoalCommand
cmd_goal_type_context_infer norm ii rng s = Interaction False $ do
typ <- B.withInteractionId ii $
prettyA =<< B.typeInMeta ii norm =<< B.parseExprIn ii rng s
cmd_goal_type_context_and (text "Have:" <+> typ) norm ii rng s
setCommandLineOptions :: CommandLineOptions -> TCM ()
setCommandLineOptions opts = do
TM.setCommandLineOptions PersistentOptions opts
liftIO . displayStatus =<< status
data Status = Status
{ sShowImplicitArguments :: Bool
, sChecked :: Bool
}
status :: TCM Status
status = do
showImpl <- showImplicitArguments
cur <- theCurrentFile <$> liftIO (readIORef theState)
checked <- case cur of
Nothing -> return False
Just (f, t) -> do
t' <- liftIO $ getModificationTime $ filePath f
case t == t' of
False -> return False
True ->
not . miWarnings . maybe __IMPOSSIBLE__ id <$>
(getVisitedModule =<<
maybe __IMPOSSIBLE__ id .
Map.lookup f <$> sourceToModule)
return $ Status { sShowImplicitArguments = showImpl
, sChecked = checked
}
showStatus :: Status -> String
showStatus s = intercalate "," $ catMaybes [checked, showImpl]
where
boolToMaybe b x = if b then Just x else Nothing
checked = boolToMaybe (sChecked s) "Checked"
showImpl = boolToMaybe (sShowImplicitArguments s) "ShowImplicit"
displayStatus :: Status -> IO ()
displayStatus s =
LocIO.putStrLn $ response $
L [A "agda2-status-action", A (quote $ showStatus s)]
display_info' :: String -> String -> IO ()
display_info' bufname content =
LocIO.putStrLn $ response $
L [ A "agda2-info-action"
, A (quote bufname)
, A (quote content)
]
display_info :: String -> String -> TCM ()
display_info bufname content = do
liftIO . displayStatus =<< status
liftIO $ display_info' bufname content
display_infoD :: String -> Doc -> TCM ()
display_infoD bufname content = display_info bufname (render content)
response :: Lisp String -> String
response l = show (text "agda2_mode_code" <+> pretty l)
responseString :: Lisp String -> String
responseString s = response $
L [A "setq", A "agda2-response", s]
respond :: Lisp String -> IO ()
respond = LocIO.putStrLn . responseString
data Lisp a = A a | L [Lisp a] | Q (Lisp a)
instance Pretty a => Pretty (Lisp a) where
pretty (A a ) = pretty a
pretty (L xs) = parens (sep (List.map pretty xs))
pretty (Q x) = text "'"<>pretty x
instance Pretty String where pretty = text
instance Pretty a => Show (Lisp a) where show = show . pretty
showNumIId = A . tail . show
takenNameStr :: TCM [String]
takenNameStr = do
xss <- sequence [ List.map (fst . unArg) <$> getContext
, Map.keys <$> asks envLetBindings
, List.map qnameName . Map.keys . sigDefinitions <$> getSignature
]
return $ concat [ parts $ nameConcrete x | x <- concat xss]
where
parts x = [ s | Id s <- nameParts x ]
refreshStr :: [String] -> String -> ([String], String)
refreshStr taken s = go nameModifiers where
go (m:mods) = let s' = s ++ m in
if s' `elem` taken then go mods else (s':taken, s')
go _ = __IMPOSSIBLE__
nameModifiers = "" : "'" : "''" : [show i | i <-[3..]]
cmd_make_case :: GoalCommand
cmd_make_case ii rng s = Interaction False $ do
cs <- makeCase ii rng s
B.withInteractionId ii $ do
pcs <- mapM prettyA cs
liftIO $ LocIO.putStrLn $ response $
L [ A "agda2-make-case-action",
Q $ L $ List.map (A . quote . renderStyle (style { mode = OneLineMode })) pcs
]
return Nothing
cmd_solveAll :: Interaction
cmd_solveAll = Interaction False $ do
out <- getInsts
liftIO $ LocIO.putStrLn $ response $
L[ A"agda2-solveAll-action" , Q . L $ concatMap prn out]
return Nothing
where
getInsts = mapM lowr =<< B.getSolvedInteractionPoints
where
lowr (i, m, e) = do
mi <- getMetaInfo <$> lookupMeta m
e <- withMetaInfo mi $ lowerMeta <$> abstractToConcrete_ e
return (i, e)
prn (ii,e)= [showNumIId ii, A $ quote $ show e]
class LowerMeta a where lowerMeta :: a -> a
instance LowerMeta SC.Expr where
lowerMeta = go where
go e = case e of
Ident _ -> e
SC.Lit _ -> e
SC.QuestionMark _ _ -> preMeta
SC.Underscore _ _ -> preUscore
SC.App r e1 ae2 -> case appView e of
SC.AppView (SC.QuestionMark _ _) _ -> preMeta
SC.AppView (SC.Underscore _ _) _ -> preUscore
_ -> SC.App r (go e1) (lowerMeta ae2)
SC.WithApp r e es -> SC.WithApp r (lowerMeta e) (lowerMeta es)
SC.Lam r bs e1 -> SC.Lam r (lowerMeta bs) (go e1)
SC.AbsurdLam r h -> SC.AbsurdLam r h
SC.Fun r ae1 e2 -> SC.Fun r (lowerMeta ae1) (go e2)
SC.Pi tb e1 -> SC.Pi (lowerMeta tb) (go e1)
SC.Set _ -> e
SC.Prop _ -> e
SC.SetN _ _ -> e
SC.ETel tel -> SC.ETel (lowerMeta tel)
SC.Let r ds e1 -> SC.Let r (lowerMeta ds) (go e1)
Paren r e1 -> case go e1 of
q@(SC.QuestionMark _ Nothing) -> q
e2 -> Paren r e2
Absurd _ -> e
As r n e1 -> As r n (go e1)
SC.Dot r e -> SC.Dot r (go e)
SC.RawApp r es -> SC.RawApp r (lowerMeta es)
SC.OpApp r x es -> SC.OpApp r x (lowerMeta es)
SC.Rec r fs -> SC.Rec r (List.map (id -*- lowerMeta) fs)
SC.HiddenArg r e -> SC.HiddenArg r (lowerMeta e)
instance LowerMeta SC.LamBinding where
lowerMeta b@(SC.DomainFree _ _) = b
lowerMeta (SC.DomainFull tb) = SC.DomainFull (lowerMeta tb)
instance LowerMeta SC.TypedBindings where
lowerMeta (SC.TypedBindings r h bs) = SC.TypedBindings r h (lowerMeta bs)
instance LowerMeta SC.TypedBinding where
lowerMeta (SC.TBind r ns e) = SC.TBind r ns (lowerMeta e)
lowerMeta (SC.TNoBind e) = SC.TNoBind (lowerMeta e)
instance LowerMeta SC.RHS where
lowerMeta (SC.RHS e) = SC.RHS (lowerMeta e)
lowerMeta SC.AbsurdRHS = SC.AbsurdRHS
instance LowerMeta SC.Declaration where
lowerMeta = go where
go d = case d of
TypeSig n e1 -> TypeSig n (lowerMeta e1)
SC.Field h n e1 -> SC.Field h n (lowerMeta e1)
FunClause lhs rhs whcl -> FunClause lhs (lowerMeta rhs) (lowerMeta whcl)
Data r ind n tel e1 cs -> Data r ind n
(lowerMeta tel) (lowerMeta e1) (lowerMeta cs)
SC.Record r n c tel e1 cs -> SC.Record r n c
(lowerMeta tel) (lowerMeta e1) (lowerMeta cs)
Infix _ _ -> d
Mutual r ds -> Mutual r (lowerMeta ds)
Abstract r ds -> Abstract r (lowerMeta ds)
Private r ds -> Private r (lowerMeta ds)
Postulate r sigs -> Postulate r (lowerMeta sigs)
SC.Primitive r sigs -> SC.Primitive r (lowerMeta sigs)
SC.Open _ _ _ -> d
SC.Import _ _ _ _ _ -> d
SC.Pragma _ -> d
ModuleMacro r n tel e1 op dir -> ModuleMacro r n
(lowerMeta tel) (lowerMeta e1) op dir
SC.Module r qn tel ds -> SC.Module r qn (lowerMeta tel) (lowerMeta ds)
instance LowerMeta SC.WhereClause where
lowerMeta SC.NoWhere = SC.NoWhere
lowerMeta (SC.AnyWhere ds) = SC.AnyWhere $ lowerMeta ds
lowerMeta (SC.SomeWhere m ds) = SC.SomeWhere m $ lowerMeta ds
instance LowerMeta a => LowerMeta [a] where
lowerMeta as = List.map lowerMeta as
instance LowerMeta a => LowerMeta (Arg a) where
lowerMeta aa = fmap lowerMeta aa
instance LowerMeta a => LowerMeta (Named name a) where
lowerMeta aa = fmap lowerMeta aa
preMeta = SC.QuestionMark noRange Nothing
preUscore = SC.Underscore noRange Nothing
cmd_compute :: Bool
-> GoalCommand
cmd_compute ignore ii rng s = Interaction False $ do
e <- B.parseExprIn ii rng s
d <- B.withInteractionId ii $ do
let c = B.evalInCurrent e
v <- if ignore then ignoreAbstractMode c else c
prettyA v
display_info "*Normal Form*" (show d)
return Nothing
parseAndDoAtToplevel
:: (SA.Expr -> TCM SA.Expr)
-> String
-> String
-> Interaction
parseAndDoAtToplevel cmd title s = Interaction False $ do
e <- liftIO $ parse exprParser s
display_info title =<< do
mCurrent <- stCurrentModule <$> get
case mCurrent of
Nothing -> return "Error: First load the file."
Just current -> do
r <- getVisitedModule (SA.toTopLevelModuleName current)
case r of
Nothing -> __IMPOSSIBLE__
Just mi -> do
setScope $ iInsideScope $ miInterface mi
showA =<< cmd =<< concreteToAbstract_ e
return Nothing
cmd_infer_toplevel
:: B.Rewrite
-> String
-> Interaction
cmd_infer_toplevel norm =
parseAndDoAtToplevel (B.typeInCurrent norm) "*Inferred Type*"
cmd_compute_toplevel :: Bool
-> String -> Interaction
cmd_compute_toplevel ignore =
parseAndDoAtToplevel (if ignore then ignoreAbstractMode . c else c)
"*Normal Form*"
where c = B.evalInCurrent
cmd_write_highlighting_info :: FilePath -> FilePath -> Interaction
cmd_write_highlighting_info source target = Interaction True $ do
liftIO . UTF8.writeFile target . showHighlightingInfo =<< do
ex <- liftIO $ doesFileExist source
case ex of
False -> return Nothing
True -> do
mmi <- (getVisitedModule =<< Imp.moduleName source)
`catchError`
\_ -> return Nothing
case mmi of
Nothing -> return Nothing
Just mi -> do
sourceT <- liftIO $ getModificationTime source
if sourceT <= miTimeStamp mi
then do
modFile <- stModuleToSource <$> get
return $ Just (iHighlighting $ miInterface mi, modFile)
else
return Nothing
return Nothing
cmd_goals :: FilePath
-> Interaction
cmd_goals f = Interaction True $ do
is <- do
ex <- liftIO $ doesFileExist f
case ex of
False -> return []
True -> do
mm <- (Just <$> Imp.moduleName f)
`catchError`
\_ -> return Nothing
mCurrent <- stCurrentModule <$> get
if mm == (SA.toTopLevelModuleName <$> mCurrent) then
theInteractionPoints <$> liftIO (readIORef theState)
else
return []
liftIO $ respond $ Q $ L $ List.map showNumIId is
return Nothing
tellEmacsToJumpToError :: Range -> IO ()
tellEmacsToJumpToError r = do
case rStart r of
Nothing -> return ()
Just (Pn { srcFile = Nothing }) -> return ()
Just (Pn { srcFile = Just f, posPos = p }) ->
LocIO.putStrLn $ response $
L [ A "annotation-goto"
, Q $ L [A (quote $ filePath f), A ".", A (show p)]
]
showImplicitArgs :: Bool
-> Interaction
showImplicitArgs showImpl = Interaction False $ do
opts <- commandLineOptions
setCommandLineOptions (opts { optShowImplicit = showImpl })
return Nothing
toggleImplicitArgs :: Interaction
toggleImplicitArgs = Interaction False $ do
opts <- commandLineOptions
setCommandLineOptions (opts { optShowImplicit =
not $ optShowImplicit opts })
return Nothing
errorTitle :: String
errorTitle = "*Error*"
displayErrorAndExit :: Status
-> Range -> String -> IO a
displayErrorAndExit status r s = do
display_info' errorTitle s
tellEmacsToJumpToError r
displayStatus status
exitWith (ExitFailure 1)
infoOnException m =
failOnException (displayErrorAndExit s) m `catchImpossible` \e ->
displayErrorAndExit s noRange (show e)
where
s = Status { sChecked = False
, sShowImplicitArguments = False
}