f0a5442 · Idris-dev · git.iko.soy

idris.cabal+1

compare with master

unifiedsplit

@@ -476,6 +476,7 @@ Library

476 , Idris.IdeSlave

477 , Idris.Imports

478 , Idris.Inliner

479+ , Idris.Output

479 , Idris.Parser

480 , Idris.Parser

480 , Idris.ParseHelpers

481 , Idris.ParseHelpers

481 , Idris.ParseOps

482 , Idris.ParseOps

src/Idris/AbsSyntax.hs−140

@@ -511,156 +511,16 @@ renderWidth = do iw <- getWidth

511 AutomaticWidth -> runIO getScreenWidth

512

513

514−iRender :: Doc a -> Idris (SimpleDoc a)

515−iRender d = do w <- getWidth

516− ist <- getIState

517− let ideSlave = case idris_outputmode ist of

518− IdeSlave _ -> True

519− _ -> False

520− case w of

521− InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

522− ColsWide n -> return $

523− if n < 1

524− then renderPretty 1.0 1000000000 d

525− else renderPretty 0.8 n d

526− AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d

527− | otherwise -> do width <- runIO getScreenWidth

528− return $ renderPretty 0.8 width d

529−

530−ihPrintResult :: Handle -> String -> Idris ()

531−ihPrintResult h s = do i <- getIState

532− case idris_outputmode i of

533− RawOutput -> case s of

534− "" -> return ()

535− s -> runIO $ hPutStrLn h s

536− IdeSlave n ->

537− let good = SexpList [SymbolAtom "ok", toSExp s] in

538− runIO $ hPutStrLn h $ convSExp "return" good n

539−

540−-- | Write a pretty-printed term to the console with semantic coloring

541−consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

542−consoleDisplayAnnotated h output = do ist <- getIState

543− rendered <- iRender $ output

544− runIO . hPutStrLn h .

545− displayDecorated (consoleDecorate ist) $

546− rendered

547−

548−

549−-- | Write pretty-printed output to IDESlave with semantic annotations

550−ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

551−ideSlaveReturnAnnotated n h out = do ist <- getIState

552− (str, spans) <- fmap displaySpans .

553− iRender .

554− fmap (fancifyAnnots ist) $

555− out

556− let good = [SymbolAtom "ok", toSExp str, toSExp spans]

557− runIO . hPutStrLn h $ convSExp "return" good n

558−

559−ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

560−ihPrintTermWithType h tm ty = do ist <- getIState

561− let output = tm <+> colon <+> ty

562− case idris_outputmode ist of

563− RawOutput -> consoleDisplayAnnotated h output

564− IdeSlave n -> ideSlaveReturnAnnotated n h output

565−

566−-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

567−ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

568−ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

569−ihPrintFunTypes h bnd n overloads = do imp <- impShow

570− ist <- getIState

571− let output = vsep (map (uncurry (ppOverload imp)) overloads)

572− case idris_outputmode ist of

573− RawOutput -> consoleDisplayAnnotated h output

574− IdeSlave n -> ideSlaveReturnAnnotated n h output

575− where fullName n = prettyName True bnd n

576− ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd [] tm)

577−

578−ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

579−ihRenderResult h d = do ist <- getIState

580− case idris_outputmode ist of

581− RawOutput -> consoleDisplayAnnotated h d

582− IdeSlave n -> ideSlaveReturnAnnotated n h d

583−

584−fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

585−fancifyAnnots ist annot@(AnnName n _ _) =

586− do let ctxt = tt_ctxt ist

587− case () of

588− _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing

589− _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing

590− _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing

591− _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) Nothing

592− _ | otherwise -> annot

593−fancifyAnnots _ annot = annot

594

514

595type1Doc :: Doc OutputAnnotation

515type1Doc :: Doc OutputAnnotation

596type1Doc = (annotate AnnConstType $ text "Type 1")

516type1Doc = (annotate AnnConstType $ text "Type 1")

597

517

598−-- | Show an error with semantic highlighting

599−ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

600−ihRenderError h e = do ist <- getIState

601− case idris_outputmode ist of

602− RawOutput -> consoleDisplayAnnotated h e

603− IdeSlave n -> do

604− (str, spans) <- fmap displaySpans .

605− iRender .

606− fmap (fancifyAnnots ist) $

