    ------------------------------------------------------------------------
    -- | 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
    forall (t :: * -> *). Foldable t => t 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 _ (A a)      = showString a
    --   showsPrec p (Cons a b) = showString "(" . showsPrec p a . showString " . " .
    --                                             showsPrec p b . showString ")"
    --   showsPrec p (L xs)     = showString "(" . foldr (.) (showString ")")
    --                                               (List.intersperse (showString " ")
    --                                                  (map (showsPrec p) xs))
    --   showsPrec p (Q x)      = showString "'" . showsPrec p 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 -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n") (String -> String)
    -> (Lisp String -> String) -> Lisp String -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Char -> Char) -> String -> String
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> Char
    replaceNewLines (String -> String)
    -> (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 (String -> String
    quote String
    header)
          , String -> Lisp String
    forall a. a -> Lisp a
    A (String -> String
    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