@@ -1218,13 +1218,18 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {
12181218 historyFile = hFile
12191219 }
12201220
1221−-- invoke as if from command line
1221+-- | Invoke as if from command line. It is an error if there are unresolved totality problems.
12221222idris :: [Opt] -> IO (Maybe IState)
1223−idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit
1223+idris opts = do res <- runErrorT $ execStateT totalMain idrisInit
12241224 case res of
12251225 Left err -> do putStrLn $ pshow idrisInit err
12261226 return Nothing
12271227 Right ist -> return (Just ist)
1228+ where totalMain = do idrisMain opts
1229+ ist <- getIState
1230+ case idris_totcheckfail ist of
1231+ ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg
1232+ [] -> return ()
12281233
12291234
12301235loadInputs :: Handle -> [FilePath] -> Idris ()