@@ -0,0 +1,173 @@
1+module Idris.Output where
2+
3+import Idris.Core.TT
4+import Idris.Core.Evaluate (isDConName, isTConName, isFnName)
5+
6+import Idris.AbsSyntax
7+import Idris.Delaborate
8+import Idris.Docstrings
9+import Idris.IdeSlave
10+
11+import Util.Pretty
12+import Util.ScreenSize (getScreenWidth)
13+
14+import System.IO (stdout, Handle, hPutStrLn)
15+
16+pshow :: IState -> Err -> String
17+pshow ist err = displayDecorated (consoleDecorate ist) .
18+ renderPretty 1.0 80 .
19+ fmap (fancifyAnnots ist) $ pprintErr ist err
20+
21+ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()
22+ihWarn h fc err = do i <- getIState
23+ case idris_outputmode i of
24+ RawOutput ->
25+ do err' <- iRender . fmap (fancifyAnnots i) $
26+ text (show fc) <> colon <//> err
27+ runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'
28+ IdeSlave n ->
29+ do err' <- iRender . fmap (fancifyAnnots i) $ err
30+ let (str, spans) = displaySpans err'
31+ runIO . hPutStrLn h $
32+ convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
33+
34+iRender :: Doc a -> Idris (SimpleDoc a)
35+iRender d = do w <- getWidth
36+ ist <- getIState
37+ let ideSlave = case idris_outputmode ist of
38+ IdeSlave _ -> True
39+ _ -> False
40+ case w of
41+ InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
42+ ColsWide n -> return $
43+ if n < 1
44+ then renderPretty 1.0 1000000000 d
45+ else renderPretty 0.8 n d
46+ AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d
47+ | otherwise -> do width <- runIO getScreenWidth
48+ return $ renderPretty 0.8 width d
49+
50+ihPrintResult :: Handle -> String -> Idris ()
51+ihPrintResult h s = do i <- getIState
52+ case idris_outputmode i of
53+ RawOutput -> case s of
54+ "" -> return ()
55+ s -> runIO $ hPutStrLn h s
56+ IdeSlave n ->
57+ let good = SexpList [SymbolAtom "ok", toSExp s] in
58+ runIO $ hPutStrLn h $ convSExp "return" good n
59+
60+-- | Write a pretty-printed term to the console with semantic coloring
61+consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
62+consoleDisplayAnnotated h output = do ist <- getIState
63+ rendered <- iRender $ output
64+ runIO . hPutStrLn h .
65+ displayDecorated (consoleDecorate ist) $
66+ rendered
67+
68+
69+-- | Write pretty-printed output to IDESlave with semantic annotations
70+ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
71+ideSlaveReturnAnnotated n h out = do ist <- getIState
72+ (str, spans) <- fmap displaySpans .
73+ iRender .
74+ fmap (fancifyAnnots ist) $
75+ out
76+ let good = [SymbolAtom "ok", toSExp str, toSExp spans]
77+ runIO . hPutStrLn h $ convSExp "return" good n
78+
79+ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
80+ihPrintTermWithType h tm ty = do ist <- getIState
81+ let output = tm <+> colon <+> ty
82+ case idris_outputmode ist of
83+ RawOutput -> consoleDisplayAnnotated h output
84+ IdeSlave n -> ideSlaveReturnAnnotated n h output
85+
86+-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
87+ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
88+ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n
89+ihPrintFunTypes h bnd n overloads = do imp <- impShow
90+ ist <- getIState
91+ let output = vsep (map (uncurry (ppOverload imp)) overloads)
92+ case idris_outputmode ist of
93+ RawOutput -> consoleDisplayAnnotated h output
94+ IdeSlave n -> ideSlaveReturnAnnotated n h output
95+ where fullName n = prettyName True bnd n
96+ ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd [] tm)
97+
98+ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
99+ihRenderResult h d = do ist <- getIState
100+ case idris_outputmode ist of
101+ RawOutput -> consoleDisplayAnnotated h d
102+ IdeSlave n -> ideSlaveReturnAnnotated n h d
103+
104+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
105+fancifyAnnots ist annot@(AnnName n _ _ _) =
106+ do let ctxt = tt_ctxt ist
107+ docs = docOverview ist n
108+ ty = Just (getTy ist n)
109+ case () of
110+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty
111+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty
112+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty
113+ _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty
114+ _ | otherwise -> annot
115+ where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs
116+ docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)
117+ let o = overview (fst docs)
118+ -- TODO make width configurable
119+ out = displayS . renderPretty 1.0 50 $ renderDocstring o
120+ return (out "")
121+ getTy :: IState -> Name -> String -- fails if name not already extant!
122+ getTy ist n = let theTy = pprintPTerm (opt_showimp (idris_options ist)) [] [] $
123+ delabTy ist n
124+ in (displayS . renderPretty 1.0 50 $ theTy) ""
125+fancifyAnnots _ annot = annot
126+
127+-- | Show an error with semantic highlighting
128+ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()
129+ihRenderError h e = do ist <- getIState
130+ case idris_outputmode ist of
131+ RawOutput -> consoleDisplayAnnotated h e
132+ IdeSlave n -> do
133+ (str, spans) <- fmap displaySpans .
134+ iRender .
135+ fmap (fancifyAnnots ist) $
136+ e
137+ let good = [SymbolAtom "error", toSExp str, toSExp spans]
138+ runIO . hPutStrLn h $ convSExp "return" good n
139+
140+ihPrintError :: Handle -> String -> Idris ()
141+ihPrintError h s = do i <- getIState
142+ case idris_outputmode i of
143+ RawOutput -> case s of
144+ "" -> return ()
145+ s -> runIO $ hPutStrLn h s
146+ IdeSlave n ->
147+ let good = SexpList [SymbolAtom "error", toSExp s] in
148+ runIO . hPutStrLn h $ convSExp "return" good n
149+
150+ihputStrLn :: Handle -> String -> Idris ()
151+ihputStrLn h s = do i <- getIState
152+ case idris_outputmode i of
153+ RawOutput -> runIO $ hPutStrLn h s
154+ IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
155+
156+iputStrLn = ihputStrLn stdout
157+iPrintError = ihPrintError stdout
158+iPrintResult = ihPrintResult stdout
159+iWarn = ihWarn stdout
160+
161+ideslavePutSExp :: SExpable a => String -> a -> Idris ()
162+ideslavePutSExp cmd info = do i <- getIState
163+ case idris_outputmode i of
164+ IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
165+ _ -> return ()
166+
167+-- this needs some typing magic and more structured output towards emacs
168+iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
169+iputGoal g = do i <- getIState
170+ case idris_outputmode i of
171+ RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
172+ IdeSlave n -> runIO . putStrLn $
173+ convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n