607− e

608− let good = [SymbolAtom "error", toSExp str, toSExp spans]

609− runIO . hPutStrLn h $ convSExp "return" good n

610−

611−ihPrintError :: Handle -> String -> Idris ()

612−ihPrintError h s = do i <- getIState

613− case idris_outputmode i of

614− RawOutput -> case s of

615− "" -> return ()

616− s -> runIO $ hPutStrLn h s

617− IdeSlave n ->

618− let good = SexpList [SymbolAtom "error", toSExp s] in

619− runIO . hPutStrLn h $ convSExp "return" good n

620−

621−ihputStrLn :: Handle -> String -> Idris ()

622−ihputStrLn h s = do i <- getIState

623− case idris_outputmode i of

624− RawOutput -> runIO $ hPutStrLn h s

625− IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n

626−

627−iputStrLn = ihputStrLn stdout

628−iPrintError = ihPrintError stdout

629−iPrintResult = ihPrintResult stdout

630−iWarn = ihWarn stdout

631−

632−ideslavePutSExp :: SExpable a => String -> a -> Idris ()

633−ideslavePutSExp cmd info = do i <- getIState

634− case idris_outputmode i of

635− IdeSlave n -> runIO . putStrLn $ convSExp cmd info n

636− _ -> return ()

637−

638−-- this needs some typing magic and more structured output towards emacs

639−iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

640−iputGoal g = do i <- getIState

641− case idris_outputmode i of

642− RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

643− IdeSlave n -> runIO . putStrLn $

644− convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n

645

518

646isetPrompt :: String -> Idris ()

519isetPrompt :: String -> Idris ()

647isetPrompt p = do i <- getIState

520isetPrompt p = do i <- getIState

648 case idris_outputmode i of

521 case idris_outputmode i of

649 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n

522 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n

650

523

651−ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()

652−ihWarn h fc err = do i <- getIState

653− case idris_outputmode i of

654− RawOutput ->

655− do err' <- iRender . fmap (fancifyAnnots i) $

656− text (show fc) <> colon <//> err

657− runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

658− IdeSlave n ->

659− do err' <- iRender . fmap (fancifyAnnots i) $ err

660− let (str, spans) = displaySpans err'

661− runIO . hPutStrLn h $

662− convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

663−

664setLogLevel :: Int -> Idris ()

524setLogLevel :: Int -> Idris ()

665setLogLevel l = do i <- getIState

525setLogLevel l = do i <- getIState

666 let opts = idris_options i

526 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+27−24

@@ -1068,13 +1068,13 @@ consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist

1068consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)

1069consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)

1070consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

1071−consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist

1071+consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist

1072− theme = idris_colourTheme ist

1072+ theme = idris_colourTheme ist

1073− in case () of

1073+ in case () of

1074− _ | isDConName n ctxt -> colouriseData theme

1074+ _ | isDConName n ctxt -> colouriseData theme

1075− _ | isFnName n ctxt -> colouriseFun theme

1075+ _ | isFnName n ctxt -> colouriseFun theme

1076− _ | isTConName n ctxt -> colouriseType theme

1076+ _ | isTConName n ctxt -> colouriseType theme

1077− _ | otherwise -> id -- don't colourise unknown names

1077+ _ | otherwise -> id -- don't colourise unknown names

1078consoleDecorate ist (AnnFC _) = id

1079consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1080 where colour BoldText = IdrisColour Nothing True False True False

@@ -1189,16 +1189,16 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1189

1190 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r

1191 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1192− prettySe p bnd (PRefl _ _) = annotate (AnnName eqCon Nothing Nothing) $ text "refl"

1192+ prettySe p bnd (PRefl _ _) = annName eqCon $ text "refl"

1193 prettySe p bnd (PResolveTC _) = text "resolvetc"

1194− prettySe p bnd (PTrue _ IsType) = annotate (AnnName unitTy Nothing Nothing) $ text "()"

1194+ prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1195− prettySe p bnd (PTrue _ IsTerm) = annotate (AnnName unitCon Nothing Nothing) $ text "()"

1195+ prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1196 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1197− prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"

1197+ prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"

1198 prettySe p bnd (PEq _ l r) =

1199 bracket p 2 . align . group $

1200 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1201− where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")

