git.iko.soy/Idris-dev
on master help sign in
List metavariables at REPL
3e47b49Edwin Brady
src/Idris/REPL.hs+18−1
compare with master
unifiedsplit
@@ -87,9 +87,11 @@ repl orig stvar mods
87 lift $ runIO $ swapMVar stvar i -- update shared state
87 lift $ runIO $ swapMVar stvar i -- update shared state
88 let colour = idris_colourRepl i
88 let colour = idris_colourRepl i
89 let theme = idris_colourTheme i
89 let theme = idris_colourTheme i
90+ let mvs = idris_metavars i
90 let prompt = if quiet
91 let prompt = if quiet
91 then ""
92 then ""
93+ else showMVs colour theme mvs ++
92− else let str = mkPrompt mods ++ ">" in
94+ let str = mkPrompt mods ++ ">" in
93 (if colour then colourisePrompt theme str else str) ++ " "
95 (if colour then colourisePrompt theme str else str) ++ " "
94 x <- getInputLine prompt
96 x <- getInputLine prompt
95 case x of
97 case x of
@@ -106,6 +108,21 @@ repl orig stvar mods
106 ctrlC e = do lift $ iputStrLn (show e)
108 ctrlC e = do lift $ iputStrLn (show e)
107 repl orig stvar mods
109 repl orig stvar mods
108
110
111+ showMVs c thm [] = ""
112+ showMVs c thm ms = "Metavariables: " ++
113+ show' 4 c thm (map fst ms) ++ "\n"
114+
115+ show' 0 c thm ms = let l = length ms in
116+ "... ( + " ++ show l
117+ ++ " other"
118+ ++ if l == 1 then ")" else "s)"
119+ show' n c thm [m] = showM c thm m
120+ show' n c thm (m : ms) = showM c thm m ++ ", " ++
121+ show' (n - 1) c thm ms
122+
123+ showM c thm n = if c then colouriseFun thm (show n)
124+ else show n
125+
109-- | Run the REPL server
126-- | Run the REPL server
110startServer :: IState -> MVar IState -> [FilePath] -> Idris ()
127startServer :: IState -> MVar IState -> [FilePath] -> Idris ()
111startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop
128startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop