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