------------------------------------------------------------------------
-- | Code for instructing Emacs to do things
------------------------------------------------------------------------

module Agda.Interaction.EmacsCommand
  ( Lisp(..)
  , response
  , putResponse
  , display_info'
  , clearRunningInfo
  , clearWarning
  , displayRunningInfo
  ) where

import qualified Data.List as List

import Agda.Utils.Pretty
import Agda.Utils.String

-- | Simple Emacs Lisp expressions.

data Lisp a
  = A a
    -- ^ Atom.
  | Cons (Lisp a) (Lisp a)
    -- Cons cell.
  | L [Lisp a]
    -- ^ List.
  | Q (Lisp a)
    -- Quoted expression.
  deriving Lisp a -> Lisp a -> Bool
(Lisp a -> Lisp a -> Bool)
-> (Lisp a -> Lisp a -> Bool) -> Eq (Lisp a)
forall a. Eq a => Lisp a -> Lisp a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Lisp a -> Lisp a -> Bool
$c/= :: forall a. Eq a => Lisp a -> Lisp a -> Bool
== :: Lisp a -> Lisp a -> Bool
$c== :: forall a. Eq a => Lisp a -> Lisp a -> Bool
Eq

instance Pretty a => Pretty (Lisp a) where
  pretty :: Lisp a -> Doc
pretty (A a
a )     = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
  pretty (Cons Lisp a
a Lisp a
b) = Doc -> Doc
parens (Lisp a -> Doc
forall a. Pretty a => a -> Doc
pretty Lisp a
a Doc -> Doc -> Doc
<+> Doc
"." Doc -> Doc -> Doc
<+> Lisp a -> Doc
forall a. Pretty a => a -> Doc
pretty Lisp a
b)
  pretty (L [Lisp a]
xs)     = Doc -> Doc
parens ([Doc] -> Doc
hsep ((Lisp a -> Doc) -> [Lisp a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Lisp a -> Doc
forall a. Pretty a => a -> Doc
pretty [Lisp a]
xs))
  pretty (Q Lisp a
x)      = Doc
"'" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Lisp a -> Doc
forall a. Pretty a => a -> Doc
pretty Lisp a
x

instance Show (Lisp String) where
  showsPrec :: Int -> Lisp String -> ShowS
showsPrec Int
_ (A String
a)      = String -> ShowS
showString String
a
  showsPrec Int
p (Cons Lisp String
a Lisp String
b) = String -> ShowS
showString String
"(" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Lisp String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Lisp String
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" . " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                            Int -> Lisp String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Lisp String
b ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
")"
  showsPrec Int
p (L [Lisp String]
xs)     = String -> ShowS
showString String
"(" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ShowS -> ShowS -> ShowS) -> ShowS -> [ShowS] -> ShowS
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) (String -> ShowS
showString String
")")
                                              (ShowS -> [ShowS] -> [ShowS]
forall a. a -> [a] -> [a]
List.intersperse (String -> ShowS
showString String
" ")
                                                 ((Lisp String -> ShowS) -> [Lisp String] -> [ShowS]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Lisp String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p) [Lisp String]
xs))
  showsPrec Int
p (Q Lisp String
x)      = String -> ShowS
showString String
"'" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Lisp String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Lisp String
x

-- | Formats a response command.
--
--   Replaces @'\n'@ with spaces to ensure that each command is a
--   single line.
response :: Lisp String -> String
response :: Lisp String -> String
response = (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n") ShowS -> (Lisp String -> String) -> Lisp String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
replaceNewLines ShowS -> (Lisp String -> String) -> Lisp String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Lisp String -> Doc) -> Lisp String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lisp String -> Doc
forall a. Pretty a => a -> Doc
pretty
  where
  replaceNewLines :: Char -> Char
replaceNewLines Char
'\n' = Char
' '
  replaceNewLines Char
c    = Char
c

-- | Writes a response command to standard output.

putResponse :: Lisp String -> IO ()
putResponse :: Lisp String -> IO ()
putResponse = String -> IO ()
putStr (String -> IO ())
-> (Lisp String -> String) -> Lisp String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lisp String -> String
response

-- | @displayInBuffer buffername append header content@ displays @content@
-- (with header @header@) in some suitable way in the buffer @buffername@.
-- If @append@ is @True@, then the content is appended to previous content
-- (if any), otherwise any previous content is deleted.

displayInBuffer :: String -> Bool -> String -> String -> Lisp String
displayInBuffer :: String -> Bool -> String -> String -> Lisp String
displayInBuffer String
buffername Bool
append String
header String
content =
    [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A String
buffername
      , String -> Lisp String
forall a. a -> Lisp a
A (ShowS
quote String
header)
      , String -> Lisp String
forall a. a -> Lisp a
A (ShowS
quote String
content)
      , String -> Lisp String
forall a. a -> Lisp a
A (if Bool
append then String
"t" else String
"nil")
      ]

display_info' :: Bool -> String -> String -> Lisp String
display_info' :: Bool -> String -> String -> Lisp String
display_info' = String -> Bool -> String -> String -> Lisp String
displayInBuffer String
"agda2-info-action"

------------------------------------------------------------------------
-- Running info

-- | The name of the running info buffer.

runningInfoBufferName :: String
runningInfoBufferName :: String
runningInfoBufferName = String
"*Type-checking*"

-- | Clear the running info buffer.

clearRunningInfo :: Lisp String
clearRunningInfo :: Lisp String
clearRunningInfo =
    Bool -> String -> String -> Lisp String
display_info' Bool
False String
runningInfoBufferName String
""

-- | Clear the warning buffer
clearWarning :: Lisp String
clearWarning :: Lisp String
clearWarning = [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-close-warning" ]

-- | Display running information about what the type-checker is up to.

displayRunningInfo :: String -> Lisp String
displayRunningInfo :: String -> Lisp String
displayRunningInfo String
s =
    Bool -> String -> String -> Lisp String
display_info' Bool
True String
runningInfoBufferName String
s