@@ -87,9 +87,11 @@ repl orig stvar mods
8787 lift $ runIO $ swapMVar stvar i -- update shared state
8888 let colour = idris_colourRepl i
8989 let theme = idris_colourTheme i
90+ let mvs = idris_metavars i
9091 let prompt = if quiet
9192 then ""
92− else let str = mkPrompt mods ++ ">" in
93+ else showMVs colour theme mvs ++
94+ let str = mkPrompt mods ++ ">" in
9395 (if colour then colourisePrompt theme str else str) ++ " "
9496 x <- getInputLine prompt
9597 case x of
@@ -106,6 +108,21 @@ repl orig stvar mods
106108 ctrlC e = do lift $ iputStrLn (show e)
107109 repl orig stvar mods
108110
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+
109126-- | Run the REPL server
110127startServer :: IState -> MVar IState -> [FilePath] -> Idris ()
111128startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop