{-|
Module      : Idris.Output
Description : Utilities to display Idris' internals and other informtation to the user.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# LANGUAGE CPP, FlexibleInstances #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

module Idris.Output (clearHighlights, emitWarning, formatMessage, idemodePutSExp,
                     iPrintError, iPrintFunTypes, iPrintResult, iPrintTermWithType,
                     iputGoal, iputStr, iputStrLn, iRender, iRenderError,
                     iRenderOutput, iRenderResult, iWarn, prettyDocumentedIst,
                     printUndefinedNames, pshow, renderExternal, sendHighlighting,
                     sendParserHighlighting, warnTotality, writeHighlights,
                     OutputDoc(..), Message(..)) where

import Idris.AbsSyntax
import Idris.Colours (hEndColourise, hStartColourise)
import Idris.Core.Evaluate (normaliseAll)
import Idris.Core.TT
import Idris.Delaborate
import Idris.Docstrings
import Idris.IdeMode
import Idris.Options

import Util.Pretty
import Util.ScreenSize (getScreenWidth)
import Util.System (isATTY)

#if (MIN_VERSION_base(4,11,0))
import Prelude hiding ((<$>), (<>))
#else
import Prelude hiding ((<$>))
#endif

import Control.Arrow (first)
import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
import Data.List (intersperse, nub)
import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)
import qualified Data.Set as S
import System.Console.Haskeline.MonadException (MonadException(controlIO),
                                                RunIO(RunIO))
import System.FilePath (replaceExtension)
import System.IO (Handle, hPutStr, hPutStrLn)
import System.IO.Error (tryIOError)

instance MonadException m => MonadException (ExceptT Err m) where
    controlIO :: (RunIO (ExceptT Err m) -> IO (ExceptT Err m a)) -> ExceptT Err m a
controlIO f :: RunIO (ExceptT Err m) -> IO (ExceptT Err m a)
f = m (Either Err a) -> ExceptT Err m a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (m (Either Err a) -> ExceptT Err m a)
-> m (Either Err a) -> ExceptT Err m a
forall a b. (a -> b) -> a -> b
$ (RunIO m -> IO (m (Either Err a))) -> m (Either Err a)
forall (m :: * -> *) a.
MonadException m =>
(RunIO m -> IO (m a)) -> m a
controlIO ((RunIO m -> IO (m (Either Err a))) -> m (Either Err a))
-> (RunIO m -> IO (m (Either Err a))) -> m (Either Err a)
forall a b. (a -> b) -> a -> b
$ \(RunIO run :: forall b. m b -> IO (m b)
run) -> let
                    run' :: RunIO (ExceptT e m)
run' = (forall b. ExceptT e m b -> IO (ExceptT e m b))
-> RunIO (ExceptT e m)
forall (m :: * -> *). (forall b. m b -> IO (m b)) -> RunIO m
RunIO ((m (Either e b) -> ExceptT e m b)
-> IO (m (Either e b)) -> IO (ExceptT e m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m (Either e b) -> ExceptT e m b
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (IO (m (Either e b)) -> IO (ExceptT e m b))
-> (ExceptT e m b -> IO (m (Either e b)))
-> ExceptT e m b
-> IO (ExceptT e m b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Either e b) -> IO (m (Either e b))
forall b. m b -> IO (m b)
run (m (Either e b) -> IO (m (Either e b)))
-> (ExceptT e m b -> m (Either e b))
-> ExceptT e m b
-> IO (m (Either e b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT e m b -> m (Either e b)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT)
                    in (ExceptT Err m a -> m (Either Err a))
-> IO (ExceptT Err m a) -> IO (m (Either Err a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ExceptT Err m a -> m (Either Err a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (IO (ExceptT Err m a) -> IO (m (Either Err a)))
-> IO (ExceptT Err m a) -> IO (m (Either Err a))
forall a b. (a -> b) -> a -> b
$ RunIO (ExceptT Err m) -> IO (ExceptT Err m a)
f RunIO (ExceptT Err m)
forall e. RunIO (ExceptT e m)
run'

pshow :: IState -> Err -> String
pshow :: IState -> Err -> String
pshow ist :: IState
ist err :: Err
err = (OutputAnnotation -> String -> String)
-> SimpleDoc OutputAnnotation -> String
forall a. (a -> String -> String) -> SimpleDoc a -> String
displayDecorated (IState -> OutputAnnotation -> String -> String
consoleDecorate IState
ist) (SimpleDoc OutputAnnotation -> String)
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty 1.0 80 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> SimpleDoc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation -> String) -> Doc OutputAnnotation -> String
forall a b. (a -> b) -> a -> b
$ IState -> Err -> Doc OutputAnnotation
pprintErr IState
ist Err
err

type OutputDoc = Doc OutputAnnotation

class Message a where
  messageExtent :: a -> FC
  messageText :: a -> OutputDoc
  messageSource :: a -> Maybe String

data Ann = AText String | ATagged OutputAnnotation Ann | ASplit Ann Ann

data SimpleWarning = SimpleWarning FC OutputDoc
instance Message SimpleWarning where
  messageExtent :: SimpleWarning -> FC
messageExtent (SimpleWarning extent :: FC
extent _) = FC
extent
  messageText :: SimpleWarning -> Doc OutputAnnotation
messageText (SimpleWarning _ msg :: Doc OutputAnnotation
msg) = Doc OutputAnnotation
msg
  messageSource :: SimpleWarning -> Maybe String
messageSource _ = Maybe String
forall a. Maybe a
Nothing

formatMessage :: Message w => w -> Idris OutputDoc
formatMessage :: w -> Idris (Doc OutputAnnotation)
formatMessage w :: w
w = do
    IState
i <- Idris IState
getIState
    Maybe String
rs <- FC -> Idris (Maybe String)
readSource FC
fc
    let maybeSource :: Maybe String
maybeSource = case Maybe String
rs of
          Just src :: String
src -> String -> Maybe String
forall a. a -> Maybe a
Just String
src
          Nothing -> w -> Maybe String
forall a. Message a => a -> Maybe String
messageSource w
w
    let maybeFormattedSource :: Maybe (Doc OutputAnnotation)
maybeFormattedSource = Maybe String
maybeSource Maybe String
-> (String -> Maybe (Doc OutputAnnotation))
-> Maybe (Doc OutputAnnotation)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FC
-> [(FC, OutputAnnotation)]
-> String
-> Maybe (Doc OutputAnnotation)
layoutSource FC
fc (Set (FC', OutputAnnotation) -> [(FC, OutputAnnotation)]
regions (IState -> Set (FC', OutputAnnotation)
idris_highlightedRegions IState
i))
    Doc OutputAnnotation -> Idris (Doc OutputAnnotation)
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc OutputAnnotation -> Idris (Doc OutputAnnotation))
-> Doc OutputAnnotation -> Idris (Doc OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ Doc OutputAnnotation
-> Maybe (Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Doc OutputAnnotation
layoutMessage (FC -> Doc OutputAnnotation
layoutFC FC
fc) Maybe (Doc OutputAnnotation)
maybeFormattedSource (w -> Doc OutputAnnotation
forall a. Message a => a -> Doc OutputAnnotation
messageText w
w)
  where
    regions :: S.Set (FC', OutputAnnotation) -> [(FC, OutputAnnotation)]
    regions :: Set (FC', OutputAnnotation) -> [(FC, OutputAnnotation)]
regions rs :: Set (FC', OutputAnnotation)
rs = ((FC', OutputAnnotation) -> (FC, OutputAnnotation))
-> [(FC', OutputAnnotation)] -> [(FC, OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\(FC' a :: FC
a,b :: OutputAnnotation
b) -> (FC
a, OutputAnnotation
b)) ([(FC', OutputAnnotation)] -> [(FC, OutputAnnotation)])
-> [(FC', OutputAnnotation)] -> [(FC, OutputAnnotation)]
forall a b. (a -> b) -> a -> b
$ Set (FC', OutputAnnotation) -> [(FC', OutputAnnotation)]
forall a. Set a -> [a]
S.toList Set (FC', OutputAnnotation)
rs

    fc :: FC
    fc :: FC
fc = w -> FC
forall a. Message a => a -> FC
messageExtent w
w

    layoutFC :: FC -> OutputDoc
    layoutFC :: FC -> Doc OutputAnnotation
layoutFC fc :: FC
fc@(FC fn :: String
fn _ _) | String
fn String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= "" = String -> Doc OutputAnnotation
forall a. String -> Doc a
text (FC -> String
forall a. Show a => a -> String
show (FC -> String) -> FC -> String
forall a b. (a -> b) -> a -> b
$ FC
fc) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon
    layoutFC _                         = Doc OutputAnnotation
forall a. Doc a
empty

    readSource :: FC -> Idris (Maybe String)
    readSource :: FC -> Idris (Maybe String)
readSource (FC fn :: String
fn _ _) = do
      Either IOError String
result <- IO (Either IOError String) -> Idris (Either IOError String)
forall a. IO a -> Idris a
runIO (IO (Either IOError String) -> Idris (Either IOError String))
-> IO (Either IOError String) -> Idris (Either IOError String)
forall a b. (a -> b) -> a -> b
$ IO String -> IO (Either IOError String)
forall a. IO a -> IO (Either IOError a)
tryIOError (String -> IO String
readFile String
fn)
      case Either IOError String
result of
        Left _  -> Maybe String -> Idris (Maybe String)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
        Right v :: String
v -> Maybe String -> Idris (Maybe String)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe String
forall a. a -> Maybe a
Just String
v)
    readSource _           = Maybe String -> Idris (Maybe String)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing

    layoutSource :: FC -> [(FC, OutputAnnotation)] -> String -> Maybe OutputDoc
    layoutSource :: FC
-> [(FC, OutputAnnotation)]
-> String
-> Maybe (Doc OutputAnnotation)
layoutSource (FC fn :: String
fn (si :: Int
si, sj :: Int
sj) (ei :: Int
ei, ej :: Int
ej)) highlights :: [(FC, OutputAnnotation)]
highlights src :: String
src =
        if Bool
haveSource
        then Doc OutputAnnotation -> Maybe (Doc OutputAnnotation)
forall a. a -> Maybe a
Just Doc OutputAnnotation
source
        else Maybe (Doc OutputAnnotation)
forall a. Maybe a
Nothing
      where
        sourceLine :: Maybe String
        sourceLine :: Maybe String
sourceLine = [String] -> Maybe String
forall a. [a] -> Maybe a
listToMaybe ([String] -> Maybe String)
-> (String -> [String]) -> String -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
drop (Int
si Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["<end of file>"]) ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
src

        haveSource :: Bool
        haveSource :: Bool
haveSource = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
sourceLine

        line1 :: OutputDoc
        line1 :: Doc OutputAnnotation
line1 = String -> Doc OutputAnnotation
forall a. String -> Doc a
text (String -> Doc OutputAnnotation) -> String -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> String
forall a. Show a => a -> String
show Int
si)) ' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++ " |"

        lineFC :: FC
        lineFC :: FC
lineFC = String -> (Int, Int) -> (Int, Int) -> FC
FC String
fn (Int
si, 1) (Int
si, String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
sourceLine))

        intersects :: FC -> FC -> Bool
        intersects :: FC -> FC -> Bool
intersects (FC fn1 :: String
fn1 s1 :: (Int, Int)
s1 e1 :: (Int, Int)
e1) (FC fn2 :: String
fn2 s2 :: (Int, Int)
s2 e2 :: (Int, Int)
e2)
          | String
fn1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
fn2 = Bool
False
          | (Int, Int)
e1 (Int, Int) -> (Int, Int) -> Bool
forall a. Ord a => a -> a -> Bool
< (Int, Int)
s2    = Bool
False
          | (Int, Int)
e2 (Int, Int) -> (Int, Int) -> Bool
forall a. Ord a => a -> a -> Bool
< (Int, Int)
s1    = Bool
False
          | Bool
otherwise  = Bool
True
        intersects _ _ = Bool
False

        intersection :: FC -> FC -> FC
        intersection :: FC -> FC -> FC
intersection fc1 :: FC
fc1@(FC fn1 :: String
fn1 s1 :: (Int, Int)
s1 e1 :: (Int, Int)
e1) fc2 :: FC
fc2@(FC _ s2 :: (Int, Int)
s2 e2 :: (Int, Int)
e2)
          | FC -> FC -> Bool
intersects FC
fc1 FC
fc2 = String -> (Int, Int) -> (Int, Int) -> FC
FC String
fn1 ((Int, Int) -> (Int, Int) -> (Int, Int)
forall a. Ord a => a -> a -> a
max (Int, Int)
s1 (Int, Int)
s2) ((Int, Int) -> (Int, Int) -> (Int, Int)
forall a. Ord a => a -> a -> a
min (Int, Int)
e1 (Int, Int)
e2)
          | Bool
otherwise          = FC
NoFC
        intersection _ _       = FC
NoFC

        width :: Ann -> Int
        width :: Ann -> Int
width (AText s :: String
s)     = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s
        width (ATagged _ n :: Ann
n) = Ann -> Int
width Ann
n
        width (ASplit l :: Ann
l r :: Ann
r)  = Ann -> Int
width Ann
l Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Ann -> Int
width Ann
r

        sourceDoc :: Ann -> OutputDoc
        sourceDoc :: Ann -> Doc OutputAnnotation
sourceDoc (AText s :: String
s)     = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
s
        sourceDoc (ATagged a :: OutputAnnotation
a n :: Ann
n) = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate OutputAnnotation
a (Ann -> Doc OutputAnnotation
sourceDoc Ann
n)
        sourceDoc (ASplit l :: Ann
l r :: Ann
r)  = Ann -> Doc OutputAnnotation
sourceDoc Ann
l Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Ann -> Doc OutputAnnotation
sourceDoc Ann
r

        insertAnnotation :: ((Int, Int), OutputAnnotation) -> Ann -> Ann
        insertAnnotation :: ((Int, Int), OutputAnnotation) -> Ann -> Ann
insertAnnotation ((sj :: Int
sj, ej :: Int
ej), oa :: OutputAnnotation
oa) (ATagged tag :: OutputAnnotation
tag n :: Ann
n) = OutputAnnotation -> Ann -> Ann
ATagged OutputAnnotation
tag (((Int, Int), OutputAnnotation) -> Ann -> Ann
insertAnnotation ((Int
sj, Int
ej), OutputAnnotation
oa) Ann
n)
        insertAnnotation ((sj :: Int
sj, ej :: Int
ej), oa :: OutputAnnotation
oa) (ASplit l :: Ann
l r :: Ann
r)
          | Int
w <- Ann -> Int
width Ann
l                   = Ann -> Ann -> Ann
ASplit (((Int, Int), OutputAnnotation) -> Ann -> Ann
insertAnnotation ((Int
sj, Int
ej), OutputAnnotation
oa) Ann
l) (((Int, Int), OutputAnnotation) -> Ann -> Ann
insertAnnotation ((Int
sj Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
w, Int
ej Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
w), OutputAnnotation
oa) Ann
r)
        insertAnnotation ((sj :: Int
sj, ej :: Int
ej), oa :: OutputAnnotation
oa) a :: Ann
a@(AText t :: String
t)
          | Int
sj Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 1, Int
ej Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Ann -> Int
width Ann
a         = OutputAnnotation -> Ann -> Ann
ATagged OutputAnnotation
oa Ann
a
          | Int
sj Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1,  Int
sj Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Ann -> Int
width Ann
a         = Ann -> Ann -> Ann
ASplit (String -> Ann
AText (String -> Ann) -> String -> Ann
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
take (Int
sj Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) String
t) (((Int, Int), OutputAnnotation) -> Ann -> Ann
insertAnnotation ((1, Int
ej Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
sj Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1), OutputAnnotation
oa) (String -> Ann
AText (String -> Ann) -> String -> Ann
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
drop (Int
sj Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) String
t))
          | Int
sj Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1, Int
ej Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 1, Int
ej Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Ann -> Int
width Ann
a = Ann -> Ann -> Ann
ASplit (((Int, Int), OutputAnnotation) -> Ann -> Ann
insertAnnotation ((1, Int
ej), OutputAnnotation
oa) (String -> Ann
AText (String -> Ann) -> String -> Ann
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
ej String
t)) (String -> Ann
AText (String -> Ann) -> String -> Ann
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
drop Int
ej String
t)
          | Bool
otherwise                      = Ann
a

        highlightedSource :: OutputDoc
        highlightedSource :: Doc OutputAnnotation
highlightedSource = Ann -> Doc OutputAnnotation
sourceDoc (Ann -> Doc OutputAnnotation)
-> ([(FC, OutputAnnotation)] -> Ann)
-> [(FC, OutputAnnotation)]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                            (((Int, Int), OutputAnnotation) -> Ann -> Ann)
-> Ann -> [((Int, Int), OutputAnnotation)] -> Ann
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Int, Int), OutputAnnotation) -> Ann -> Ann
insertAnnotation (String -> Ann
AText (String -> Ann) -> String -> Ann
forall a b. (a -> b) -> a -> b
$ Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
sourceLine) ([((Int, Int), OutputAnnotation)] -> Ann)
-> ([(FC, OutputAnnotation)] -> [((Int, Int), OutputAnnotation)])
-> [(FC, OutputAnnotation)]
-> Ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                            ((FC, OutputAnnotation) -> ((Int, Int), OutputAnnotation))
-> [(FC, OutputAnnotation)] -> [((Int, Int), OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\(FC _ (_, sj :: Int
sj) (_, ej :: Int
ej), ann :: OutputAnnotation
ann) -> ((Int
sj, Int
ej), OutputAnnotation
ann)) ([(FC, OutputAnnotation)] -> [((Int, Int), OutputAnnotation)])
-> ([(FC, OutputAnnotation)] -> [(FC, OutputAnnotation)])
-> [(FC, OutputAnnotation)]
-> [((Int, Int), OutputAnnotation)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                            ((FC, OutputAnnotation) -> (FC, OutputAnnotation))
-> [(FC, OutputAnnotation)] -> [(FC, OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map ((FC -> FC) -> (FC, OutputAnnotation) -> (FC, OutputAnnotation)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (FC -> FC -> FC
intersection FC
lineFC)) ([(FC, OutputAnnotation)] -> [(FC, OutputAnnotation)])
-> ([(FC, OutputAnnotation)] -> [(FC, OutputAnnotation)])
-> [(FC, OutputAnnotation)]
-> [(FC, OutputAnnotation)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                            ((FC, OutputAnnotation) -> Bool)
-> [(FC, OutputAnnotation)] -> [(FC, OutputAnnotation)]
forall a. (a -> Bool) -> [a] -> [a]
filter (FC -> FC -> Bool
intersects FC
lineFC (FC -> Bool)
-> ((FC, OutputAnnotation) -> FC) -> (FC, OutputAnnotation) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FC, OutputAnnotation) -> FC
forall a b. (a, b) -> a
fst) ([(FC, OutputAnnotation)] -> Doc OutputAnnotation)
-> [(FC, OutputAnnotation)] -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
                            [(FC, OutputAnnotation)]
highlights

        line2 :: OutputDoc
        line2 :: Doc OutputAnnotation
line2 = String -> Doc OutputAnnotation
forall a. String -> Doc a
text (Int -> String
forall a. Show a => a -> String
show Int
si String -> String -> String
forall a. [a] -> [a] -> [a]
++ " | ") Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
highlightedSource

        indicator :: OutputDoc
        indicator :: Doc OutputAnnotation
indicator = String -> Doc OutputAnnotation
forall a. String -> Doc a
text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
sj Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Char
ch) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
ellipsis
          where
            (end :: Int
end, ch :: Char
ch, ellipsis :: Doc a
ellipsis) = case (Int
si Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ei, Int
sj Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ej) of
              (True , True ) -> (Int
ej, '^', Doc a
forall a. Doc a
empty)
              (True , False) -> (Int
ej, '~', Doc a
forall a. Doc a
empty)
              (False, _    ) -> (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
sourceLine), '~', String -> Doc a
forall a. String -> Doc a
text " ...")

        line3 :: OutputDoc
        line3 :: Doc OutputAnnotation
line3 = Doc OutputAnnotation
line1 Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
sj ' ') Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
indicator

        source :: OutputDoc
        source :: Doc OutputAnnotation
source = Doc OutputAnnotation
line1 Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$$> Doc OutputAnnotation
line2 Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$$> Doc OutputAnnotation
line3
    layoutSource _ _ _                                    = Maybe (Doc OutputAnnotation)
forall a. Maybe a
Nothing

    layoutMessage :: OutputDoc -> Maybe OutputDoc -> OutputDoc -> OutputDoc
    layoutMessage :: Doc OutputAnnotation
-> Maybe (Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Doc OutputAnnotation
layoutMessage loc :: Doc OutputAnnotation
loc (Just src :: Doc OutputAnnotation
src) err :: Doc OutputAnnotation
err = Doc OutputAnnotation
loc Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$$> Doc OutputAnnotation
src Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$$> Doc OutputAnnotation
err Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$$> Doc OutputAnnotation
forall a. Doc a
empty
    layoutMessage loc :: Doc OutputAnnotation
loc Nothing    err :: Doc OutputAnnotation
err = Doc OutputAnnotation
loc Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
</> Doc OutputAnnotation
err

iWarn :: FC -> OutputDoc -> Idris ()
iWarn :: FC -> Doc OutputAnnotation -> Idris ()
iWarn fc :: FC
fc err :: Doc OutputAnnotation
err = SimpleWarning -> Idris ()
forall w. Message w => w -> Idris ()
emitWarning (SimpleWarning -> Idris ()) -> SimpleWarning -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> Doc OutputAnnotation -> SimpleWarning
SimpleWarning FC
fc Doc OutputAnnotation
err

emitWarning :: Message w => w -> Idris ()
emitWarning :: w -> Idris ()
emitWarning w :: w
w =
  do IState
i <- Idris IState
getIState
     case IState -> OutputMode
idris_outputmode IState
i of
       RawOutput h :: Handle
h ->
         do Doc OutputAnnotation
formattedErr <- w -> Idris (Doc OutputAnnotation)
forall w. Message w => w -> Idris (Doc OutputAnnotation)
formatMessage w
w
            SimpleDoc OutputAnnotation
err' <- Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation)
forall a. Doc a -> Idris (SimpleDoc a)
iRender (Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation))
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Idris (SimpleDoc OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
i Bool
True) (Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation))
-> Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ Doc OutputAnnotation
formattedErr
            Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()
hWriteDoc Handle
h IState
i SimpleDoc OutputAnnotation
err'
       IdeMode n :: Integer
n h :: Handle
h ->
         do SimpleDoc OutputAnnotation
err' <- Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation)
forall a. Doc a -> Idris (SimpleDoc a)
iRender (Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation))
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Idris (SimpleDoc OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
i Bool
True) (Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation))
-> Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ w -> Doc OutputAnnotation
forall a. Message a => a -> Doc OutputAnnotation
messageText w
w
            let fc :: FC
fc = w -> FC
forall a. Message a => a -> FC
messageExtent w
w
            let (str :: String
str, spans :: SpanList OutputAnnotation
spans) = SimpleDoc OutputAnnotation -> (String, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (String, SpanList a)
displaySpans SimpleDoc OutputAnnotation
err'
            IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (String -> IO ()) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$
              String
-> (String, (Int, Int), (Int, Int), String,
    SpanList OutputAnnotation)
-> Integer
-> String
forall a. SExpable a => String -> a -> Integer -> String
convSExp "warning" (FC -> String
fc_fname FC
fc, FC -> (Int, Int)
fc_start FC
fc, FC -> (Int, Int)
fc_end FC
fc, String
str, SpanList OutputAnnotation
spans) Integer
n

iRender :: Doc a -> Idris (SimpleDoc a)
iRender :: Doc a -> Idris (SimpleDoc a)
iRender d :: Doc a
d = do ConsoleWidth
w <- Idris ConsoleWidth
getWidth
               IState
ist <- Idris IState
getIState
               let ideMode :: Bool
ideMode = case IState -> OutputMode
idris_outputmode IState
ist of
                                IdeMode _ _ -> Bool
True
                                _            -> Bool
False
               Bool
tty <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO IO Bool
isATTY
               case ConsoleWidth
w of
                 InfinitelyWide -> SimpleDoc a -> Idris (SimpleDoc a)
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleDoc a -> Idris (SimpleDoc a))
-> SimpleDoc a -> Idris (SimpleDoc a)
forall a b. (a -> b) -> a -> b
$ Float -> Int -> Doc a -> SimpleDoc a
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty 1.0 1000000000 Doc a
d
                 ColsWide n :: Int
n -> SimpleDoc a -> Idris (SimpleDoc a)
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleDoc a -> Idris (SimpleDoc a))
-> SimpleDoc a -> Idris (SimpleDoc a)
forall a b. (a -> b) -> a -> b
$
                               if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1
                                 then Float -> Int -> Doc a -> SimpleDoc a
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty 1.0 1000000000 Doc a
d
                                 else Float -> Int -> Doc a -> SimpleDoc a
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty 0.8 Int
n Doc a
d
                 AutomaticWidth | Bool
ideMode Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
tty -> SimpleDoc a -> Idris (SimpleDoc a)
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleDoc a -> Idris (SimpleDoc a))
-> SimpleDoc a -> Idris (SimpleDoc a)
forall a b. (a -> b) -> a -> b
$ Float -> Int -> Doc a -> SimpleDoc a
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty 1.0 80 Doc a
d
                                | Bool
otherwise -> do Int
width <- IO Int -> Idris Int
forall a. IO a -> Idris a
runIO IO Int
getScreenWidth
                                                  SimpleDoc a -> Idris (SimpleDoc a)
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleDoc a -> Idris (SimpleDoc a))
-> SimpleDoc a -> Idris (SimpleDoc a)
forall a b. (a -> b) -> a -> b
$ Float -> Int -> Doc a -> SimpleDoc a
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty 0.8 Int
width Doc a
d

hWriteDoc :: Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()
hWriteDoc :: Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()
hWriteDoc h :: Handle
h ist :: IState
ist rendered :: SimpleDoc OutputAnnotation
rendered =
    do IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ (String -> IO ())
-> (Maybe IdrisColour -> IO ())
-> (Maybe IdrisColour -> IO ())
-> SimpleDoc (Maybe IdrisColour)
-> IO ()
forall (f :: * -> *) b a.
(Applicative f, Monoid b) =>
(String -> f b) -> (a -> f b) -> (a -> f b) -> SimpleDoc a -> f b
displayDecoratedA
                 (Handle -> String -> IO ()
hPutStr Handle
h)
                 (IO () -> (IdrisColour -> IO ()) -> Maybe IdrisColour -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Handle -> IdrisColour -> IO ()
hStartColourise Handle
h))
                 (IO () -> (IdrisColour -> IO ()) -> Maybe IdrisColour -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Handle -> IdrisColour -> IO ()
hEndColourise Handle
h))
                 ((OutputAnnotation -> Maybe IdrisColour)
-> SimpleDoc OutputAnnotation -> SimpleDoc (Maybe IdrisColour)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> OutputAnnotation -> Maybe IdrisColour
annotationColour IState
ist) SimpleDoc OutputAnnotation
rendered)
       IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStr Handle
h "\n" -- newline translation on the output
                              -- stream should take care of this for
                              -- Windows

-- | Write a pretty-printed term to the console with semantic coloring
consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
consoleDisplayAnnotated h :: Handle
h output :: Doc OutputAnnotation
output =
    do IState
ist <- Idris IState
getIState
       SimpleDoc OutputAnnotation
rendered <- Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation)
forall a. Doc a -> Idris (SimpleDoc a)
iRender Doc OutputAnnotation
output
       Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()
hWriteDoc Handle
h IState
ist SimpleDoc OutputAnnotation
rendered

iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
iPrintTermWithType tm :: Doc OutputAnnotation
tm ty :: Doc OutputAnnotation
ty = Doc OutputAnnotation -> Idris ()
iRenderResult (Doc OutputAnnotation
tm Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align Doc OutputAnnotation
ty)

-- | Pretty-print a collection of overloadings to REPL or IDEMode - corresponds to :t name
iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
iPrintFunTypes :: [(Name, Bool)]
-> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
iPrintFunTypes bnd :: [(Name, Bool)]
bnd n :: Name
n []        = String -> Idris ()
iPrintError (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "No such variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
iPrintFunTypes bnd :: [(Name, Bool)]
bnd n :: Name
n overloads :: [(Name, Doc OutputAnnotation)]
overloads = do IState
ist <- Idris IState
getIState
                                    let ppo :: PPOption
ppo = IState -> PPOption
ppOptionIst IState
ist
                                    let infixes :: [FixDecl]
infixes = IState -> [FixDecl]
idris_infixes IState
ist
                                    let output :: Doc OutputAnnotation
output = [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (((Name, Doc OutputAnnotation) -> Doc OutputAnnotation)
-> [(Name, Doc OutputAnnotation)] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name, Doc OutputAnnotation) -> Doc OutputAnnotation
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (PPOption
-> [FixDecl]
-> Name
-> Doc OutputAnnotation
-> Doc OutputAnnotation
forall p.
PPOption
-> p -> Name -> Doc OutputAnnotation -> Doc OutputAnnotation
ppOverload PPOption
ppo [FixDecl]
infixes)) [(Name, Doc OutputAnnotation)]
overloads)
                                    Doc OutputAnnotation -> Idris ()
iRenderResult Doc OutputAnnotation
output
  where fullName :: PPOption -> Name -> Doc OutputAnnotation
fullName ppo :: PPOption
ppo n :: Name
n | [(Name, Doc OutputAnnotation)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Doc OutputAnnotation)]
overloads Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 = Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True [(Name, Bool)]
bnd Name
n
                       | Bool
otherwise = Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True (PPOption -> Bool
ppopt_impl PPOption
ppo) [(Name, Bool)]
bnd Name
n
        ppOverload :: PPOption
-> p -> Name -> Doc OutputAnnotation -> Doc OutputAnnotation
ppOverload ppo :: PPOption
ppo infixes :: p
infixes n :: Name
n tm :: Doc OutputAnnotation
tm =
          PPOption -> Name -> Doc OutputAnnotation
fullName PPOption
ppo Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align Doc OutputAnnotation
tm

iRenderOutput :: Doc OutputAnnotation -> Idris ()
iRenderOutput :: Doc OutputAnnotation -> Idris ()
iRenderOutput doc :: Doc OutputAnnotation
doc =
  do IState
i <- Idris IState
getIState
     case IState -> OutputMode
idris_outputmode IState
i of
       RawOutput h :: Handle
h -> do SimpleDoc OutputAnnotation
out <- Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation)
forall a. Doc a -> Idris (SimpleDoc a)
iRender Doc OutputAnnotation
doc
                         Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()
hWriteDoc Handle
h IState
i SimpleDoc OutputAnnotation
out

       IdeMode n :: Integer
n h :: Handle
h ->
        do (str :: String
str, spans :: SpanList OutputAnnotation
spans) <- (SimpleDoc OutputAnnotation -> (String, SpanList OutputAnnotation))
-> Idris (SimpleDoc OutputAnnotation)
-> StateT
     IState (ExceptT Err IO) (String, SpanList OutputAnnotation)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SimpleDoc OutputAnnotation -> (String, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (String, SpanList a)
displaySpans (Idris (SimpleDoc OutputAnnotation)
 -> StateT
      IState (ExceptT Err IO) (String, SpanList OutputAnnotation))
-> (Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation))
-> Doc OutputAnnotation
-> StateT
     IState (ExceptT Err IO) (String, SpanList OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation)
forall a. Doc a -> Idris (SimpleDoc a)
iRender (Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation))
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Idris (SimpleDoc OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
i Bool
True) (Doc OutputAnnotation
 -> StateT
      IState (ExceptT Err IO) (String, SpanList OutputAnnotation))
