9e8930d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2857 from LeifW/watch_files_for_changes

9e8930dEdwin Brady11 years ago

idris.cabal+2

compare with master

unifiedsplit

@@ -977,6 +977,8 @@ Library

977 , vector-binary-instances < 0.3

978 , zip-archive > 0.2.3.5 && < 0.2.4

979 , safe

980+ , fsnotify < 2.2

981+ , async < 2.1

980 -- zlib >= 0.6.1 is broken with GHC < 7.10.3

982 -- zlib >= 0.6.1 is broken with GHC < 7.10.3

981 if impl(ghc < 7.10.3)

983 if impl(ghc < 7.10.3)

982 build-depends: zlib < 0.6.1

984 build-depends: zlib < 0.6.1

src/IRTS/System.hs+3−7

@@ -21,10 +21,7 @@ getCC :: IO String

21getCC = fromMaybe "gcc" <$> environment "IDRIS_CC"

23getEnvFlags :: IO [String]

24−getEnvFlags = do flags <- environment "IDRIS_CFLAGS"

24+getEnvFlags = maybe [] (splitOn " ") <$> environment "IDRIS_CFLAGS"

25− case flags of

26− Nothing -> return $ []

27− Just s -> return $ splitOn " " s

29mvnCommand :: String

26mvnCommand :: String

30#ifdef mingw32_HOST_OS

27#ifdef mingw32_HOST_OS

@@ -37,9 +34,8 @@ getMvn :: IO String

37getMvn = fromMaybe mvnCommand <$> environment "IDRIS_MVN"

34getMvn = fromMaybe mvnCommand <$> environment "IDRIS_MVN"

39environment :: String -> IO (Maybe String)

36environment :: String -> IO (Maybe String)

40−environment x = catchIO (do e <- getEnv x

37+environment x = catchIO (Just <$> getEnv x)

41− return (Just e))

42− (\_ -> return Nothing)

38+ (\_ -> return Nothing)

44getTargetDir :: IO String

40getTargetDir :: IO String

45getTargetDir = environment "TARGET" >>= maybe getDataDir return

41getTargetDir = environment "TARGET" >>= maybe getDataDir return

src/Idris/AbsSyntaxTree.hs+1

@@ -393,6 +393,7 @@ data Command = Quit

393 | DocStr (Either Name Const) HowMuchDocs

394 | TotCheck Name

395 | Reload

396+ | Watch

396 | Load FilePath (Maybe Int) -- up to maximum line number

397 | Load FilePath (Maybe Int) -- up to maximum line number

397 | ChangeDirectory FilePath

398 | ChangeDirectory FilePath

398 | ModImport String

399 | ModImport String

src/Idris/ProofSearch.hs+1−2

@@ -478,8 +478,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist

478 return (num + 1)

479 _ -> return 0

480

481− solven 0 = return ()

481+ solven n = replicateM_ n solve

482− solven n = do solve; solven (n - 1)

483

482

484 resolve n depth

483 resolve n depth

485 | depth == 0 = fail $ "Can't resolve type class"

484 | depth == 0 = fail $ "Can't resolve type class"

src/Idris/REPL.hs+46−24

@@ -94,6 +94,10 @@ import Data.Word (Word)

94import Data.Either (partitionEithers)

95import Control.DeepSeq

97+import Control.Concurrent.Async (race)

98+import System.FSNotify (withManager, watchDir)

99+import System.FSNotify.Devel (allEvents, doAllEvents)

100+

97import Numeric ( readHex )

101import Numeric ( readHex )

102

99import Debug.Trace

103import Debug.Trace

@@ -126,10 +130,8 @@ repl orig mods efile

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

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

127 (ctrlC (return (Just mods)))

131 (ctrlC (return (Just mods)))

128 case ms of

132 case ms of

129− Just mods -> let efile' = case mods of

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

130− [] -> efile

131− (e:_) -> e in

132− repl orig mods efile'

134+ in repl orig mods efile'

133 Nothing -> return ()

135 Nothing -> return ()

134-- ctrlC)

136-- ctrlC)

135-- ctrlC

137-- ctrlC

@@ -154,15 +156,13 @@ repl orig mods efile

154

156

155-- | Run the REPL server

157-- | Run the REPL server

156startServer :: PortID -> IState -> [FilePath] -> Idris ()

158startServer :: PortID -> IState -> [FilePath] -> Idris ()

157−startServer port orig fn_in = do tid <- runIO $ forkOS (serverLoop port)

159+startServer port orig fn_in = do tid <- runIO $ forkIO (serverLoop port)

158 return ()

160 return ()

159 where serverLoop port = withSocketsDo $

161 where serverLoop port = withSocketsDo $

160 do sock <- listenOnLocalhost port

162 do sock <- listenOnLocalhost port

161 loop fn orig { idris_colourRepl = False } sock

163 loop fn orig { idris_colourRepl = False } sock

162

164

163− fn = case fn_in of

165+ fn = fromMaybe "" (listToMaybe fn_in)

164− (f:_) -> f

165− _ -> ""

166

167 loop fn ist sock

168 = do (h,_,_) <- accept sock

@@ -276,9 +276,7 @@ idemode h orig mods

276 i <- getIState

277 putIState $ i { idris_outputmode = (IdeMode id h) }

278 idrisCatch -- to report correct id back!

279− (do let fn = case mods of

279+ (do let fn = fromMaybe "" (listToMaybe mods)

280− (f:_) -> f

281− _ -> ""

282 case IdeMode.sexpToCommand sexp of

280 case IdeMode.sexpToCommand sexp of

283 Just cmd -> runIdeModeCommand h id orig fn mods cmd

281 Just cmd -> runIdeModeCommand h id orig fn mods cmd

284 Nothing -> iPrintError "did not understand" )

282 Nothing -> iPrintError "did not understand" )

@@ -677,30 +675,54 @@ lit f = case splitExtension f of

677 (_, ".lidr") -> True

675 (_, ".lidr") -> True

678 _ -> False

676 _ -> False

679

677

678+reload :: IState -> [FilePath] -> Idris (Maybe [FilePath])

679+reload orig inputs = do

680+ i <- getIState

681+ -- The $!! here prevents a space leak on reloading.

682+ -- This isn't a solution - but it's a temporary stopgap.

683+ -- See issue #2386

684+ putIState $!! orig { idris_options = idris_options i

685+ , idris_colourTheme = idris_colourTheme i

686+ , imported = imported i

687+ }

688+ clearErr

689+ fmap Just $ loadInputs inputs Nothing

690+

691+watch :: IState -> [FilePath] -> Idris (Maybe [FilePath])

692+watch orig inputs = do

693+ let inputSet = S.fromList inputs

694+ let dirs = nub $ map takeDirectory inputs

695+ resp <- runIO $ do

696+ signal <- newEmptyMVar

697+ withManager $ \mgr -> do

698+ forM_ dirs $ \dir ->

699+ watchDir mgr dir (allEvents $ flip S.member inputSet) (doAllEvents $ putMVar signal)

700+ race getLine (takeMVar signal)

701+ case resp of

702+ Left _ -> return (Just inputs) -- canceled, so nop

703+ Right _ -> reload orig inputs >> watch orig inputs

704+

680processInput :: String ->

705processInput :: String ->

681 IState -> [FilePath] -> FilePath -> Idris (Maybe [FilePath])

706 IState -> [FilePath] -> FilePath -> Idris (Maybe [FilePath])

682processInput cmd orig inputs efile

707processInput cmd orig inputs efile

683 = do i <- getIState

708 = do i <- getIState

684 let opts = idris_options i

709 let opts = idris_options i

685 let quiet = opt_quiet opts

710 let quiet = opt_quiet opts

686− let fn = case inputs of

711+ let fn = fromMaybe "" (listToMaybe inputs)

687− (f:_) -> f

688− _ -> ""

689 c <- colourise

712 c <- colourise

690 case parseCmd i "(input)" cmd of

713 case parseCmd i "(input)" cmd of

691 Failure err -> do iputStrLn $ show (fixColour c err)

714 Failure err -> do iputStrLn $ show (fixColour c err)

692 return (Just inputs)

715 return (Just inputs)

693 Success (Right Reload) ->

716 Success (Right Reload) ->

694− -- The $!! here prevents a space leak on reloading.

717+ reload orig inputs

695− -- This isn't a solution - but it's a temporary stopgap.

718+ Success (Right Watch) ->

696− -- See issue #2386

719+ if null inputs then

697− do putIState $!! orig { idris_options = idris_options i

720+ do iputStrLn "No loaded files to watch."

698− , idris_colourTheme = idris_colourTheme i

699− , imported = imported i

700− }

701− clearErr

702− mods <- loadInputs inputs Nothing

703− return (Just mods)

721+ return (Just inputs)

722+ else

723+ do iputStrLn efile

724+ iputStrLn $ "Watching for .idr changes in " ++ show inputs ++ ", press enter to cancel."

725+ watch orig inputs

704 Success (Right (Load f toline)) ->

726 Success (Right (Load f toline)) ->

705 -- The $!! here prevents a space leak on reloading.

727 -- The $!! here prevents a space leak on reloading.

706 -- This isn't a solution - but it's a temporary stopgap.

728 -- This isn't a solution - but it's a temporary stopgap.

src/Idris/REPLParser.hs+2−1

@@ -67,6 +67,7 @@ parserCommandsForHelp =

67 , namespaceArgCmd ["browse"] Browse "List the contents of some namespace"

68 , nameArgCmd ["total"] TotCheck "Check the totality of a name"

69 , noArgCmd ["r", "reload"] Reload "Reload current file"

70+ , noArgCmd ["w", "watch"] Watch "Watch the current file for changes"

70 , (["l", "load"], FileArg, "Load a new file"

71 , (["l", "load"], FileArg, "Load a new file"

71 , strArg (\f -> Load f Nothing))

72 , strArg (\f -> Load f Nothing))

72 , (["cd"], FileArg, "Change working directory"

73 , (["cd"], FileArg, "Change working directory"

@@ -98,7 +99,7 @@ parserCommandsForHelp =

98 , (["consolewidth"], ConsoleWidthArg, "Set the width of the console", cmd_consolewidth)

99 , (["consolewidth"], ConsoleWidthArg, "Set the width of the console", cmd_consolewidth)

99 , (["printerdepth"], OptionalArg NumberArg, "Set the maximum pretty-printer depth (no arg for infinite)", cmd_printdepth)

100 , (["printerdepth"], OptionalArg NumberArg, "Set the maximum pretty-printer depth (no arg for infinite)", cmd_printdepth)

100 , noArgCmd ["q", "quit"] Quit "Exit the Idris system"

101 , noArgCmd ["q", "quit"] Quit "Exit the Idris system"

101− , noArgCmd ["w", "warranty"] Warranty "Displays warranty information"

102+ , noArgCmd ["warranty"] Warranty "Displays warranty information"

102 , (["let"], ManyArgs DeclArg

103 , (["let"], ManyArgs DeclArg

103 , "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"

104 , "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"

104 , cmd_let)

105 , cmd_let)