{-# 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 Data.List (intersperse, nub)
import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)
import qualified Data.Set as S
import System.FilePath (replaceExtension)
import System.IO (Handle, hPutStr, hPutStrLn)
import System.IO.Error (tryIOError)
pshow :: IState -> Err -> String
pshow :: IState -> Err -> String
pshow IState
ist 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 Float
1.0 Int
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 a b. (a -> b) -> Doc a -> Doc b
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 FC
extent Doc OutputAnnotation
_) = FC
extent
messageText :: SimpleWarning -> Doc OutputAnnotation
messageText (SimpleWarning FC
_ Doc OutputAnnotation
msg) = Doc OutputAnnotation
msg
messageSource :: SimpleWarning -> Maybe String
messageSource SimpleWarning
_ = Maybe String
forall a. Maybe a
Nothing
formatMessage :: Message w => w -> Idris OutputDoc
formatMessage :: forall w. Message w => w -> Idris (Doc OutputAnnotation)
formatMessage 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 String
src -> String -> Maybe String
forall a. a -> Maybe a
Just String
src
Maybe String
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 a b. Maybe a -> (a -> Maybe b) -> Maybe b
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 a. a -> StateT IState (ExceptT Err IO) a
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 Set (FC', OutputAnnotation)
rs = ((FC', OutputAnnotation) -> (FC, OutputAnnotation))
-> [(FC', OutputAnnotation)] -> [(FC, OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\(FC' FC
a,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 String
fn (Int, Int)
_ (Int, Int)
_) | String
fn String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"" = 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 FC
_ = Doc OutputAnnotation
forall a. Doc a
empty
readSource :: FC -> Idris (Maybe String)
readSource :: FC -> Idris (Maybe String)
readSource (FC String
fn (Int, Int)
_ (Int, Int)
_) = 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 IOError
_ -> Maybe String -> Idris (Maybe String)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
Right String
v -> Maybe String -> Idris (Maybe String)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe String
forall a. a -> Maybe a
Just String
v)
readSource FC
_ = Maybe String -> Idris (Maybe String)
forall a. a -> StateT IState (ExceptT Err IO) a
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 String
fn (Int
si, Int
sj) (Int
ei, Int
ej)) [(FC, OutputAnnotation)]
highlights 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
- Int
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]
++ [String
"<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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> String
forall a. Show a => a -> String
show Int
si)) Char
' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" |"
lineFC :: FC
lineFC :: FC
lineFC = String -> (Int, Int) -> (Int, Int) -> FC
FC String
fn (Int
si, Int
1) (Int
si, String -> Int
forall a. [a] -> 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 String
fn1 (Int, Int)
s1 (Int, Int)
e1) (FC String
fn2 (Int, Int)
s2 (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 FC
_ FC
_ = Bool
False
intersection :: FC -> FC -> FC
intersection :: FC -> FC -> FC
intersection fc1 :: FC
fc1@(FC String
fn1 (Int, Int)
s1 (Int, Int)
e1) fc2 :: FC
fc2@(FC String
_ (Int, Int)
s2 (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
_ FC
_ = FC
NoFC
width :: Ann -> Int
width :: Ann -> Int
width (AText String
s) = String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s
width (ATagged OutputAnnotation
_ Ann
n) = Ann -> Int
width Ann
n
width (ASplit Ann
l 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 String
s) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
s
sourceDoc (ATagged OutputAnnotation
a 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 Ann
l 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 ((Int
sj, Int
ej), OutputAnnotation
oa) (ATagged OutputAnnotation
tag Ann
n) = OutputAnnotation -> Ann -> Ann
ATagged OutputAnnotation
tag (((Int, Int), OutputAnnotation) -> Ann -> Ann
insertAnnotation ((Int
sj, Int
ej), OutputAnnotation
oa) Ann
n)
insertAnnotation ((Int
sj, Int
ej), OutputAnnotation
oa) (ASplit Ann
l 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 ((Int
sj, Int
ej), OutputAnnotation
oa) a :: Ann
a@(AText String
t)
| Int
sj Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
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
> Int
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
- Int
1) String
t) (((Int, Int), OutputAnnotation) -> Ann -> Ann
insertAnnotation ((Int
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
+ Int
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
- Int
1) String
t))
| Int
sj Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1, Int
ej Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
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 ((Int
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 a b. (a -> b -> b) -> b -> [a] -> b
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 String
_ (Int
_, Int
sj) (Int
_, Int
ej), 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 b c d. (b -> c) -> (b, d) -> (c, d)
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]
++ String
" | ") 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
+ Int
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
(Int
end, Char
ch, 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
(Bool
True , Bool
True ) -> (Int
ej, Char
'^', Doc a
forall a. Doc a
empty)
(Bool
True , Bool
False) -> (Int
ej, Char
'~', Doc a
forall a. Doc a
empty)
(Bool
False, Bool
_ ) -> (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
sourceLine), Char
'~', String -> Doc a
forall a. String -> Doc a
text String
" ...")
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 Char
' ') 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 FC
_ [(FC, OutputAnnotation)]
_ String
_ = 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 Doc OutputAnnotation
loc (Just Doc OutputAnnotation
src) 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 Doc OutputAnnotation
loc Maybe (Doc OutputAnnotation)
Nothing 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 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 :: forall w. Message w => w -> Idris ()
emitWarning w
w =
do IState
i <- Idris IState
getIState
case IState -> OutputMode
idris_outputmode IState
i of
RawOutput 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 a b. (a -> b) -> Doc a -> Doc b
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 Integer
n 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 a b. (a -> b) -> Doc a -> Doc b
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 (String
str, 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 String
"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 :: forall a. Doc a -> Idris (SimpleDoc a)
iRender 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 Integer
_ Handle
_ -> Bool
True
OutputMode
_ -> Bool
False
Bool
tty <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO IO Bool
isATTY
case ConsoleWidth
w of
ConsoleWidth
InfinitelyWide -> SimpleDoc a -> Idris (SimpleDoc a)
forall a. a -> StateT IState (ExceptT Err IO) 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 Float
1.0 Int
1000000000 Doc a
d
ColsWide Int
n -> SimpleDoc a -> Idris (SimpleDoc a)
forall a. a -> StateT IState (ExceptT Err IO) 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
< Int
1
then Float -> Int -> Doc a -> SimpleDoc a
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
1000000000 Doc a
d
else Float -> Int -> Doc a -> SimpleDoc a
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.8 Int
n Doc a
d
ConsoleWidth
AutomaticWidth | Bool
ideMode Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
tty -> SimpleDoc a -> Idris (SimpleDoc a)
forall a. a -> StateT IState (ExceptT Err IO) 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 Float
1.0 Int
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 a. a -> StateT IState (ExceptT Err IO) 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 Float
0.8 Int
width Doc a
d
hWriteDoc :: Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()
hWriteDoc :: Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()
hWriteDoc Handle
h IState
ist 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 a. a -> IO a
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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Handle -> IdrisColour -> IO ()
hEndColourise Handle
h))
((OutputAnnotation -> Maybe IdrisColour)
-> SimpleDoc OutputAnnotation -> SimpleDoc (Maybe IdrisColour)
forall a b. (a -> b) -> SimpleDoc a -> SimpleDoc b
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 String
"\n"
consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
consoleDisplayAnnotated Handle
h 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 Doc OutputAnnotation
tm 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 [(Name, Bool)]
bnd Name
n [] = String -> Idris ()
iPrintError (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"No such variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
iPrintFunTypes [(Name, Bool)]
bnd Name
n [(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 PPOption
ppo Name
n | [(Name, Doc OutputAnnotation)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Doc OutputAnnotation)]
overloads Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
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 PPOption
ppo p
infixes Name
n 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 OutputAnnotation
doc =
do IState
i <- Idris IState
getIState
case IState -> OutputMode
idris_outputmode IState
i of
RawOutput 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 Integer
n Handle
h ->
do (String
str, SpanList OutputAnnotation
spans) <- (SimpleDoc OutputAnnotation -> (String, SpanList OutputAnnotation))
-> Idris (SimpleDoc OutputAnnotation)
-> StateT
IState (ExceptT Err IO) (String, SpanList OutputAnnotation)
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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 a b. (a -> b) -> Doc a -> Doc b
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 String
"write-decorated" [SExp]
out Integer
n
iRenderResult :: Doc OutputAnnotation -> Idris ()
iRenderResult :: Doc OutputAnnotation -> Idris ()
iRenderResult Doc OutputAnnotation
d = do IState
ist <- Idris IState
getIState
case IState -> OutputMode
idris_outputmode IState
ist of
RawOutput Handle
h -> Handle -> Doc OutputAnnotation -> Idris ()
consoleDisplayAnnotated Handle
h Doc OutputAnnotation
d
IdeMode Integer
n 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 String
status Integer
n Handle
h Doc OutputAnnotation
out = do
IState
ist <- Idris IState
getIState
(String
str, SpanList OutputAnnotation
spans) <- (SimpleDoc OutputAnnotation -> (String, SpanList OutputAnnotation))
-> Idris (SimpleDoc OutputAnnotation)
-> StateT
IState (ExceptT Err IO) (String, SpanList OutputAnnotation)
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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 a b. (a -> b) -> Doc a -> Doc b
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 String
"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 String
"ok"
iRenderError :: Doc OutputAnnotation -> Idris ()
iRenderError :: Doc OutputAnnotation -> Idris ()
iRenderError Doc OutputAnnotation
e = do IState
ist <- Idris IState
getIState
case IState -> OutputMode
idris_outputmode IState
ist of
RawOutput Handle
h -> Handle -> Doc OutputAnnotation -> Idris ()
consoleDisplayAnnotated Handle
h Doc OutputAnnotation
e
IdeMode Integer
n Handle
h -> String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideModeReturnWithStatus String
"error" Integer
n Handle
h Doc OutputAnnotation
e
iPrintWithStatus :: String -> String -> Idris ()
iPrintWithStatus :: String -> String -> Idris ()
iPrintWithStatus String
status String
s = do
IState
i <- Idris IState
getIState
case IState -> OutputMode
idris_outputmode IState
i of
RawOutput Handle
h -> case String
s of
String
"" -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
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 Integer
n 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 String
"return" SExp
good Integer
n
iPrintResult :: String -> Idris ()
iPrintResult :: String -> Idris ()
iPrintResult = String -> String -> Idris ()
iPrintWithStatus String
"ok"
iPrintError :: String -> Idris ()
iPrintError :: String -> Idris ()
iPrintError = String -> String -> Idris ()
iPrintWithStatus String
"error"
iputStrLn :: String -> Idris ()
iputStrLn :: String -> Idris ()
iputStrLn String
s = do IState
i <- Idris IState
getIState
case IState -> OutputMode
idris_outputmode IState
i of
RawOutput 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 Integer
n 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 String
"write-string" String
s Integer
n
iputStr :: String -> Idris ()
iputStr :: String -> Idris ()
iputStr String
s = do IState
i <- Idris IState
getIState
case IState -> OutputMode
idris_outputmode IState
i of
RawOutput 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 Integer
n 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 String
"write-string" String
s Integer
n
idemodePutSExp :: SExpable a => String -> a -> Idris ()
idemodePutSExp :: forall a. SExpable a => String -> a -> Idris ()
idemodePutSExp String
cmd a
info = do IState
i <- Idris IState
getIState
case IState -> OutputMode
idris_outputmode IState
i of
IdeMode Integer
n 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
OutputMode
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
iputGoal SimpleDoc OutputAnnotation
g = do IState
i <- Idris IState
getIState
case IState -> OutputMode
idris_outputmode IState
i of
RawOutput Handle
h -> Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()
hWriteDoc Handle
h IState
i SimpleDoc OutputAnnotation
g
IdeMode Integer
n Handle
h ->
let (String
str, 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 a b. (a -> b) -> SimpleDoc a -> SimpleDoc b
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 String
"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 IState
ist (FC
fc, 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 [Name]
ns = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"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 String
"."
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 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 IState
ist (Name
name, PTerm
ty, 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 a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\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 = S.empty}
sendHighlighting :: S.Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting :: Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights =
do IState
ist <- Idris IState
getIState
case IState -> OutputMode
idris_outputmode IState
ist of
RawOutput Handle
_ -> (IState -> IState) -> Idris ()
updateIState ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$
\IState
ist -> IState
ist { idris_highlightedRegions =
S.union highlights (idris_highlightedRegions ist) }
IdeMode Integer
n 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, 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 a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[SExp]
_ -> 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 String
"output"
(String -> SExp
SymbolAtom String
"ok",
(String -> SExp
SymbolAtom String
"highlight-source", [SExp]
fancier)) Integer
n
where fullFC :: FC -> Bool
fullFC (FC String
_ (Int, Int)
_ (Int, Int)
_) = Bool
True
fullFC FC
_ = Bool
False
writeHighlights :: FilePath -> Idris ()
writeHighlights :: String -> Idris ()
writeHighlights 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' FC
a, 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 String
"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 String
_ (Int, Int)
_ (Int, Int)
_), 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
$ \IState
ist -> IState
ist { idris_highlightedRegions = S.empty }
renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
renderExternal OutputFmt
fmt Int
width Doc OutputAnnotation
doc
| Int
width Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
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
$ String
"There must be at least one column for the pretty-printer."
| Bool
otherwise =
do IState
ist <- Idris IState
getIState
String -> Idris String
forall a. a -> StateT IState (ExceptT Err IO) a
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 Float
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 a b. (a -> b) -> Doc a -> Doc b
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 OutputFmt
_ (AnnFC FC
_) = String -> String
forall a. a -> a
id
decorate OutputFmt
HTMLOutput (AnnName Name
_ (Just NameOutput
TypeOutput) Maybe String
d Maybe String
_) =
String -> Maybe String -> String -> String
tag String
"idris-type" Maybe String
d
decorate OutputFmt
HTMLOutput (AnnName Name
_ (Just NameOutput
FunOutput) Maybe String
d Maybe String
_) =
String -> Maybe String -> String -> String
tag String
"idris-function" Maybe String
d
decorate OutputFmt
HTMLOutput (AnnName Name
_ (Just NameOutput
DataOutput) Maybe String
d Maybe String
_) =
String -> Maybe String -> String -> String
tag String
"idris-data" Maybe String
d
decorate OutputFmt
HTMLOutput (AnnName Name
_ (Just NameOutput
MetavarOutput) Maybe String
d Maybe String
_) =
String -> Maybe String -> String -> String
tag String
"idris-metavar" Maybe String
d
decorate OutputFmt
HTMLOutput (AnnName Name
_ (Just NameOutput
PostulateOutput) Maybe String
d Maybe String
_) =
String -> Maybe String -> String -> String
tag String
"idris-postulate" Maybe String
d
decorate OutputFmt
HTMLOutput (AnnName Name
_ Maybe NameOutput
_ Maybe String
_ Maybe String
_) = String -> String
forall a. a -> a
id
decorate OutputFmt
HTMLOutput (AnnBoundName Name
_ Bool
True) = String -> Maybe String -> String -> String
tag String
"idris-bound idris-implicit" Maybe String
forall a. Maybe a
Nothing
decorate OutputFmt
HTMLOutput (AnnBoundName Name
_ Bool
False) = String -> Maybe String -> String -> String
tag String
"idris-bound" Maybe String
forall a. Maybe a
Nothing
decorate OutputFmt
HTMLOutput (AnnConst Const
c) =
String -> Maybe String -> String -> String
tag (if Const -> Bool
constIsType Const
c then String
"idris-type" else String
"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 OutputFmt
HTMLOutput (AnnData String
_ String
_) = String -> Maybe String -> String -> String
tag String
"idris-data" Maybe String
forall a. Maybe a
Nothing
decorate OutputFmt
HTMLOutput (AnnType String
_ String
_) = String -> Maybe String -> String -> String
tag String
"idris-type" Maybe String
forall a. Maybe a
Nothing
decorate OutputFmt
HTMLOutput OutputAnnotation
AnnKeyword = String -> Maybe String -> String -> String
tag String
"idris-keyword" Maybe String
forall a. Maybe a
Nothing
decorate OutputFmt
HTMLOutput (AnnTextFmt TextFormatting
fmt) =
case TextFormatting
fmt of
TextFormatting
BoldText -> String -> String -> String
mkTag String
"strong"
TextFormatting
ItalicText -> String -> String -> String
mkTag String
"em"
TextFormatting
UnderlineText -> String -> Maybe String -> String -> String
tag String
"idris-underlined" Maybe String
forall a. Maybe a
Nothing
where mkTag :: String -> String -> String
mkTag String
t String
x = String
"<"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
tString -> String -> String
forall a. [a] -> [a] -> [a]
++String
">"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
xString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"</"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
tString -> String -> String
forall a. [a] -> [a] -> [a]
++String
">"
decorate OutputFmt
HTMLOutput (AnnTerm [(Name, Bool)]
_ Term
_) = String -> String
forall a. a -> a
id
decorate OutputFmt
HTMLOutput (AnnSearchResult Ordering
_) = String -> String
forall a. a -> a
id
decorate OutputFmt
HTMLOutput (AnnErr Err
_) = String -> String
forall a. a -> a
id
decorate OutputFmt
HTMLOutput (AnnNamespace [Text]
_ Maybe String
_) = String -> String
forall a. a -> a
id
decorate OutputFmt
HTMLOutput (AnnLink String
url) =
\String
txt -> String
"<a href=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
url String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\">" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
txt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"</a>"
decorate OutputFmt
HTMLOutput OutputAnnotation
AnnQuasiquote = String -> String
forall a. a -> a
id
decorate OutputFmt
HTMLOutput OutputAnnotation
AnnAntiquote = String -> String
forall a. a -> a
id
decorate OutputFmt
HTMLOutput (AnnSyntax String
c) = \String
txt -> String
c
decorate OutputFmt
LaTeXOutput (AnnName Name
_ (Just NameOutput
TypeOutput) Maybe String
_ Maybe String
_) =
String -> String -> String
latex String
"IdrisType"
decorate OutputFmt
LaTeXOutput (AnnName Name
_ (Just NameOutput
FunOutput) Maybe String
_ Maybe String
_) =
String -> String -> String
latex String
"IdrisFunction"
decorate OutputFmt
LaTeXOutput (AnnName Name
_ (Just NameOutput
DataOutput) Maybe String
_ Maybe String
_) =
String -> String -> String
latex String
"IdrisData"
decorate OutputFmt
LaTeXOutput (AnnName Name
_ (Just NameOutput
MetavarOutput) Maybe String
_ Maybe String
_) =
String -> String -> String
latex String
"IdrisMetavar"
decorate OutputFmt
LaTeXOutput (AnnName Name
_ (Just NameOutput
PostulateOutput) Maybe String
_ Maybe String
_) =
String -> String -> String
latex String
"IdrisPostulate"
decorate OutputFmt
LaTeXOutput (AnnName Name
_ Maybe NameOutput
_ Maybe String
_ Maybe String
_) = String -> String
forall a. a -> a
id
decorate OutputFmt
LaTeXOutput (AnnBoundName Name
_ Bool
True) = String -> String -> String
latex String
"IdrisImplicit"
decorate OutputFmt
LaTeXOutput (AnnBoundName Name
_ Bool
False) = String -> String -> String
latex String
"IdrisBound"
decorate OutputFmt
LaTeXOutput (AnnConst 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 String
"IdrisType" else String
"IdrisData"
decorate OutputFmt
LaTeXOutput (AnnData String
_ String
_) = String -> String -> String
latex String
"IdrisData"
decorate OutputFmt
LaTeXOutput (AnnType String
_ String
_) = String -> String -> String
latex String
"IdrisType"
decorate OutputFmt
LaTeXOutput OutputAnnotation
AnnKeyword = String -> String -> String
latex String
"IdrisKeyword"
decorate OutputFmt
LaTeXOutput (AnnTextFmt TextFormatting
fmt) =
case TextFormatting
fmt of
TextFormatting
BoldText -> String -> String -> String
latex String
"textbf"
TextFormatting
ItalicText -> String -> String -> String
latex String
"emph"
TextFormatting
UnderlineText -> String -> String -> String
latex String
"underline"
decorate OutputFmt
LaTeXOutput (AnnTerm [(Name, Bool)]
_ Term
_) = String -> String
forall a. a -> a
id
decorate OutputFmt
LaTeXOutput (AnnSearchResult Ordering
_) = String -> String
forall a. a -> a
id
decorate OutputFmt
LaTeXOutput (AnnErr Err
_) = String -> String
forall a. a -> a
id
decorate OutputFmt
LaTeXOutput (AnnNamespace [Text]
_ Maybe String
_) = String -> String
forall a. a -> a
id
decorate OutputFmt
LaTeXOutput (AnnLink String
url) = (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(\\url{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
url String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"})")
decorate OutputFmt
LaTeXOutput OutputAnnotation
AnnQuasiquote = String -> String
forall a. a -> a
id
decorate OutputFmt
LaTeXOutput OutputAnnotation
AnnAntiquote = String -> String
forall a. a -> a
id
decorate OutputFmt
LaTeXOutput (AnnSyntax String
c) = \String
txt ->
case String
c of
String
"\\" -> String
"\\textbackslash"
String
"{" -> String
"\\{"
String
"}" -> String
"\\}"
String
"%" -> String
"\\%"
String
_ -> String
c
tag :: String -> Maybe String -> String -> String
tag String
cls Maybe String
docs String
str = String
"<span class=\""String -> String -> String
forall a. [a] -> [a] -> [a]
++String
clsString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"\""String -> String -> String
forall a. [a] -> [a] -> [a]
++String
titleString -> String -> String
forall a. [a] -> [a] -> [a]
++String
">" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"</span>"
where title :: String
title = String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (\String
d->String
" title=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\"") Maybe String
docs
latex :: String -> String -> String
latex String
cmd String
str = String
"\\"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
cmdString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"{"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
strString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"}"
wrap :: OutputFmt -> String -> String
wrap OutputFmt
HTMLOutput String
str =
String
"<!doctype html><html><head><style>" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
css String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"</style></head>" String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"<body><!-- START CODE --><pre>" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"</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 String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
[String
".idris-data { color: red; } ",
String
".idris-type { color: blue; }",
String
".idris-function {color: green; }",
String
".idris-metavar {color: turquoise; }",
String
".idris-keyword { font-weight: bold; }",
String
".idris-bound { color: purple; }",
String
".idris-implicit { font-style: italic; }",
String
".idris-underlined { text-decoration: underline; }"]
wrap OutputFmt
LaTeXOutput 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 String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
[String
"\\documentclass{article}",
String
"\\usepackage{fancyvrb}",
String
"\\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 (\(String
cmd, String
color) ->
String
"\\newcommand{\\"String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cmd String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"}[1]{\\textcolor{"String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
color String -> String -> String
forall a. [a] -> [a] -> [a]
++String
"}{#1}}")
[(String
"IdrisData", String
"red"), (String
"IdrisType", String
"blue"),
(String
"IdrisBound", String
"magenta"), (String
"IdrisFunction", String
"green"),
(String
"IdrisMetavar", String
"cyan")] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[String
"\\newcommand{\\IdrisKeyword}[1]{{\\underline{#1}}}",
String
"\\newcommand{\\IdrisImplicit}[1]{{\\itshape \\IdrisBound{#1}}}",
String
"\n",
String
"\\begin{document}",
String
"% START CODE",
String
"\\begin{Verbatim}[commandchars=\\\\\\{\\}]",
String
str,
String
"\\end{Verbatim}",
String
"% END CODE",
String
"\\end{document}"]