-> Doc OutputAnnotation
-> StateT
     IState (ExceptT Err IO) (String, SpanList OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ Doc OutputAnnotation
doc
           let out :: [SExp]
out = [String -> SExp
forall a. SExpable a => a -> SExp
toSExp String
str, SpanList OutputAnnotation -> SExp
forall a. SExpable a => a -> SExp
toSExp SpanList OutputAnnotation
spans]
           IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (String -> IO ()) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> [SExp] -> Integer -> String
forall a. SExpable a => String -> a -> Integer -> String
convSExp "write-decorated" [SExp]
out Integer
n

iRenderResult :: Doc OutputAnnotation -> Idris ()
iRenderResult :: Doc OutputAnnotation -> Idris ()
iRenderResult d :: Doc OutputAnnotation
d = do IState
ist <- Idris IState
getIState
                     case IState -> OutputMode
idris_outputmode IState
ist of
                       RawOutput h :: Handle
h  -> Handle -> Doc OutputAnnotation -> Idris ()
consoleDisplayAnnotated Handle
h Doc OutputAnnotation
d
                       IdeMode n :: Integer
n h :: Handle
h -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideModeReturnAnnotated Integer
n Handle
h Doc OutputAnnotation
d

ideModeReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideModeReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideModeReturnWithStatus status :: String
status n :: Integer
n h :: Handle
h out :: Doc OutputAnnotation
out = do
  IState
ist <- Idris IState
getIState
  (str :: String
str, spans :: SpanList OutputAnnotation
spans) <- (SimpleDoc OutputAnnotation -> (String, SpanList OutputAnnotation))
-> Idris (SimpleDoc OutputAnnotation)
-> StateT
     IState (ExceptT Err IO) (String, SpanList OutputAnnotation)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SimpleDoc OutputAnnotation -> (String, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (String, SpanList a)
displaySpans (Idris (SimpleDoc OutputAnnotation)
 -> StateT
      IState (ExceptT Err IO) (String, SpanList OutputAnnotation))
-> (Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation))
-> Doc OutputAnnotation
-> StateT
     IState (ExceptT Err IO) (String, SpanList OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                  Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation)
forall a. Doc a -> Idris (SimpleDoc a)
iRender (Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation))
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Idris (SimpleDoc OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                  (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation
 -> StateT
      IState (ExceptT Err IO) (String, SpanList OutputAnnotation))
-> Doc OutputAnnotation
-> StateT
     IState (ExceptT Err IO) (String, SpanList OutputAnnotation)
forall a b. (a -> b) -> a -> b
$
                  Doc OutputAnnotation
out
  let good :: [SExp]
good = [String -> SExp
SymbolAtom String
status, String -> SExp
forall a. SExpable a => a -> SExp
toSExp String
str, SpanList OutputAnnotation -> SExp
forall a. SExpable a => a -> SExp
toSExp SpanList OutputAnnotation
spans]
  IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (String -> IO ()) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> [SExp] -> Integer -> String
forall a. SExpable a => String -> a -> Integer -> String
convSExp "return" [SExp]
good Integer
n


-- | Write pretty-printed output to IDEMode with semantic annotations
ideModeReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideModeReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideModeReturnAnnotated = String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideModeReturnWithStatus "ok"

-- | Show an error with semantic highlighting
iRenderError :: Doc OutputAnnotation -> Idris ()
iRenderError :: Doc OutputAnnotation -> Idris ()
iRenderError e :: Doc OutputAnnotation
e = do IState
ist <- Idris IState
getIState
                    case IState -> OutputMode
idris_outputmode IState
ist of
                      RawOutput h :: Handle
h  -> Handle -> Doc OutputAnnotation -> Idris ()
consoleDisplayAnnotated Handle
h Doc OutputAnnotation
e
                      IdeMode n :: Integer
n h :: Handle
h -> String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideModeReturnWithStatus "error" Integer
n Handle
h Doc OutputAnnotation
e

iPrintWithStatus :: String -> String -> Idris ()
iPrintWithStatus :: String -> String -> Idris ()
iPrintWithStatus status :: String
status s :: String
s = do
  IState
i <- Idris IState
getIState
  case IState -> OutputMode
idris_outputmode IState
i of
    RawOutput h :: Handle
h -> case String
s of
      "" -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      s :: String
s  -> IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
h String
s
    IdeMode n :: Integer
n h :: Handle
h ->
      let good :: SExp
good = [SExp] -> SExp
SexpList [String -> SExp
SymbolAtom String
status, String -> SExp
forall a. SExpable a => a -> SExp
toSExp String
s] in
      IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
h (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> SExp -> Integer -> String
forall a. SExpable a => String -> a -> Integer -> String
convSExp "return" SExp
good Integer
n


iPrintResult :: String -> Idris ()
iPrintResult :: String -> Idris ()
iPrintResult = String -> String -> Idris ()
iPrintWithStatus "ok"

iPrintError :: String -> Idris ()
iPrintError :: String -> Idris ()
iPrintError = String -> String -> Idris ()
iPrintWithStatus "error"

iputStrLn :: String -> Idris ()
iputStrLn :: String -> Idris ()
iputStrLn s :: String
s = do IState
i <- Idris IState
getIState
                 case IState -> OutputMode
idris_outputmode IState
i of
                   RawOutput h :: Handle
h  -> IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
h String
s
                   IdeMode n :: Integer
n h :: Handle
h -> IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (String -> IO ()) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> String -> Integer -> String
forall a. SExpable a => String -> a -> Integer -> String
convSExp "write-string" String
s Integer
n

iputStr :: String -> Idris ()
iputStr :: String -> Idris ()
iputStr s :: String
s = do IState
i <- Idris IState
getIState
               case IState -> OutputMode
idris_outputmode IState
i of
                   RawOutput h :: Handle
h  -> IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStr Handle
h String
s
                   IdeMode n :: Integer
n h :: Handle
h -> IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (String -> IO ()) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStr Handle
h (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> String -> Integer -> String
forall a. SExpable a => String -> a -> Integer -> String
convSExp "write-string" String
s Integer
n

idemodePutSExp :: SExpable a => String -> a -> Idris ()
idemodePutSExp :: String -> a -> Idris ()
idemodePutSExp cmd :: String
cmd info :: a
info = do IState
i <- Idris IState
getIState
                             case IState -> OutputMode
idris_outputmode IState
i of
                               IdeMode n :: Integer
n h :: Handle
h ->
                                 IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (String -> IO ()) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$
                                   String -> a -> Integer -> String
forall a. SExpable a => String -> a -> Integer -> String
convSExp String
cmd a
info Integer
n
                               _ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- TODO: send structured output similar to the metavariable list
iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
iputGoal g :: SimpleDoc OutputAnnotation
g = do IState
i <- Idris IState
getIState
                case IState -> OutputMode
idris_outputmode IState
i of
                  RawOutput h :: Handle
h -> Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()
hWriteDoc Handle
h IState
i SimpleDoc OutputAnnotation
g
                  IdeMode n :: Integer
n h :: Handle
h ->
                    let (str :: String
str, spans :: SpanList OutputAnnotation
spans) = SimpleDoc OutputAnnotation -> (String, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (String, SpanList a)
displaySpans (SimpleDoc OutputAnnotation -> (String, SpanList OutputAnnotation))
-> (SimpleDoc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> SimpleDoc OutputAnnotation
-> (String, SpanList OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OutputAnnotation -> OutputAnnotation)
-> SimpleDoc OutputAnnotation -> SimpleDoc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
i Bool
True) (SimpleDoc OutputAnnotation -> (String, SpanList OutputAnnotation))
-> SimpleDoc OutputAnnotation
-> (String, SpanList OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ SimpleDoc OutputAnnotation
g
                        goal :: [SExp]
goal = [String -> SExp
forall a. SExpable a => a -> SExp
toSExp String
str, SpanList OutputAnnotation -> SExp
forall a. SExpable a => a -> SExp
toSExp SpanList OutputAnnotation
spans]
                    in IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (String -> IO ()) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> [SExp] -> Integer -> String
forall a. SExpable a => String -> a -> Integer -> String
convSExp "write-goal" [SExp]
goal Integer
n

-- | Warn about totality problems without failing to compile
warnTotality :: Idris ()
warnTotality :: Idris ()
warnTotality = do IState
ist <- Idris IState
getIState
                  ((FC, String) -> Idris ()) -> [(FC, String)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IState -> (FC, String) -> Idris ()
warn IState
ist) ([(FC, String)] -> [(FC, String)]
forall a. Eq a => [a] -> [a]
nub (IState -> [(FC, String)]
idris_totcheckfail IState
ist))
  where warn :: IState -> (FC, String) -> Idris ()
warn ist :: IState
ist (fc :: FC
fc, e :: String
e) = FC -> Doc OutputAnnotation -> Idris ()
iWarn FC
fc (IState -> Err -> Doc OutputAnnotation
pprintErr IState
ist (String -> Err
forall t. String -> Err' t
Msg String
e))


printUndefinedNames :: [Name] -> Doc OutputAnnotation
printUndefinedNames :: [Name] -> Doc OutputAnnotation
printUndefinedNames ns :: [Name]
ns = String -> Doc OutputAnnotation
forall a. String -> Doc a
text "Undefined " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
names Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text "."
  where names :: Doc OutputAnnotation
names = Doc OutputAnnotation
-> Doc OutputAnnotation
-> Doc OutputAnnotation
-> [Doc OutputAnnotation]
-> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a -> [Doc a] -> Doc a
encloseSep Doc OutputAnnotation
forall a. Doc a
empty Doc OutputAnnotation
forall a. Doc a
empty (Char -> Doc OutputAnnotation
forall a. Char -> Doc a
char ',') ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ (Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc OutputAnnotation
ppName [Name]
ns
        ppName :: Name -> Doc OutputAnnotation
ppName = Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True []


prettyDocumentedIst :: IState
                    -> (Name, PTerm, Maybe (Docstring DocTerm))
                    -> Doc OutputAnnotation
prettyDocumentedIst :: IState
-> (Name, PTerm, Maybe (Docstring DocTerm)) -> Doc OutputAnnotation
prettyDocumentedIst ist :: IState
ist (name :: Name
name, ty :: PTerm
ty, docs :: Maybe (Docstring DocTerm)
docs) =
          Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True [] Name
name Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
ist PTerm
ty) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
          Doc OutputAnnotation
-> Maybe (Doc OutputAnnotation) -> Doc OutputAnnotation
forall a. a -> Maybe a -> a
fromMaybe Doc OutputAnnotation
forall a. Doc a
empty ((Docstring DocTerm -> Doc OutputAnnotation)
-> Maybe (Docstring DocTerm) -> Maybe (Doc OutputAnnotation)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\d :: Docstring DocTerm
d -> (DocTerm -> String -> Doc OutputAnnotation)
-> Docstring DocTerm -> Doc OutputAnnotation
forall a.
(a -> String -> Doc OutputAnnotation)
-> Docstring a -> Doc OutputAnnotation
renderDocstring ((Term -> Doc OutputAnnotation)
-> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation
renderDocTerm Term -> Doc OutputAnnotation
ppTm Term -> Term
norm) Docstring DocTerm
d Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line) Maybe (Docstring DocTerm)
docs)
  where ppTm :: Term -> Doc OutputAnnotation
ppTm = IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist
        norm :: Term -> Term
norm = Context -> Env -> Term -> Term
normaliseAll (IState -> Context
tt_ctxt IState
ist) []

sendParserHighlighting :: Idris ()
sendParserHighlighting :: Idris ()
sendParserHighlighting =
  do IState
ist <- Idris IState
getIState
     let hs :: Set (FC', OutputAnnotation)
hs = IState -> Set (FC', OutputAnnotation)
idris_parserHighlights IState
ist
     Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
hs
     IState
ist <- Idris IState
getIState
     IState -> Idris ()
putIState IState
ist {idris_parserHighlights :: Set (FC', OutputAnnotation)
idris_parserHighlights = Set (FC', OutputAnnotation)
forall a. Set a
S.empty}

sendHighlighting :: S.Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting :: Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting highlights :: Set (FC', OutputAnnotation)
highlights =
  do IState
ist <- Idris IState
getIState
     case IState -> OutputMode
idris_outputmode IState
ist of
       RawOutput _ -> (IState -> IState) -> Idris ()
updateIState ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$
                      \ist :: IState
ist -> IState
ist { idris_highlightedRegions :: Set (FC', OutputAnnotation)
idris_highlightedRegions =
                                      Set (FC', OutputAnnotation)
-> Set (FC', OutputAnnotation) -> Set (FC', OutputAnnotation)
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (FC', OutputAnnotation)
highlights (IState -> Set (FC', OutputAnnotation)
idris_highlightedRegions IState
ist) }
       IdeMode n :: Integer
n h :: Handle
h ->
         let fancier :: [SExp]
fancier = [ (FC, OutputAnnotation) -> SExp
forall a. SExpable a => a -> SExp
toSExp (FC
fc, IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
False OutputAnnotation
annot)
                       | (FC' fc :: FC
fc, annot :: OutputAnnotation
annot) <- Set (FC', OutputAnnotation) -> [(FC', OutputAnnotation)]
forall a. Set a -> [a]
S.toList Set (FC', OutputAnnotation)
highlights, FC -> Bool
fullFC FC
fc
                       ] in
            case [SExp]
fancier of
              [] -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              _  -> IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (String -> IO ()) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$
                      String -> (SExp, (SExp, [SExp])) -> Integer -> String
forall a. SExpable a => String -> a -> Integer -> String
convSExp "output"
                               (String -> SExp
SymbolAtom "ok",
                                (String -> SExp
SymbolAtom "highlight-source", [SExp]
fancier)) Integer
n

  where fullFC :: FC -> Bool
fullFC (FC _ _ _) = Bool
True
        fullFC _          = Bool
False

-- | Write the highlighting information to a file, for use in external tools
-- or in editors that don't support the IDE protocol
writeHighlights :: FilePath -> Idris ()
writeHighlights :: String -> Idris ()
writeHighlights f :: String
f =
  do IState
ist <- Idris IState
getIState
     let hs :: [(FC, OutputAnnotation)]
hs = [(FC, OutputAnnotation)] -> [(FC, OutputAnnotation)]
forall a. [a] -> [a]
reverse ([(FC, OutputAnnotation)] -> [(FC, OutputAnnotation)])
-> [(FC, OutputAnnotation)] -> [(FC, OutputAnnotation)]
forall a b. (a -> b) -> a -> b
$ ((FC', OutputAnnotation) -> (FC, OutputAnnotation))
-> [(FC', OutputAnnotation)] -> [(FC, OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\(FC' a :: FC
a, b :: OutputAnnotation
b) -> (FC
a,OutputAnnotation
b)) ([(FC', OutputAnnotation)] -> [(FC, OutputAnnotation)])
-> [(FC', OutputAnnotation)] -> [(FC, OutputAnnotation)]
forall a b. (a -> b) -> a -> b
$ Set (FC', OutputAnnotation) -> [(FC', OutputAnnotation)]
forall a. Set a -> [a]
S.toList (IState -> Set (FC', OutputAnnotation)
idris_highlightedRegions IState
ist)
     let hfile :: String
hfile = String -> String -> String
replaceExtension String
f "idh"
     let annots :: SExp
annots = [(FC, OutputAnnotation)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [ (FC
fc, IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
False OutputAnnotation
annot)
                         | (fc :: FC
fc@(FC _ _ _), annot :: OutputAnnotation
annot) <- [(FC, OutputAnnotation)]
hs
                         ]
     IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile String
hfile (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SExp -> String
sExpToString SExp
annots

clearHighlights :: Idris ()
clearHighlights :: Idris ()
clearHighlights = (IState -> IState) -> Idris ()
updateIState ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$ \ist :: IState
ist -> IState
ist { idris_highlightedRegions :: Set (FC', OutputAnnotation)
idris_highlightedRegions = Set (FC', OutputAnnotation)
forall a. Set a
S.empty }

renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
renderExternal fmt :: OutputFmt
fmt width :: Int
width doc :: Doc OutputAnnotation
doc
  | Int
width Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = Err -> Idris String
forall a. Err -> Idris a
throwError (Err -> Idris String) -> (String -> Err) -> String -> Idris String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Idris String) -> String -> Idris String
forall a b. (a -> b) -> a -> b
$ "There must be at least one column for the pretty-printer."
  | Bool
otherwise =
    do IState
ist <- Idris IState
getIState
       String -> Idris String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Idris String)
-> (Doc OutputAnnotation -> String)
-> Doc OutputAnnotation
-> Idris String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputFmt -> String -> String
wrap OutputFmt
fmt (String -> String)
-> (Doc OutputAnnotation -> String)
-> Doc OutputAnnotation
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
         (OutputAnnotation -> String -> String)
-> SimpleDoc OutputAnnotation -> String
forall a. (a -> String -> String) -> SimpleDoc a -> String
displayDecorated (OutputFmt -> OutputAnnotation -> String -> String
decorate OutputFmt
fmt) (SimpleDoc OutputAnnotation -> String)
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
         Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty 1.0 Int
width (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> SimpleDoc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
         (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation -> Idris String)
-> Doc OutputAnnotation -> Idris String
forall a b. (a -> b) -> a -> b
$
           Doc OutputAnnotation
doc
  where
    decorate :: OutputFmt -> OutputAnnotation -> String -> String
decorate _ (AnnFC _) = String -> String
forall a. a -> a
id

    decorate HTMLOutput (AnnName _ (Just TypeOutput) d :: Maybe String
d _) =
      String -> Maybe String -> String -> String
tag "idris-type" Maybe String
d
    decorate HTMLOutput (AnnName _ (Just FunOutput) d :: Maybe String
d _) =
      String -> Maybe String -> String -> String
tag "idris-function" Maybe String
d
    decorate HTMLOutput (AnnName _ (Just DataOutput) d :: Maybe String
d _) =
      String -> Maybe String -> String -> String
tag "idris-data" Maybe String
d
    decorate HTMLOutput (AnnName _ (Just MetavarOutput) d :: Maybe String
d _) =
      String -> Maybe String -> String -> String
tag "idris-metavar" Maybe String
d
    decorate HTMLOutput (AnnName _ (Just PostulateOutput) d :: Maybe String
d _) =
      String -> Maybe String -> String -> String
tag "idris-postulate" Maybe String
d
    decorate HTMLOutput (AnnName _ _ _ _) = String -> String
forall a. a -> a
id
    decorate HTMLOutput (AnnBoundName _ True) = String -> Maybe String -> String -> String
tag "idris-bound idris-implicit" Maybe String
forall a. Maybe a
Nothing
    decorate HTMLOutput (AnnBoundName _ False) = String -> Maybe String -> String -> String
tag "idris-bound" Maybe String
forall a. Maybe a
Nothing
    decorate HTMLOutput (AnnConst c :: Const
c) =
      String -> Maybe String -> String -> String
tag (if Const -> Bool
constIsType Const
c then "idris-type" else "idris-data")
          (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Const -> String
constDocs Const
c)
    decorate HTMLOutput (AnnData _ _) = String -> Maybe String -> String -> String
tag "idris-data" Maybe String
forall a. Maybe a
Nothing
    decorate HTMLOutput (AnnType _ _) = String -> Maybe String -> String -> String
tag "idris-type" Maybe String
forall a. Maybe a
Nothing
    decorate HTMLOutput AnnKeyword = String -> Maybe String -> String -> String
tag "idris-keyword" Maybe String
forall a. Maybe a
Nothing
    decorate HTMLOutput (AnnTextFmt fmt :: TextFormatting
fmt) =
      case TextFormatting
fmt of
        BoldText -> String -> String -> String
mkTag "strong"
        ItalicText -> String -> String -> String
mkTag "em"
        UnderlineText -> String -> Maybe String -> String -> String
tag "idris-underlined" Maybe String
forall a. Maybe a
Nothing
      where mkTag :: String -> String -> String
mkTag t :: String
t x :: String
x = "<"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
tString -> String -> String
forall a. [a] -> [a] -> [a]
++">"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
xString -> String -> String
forall a. [a] -> [a] -> [a]
++"</"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
tString -> String -> String
forall a. [a] -> [a] -> [a]
++">"
    decorate HTMLOutput (AnnTerm _ _) = String -> String
forall a. a -> a
id
    decorate HTMLOutput (AnnSearchResult _) = String -> String
forall a. a -> a
id
    decorate HTMLOutput (AnnErr _) = String -> String
forall a. a -> a
id
    decorate HTMLOutput (AnnNamespace _ _) = String -> String
forall a. a -> a
id
    decorate HTMLOutput (AnnLink url :: String
url) =
      \txt :: String
txt -> "<a href=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
url String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\">" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
txt String -> String -> String
forall a. [a] -> [a] -> [a]
++ "</a>"
    decorate HTMLOutput AnnQuasiquote = String -> String
forall a. a -> a
id
    decorate HTMLOutput AnnAntiquote = String -> String
forall a. a -> a
id
    decorate HTMLOutput (AnnSyntax c :: String
c) = \txt :: String
txt -> String
c

    decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
      String -> String -> String
latex "IdrisType"
    decorate LaTeXOutput (AnnName _ (Just FunOutput) _ _) =
      String -> String -> String
latex "IdrisFunction"
    decorate LaTeXOutput (AnnName _ (Just DataOutput) _ _) =
      String -> String -> String
latex "IdrisData"
    decorate LaTeXOutput (AnnName _ (Just MetavarOutput) _ _) =
      String -> String -> String
latex "IdrisMetavar"
    decorate LaTeXOutput (AnnName _ (Just PostulateOutput) _ _) =
      String -> String -> String
latex "IdrisPostulate"
    decorate LaTeXOutput (AnnName _ _ _ _) = String -> String
forall a. a -> a
id
    decorate LaTeXOutput (AnnBoundName _ True) = String -> String -> String
latex "IdrisImplicit"
    decorate LaTeXOutput (AnnBoundName _ False) = String -> String -> String
latex "IdrisBound"
    decorate LaTeXOutput (AnnConst c :: Const
c) =
      String -> String -> String
latex (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$ if Const -> Bool
constIsType Const
c then "IdrisType" else "IdrisData"
    decorate LaTeXOutput (AnnData _ _) = String -> String -> String
latex "IdrisData"
    decorate LaTeXOutput (AnnType _ _) = String -> String -> String
latex "IdrisType"
    decorate LaTeXOutput AnnKeyword = String -> String -> String
latex "IdrisKeyword"
    decorate LaTeXOutput (AnnTextFmt fmt :: TextFormatting
fmt) =
      case TextFormatting
fmt of
        BoldText -> String -> String -> String
latex "textbf"
        ItalicText -> String -> String -> String
latex "emph"
        UnderlineText -> String -> String -> String
latex "underline"
    decorate LaTeXOutput (AnnTerm _ _) = String -> String
forall a. a -> a
id
    decorate LaTeXOutput (AnnSearchResult _) = String -> String
forall a. a -> a
id
    decorate LaTeXOutput (AnnErr _) = String -> String
forall a. a -> a
id
    decorate LaTeXOutput (AnnNamespace _ _) = String -> String
forall a. a -> a
id
    decorate LaTeXOutput (AnnLink url :: String
url) = (String -> String -> String
forall a. [a] -> [a] -> [a]
++ "(\\url{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
url String -> String -> String
forall a. [a] -> [a] -> [a]
++ "})")
    decorate LaTeXOutput AnnQuasiquote = String -> String
forall a. a -> a
id
    decorate LaTeXOutput AnnAntiquote = String -> String
forall a. a -> a
id
    decorate LaTeXOutput (AnnSyntax c :: String
c) = \txt :: String
txt ->
      case String
c of
        "\\" -> "\\textbackslash"
        "{" -> "\\{"
        "}" -> "\\}"
        "%" -> "\\%"
        _ -> String
c

    tag :: String -> Maybe String -> String -> String
tag cls :: String
cls docs :: Maybe String
docs str :: String
str = "<span class=\""String -> String -> String
forall a. [a] -> [a] -> [a]
++String
clsString -> String -> String
forall a. [a] -> [a] -> [a]
++"\""String -> String -> String
forall a. [a] -> [a] -> [a]
++String
titleString -> String -> String
forall a. [a] -> [a] -> [a]
++">" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ "</span>"
      where title :: String
title = String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" (\d :: String
d->" title=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\"") Maybe String
docs

    latex :: String -> String -> String
latex cmd :: String
cmd str :: String
str = "\\"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
cmdString -> String -> String
forall a. [a] -> [a] -> [a]
++"{"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
strString -> String -> String
forall a. [a] -> [a] -> [a]
++"}"

    wrap :: OutputFmt -> String -> String
wrap HTMLOutput str :: String
str =
      "<!doctype html><html><head><style>" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
css String -> String -> String
forall a. [a] -> [a] -> [a]
++ "</style></head>" String -> String -> String
forall a. [a] -> [a] -> [a]
++
      "<body><!-- START CODE --><pre>" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ "</pre><!-- END CODE --></body></html>"
      where css :: String
css = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
                    [".idris-data { color: red; } ",
                     ".idris-type { color: blue; }",
                     ".idris-function {color: green; }",
                     ".idris-metavar {color: turquoise; }",
                     ".idris-keyword { font-weight: bold; }",
                     ".idris-bound { color: purple; }",
                     ".idris-implicit { font-style: italic; }",
                     ".idris-underlined { text-decoration: underline; }"]
    wrap LaTeXOutput str :: String
str =
      [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
        ["\\documentclass{article}",
         "\\usepackage{fancyvrb}",
         "\\usepackage[usenames]{xcolor}"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
        ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(cmd :: String
cmd, color :: String
color) ->
               "\\newcommand{\\"String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cmd String -> String -> String
forall a. [a] -> [a] -> [a]
++
               "}[1]{\\textcolor{"String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
color String -> String -> String
forall a. [a] -> [a] -> [a]
++"}{#1}}")
             [("IdrisData", "red"), ("IdrisType", "blue"),
              ("IdrisBound", "magenta"), ("IdrisFunction", "green"),
              ("IdrisMetavar", "cyan")] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
        ["\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",
         "\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",
         "\n",
         "\\begin{document}",
         "% START CODE",
         "\\begin{Verbatim}[commandchars=\\\\\\{\\}]",
         String
str,
         "\\end{Verbatim}",
         "% END CODE",
         "\\end{document}"]