git.iko.soy/Idris-dev
on b0cb4e2 help sign in
Idris-dev/src/Idris/Output.hs
156 lines 6.8 kB history raw
1module Idris.Output where
3import Idris.Core.TT
4import Idris.Core.Evaluate (isDConName, isTConName, isFnName)
6import Idris.AbsSyntax
7import Idris.Delaborate
8import Idris.Docstrings
9import Idris.IdeSlave
11import Util.Pretty
12import Util.ScreenSize (getScreenWidth)
14import Debug.Trace
16import System.IO (stdout, Handle, hPutStrLn)
18import Data.Char (isAlpha)
19import Data.List (nub)
20import Data.Maybe (fromMaybe)
22pshow :: IState -> Err -> String
23pshow ist err = displayDecorated (consoleDecorate ist) .
24 renderPretty 1.0 80 .
25 fmap (fancifyAnnots ist) $ pprintErr ist err
27ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()
28ihWarn h fc err = do i <- getIState
29 case idris_outputmode i of
30 RawOutput ->
31 do err' <- iRender . fmap (fancifyAnnots i) $
32 if fc_fname fc /= ""
33 then text (show fc) <> colon <//> err
34 else err
35 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'
36 IdeSlave n ->
37 do err' <- iRender . fmap (fancifyAnnots i) $ err
38 let (str, spans) = displaySpans err'
39 runIO . hPutStrLn h $
40 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
42iRender :: Doc a -> Idris (SimpleDoc a)
43iRender d = do w <- getWidth
44 ist <- getIState
45 let ideSlave = case idris_outputmode ist of
46 IdeSlave _ -> True
47 _ -> False
48 case w of
49 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
50 ColsWide n -> return $
51 if n < 1
52 then renderPretty 1.0 1000000000 d
53 else renderPretty 0.8 n d
54 AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d
55 | otherwise -> do width <- runIO getScreenWidth
56 return $ renderPretty 0.8 width d
58-- | Write a pretty-printed term to the console with semantic coloring
59consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
60consoleDisplayAnnotated h output = do ist <- getIState
61 rendered <- iRender $ output
62 runIO . hPutStrLn h .
63 displayDecorated (consoleDecorate ist) $
64 rendered
66ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
67ihPrintTermWithType h tm ty = ihRenderResult h (tm <+> colon <+> align ty)
69-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
70ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
71ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n
72ihPrintFunTypes h bnd n overloads = do ist <- getIState
73 let ppo = ppOptionIst ist
74 let infixes = idris_infixes ist
75 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
76 ihRenderResult h output
77 where fullName n = prettyName True True bnd n
78 ppOverload ppo infixes n tm =
79 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)
81ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
82ihRenderResult h d = do ist <- getIState
83 case idris_outputmode ist of
84 RawOutput -> consoleDisplayAnnotated h d
85 IdeSlave n -> ideSlaveReturnAnnotated n h d
87ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
88ideSlaveReturnWithStatus status n h out = do
89 ist <- getIState
90 (str, spans) <- fmap displaySpans .
91 iRender .
92 fmap (fancifyAnnots ist) $
93 out
94 let good = [SymbolAtom status, toSExp str, toSExp spans]
95 runIO . hPutStrLn h $ convSExp "return" good n
98-- | Write pretty-printed output to IDESlave with semantic annotations
99ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
100ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"
102-- | Show an error with semantic highlighting
103ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()
104ihRenderError h e = do ist <- getIState
105 case idris_outputmode ist of
106 RawOutput -> consoleDisplayAnnotated h e
107 IdeSlave n -> ideSlaveReturnWithStatus "error" n h e
109ihPrintWithStatus :: String -> Handle -> String -> Idris ()
110ihPrintWithStatus status h s = do
111 i <- getIState
112 case idris_outputmode i of
113 RawOutput -> case s of
114 "" -> return ()
115 s -> runIO $ hPutStrLn h s
116 IdeSlave n ->
117 let good = SexpList [SymbolAtom status, toSExp s] in
118 runIO $ hPutStrLn h $ convSExp "return" good n
121ihPrintResult :: Handle -> String -> Idris ()
122ihPrintResult = ihPrintWithStatus "ok"
124ihPrintError :: Handle -> String -> Idris ()
125ihPrintError = ihPrintWithStatus "error"
127ihputStrLn :: Handle -> String -> Idris ()
128ihputStrLn h s = do i <- getIState
129 case idris_outputmode i of
130 RawOutput -> runIO $ hPutStrLn h s
131 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
133iputStrLn = ihputStrLn stdout
134iPrintError = ihPrintError stdout
135iPrintResult = ihPrintResult stdout
136iWarn = ihWarn stdout
138ideslavePutSExp :: SExpable a => String -> a -> Idris ()
139ideslavePutSExp cmd info = do i <- getIState
140 case idris_outputmode i of
141 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
142 _ -> return ()
144-- this needs some typing magic and more structured output towards emacs
145iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
146iputGoal g = do i <- getIState
147 case idris_outputmode i of
148 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
149 IdeSlave n -> runIO . putStrLn $
150 convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n
152-- | Warn about totality problems without failing to compile
153warnTotality :: Idris ()
154warnTotality = do ist <- getIState
155 mapM_ (warn ist) (nub (idris_totcheckfail ist))
156 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))