1201+ where eq = annName eqTy (text "=")

1202 prettySe p bnd (PRewrite _ l r _) =

1203 bracket p 2 $

1204 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

@@ -1210,28 +1210,28 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1210 map (prettySe 10 bnd) elts

1211 where ann = case pun of

1212 TypeOrTerm -> id

1213− IsType -> annotate (AnnName pairTy Nothing Nothing)

1213+ IsType -> annName pairTy

1214− IsTerm -> annotate (AnnName pairCon Nothing Nothing)

1214+ IsTerm -> annName pairCon

1215 prettySe p bnd (PDPair _ TypeOrTerm l t r) =

1216 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen

1217 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =

1218− annotate (AnnName sigmaTy Nothing Nothing) lparen <>

1218+ annName sigmaTy lparen <>

1219 bindingOf n False <+>

1220− annotate (AnnName sigmaTy Nothing Nothing) (text "**") <+>

1220+ annName sigmaTy (text "**") <+>

1221 prettySe 10 ((n, False):bnd) r <>

1222− annotate (AnnName sigmaTy Nothing Nothing) rparen

1222+ annName sigmaTy rparen

1223 prettySe p bnd (PDPair _ IsType l t r) =

1224− annotate (AnnName sigmaTy Nothing Nothing) lparen <>

1224+ annName sigmaTy lparen <>

1225 prettySe 10 bnd l <+>

1226− annotate (AnnName sigmaTy Nothing Nothing) (text "**") <+>

1226+ annName sigmaTy (text "**") <+>

1227 prettySe 10 bnd r <>

1228− annotate (AnnName sigmaTy Nothing Nothing) rparen

1228+ annName sigmaTy rparen

1229 prettySe p bnd (PDPair _ IsTerm l t r) =

1230− annotate (AnnName existsCon Nothing Nothing) lparen <>

1230+ annName existsCon lparen <>

1231 prettySe 10 bnd l <+>

1232− annotate (AnnName existsCon Nothing Nothing) (text "**") <+>

1232+ annName existsCon (text "**") <+>

1233 prettySe 10 bnd r <>

1234− annotate (AnnName existsCon Nothing Nothing) rparen

1234+ annName existsCon rparen

1235 prettySe p bnd (PAlternative a as) =

1236 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1237 where

@@ -1268,6 +1268,9 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1268 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace

1269 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1270

1271+ annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

1272+ annName n = annotate (AnnName n Nothing Nothing Nothing)

1273+

1271 basename :: Name -> Name

1274 basename :: Name -> Name

1272 basename (NS n _) = basename n

1275 basename (NS n _) = basename n

1273 basename n = n

1276 basename n = n

@@ -1333,7 +1336,7 @@ prettyName :: Bool -- ^^ whether to show namespaces

1333 -> Name -- ^^ the name to pprint

1336 -> Name -- ^^ the name to pprint

1334 -> Doc OutputAnnotation

1337 -> Doc OutputAnnotation

1335prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))

1338prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))

1336− | otherwise = annotate (AnnName n Nothing Nothing) (text (strName n))

1339+ | otherwise = annotate (AnnName n Nothing Nothing Nothing) (text (strName n))

1337 where strName (UN n) = T.unpack n

1340 where strName (UN n) = T.unpack n

1338 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1341 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1339 | otherwise = strName n

1342 | otherwise = strName n

src/Idris/CaseSplit.hs+1

@@ -14,6 +14,7 @@ import Idris.ElabTerm

14import Idris.Delaborate

15import Idris.Parser

16import Idris.Error

17+import Idris.Output

17

18

18import Idris.Core.TT

19import Idris.Core.TT

19import Idris.Core.Typecheck

20import Idris.Core.Typecheck

src/Idris/Core/TT.hs+7−5

@@ -88,8 +88,10 @@ data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput

88data TextFormatting = BoldText | ItalicText | UnderlineText

89

90-- | Output annotations for pretty-printing

91−data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)

91+data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)

92+ -- ^^ The name, classification, docs overview, and pretty-printed type

92 | AnnBoundName Name Bool

93 | AnnBoundName Name Bool

94+ -- ^^ The name and whether it is implicit

93 | AnnConstData

95 | AnnConstData

94 | AnnConstType

96 | AnnConstType

95 | AnnKeyword

