summaryrefslogtreecommitdiff
path: root/src/full/Agda/Interaction/EmacsCommand.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Interaction/EmacsCommand.hs')
-rw-r--r--src/full/Agda/Interaction/EmacsCommand.hs29
1 files changed, 20 insertions, 9 deletions
diff --git a/src/full/Agda/Interaction/EmacsCommand.hs b/src/full/Agda/Interaction/EmacsCommand.hs
index 3c2ae04..96eee10 100644
--- a/src/full/Agda/Interaction/EmacsCommand.hs
+++ b/src/full/Agda/Interaction/EmacsCommand.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE FlexibleInstances #-}
------------------------------------------------------------------------
-- | Code for instructing Emacs to do things
@@ -9,7 +8,9 @@ module Agda.Interaction.EmacsCommand
, response
, putResponse
, display_info'
+ , display_warning
, clearRunningInfo
+ , clearWarning
, displayRunningInfo
) where
@@ -60,19 +61,25 @@ response = (++ "\n") . map replaceNewLines . show . pretty
putResponse :: Lisp String -> IO ()
putResponse = putStr . response
--- | @display_info' append header content@ displays @content@ (with
--- header @header@) in some suitable way. If @append@ is @True@, then
--- the content is appended to previous content (if any), otherwise any
--- previous content is deleted.
+-- | @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.
-display_info' :: Bool -> String -> String -> Lisp String
-display_info' append bufname content =
- L [ A "agda2-info-action"
- , A (quote bufname)
+displayInBuffer :: String -> Bool -> String -> String -> Lisp String
+displayInBuffer buffername append header content =
+ L [ A buffername
+ , A (quote header)
, A (quote content)
, A (if append then "t" else "nil")
]
+display_info' :: Bool -> String -> String -> Lisp String
+display_info' = displayInBuffer "agda2-info-action"
+
+display_warning :: String -> String -> Lisp String
+display_warning = displayInBuffer "agda2-warning-action" False
+
------------------------------------------------------------------------
-- Running info
@@ -87,6 +94,10 @@ clearRunningInfo :: Lisp String
clearRunningInfo =
display_info' False runningInfoBufferName ""
+-- | Clear the warning buffer
+clearWarning :: Lisp String
+clearWarning = L [ A "agda2-close-warning" ]
+
-- | Display running information about what the type-checker is up to.
displayRunningInfo :: String -> Lisp String