{-# 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"
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)
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
ideModeReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideModeReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideModeReturnAnnotated = String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideModeReturnWithStatus "ok"
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 ()
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
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
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}"]