97 | AnnKeyword

@@ -312,11 +314,11 @@ instance Sized Name where

312 size _ = 1

314 size _ = 1

313

315

314instance Pretty Name OutputAnnotation where

316instance Pretty Name OutputAnnotation where

315− pretty n@(UN n') = annotate (AnnName n Nothing Nothing) $ text (T.unpack n')

317+ pretty n@(UN n') = annotate (AnnName n Nothing Nothing Nothing) $ text (T.unpack n')

316− pretty n@(NS un s) = annotate (AnnName n Nothing Nothing) . noAnnotate $ pretty un

318+ pretty n@(NS un s) = annotate (AnnName n Nothing Nothing Nothing) . noAnnotate $ pretty un

317− pretty n@(MN i s) = annotate (AnnName n Nothing Nothing) $

319+ pretty n@(MN i s) = annotate (AnnName n Nothing Nothing Nothing) $

318 lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace

320 lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace

319− pretty n@(SN s) = annotate (AnnName n Nothing Nothing) $ text (show s)

321+ pretty n@(SN s) = annotate (AnnName n Nothing Nothing Nothing) $ text (show s)

320

322

321instance Pretty [Name] OutputAnnotation where

323instance Pretty [Name] OutputAnnotation where

322 pretty = encloseSep empty empty comma . map pretty

324 pretty = encloseSep empty empty comma . map pretty

src/Idris/Coverage.hs+1

@@ -9,6 +9,7 @@ import Idris.Core.CaseTree

9import Idris.AbsSyntax

10import Idris.Delaborate

11import Idris.Error

12+import Idris.Output (iputStrLn)

12

13

13import Data.List

14import Data.List

14import Data.Either

15import Data.Either

src/Idris/Delaborate.hs+2−7

@@ -1,5 +1,5 @@

1{-# LANGUAGE PatternGuards #-}

2−module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pshow, pprintErr) where

2+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pprintErr) where

3

4-- Convert core TT back into high level syntax, primarily for display

5-- purposes.

@@ -140,11 +140,6 @@ pprintTerm ist = pprintTerm' ist []

140pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

141pprintTerm' ist bnd tm = pprintPTerm (opt_showimp (idris_options ist)) bnd [] tm

142

143−pshow :: IState -> Err -> String

144−pshow ist err = displayDecorated (consoleDecorate ist) .

145− renderPretty 1.0 80 .

146− fmap (fancifyAnnots ist) $ pprintErr ist err

147−

148pprintErr :: IState -> Err -> Doc OutputAnnotation

143pprintErr :: IState -> Err -> Doc OutputAnnotation

149pprintErr i err = pprintErr' i (fmap (errReverse i) err)

144pprintErr i err = pprintErr' i (fmap (errReverse i) err)

150

145

@@ -261,7 +256,7 @@ annName :: Name -> Doc OutputAnnotation

261annName n = annName' n (showbasic n)

256annName n = annName' n (showbasic n)

262

257

263annName' :: Name -> String -> Doc OutputAnnotation

258annName' :: Name -> String -> Doc OutputAnnotation

264−annName' n str = annotate (AnnName n Nothing Nothing) (text str)

259+annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)

265

260

266showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

261showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

267showSc i [] = empty

262showSc i [] = empty

src/Idris/ElabDecls.hs+1

@@ -16,6 +16,7 @@ import Idris.Primitives

16import Idris.Inliner

17import Idris.PartialEval

18import Idris.DeepSeq

19+import Idris.Output (iputStrLn, pshow, iWarn)

19import IRTS.Lang

20import IRTS.Lang

20import Paths_idris

21import Paths_idris

21

22

src/Idris/ElabTerm.hs+1

@@ -7,6 +7,7 @@ import Idris.DSL

7import Idris.Delaborate

8import Idris.Error

9import Idris.ProofSearch

10+import Idris.Output (pshow)

10

11

11import Idris.Core.Elaborate hiding (Tactic(..))

12import Idris.Core.Elaborate hiding (Tactic(..))

12import Idris.Core.TT

13import Idris.Core.TT

src/Idris/Error.hs+1

@@ -5,6 +5,7 @@ module Idris.Error where

5import Prelude hiding (catch)

6import Idris.AbsSyntax

7import Idris.Delaborate

