dc7fd3b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2942 from projedi/sigint-handling

dc7fd3bNiklas Larsson11 years ago

src/Idris/Prover.hs+23−6

compare with master

unifiedsplit

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

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

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

273

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

274

289

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

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

276elabloop fn d prompt prf e prev h env

291elabloop fn d prompt prf e prev h env

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

283 do case h of

298 do case h of

284 Just history -> putHistory history

299 Just history -> putHistory history

285 Nothing -> return ()

300 Nothing -> return ()

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

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

287 h' <- getHistory

302 h' <- getHistory

288 return (l, Just h')

303 return (l, Just h')

289 IdeMode _ handle ->

304 IdeMode _ handle ->

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

375 Right ok ->

390 Right ok ->

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

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

377 return (tm, prf')

392 return (tm, prf')

378− else do ok

393+ else runWithInterrupt e ok

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

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

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

380

396

381 where

397 where

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

398 -- 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

401 do case h of

417 do case h of

402 Just history -> putHistory history

418 Just history -> putHistory history

403 Nothing -> return ()

419 Nothing -> return ()

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

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

405 h' <- getHistory

421 h' <- getHistory

406 return (l, Just h')

422 return (l, Just h')

407 IdeMode _ handle ->

423 IdeMode _ handle ->

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

445 Right ok ->

461 Right ok ->

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

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

447 return (tm, prf')

463 return (tm, prf')

448− else do ok

464+ else runWithInterrupt e ok

449− ploop fn d prompt prf' st h'

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

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

450

467

451

468

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

469envCtxt 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

122 (if colour && not isWindows

123 then colourisePrompt theme str

124 else str) ++ " "

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

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

126− (ctrlC (return Nothing))

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

127 case x of

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

129 return ()

130 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)

132 (ctrlC (return (Just mods)))

133 case ms of

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