{-# 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 = forall a. (a -> String -> String) -> SimpleDoc a -> String
displayDecorated (IState -> OutputAnnotation -> String -> String
consoleDecorate IState
ist) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
80 forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) 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
_ = 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 -> forall a. a -> Maybe a
Just String
src
Maybe String
Nothing -> forall a. Message a => a -> Maybe String
messageSource w
w
let maybeFormattedSource :: Maybe (Doc OutputAnnotation)
maybeFormattedSource = Maybe String
maybeSource 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))
forall (m :: * -> *) a. Monad m => a -> m a
return 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 (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 = forall a b. (a -> b) -> [a] -> [b]
map (\(FC' FC
a,OutputAnnotation
b) -> (FC
a, OutputAnnotation
b)) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList Set (FC', OutputAnnotation)
rs
fc :: FC
fc :: FC
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 forall a. Eq a => a -> a -> Bool
/= String
"" = forall a. String -> Doc a
text (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ FC
fc) forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
colon
layoutFC FC
_ = 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 <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ forall a. IO a -> IO (Either IOError a)
tryIOError (String -> IO String
readFile String
fn)
case Either IOError String
result of
Left IOError
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
Right String
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just String
v)
readSource FC
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 forall a. a -> Maybe a
Just Doc OutputAnnotation
source
else forall a. Maybe a
Nothing
where
sourceLine :: Maybe String
sourceLine :: Maybe String
sourceLine = forall a. [a] -> Maybe a
listToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
drop (Int
si forall a. Num a => a -> a -> a
- Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. [a] -> [a] -> [a]
++ [String
"<end of file>"]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines forall a b. (a -> b) -> a -> b
$ String
src
haveSource :: Bool
haveSource :: Bool
haveSource = forall a. Maybe a -> Bool
isJust Maybe String
sourceLine
line1 :: OutputDoc
line1 :: Doc OutputAnnotation
line1 = forall a. String -> Doc a
text forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Show a => a -> String
show Int
si)) Char
' ' 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, forall (t :: * -> *) a. Foldable t => t a -> Int
length (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 forall a. Eq a => a -> a -> Bool
/= String
fn2 = Bool
False
| (Int, Int)
e1 forall a. Ord a => a -> a -> Bool
< (Int, Int)
s2 = Bool
False
| (Int, Int)
e2 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 (forall a. Ord a => a -> a -> a
max (Int, Int)
s1 (Int, Int)
s2) (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) = 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 forall a. Num a => a -> a -> a
+ Ann -> Int
width Ann
r
sourceDoc :: Ann -> OutputDoc
sourceDoc :: Ann -> Doc OutputAnnotation
sourceDoc (AText String
s) = forall a. String -> Doc a
text String
s
sourceDoc (ATagged OutputAnnotation
a Ann
n) = 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 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 forall a. Num a => a -> a -> a
- Int
w, Int
ej 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 forall a. Ord a => a -> a -> Bool
<= Int
1, Int
ej forall a. Ord a => a -> a -> Bool
>= Ann -> Int
width Ann
a = OutputAnnotation -> Ann -> Ann
ATagged OutputAnnotation
oa Ann
a
| Int
sj forall a. Ord a => a -> a -> Bool
> Int
1, Int
sj forall a. Ord a => a -> a -> Bool
<= Ann -> Int
width Ann
a = Ann -> Ann -> Ann
ASplit (String -> Ann
AText forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take (Int
sj forall a. Num a => a -> a -> a
- Int
1) String
t) (((Int, Int), OutputAnnotation) -> Ann -> Ann
insertAnnotation ((Int
1, Int
ej forall a. Num a => a -> a -> a
- Int
sj forall a. Num a => a -> a -> a
+ Int
1), OutputAnnotation
oa) (String -> Ann
AText forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop (Int
sj forall a. Num a => a -> a -> a
- Int
1) String
t))
| Int
sj forall a. Eq a => a -> a -> Bool
== Int
1, Int
ej forall a. Ord a => a -> a -> Bool
>= Int
1, Int
ej 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 forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
ej String
t)) (String -> Ann
AText forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
ej String
t)
| Bool
otherwise = Ann
a
highlightedSource :: OutputDoc
highlightedSource :: Doc OutputAnnotation
highlightedSource = Ann -> Doc OutputAnnotation
sourceDoc forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Int, Int), OutputAnnotation) -> Ann -> Ann
insertAnnotation (String -> Ann
AText forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
sourceLine) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a b. (a -> b) -> [a] -> [b]
map (\(FC String
_ (Int
_, Int
sj) (Int
_, Int
ej), OutputAnnotation
ann) -> ((Int
sj, Int
ej), OutputAnnotation
ann)) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (FC -> FC -> FC
intersection FC
lineFC)) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a. (a -> Bool) -> [a] -> [a]
filter (FC -> FC -> Bool
intersects FC
lineFC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$
[(FC, OutputAnnotation)]
highlights
line2 :: OutputDoc
line2 :: Doc OutputAnnotation
line2 = forall a. String -> Doc a
text (forall a. Show a => a -> String
show Int
si forall a. [a] -> [a] -> [a]
++ String
" | ") forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
highlightedSource
indicator :: OutputDoc
indicator :: Doc OutputAnnotation
indicator = forall a. String -> Doc a
text (forall a. Int -> a -> [a]
replicate (Int
end forall a. Num a => a -> a -> a
- Int
sj forall a. Num a => a -> a -> a
+ Int
1) Char
ch) forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
ellipsis
where
(Int
end, Char
ch, Doc a
ellipsis) = case (Int
si forall a. Eq a => a -> a -> Bool
== Int
ei, Int
sj forall a. Eq a => a -> a -> Bool
== Int
ej) of
(Bool
True , Bool
True ) -> (Int
ej, Char
'^', forall a. Doc a
empty)
(Bool
True , Bool
False) -> (Int
ej, Char
'~', forall a. Doc a
empty)
(Bool
False, Bool
_ ) -> (forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
sourceLine), Char
'~', forall a. String -> Doc a
text String
" ...")
line3 :: OutputDoc
line3 :: Doc OutputAnnotation
line3 = Doc OutputAnnotation
line1 forall a. Doc a -> Doc a -> Doc a
<> forall a. String -> Doc a
text (forall a. Int -> a -> [a]
replicate Int
sj Char
' ') forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
indicator
source :: OutputDoc
source :: Doc OutputAnnotation
source = Doc OutputAnnotation
line1 forall a. Doc a -> Doc a -> Doc a
<$$> Doc OutputAnnotation
line2 forall a. Doc a -> Doc a -> Doc a
<$$> Doc OutputAnnotation
line3
layoutSource FC
_ [(FC, OutputAnnotation)]
_ String
_ = 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 forall a. Doc a -> Doc a -> Doc a
<$$> Doc OutputAnnotation
src forall a. Doc a -> Doc a -> Doc a
<$$> Doc OutputAnnotation
err forall a. Doc a -> Doc a -> Doc a
<$$> forall a. Doc a
empty
layoutMessage Doc OutputAnnotation
loc Maybe (Doc OutputAnnotation)
Nothing Doc OutputAnnotation
err = Doc OutputAnnotation
loc 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 = forall w. Message w => w -> Idris ()
emitWarning 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 <- forall w. Message w => w -> Idris (Doc OutputAnnotation)
formatMessage w
w
SimpleDoc OutputAnnotation
err' <- forall a. Doc a -> Idris (SimpleDoc a)
iRender forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
i Bool
True) 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' <- forall a. Doc a -> Idris (SimpleDoc a)
iRender forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
i Bool
True) forall a b. (a -> b) -> a -> b
$ forall a. Message a => a -> Doc OutputAnnotation
messageText w
w
let fc :: FC
fc = forall a. Message a => a -> FC
messageExtent w
w
let (String
str, SpanList OutputAnnotation
spans) = forall a. SimpleDoc a -> (String, SpanList a)
displaySpans SimpleDoc OutputAnnotation
err'
forall a. IO a -> Idris a
runIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$
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 <- forall a. IO a -> Idris a
runIO IO Bool
isATTY
case ConsoleWidth
w of
ConsoleWidth
InfinitelyWide -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
1000000000 Doc a
d
ColsWide Int
n -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
if Int
n forall a. Ord a => a -> a -> Bool
< Int
1
then forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
1000000000 Doc a
d
else 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
80 Doc a
d
| Bool
otherwise -> do Int
width <- forall a. IO a -> Idris a
runIO IO Int
getScreenWidth
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ 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)
(forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Handle -> IdrisColour -> IO ()
hStartColourise Handle
h))
(forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Handle -> IdrisColour -> IO ()
hEndColourise Handle
h))
(forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> OutputAnnotation -> Maybe IdrisColour
annotationColour IState
ist) SimpleDoc OutputAnnotation
rendered)
forall a. IO a -> Idris a
runIO 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 <- 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 forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+> 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 forall a b. (a -> b) -> a -> b
$ String
"No such variable " forall a. [a] -> [a] -> [a]
++ 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 = forall a. [Doc a] -> Doc a
vsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (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 | forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Doc OutputAnnotation)]
overloads 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 forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+> 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 <- 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) <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. SimpleDoc a -> (String, SpanList a)
displaySpans forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Idris (SimpleDoc a)
iRender forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
i Bool
True) forall a b. (a -> b) -> a -> b
$ Doc OutputAnnotation
doc
let out :: [SExp]
out = [forall a. SExpable a => a -> SExp
toSExp String
str, forall a. SExpable a => a -> SExp
toSExp SpanList OutputAnnotation
spans]
forall a. IO a -> Idris a
runIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ 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) <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. SimpleDoc a -> (String, SpanList a)
displaySpans forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a. Doc a -> Idris (SimpleDoc a)
iRender forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) forall a b. (a -> b) -> a -> b
$
Doc OutputAnnotation
out
let good :: [SExp]
good = [String -> SExp
SymbolAtom String
status, forall a. SExpable a => a -> SExp
toSExp String
str, forall a. SExpable a => a -> SExp
toSExp SpanList OutputAnnotation
spans]
forall a. IO a -> Idris a
runIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ 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
"" -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
String
s -> forall a. IO a -> Idris a
runIO 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, forall a. SExpable a => a -> SExp
toSExp String
s] in
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ 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 -> forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
h String
s
IdeMode Integer
n Handle
h -> forall a. IO a -> Idris a
runIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ 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 -> forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStr Handle
h String
s
IdeMode Integer
n Handle
h -> forall a. IO a -> Idris a
runIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ 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 ->
forall a. IO a -> Idris a
runIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$
forall a. SExpable a => String -> a -> Integer -> String
convSExp String
cmd a
info Integer
n
OutputMode
_ -> 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) = forall a. SimpleDoc a -> (String, SpanList a)
displaySpans forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
i Bool
True) forall a b. (a -> b) -> a -> b
$ SimpleDoc OutputAnnotation
g
goal :: [SExp]
goal = [forall a. SExpable a => a -> SExp
toSExp String
str, forall a. SExpable a => a -> SExp
toSExp SpanList OutputAnnotation
spans]
in forall a. IO a -> Idris a
runIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ 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
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IState -> (FC, String) -> Idris ()
warn IState
ist) (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 (forall t. String -> Err' t
Msg String
e))
printUndefinedNames :: [Name] -> Doc OutputAnnotation
printUndefinedNames :: [Name] -> Doc OutputAnnotation
printUndefinedNames [Name]
ns = forall a. String -> Doc a
text String
"Undefined " forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
names forall a. Doc a -> Doc a -> Doc a
<> forall a. String -> Doc a
text String
"."
where names :: Doc OutputAnnotation
names = forall a. Doc a -> Doc a -> Doc a -> [Doc a] -> Doc a
encloseSep forall a. Doc a
empty forall a. Doc a
empty (forall a. Char -> Doc a
char Char
',') forall a b. (a -> b) -> a -> b
$ 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 forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a -> Doc a
align (IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
ist PTerm
ty) forall a. Doc a -> Doc a -> Doc a
<$>
forall a. a -> Maybe a -> a
fromMaybe forall a. Doc a
empty (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Docstring DocTerm
d -> 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 forall a. Doc a -> Doc a -> Doc a
<> 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 = forall a. Set a
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 forall a b. (a -> b) -> a -> b
$
\IState
ist -> IState
ist { idris_highlightedRegions :: Set (FC', OutputAnnotation)
idris_highlightedRegions =
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 Integer
n Handle
h ->
let fancier :: [SExp]
fancier = [ 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) <- forall a. Set a -> [a]
S.toList Set (FC', OutputAnnotation)
highlights, FC -> Bool
fullFC FC
fc
] in
case [SExp]
fancier of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
[SExp]
_ -> forall a. IO a -> Idris a
runIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$
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 = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(FC' FC
a, OutputAnnotation
b) -> (FC
a,OutputAnnotation
b)) forall a b. (a -> b) -> a -> b
$ 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 = 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
]
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile String
hfile forall a b. (a -> b) -> a -> b
$ SExp -> String
sExpToString SExp
annots
clearHighlights :: Idris ()
clearHighlights :: Idris ()
clearHighlights = (IState -> IState) -> Idris ()
updateIState forall a b. (a -> b) -> a -> b
$ \IState
ist -> IState
ist { idris_highlightedRegions :: Set (FC', OutputAnnotation)
idris_highlightedRegions = forall a. Set a
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 forall a. Ord a => a -> a -> Bool
< Int
1 = forall a. Err -> Idris a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg 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
forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputFmt -> String -> String
wrap OutputFmt
fmt forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a. (a -> String -> String) -> SimpleDoc a -> String
displayDecorated (OutputFmt -> OutputAnnotation -> String -> String
decorate OutputFmt
fmt) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
width forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) forall a b. (a -> b) -> a -> b
$
Doc OutputAnnotation
doc
where
decorate :: OutputFmt -> OutputAnnotation -> String -> String
decorate OutputFmt
_ (AnnFC FC
_) = 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
_) = forall a. a -> a
id
decorate OutputFmt
HTMLOutput (AnnBoundName Name
_ Bool
True) = String -> Maybe String -> String -> String
tag String
"idris-bound idris-implicit" forall a. Maybe a
Nothing
decorate OutputFmt
HTMLOutput (AnnBoundName Name
_ Bool
False) = String -> Maybe String -> String -> String
tag String
"idris-bound" 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")
(forall a. a -> Maybe a
Just 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" forall a. Maybe a
Nothing
decorate OutputFmt
HTMLOutput (AnnType String
_ String
_) = String -> Maybe String -> String -> String
tag String
"idris-type" forall a. Maybe a
Nothing
decorate OutputFmt
HTMLOutput OutputAnnotation
AnnKeyword = String -> Maybe String -> String -> String
tag String
"idris-keyword" 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" forall a. Maybe a
Nothing
where mkTag :: String -> String -> String
mkTag String
t String
x = String
"<"forall a. [a] -> [a] -> [a]
++String
tforall a. [a] -> [a] -> [a]
++String
">"forall a. [a] -> [a] -> [a]
++String
xforall a. [a] -> [a] -> [a]
++String
"</"forall a. [a] -> [a] -> [a]
++String
tforall a. [a] -> [a] -> [a]
++String
">"
decorate OutputFmt
HTMLOutput (AnnTerm [(Name, Bool)]
_ Term
_) = forall a. a -> a
id
decorate OutputFmt
HTMLOutput (AnnSearchResult Ordering
_) = forall a. a -> a
id
decorate OutputFmt
HTMLOutput (AnnErr Err
_) = forall a. a -> a
id
decorate OutputFmt
HTMLOutput (AnnNamespace [Text]
_ Maybe String
_) = forall a. a -> a
id
decorate OutputFmt
HTMLOutput (AnnLink String
url) =
\String
txt -> String
"<a href=\"" forall a. [a] -> [a] -> [a]
++ String
url forall a. [a] -> [a] -> [a]
++ String
"\">" forall a. [a] -> [a] -> [a]
++ String
txt forall a. [a] -> [a] -> [a]
++ String
"</a>"
decorate OutputFmt
HTMLOutput OutputAnnotation
AnnQuasiquote = forall a. a -> a
id
decorate OutputFmt
HTMLOutput OutputAnnotation
AnnAntiquote = 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
_) = 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 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
_) = forall a. a -> a
id
decorate OutputFmt
LaTeXOutput (AnnSearchResult Ordering
_) = forall a. a -> a
id
decorate OutputFmt
LaTeXOutput (AnnErr Err
_) = forall a. a -> a
id
decorate OutputFmt
LaTeXOutput (AnnNamespace [Text]
_ Maybe String
_) = forall a. a -> a
id
decorate OutputFmt
LaTeXOutput (AnnLink String
url) = (forall a. [a] -> [a] -> [a]
++ String
"(\\url{" forall a. [a] -> [a] -> [a]
++ String
url forall a. [a] -> [a] -> [a]
++ String
"})")
decorate OutputFmt
LaTeXOutput OutputAnnotation
AnnQuasiquote = forall a. a -> a
id
decorate OutputFmt
LaTeXOutput OutputAnnotation
AnnAntiquote = 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=\""forall a. [a] -> [a] -> [a]
++String
clsforall a. [a] -> [a] -> [a]
++String
"\""forall a. [a] -> [a] -> [a]
++String
titleforall a. [a] -> [a] -> [a]
++String
">" forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
"</span>"
where title :: String
title = forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (\String
d->String
" title=\"" forall a. [a] -> [a] -> [a]
++ String
d forall a. [a] -> [a] -> [a]
++ String
"\"") Maybe String
docs
latex :: String -> String -> String
latex String
cmd String
str = String
"\\"forall a. [a] -> [a] -> [a]
++String
cmdforall a. [a] -> [a] -> [a]
++String
"{"forall a. [a] -> [a] -> [a]
++String
strforall a. [a] -> [a] -> [a]
++String
"}"
wrap :: OutputFmt -> String -> String
wrap OutputFmt
HTMLOutput String
str =
String
"<!doctype html><html><head><style>" forall a. [a] -> [a] -> [a]
++ String
css forall a. [a] -> [a] -> [a]
++ String
"</style></head>" forall a. [a] -> [a] -> [a]
++
String
"<body><!-- START CODE --><pre>" forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
"</pre><!-- END CODE --></body></html>"
where css :: String
css = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a] -> [a]
intersperse String
"\n" 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 =
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a] -> [a]
intersperse String
"\n" forall a b. (a -> b) -> a -> b
$
[String
"\\documentclass{article}",
String
"\\usepackage{fancyvrb}",
String
"\\usepackage[usenames]{xcolor}"] forall a. [a] -> [a] -> [a]
++
forall a b. (a -> b) -> [a] -> [b]
map (\(String
cmd, String
color) ->
String
"\\newcommand{\\"forall a. [a] -> [a] -> [a]
++ String
cmd forall a. [a] -> [a] -> [a]
++
String
"}[1]{\\textcolor{"forall a. [a] -> [a] -> [a]
++ String
color 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")] 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}"]