8+import Idris.Output

8

9

9import Idris.Core.TT

10import Idris.Core.TT

10import Idris.Core.Typecheck

11import Idris.Core.Typecheck

src/Idris/IBC.hs+1

@@ -10,6 +10,7 @@ import Idris.Imports

10import Idris.Error

11import Idris.Delaborate

12import Idris.Docstrings

13+import Idris.Output

13

14

14import qualified Cheapskate.Types as CT

15import qualified Cheapskate.Types as CT

15

16

src/Idris/IdeSlave.hs+9−5

@@ -79,12 +79,16 @@ instance SExpable NameOutput where

79 toSExp DataOutput = SymbolAtom "data"

80 toSExp MetavarOutput = SymbolAtom "metavar"

81

82+maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]

83+maybeProps [] = []

84+maybeProps ((n, Just p):ps) = (SymbolAtom n, toSExp p) : maybeProps ps

85+maybeProps ((n, Nothing):ps) = maybeProps ps

86+

82instance SExpable OutputAnnotation where

87instance SExpable OutputAnnotation where

83− toSExp (AnnName n Nothing _) = toSExp [(SymbolAtom "name", StringAtom (show n)),

88+ toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),

84− (SymbolAtom "implicit", BoolAtom False)]

89+ (SymbolAtom "implicit", BoolAtom False)] ++

85− toSExp (AnnName n (Just ty) _) = toSExp [(SymbolAtom "name", StringAtom (show n)),

90+ maybeProps [("decor", ty)] ++

86− (SymbolAtom "decor", toSExp ty),

91+ maybeProps [("doc-overview", d), ("type", t)]

87− (SymbolAtom "implicit", BoolAtom False)]

88 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),

92 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),

89 (SymbolAtom "decor", SymbolAtom "bound"),

93 (SymbolAtom "decor", SymbolAtom "bound"),

90 (SymbolAtom "implicit", BoolAtom imp)]

94 (SymbolAtom "implicit", BoolAtom imp)]

src/Idris/Output.hsnew file+173

@@ -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

src/Idris/ParseHelpers.hs+1

@@ -17,6 +17,7 @@ import Idris.Core.TT

17import Idris.Core.Evaluate

18import Idris.Delaborate (pprintErr)

19import Idris.Docstrings

20+import Idris.Output (ihWarn)

20

21

21import qualified Util.Pretty as Pretty (text)

22import qualified Util.Pretty as Pretty (text)

22

23

src/Idris/Parser.hs+1

@@ -29,6 +29,7 @@ import Idris.Coverage

29import Idris.IBC

30import Idris.Unlit

31import Idris.Providers

32+import Idris.Output

32

33

33import Idris.ParseHelpers

34import Idris.ParseHelpers

34import Idris.ParseOps

35import Idris.ParseOps

src/Idris/Prover.hs+1

@@ -15,6 +15,7 @@ import Idris.Error

15import Idris.DataOpts

16import Idris.Completion

17import Idris.IdeSlave

18+import Idris.Output

18

19

19import Text.Trifecta.Result(Result(..))

20import Text.Trifecta.Result(Result(..))

20

21

src/Idris/REPL.hs+2−1

@@ -27,6 +27,7 @@ import Idris.Colours hiding (colourise)

27import Idris.Inliner

28import Idris.CaseSplit

29import Idris.DeepSeq

30+import Idris.Output

30

31

31import Paths_idris

32import Paths_idris

32import Version_idris (gitHash)

33import Version_idris (gitHash)

@@ -532,7 +533,7 @@ process h fn (Check (PRef _ n))

532 putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc

533 putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc

533 putGoal imp ist bnd g

534 putGoal imp ist bnd g

534 = text "--------------------------------------" <$>

535 = text "--------------------------------------" <$>

535− annotate (AnnName n Nothing Nothing) (text $ show n) <+> colon <+>

536+ annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>

536 align (tPretty bnd ist g)

537 align (tPretty bnd ist g)

537

538

538 tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] t

539 tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] t

src/Pkg/Package.hs+1

@@ -17,6 +17,7 @@ import Data.List.Split(splitOn)

17import Idris.Core.TT

18import Idris.REPL

19import Idris.AbsSyntax

20+import Idris.Output

20

21

21import IRTS.System

22import IRTS.System

22

23