2aae0b3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Do not quit the REPL on Ctrl-C.

Now pressing Ctrl-C during REPL input is exactly the same as feeding an empty line. Pressing Ctrl-C during computation will drop you back into the REPL and it's supported for the main REPL and both provers REPLs.

commit2aae0b3a76922e15ce0a60f79d7f7a0fde205435 authorAlexander Shabalin <shabalyn.a@gmail.com> dateTue 2 Feb 2016, 21:57 (11 years ago) parent0cbea4a

2 files changed+26−9

compare with master

unifiedsplit

src/Idris/Prover.hs+23−6 src/Idris/REPL.hs+3−3

src/Idris/Prover.hs+23−6

@@ -271,6 +271,21 @@ undoElab prf env st [] = ifail "Nothing to undo"

271271undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h

272272 return (prf', env', st', hs)

273273

274+runWithInterrupt

275+ :: ElabState EState

276+ -> Idris a -- ^ run with SIGINT handler

277+ -> Idris b -- ^ run if mTry finished

278+ -> Idris b -- ^ run if mTry was interrupted

279+ -> Idris b

280+runWithInterrupt elabState mTry mSuccess mFailure = do

281+ ist <- getIState

282+ case idris_outputmode ist of

283+ RawOutput _ -> do

284+ success <- runInputT (proverSettings elabState) $

285+ handleInterrupt (return False) $

286+ withInterrupt (lift mTry >> return True)

287+ if success then mSuccess else mFailure

288+ IdeMode _ _ -> mTry >> mSuccess

274289

275290elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])

276291elabloop fn d prompt prf e prev h env

@@ -283,7 +298,7 @@ elabloop fn d prompt prf e prev h env

283298 do case h of

284299 Just history -> putHistory history

285300 Nothing -> return ()

286− l <- getInputLine (prompt ++ "> ")

301+ l <- handleInterrupt (return $ Just "") $ withInterrupt $ getInputLine (prompt ++ "> ")

287302 h' <- getHistory

288303 return (l, Just h')

289304 IdeMode _ handle ->

@@ -375,8 +390,9 @@ elabloop fn d prompt prf e prev h env

375390 Right ok ->

376391 if done then do (tm, _) <- elabStep st get_term

377392 return (tm, prf')

378− else do ok

379− elabloop fn d prompt prf' st prev' h' env'

393+ else runWithInterrupt e ok

394+ (elabloop fn d prompt prf' st prev' h' env')

395+ (elabloop fn d prompt prf e prev h' env)

380396

381397 where

382398 -- A bit of a hack: wrap the value up in a let binding, which will

@@ -401,7 +417,7 @@ ploop fn d prompt prf e h

401417 do case h of

402418 Just history -> putHistory history

403419 Nothing -> return ()

404− l <- getInputLine (prompt ++ "> ")

420+ l <- handleInterrupt (return $ Just "") $ withInterrupt $ getInputLine (prompt ++ "> ")

405421 h' <- getHistory

406422 return (l, Just h')

407423 IdeMode _ handle ->

@@ -445,8 +461,9 @@ ploop fn d prompt prf e h

445461 Right ok ->

446462 if done then do (tm, _) <- elabStep st get_term

447463 return (tm, prf')

448− else do ok

449− ploop fn d prompt prf' st h'

464+ else runWithInterrupt e ok

465+ (ploop fn d prompt prf' st h')

466+ (ploop fn d prompt prf e h')

450467

451468

452469envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

src/Idris/REPL.hs+3−3

@@ -122,13 +122,13 @@ repl orig mods efile

122122 (if colour && not isWindows

123123 then colourisePrompt theme str

124124 else str) ++ " "

125− x <- H.catch (getInputLine prompt)

126− (ctrlC (return Nothing))

125+ x <- H.catch (H.withInterrupt $ getInputLine prompt)

126+ (ctrlC (return $ Just ""))

127127 case x of

128128 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")

129129 return ()

130130 Just input -> -- H.catch

131− do ms <- H.catch (lift $ processInput input orig mods efile)

131+ do ms <- H.catch (H.withInterrupt $ lift $ processInput input orig mods efile)

132132 (ctrlC (return (Just mods)))

133133 case ms of

134134 Just mods -> let efile' = fromMaybe efile (listToMaybe mods)