git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/Output.hs
383 lines 16 kB history raw
1{-|
2Module : Idris.Output
3Description : Utilities to display Idris' internals and other informtation to the user.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
11module Idris.Output where
13import Idris.AbsSyntax
14import Idris.Colours (hEndColourise, hStartColourise)
15import Idris.Core.Evaluate (isDConName, isFnName, isTConName, normaliseAll)
16import Idris.Core.TT
17import Idris.Delaborate
18import Idris.Docstrings
19import Idris.IdeMode
20import Idris.Options
22import Util.Pretty
23import Util.ScreenSize (getScreenWidth)
24import Util.System (isATTY)
26import Prelude hiding ((<$>))
28import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
29import Data.Char (isAlpha)
30import Data.List (intersperse, nub)
31import Data.Maybe (fromMaybe)
32import System.Console.Haskeline.MonadException (MonadException(controlIO),
33 RunIO(RunIO))
34import System.FilePath (replaceExtension)
35import System.IO (Handle, hPutStr, hPutStrLn, stdout)
37instance MonadException m => MonadException (ExceptT Err m) where
38 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
39 run' = RunIO (fmap ExceptT . run . runExceptT)
40 in fmap runExceptT $ f run'
42pshow :: IState -> Err -> String
43pshow ist err = displayDecorated (consoleDecorate ist) .
44 renderPretty 1.0 80 .
45 fmap (fancifyAnnots ist True) $ pprintErr ist err
47iWarn :: FC -> Doc OutputAnnotation -> Idris ()
48iWarn fc err =
49 do i <- getIState
50 case idris_outputmode i of
51 RawOutput h ->
52 do err' <- iRender . fmap (fancifyAnnots i True) $
53 case fc of
54 FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err
55 _ -> err
56 hWriteDoc h i err'
57 IdeMode n h ->
58 do err' <- iRender . fmap (fancifyAnnots i True) $ err
59 let (str, spans) = displaySpans err'
60 runIO . hPutStrLn h $
61 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
63iRender :: Doc a -> Idris (SimpleDoc a)
64iRender d = do w <- getWidth
65 ist <- getIState
66 let ideMode = case idris_outputmode ist of
67 IdeMode _ _ -> True
68 _ -> False
69 tty <- runIO isATTY
70 case w of
71 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
72 ColsWide n -> return $
73 if n < 1
74 then renderPretty 1.0 1000000000 d
75 else renderPretty 0.8 n d
76 AutomaticWidth | ideMode || not tty -> return $ renderPretty 1.0 80 d
77 | otherwise -> do width <- runIO getScreenWidth
78 return $ renderPretty 0.8 width d
80hWriteDoc :: Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()
81hWriteDoc h ist rendered =
82 do runIO $ displayDecoratedA
83 (hPutStr h)
84 (maybe (return ()) (hStartColourise h))
85 (maybe (return ()) (hEndColourise h))
86 (fmap (annotationColour ist) rendered)
87 runIO $ hPutStr h "\n" -- newline translation on the output
88 -- stream should take care of this for
89 -- Windows
91-- | Write a pretty-printed term to the console with semantic coloring
92consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
93consoleDisplayAnnotated h output =
94 do ist <- getIState
95 rendered <- iRender output
96 hWriteDoc h ist rendered
98iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
99iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)
101-- | Pretty-print a collection of overloadings to REPL or IDEMode - corresponds to :t name
102iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
103iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n
104iPrintFunTypes bnd n overloads = do ist <- getIState
105 let ppo = ppOptionIst ist
106 let infixes = idris_infixes ist
107 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
108 iRenderResult output
109 where fullName ppo n | length overloads > 1 = prettyName True True bnd n
110 | otherwise = prettyName True (ppopt_impl ppo) bnd n
111 ppOverload ppo infixes n tm =
112 fullName ppo n <+> colon <+> align tm
114iRenderOutput :: Doc OutputAnnotation -> Idris ()
115iRenderOutput doc =
116 do i <- getIState
117 case idris_outputmode i of
118 RawOutput h -> do out <- iRender doc
119 hWriteDoc h i out
121 IdeMode n h ->
122 do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i True) $ doc
123 let out = [toSExp str, toSExp spans]
124 runIO . hPutStrLn h $ convSExp "write-decorated" out n
126iRenderResult :: Doc OutputAnnotation -> Idris ()
127iRenderResult d = do ist <- getIState
128 case idris_outputmode ist of
129 RawOutput h -> consoleDisplayAnnotated h d
130 IdeMode n h -> ideModeReturnAnnotated n h d
132ideModeReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
133ideModeReturnWithStatus status n h out = do
134 ist <- getIState
135 (str, spans) <- fmap displaySpans .
136 iRender .
137 fmap (fancifyAnnots ist True) $
138 out
139 let good = [SymbolAtom status, toSExp str, toSExp spans]
140 runIO . hPutStrLn h $ convSExp "return" good n
143-- | Write pretty-printed output to IDEMode with semantic annotations
144ideModeReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
145ideModeReturnAnnotated = ideModeReturnWithStatus "ok"
147-- | Show an error with semantic highlighting
148iRenderError :: Doc OutputAnnotation -> Idris ()
149iRenderError e = do ist <- getIState
150 case idris_outputmode ist of
151 RawOutput h -> consoleDisplayAnnotated h e
152 IdeMode n h -> ideModeReturnWithStatus "error" n h e
154iPrintWithStatus :: String -> String -> Idris ()
155iPrintWithStatus status s = do
156 i <- getIState
157 case idris_outputmode i of
158 RawOutput h -> case s of
159 "" -> return ()
160 s -> runIO $ hPutStrLn h s
161 IdeMode n h ->
162 let good = SexpList [SymbolAtom status, toSExp s] in
163 runIO $ hPutStrLn h $ convSExp "return" good n
166iPrintResult :: String -> Idris ()
167iPrintResult = iPrintWithStatus "ok"
169iPrintError :: String -> Idris ()
170iPrintError = iPrintWithStatus "error"
172iputStrLn :: String -> Idris ()
173iputStrLn s = do i <- getIState
174 case idris_outputmode i of
175 RawOutput h -> runIO $ hPutStrLn h s
176 IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n
178iputStr :: String -> Idris ()
179iputStr s = do i <- getIState
180 case idris_outputmode i of
181 RawOutput h -> runIO $ hPutStr h s
182 IdeMode n h -> runIO . hPutStr h $ convSExp "write-string" s n
184idemodePutSExp :: SExpable a => String -> a -> Idris ()
185idemodePutSExp cmd info = do i <- getIState
186 case idris_outputmode i of
187 IdeMode n h ->
188 runIO . hPutStrLn h $
189 convSExp cmd info n
190 _ -> return ()
192-- TODO: send structured output similar to the metavariable list
193iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
194iputGoal g = do i <- getIState
195 case idris_outputmode i of
196 RawOutput h -> hWriteDoc h i g
197 IdeMode n h ->
198 let (str, spans) = displaySpans . fmap (fancifyAnnots i True) $ g
199 goal = [toSExp str, toSExp spans]
200 in runIO . hPutStrLn h $ convSExp "write-goal" goal n
202-- | Warn about totality problems without failing to compile
203warnTotality :: Idris ()
204warnTotality = do ist <- getIState
205 mapM_ (warn ist) (nub (idris_totcheckfail ist))
206 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))
209printUndefinedNames :: [Name] -> Doc OutputAnnotation
210printUndefinedNames ns = text "Undefined " <> names <> text "."
211 where names = encloseSep empty empty (char ',') $ map ppName ns
212 ppName = prettyName True True []
215prettyDocumentedIst :: IState
216 -> (Name, PTerm, Maybe (Docstring DocTerm))
217 -> Doc OutputAnnotation
218prettyDocumentedIst ist (name, ty, docs) =
219 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
220 fromMaybe empty (fmap (\d -> renderDocstring (renderDocTerm ppTm norm) d <> line) docs)
221 where ppTm = pprintDelab ist
222 norm = normaliseAll (tt_ctxt ist) []
224sendParserHighlighting :: Idris ()
225sendParserHighlighting =
226 do ist <- getIState
227 let hs = map unwrap . nub . map wrap $ idris_parserHighlights ist
228 sendHighlighting hs
229 ist <- getIState
230 putIState ist {idris_parserHighlights = []}
231 where wrap (fc, a) = (FC' fc, a)
232 unwrap (fc', a) = (unwrapFC fc', a)
234sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()
235sendHighlighting highlights =
236 do ist <- getIState
237 case idris_outputmode ist of
238 RawOutput _ -> updateIState $
239 \ist -> ist { idris_highlightedRegions =
240 highlights ++ idris_highlightedRegions ist }
241 IdeMode n h ->
242 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)
243 | (fc, annot) <- highlights, fullFC fc
244 ]
245 in case fancier of
246 [] -> return ()
247 _ -> runIO . hPutStrLn h $
248 convSExp "output"
249 (SymbolAtom "ok",
250 (SymbolAtom "highlight-source", fancier)) n
252 where fullFC (FC _ _ _) = True
253 fullFC _ = False
255-- | Write the highlighting information to a file, for use in external tools
256-- or in editors that don't support the IDE protocol
257writeHighlights :: FilePath -> Idris ()
258writeHighlights f =
259 do ist <- getIState
260 let hs = reverse $ idris_highlightedRegions ist
261 let hfile = replaceExtension f "idh"
262 let annots = toSExp [ (fc, fancifyAnnots ist False annot)
263 | (fc@(FC _ _ _), annot) <- hs
264 ]
265 runIO $ writeFile hfile $ sExpToString annots
267clearHighlights :: Idris ()
268clearHighlights = updateIState $ \ist -> ist { idris_highlightedRegions = [] }
270renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
271renderExternal fmt width doc
272 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."
273 | otherwise =
274 do ist <- getIState
275 return . wrap fmt .
276 displayDecorated (decorate fmt) .
277 renderPretty 1.0 width .
278 fmap (fancifyAnnots ist True) $
279 doc
280 where
281 decorate _ (AnnFC _) = id
283 decorate HTMLOutput (AnnName _ (Just TypeOutput) d _) =
284 tag "idris-type" d
285 decorate HTMLOutput (AnnName _ (Just FunOutput) d _) =
286 tag "idris-function" d
287 decorate HTMLOutput (AnnName _ (Just DataOutput) d _) =
288 tag "idris-data" d
289 decorate HTMLOutput (AnnName _ (Just MetavarOutput) d _) =
290 tag "idris-metavar" d
291 decorate HTMLOutput (AnnName _ (Just PostulateOutput) d _) =
292 tag "idris-postulate" d
293 decorate HTMLOutput (AnnName _ _ _ _) = id
294 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
295 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
296 decorate HTMLOutput (AnnConst c) =
297 tag (if constIsType c then "idris-type" else "idris-data")
298 (Just $ constDocs c)
299 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
300 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
301 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
302 decorate HTMLOutput (AnnTextFmt fmt) =
303 case fmt of
304 BoldText -> mkTag "strong"
305 ItalicText -> mkTag "em"
306 UnderlineText -> tag "idris-underlined" Nothing
307 where mkTag t x = "<"++t++">"++x++"</"++t++">"
308 decorate HTMLOutput (AnnTerm _ _) = id
309 decorate HTMLOutput (AnnSearchResult _) = id
310 decorate HTMLOutput (AnnErr _) = id
311 decorate HTMLOutput (AnnNamespace _ _) = id
312 decorate HTMLOutput (AnnLink url) =
313 \txt -> "<a href=\"" ++ url ++ "\">" ++ txt ++ "</a>"
314 decorate HTMLOutput AnnQuasiquote = id
315 decorate HTMLOutput AnnAntiquote = id
317 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
318 latex "IdrisType"
319 decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =
320 latex "IdrisFunction"
321 decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =
322 latex "IdrisData"
323 decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =
324 latex "IdrisMetavar"
325 decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =
326 latex "IdrisPostulate"
327 decorate LaTeXOutput (AnnName _ _ _ _) = id
328 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
329 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
330 decorate LaTeXOutput (AnnConst c) =
331 latex $ if constIsType c then "IdrisType" else "IdrisData"
332 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
333 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
334 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"
335 decorate LaTeXOutput (AnnTextFmt fmt) =
336 case fmt of
337 BoldText -> latex "textbf"
338 ItalicText -> latex "emph"
339 UnderlineText -> latex "underline"
340 decorate LaTeXOutput (AnnTerm _ _) = id
341 decorate LaTeXOutput (AnnSearchResult _) = id
342 decorate LaTeXOutput (AnnErr _) = id
343 decorate LaTeXOutput (AnnNamespace _ _) = id
344 decorate LaTeXOutput (AnnLink url) = (++ "(\\url{" ++ url ++ "})")
345 decorate LaTeXOutput AnnQuasiquote = id
346 decorate LaTeXOutput AnnAntiquote = id
348 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"
349 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs
351 latex cmd str = "\\"++cmd++"{"++str++"}"
353 wrap HTMLOutput str =
354 "<!doctype html><html><head><style>" ++ css ++ "</style></head>" ++
355 "<body><!-- START CODE --><pre>" ++ str ++ "</pre><!-- END CODE --></body></html>"
356 where css = concat . intersperse "\n" $
357 [".idris-data { color: red; } ",
358 ".idris-type { color: blue; }",
359 ".idris-function {color: green; }",
360 ".idris-keyword { font-weight: bold; }",
361 ".idris-bound { color: purple; }",
362 ".idris-implicit { font-style: italic; }",
363 ".idris-underlined { text-decoration: underline; }"]
364 wrap LaTeXOutput str =
365 concat . intersperse "\n" $
366 ["\\documentclass{article}",
367 "\\usepackage{fancyvrb}",
368 "\\usepackage[usenames]{xcolor}"] ++
369 map (\(cmd, color) ->
370 "\\newcommand{\\"++ cmd ++
371 "}[1]{\\textcolor{"++ color ++"}{#1}}")
372 [("IdrisData", "red"), ("IdrisType", "blue"),
373 ("IdrisBound", "magenta"), ("IdrisFunction", "green")] ++
374 ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",
375 "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",
376 "\n",
377 "\\begin{document}",
378 "% START CODE",
379 "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",
380 str,
381 "\\end{Verbatim}",
382 "% END CODE",
383 "\\end{document}"]