Move the EchoArea into the Brick UI

surveyor-brick/src/Surveyor/Brick.hs

@@ -40,6 +40,7 @@ import qualified Graphics.Vty as V
 
 import           Surveyor.Brick.Attributes
 import qualified Surveyor.Brick.Command as SBC
+import qualified Surveyor.Brick.EchoArea as SBEA
 import qualified Surveyor.Brick.Extension as SBE
 import qualified Surveyor.Brick.Handlers as BH
 import qualified Surveyor.Brick.Keymap as SBK
@@ -145,7 +146,7 @@ drawAppShell s w =
         C.SomeMiniBuffer (C.MiniBuffer _)
           | mb <- s ^. C.lUIExtension . BH.minibufferG ->
             MB.renderMinibuffer True mb
-        _ -> maybe B.emptyWidget B.txt (C.getEchoAreaText (C.sEchoArea s))
+        _ -> maybe B.emptyWidget B.txt (SBEA.getEchoAreaText (SBE.sEchoArea (C.sUIExtension s)))
 
 drawKeyBindings :: (C.Architecture arch s) => C.S BH.BrickUIExtension BH.BrickUIState arch s -> B.Widget Names
 drawKeyBindings s = B.hBox (mapMaybe toKeyHint keys)
@@ -237,10 +238,6 @@ appAttrMap _ = B.attrMap V.defAttr [ (focusedListAttr, V.blue `B.on` V.white)
 appStartEvent :: C.State BH.BrickUIExtension BH.BrickUIState s -> B.EventM Names (C.State BH.BrickUIExtension BH.BrickUIState s)
 appStartEvent s0 = return s0
 
-resetEchoArea :: C.Chan (C.Events s (C.S BH.BrickUIExtension BH.BrickUIState)) -> IO ()
-resetEchoArea customEventChan =
-  C.emitEvent customEventChan C.ResetEchoArea
-
 surveyor :: Maybe FilePath -> IO ()
 surveyor mExePath = PN.withIONonceGenerator $ \ng -> do
   customEventChan <- B.newBChan 100
@@ -297,7 +294,6 @@ emptyState mfp mloader ng customEventChan = do
                                                 , C.sFileLogger = Just fileLogger
                                                 }
              , C.sDiagnosticLevel = C.Debug
-             , C.sEchoArea = C.echoArea 10 (resetEchoArea customEventChan)
              , C.sUIMode = C.SomeUIMode C.Diags
              , C.sAppState = maybe C.AwaitingFile (const C.Loading) mfp
              , C.sEventChannel = customEventChan
@@ -347,7 +343,6 @@ emptyArchState mfp ng n0 mkAnalysisResult chan = do
                                                 , C.sFileLogger = Just fileLogger
                                                 }
              , C.sDiagnosticLevel = C.Debug
-             , C.sEchoArea = C.echoArea 10 (resetEchoArea chan)
              , C.sUIMode = C.SomeUIMode C.Diags
              , C.sAppState = maybe C.AwaitingFile (const C.Loading) mfp
              , C.sEventChannel = chan

surveyor-brick/src/Surveyor/Brick/Command.hs

@@ -31,6 +31,7 @@ import qualified Data.Parameterized.List as PL
 import qualified Data.Parameterized.Nonce as PN
 import qualified Data.Text as T
 
+import qualified Surveyor.Brick.EchoArea as SBEA
 import qualified Surveyor.Brick.Extension as SBE
 import           Surveyor.Brick.Names ( Names(..) )
 import qualified Surveyor.Brick.Widget.Minibuffer as MB
@@ -48,6 +49,7 @@ mkExtension :: forall (arch :: Type) s
             -> (String -> Maybe (C.SomeAddress s)) -> T.Text -> SBE.BrickUIExtension s
 mkExtension emitEvent archNonce addrParser prompt =
   SBE.BrickUIExtension { SBE.sMinibuffer = MB.minibuffer addrParser updater MinibufferEditor MinibufferCompletionList prompt (C.allCommands ++ extraCommands)
+                       , SBE.sEchoArea = SBEA.echoArea 10 (emitEvent (C.toEvent SBE.ResetEchoArea))
                        }
   where
     updater = SBE.updateMinibufferCompletions emitEvent archNonce

surveyor-core/src/Surveyor/Core/EchoArea.hs → surveyor-brick/src/Surveyor/Brick/EchoArea.hs

@@ -1,7 +1,7 @@
 -- | A data abstraction around a text value that can timeout
 --
 -- This could probably be generalized beyond just the echo area
-module Surveyor.Core.EchoArea (
+module Surveyor.Brick.EchoArea (
   EchoArea,
   echoArea,
   resetEchoArea,

surveyor-brick/src/Surveyor/Brick/Extension.hs

@@ -17,6 +17,7 @@ module Surveyor.Brick.Extension (
   -- * Lenses
   minibufferL,
   minibufferG,
+  echoAreaL,
   functionSelectorL,
   functionSelectorG,
   blockSelectorL,
@@ -39,10 +40,12 @@ import qualified Data.Parameterized.Nonce as PN
 import qualified Data.Text as T
 import qualified Data.Vector as V
 import           GHC.Generics ( Generic )
+import qualified Prettyprinter as PP
 import qualified Surveyor.Core as C
 
 import qualified Brick.Widget.Minibuffer as MBW
 
+import qualified Surveyor.Brick.EchoArea as SBEA
 import           Surveyor.Brick.Names ( Names(..) )
 import qualified Surveyor.Brick.Widget.BlockSelector as BS
 import qualified Surveyor.Brick.Widget.BlockViewer as BV
@@ -60,6 +63,7 @@ import qualified Surveyor.Brick.Widget.SymbolicExecution as SEM
 data BrickUIExtension s =
   BrickUIExtension { sMinibuffer :: !(MB.Minibuffer (C.SurveyorCommand s (C.S BrickUIExtension BrickUIState)) T.Text Names)
                    -- ^ The persistent state of the minibuffer
+                   , sEchoArea :: SBEA.EchoArea
                    }
   deriving (Generic)
 
@@ -77,7 +81,9 @@ data BrickUIState arch s =
   deriving (Generic)
 
 L.makeLensesFor
-  [("sMinibuffer", "minibufferL")]
+  [ ("sMinibuffer", "minibufferL")
+  , ("sEchoArea", "echoAreaL")
+  ]
   ''BrickUIExtension
 
 L.makeLensesFor
@@ -101,6 +107,12 @@ data BrickUIEvent s (st :: Type -> Type -> Type) where
   OpenMinibuffer :: BrickUIEvent s st
   ShowSymbolicExecution :: BrickUIEvent s st
 
+  -- | Display a transient message to the user
+  EchoText :: !(PP.Doc ()) -> BrickUIEvent s st
+  -- | A message sent by the system (after a time delay) to reset the transient
+  -- message area
+  ResetEchoArea :: BrickUIEvent s st
+
   ListBlocks :: PN.Nonce s arch -> [C.Block arch s] -> BrickUIEvent s st
   ListFunctions :: PN.Nonce s arch -> [C.FunctionHandle arch s] -> BrickUIEvent s st
   FindFunctionsContaining :: PN.Nonce s arch -> Maybe (C.Address arch s) -> BrickUIEvent s st

surveyor-brick/src/Surveyor/Brick/Handlers.hs

@@ -141,6 +141,13 @@ handleCustomEvent s0 evt =
       handleSymbolicExecutionEvent s1 se
     C.LoggingEvent le -> do
       s1 <- C.handleLoggingEvent s0 le
+      -- Take the first line of any logs (that are not debug spam) and reflect
+      -- them into the echo area
+      case le of
+        C.LogDiagnostic msg
+          | C.logLevel (C.logMsg msg) > C.Debug
+          , firstLine : _ <- C.logText (C.logMsg msg) -> liftIO $ C.sEmitEvent s0 (SBE.EchoText firstLine)
+        _ -> return ()
       B.continue s1
     C.InfoEvent ie -> do
       s1 <- C.handleInfoEvent s0 ie

surveyor-brick/src/Surveyor/Brick/Handlers/Extension.hs

@@ -2,14 +2,16 @@
 module Surveyor.Brick.Handlers.Extension ( handleExtensionEvent ) where
 
 import qualified Brick as B
-import           Control.Lens ( (&), (.~), (^.), _Just )
+import           Control.Lens ( (&), (.~), (^.), (%~), _Just )
 import           Control.Monad.IO.Class ( liftIO )
 import qualified Data.Parameterized.Classes as PC
 import qualified Data.Text as T
 import qualified Prettyprinter as PP
+import qualified Prettyprinter.Render.Text as PPT
 import qualified Surveyor.Core as C
 
 import           Surveyor.Brick.Attributes ( focusedListAttr )
+import qualified Surveyor.Brick.EchoArea as SBEA
 import qualified Surveyor.Brick.Extension as SBE
 import qualified Surveyor.Brick.Widget.BlockSelector as BS
 import qualified Surveyor.Brick.Widget.FunctionSelector as FS
@@ -115,3 +117,7 @@ handleExtensionEvent s0 evt =
               let s1 = s0 & C.lUIExtension . SBE.minibufferL .~ mb'
               B.continue $! C.State s1
       | otherwise -> B.continue (C.State s0)
+    SBE.EchoText txt -> do
+      ea' <- liftIO (SBEA.setEchoAreaText (SBE.sEchoArea (C.sUIExtension s0)) (PPT.renderStrict (PP.layoutCompact txt)))
+      B.continue $! C.State (s0 & C.lUIExtension . SBE.echoAreaL .~ ea')
+    SBE.ResetEchoArea -> B.continue $! C.State (s0 & C.lUIExtension . SBE.echoAreaL %~ SBEA.resetEchoArea)

surveyor-brick/src/Surveyor/Brick/Handlers/Load.hs

@@ -23,6 +23,7 @@ import qualified Surveyor.Core as C
 
 import           Surveyor.Brick.Attributes ( focusedListAttr )
 import qualified Surveyor.Brick.Command as BC
+import qualified Surveyor.Brick.EchoArea as SBEA
 import qualified Surveyor.Brick.Extension as SBE
 import qualified Surveyor.Brick.Keymap as SBK
 import qualified Surveyor.Brick.Widget.BlockSelector as BS
@@ -139,6 +140,9 @@ stateFromAnalysisResult s0 ares newDiags state uiMode = do
         return (C.appendLog msg ls)
   nextLogStore <- F.foldlM appendTextLog (C.sLogStore s0) (fmap PP.pretty newDiags)
   sem <- SEM.symbolicExecutionManager (C.sNonceGenerator s0) (Some (C.Configuring ses))
+  let uiExt = SBE.BrickUIExtension { SBE.sMinibuffer = MB.minibuffer addrParser (SBE.updateMinibufferCompletions (C.sEmitEvent s0) (C.archNonce ares)) MinibufferEditor MinibufferCompletionList (T.pack "M-x") (C.allCommands ++ BC.extraCommands)
+                                   , SBE.sEchoArea = SBEA.echoArea 10 (C.emitEvent (C.sEventChannel s0) (C.toEvent SBE.ResetEchoArea))
+                                   }
   return C.S { C.sLogStore = nextLogStore
              , C.sDiagnosticLevel = C.sDiagnosticLevel s0
              , C.sLogActions = C.LoggingActions { C.sStateLogger = C.logToState (C.sEventChannel s0)
@@ -148,7 +152,6 @@ stateFromAnalysisResult s0 ares newDiags state uiMode = do
              , C.sAppState = state
              , C.sEventChannel = C.sEventChannel s0
              , C.sNonceGenerator = C.sNonceGenerator s0
-             , C.sEchoArea = C.sEchoArea s0
              , C.sInputFile = C.sInputFile s0
              , C.sLoader = C.sLoader s0
              , C.sKeymap = keymap
@@ -194,7 +197,4 @@ stateFromAnalysisResult s0 ares newDiags state uiMode = do
              }
   where
     addrParser s = C.SomeAddress (C.archNonce ares) <$> C.parseAddress s
-    uiExt = SBE.BrickUIExtension { SBE.sMinibuffer = MB.minibuffer addrParser (SBE.updateMinibufferCompletions (C.sEmitEvent s0) (C.archNonce ares)) MinibufferEditor MinibufferCompletionList (T.pack "M-x") (C.allCommands ++ BC.extraCommands)
-                                 }
-
     keymap = SBK.defaultKeymap (Just (C.archNonce ares))

surveyor-brick/surveyor-brick.cabal

@@ -15,6 +15,7 @@ cabal-version:       >=1.10
 library
   exposed-modules:     Surveyor.Brick
                        Surveyor.Brick.Attributes
+                       Surveyor.Brick.EchoArea
                        Surveyor.Brick.Extension
                        Surveyor.Brick.Handlers
                        Surveyor.Brick.Names

surveyor-core/src/Surveyor/Core.hs

@@ -197,12 +197,6 @@ module Surveyor.Core (
   -- * Translation Cache
   TC.TranslationCache,
   TC.newTranslationCache,
-  -- * The EchoArea abstraction
-  EA.EchoArea,
-  EA.echoArea,
-  EA.getEchoAreaText,
-  EA.setEchoAreaText,
-  EA.resetEchoArea,
   -- * Handlers
   module Surveyor.Core.HandlerMonad,
   HC.handleContextEvent,
@@ -249,7 +243,6 @@ import qualified Surveyor.Core.Chan as CS
 import qualified Surveyor.Core.Command as CC
 import           Surveyor.Core.Commands
 import qualified Surveyor.Core.Context as CCX
-import qualified Surveyor.Core.EchoArea as EA
 import qualified Surveyor.Core.Events as CE
 import qualified Surveyor.Core.Handlers.Context as HC
 import qualified Surveyor.Core.Handlers.Info as HI

surveyor-core/src/Surveyor/Core/Events.hs

@@ -33,7 +33,6 @@ import qualified Lang.Crucible.Backend as CB
 import qualified Lang.Crucible.CFG.Core as CCC
 import qualified Lang.Crucible.Simulator.Profiling as CSP
 import qualified Lang.Crucible.Simulator.RegMap as LMCR
-import qualified Prettyprinter as PP
 import qualified What4.BaseTypes as WT
 import qualified What4.Expr.Builder as WEB
 
@@ -83,11 +82,6 @@ data InfoEvent s st where
   -- | Show a description (help text and expected arguments) of a command in a
   -- manner suitable for the UI
   DescribeCommand :: (C.CommandLike cmd) => C.SomeCommand cmd -> InfoEvent s st
-  -- | Display a transient message to the user
-  EchoText :: !(PP.Doc ()) -> InfoEvent s st
-  -- | A message sent by the system (after a time delay) to reset the transient
-  -- message area
-  ResetEchoArea :: InfoEvent s st
   -- | Display a description of the keybindings active in the current context in
   -- a manner suitable for the UI
   DescribeKeys :: InfoEvent s st

surveyor-core/src/Surveyor/Core/Handlers/Info.hs

@@ -5,17 +5,15 @@ module Surveyor.Core.Handlers.Info (
 
 import qualified Control.Concurrent.Async as CCA
 import qualified Control.Exception as X
-import           Control.Lens ( (&), (^.), (.~), (%~) )
+import           Control.Lens ( (&), (^.), (.~) )
 import           Control.Monad.IO.Class ( MonadIO, liftIO )
 import qualified Data.GraphViz as DG
 import qualified Data.Text as T
 import qualified Data.Text.Prettyprint.Doc as PP
-import qualified Prettyprinter.Render.Text as PPT
 import           System.FilePath ( (<.>) )
 
 import qualified Surveyor.Core.Architecture as SCA
 import qualified Surveyor.Core.Command as SCC
-import qualified Surveyor.Core.EchoArea as SCEA
 import qualified Surveyor.Core.Events as SCE
 import qualified Surveyor.Core.GraphViz as SCG
 import qualified Surveyor.Core.Keymap as SCK
@@ -33,18 +31,12 @@ handleInfoEvent :: ( SCA.Architecture arch s
 handleInfoEvent s0 evt =
   case evt of
     SCE.DescribeCommand (SCC.SomeCommand cmd) -> do
-      let msg = PP.pretty (SCC.cmdName cmd) <> PP.pretty ": " <> SCC.cmdDocstring cmd
-      liftIO (SCS.sEmitEvent s0 (SCE.EchoText msg))
+      let msg = SCL.msgWith { SCL.logLevel = SCL.Requested
+                            , SCL.logSource = SCL.EventHandler (T.pack "DescribeCommand")
+                            , SCL.logText = [PP.pretty (SCC.cmdName cmd) <> PP.pretty ": " <> SCC.cmdDocstring cmd]
+                            }
+      liftIO $ SCS.logMessage s0 msg
       return $! SCS.State s0
-    SCE.EchoText txt -> do
-      -- All echo area text is mirrored into the log
-      liftIO $ SCS.logMessage s0 (SCL.msgWith { SCL.logLevel = SCL.Requested
-                                              , SCL.logSource = SCL.EchoAreaUpdate
-                                              , SCL.logText = [txt]
-                                              })
-      ea' <- liftIO (SCEA.setEchoAreaText (SCS.sEchoArea s0) (PPT.renderStrict (PP.layoutCompact txt)))
-      return $! SCS.State (s0 & SCS.lEchoArea .~ ea')
-    SCE.ResetEchoArea -> return $! SCS.State (s0 & SCS.lEchoArea %~ SCEA.resetEchoArea)
     SCE.DescribeKeys -> do
       withBaseMode (s0 ^. SCS.lUIMode) $ \normalMode -> do
         let keys = SCK.modeKeybindings (s0 ^. SCS.lKeymap) (SCM.SomeUIMode normalMode)

surveyor-core/src/Surveyor/Core/State.hs

@@ -34,7 +34,6 @@ module Surveyor.Core.State (
   lLoader,
   lLogStore,
   diagnosticLevelL,
-  lEchoArea,
   lUIMode,
   lAppState,
   lEventChannel,
@@ -70,7 +69,6 @@ import qualified Surveyor.Core.Architecture as A
 import qualified Surveyor.Core.Arguments as AR
 import qualified Surveyor.Core.Chan as C
 import qualified Surveyor.Core.Context as CC
-import qualified Surveyor.Core.EchoArea as EA
 import qualified Surveyor.Core.Events as SCE
 import qualified Surveyor.Core.IRRepr as IR
 import           Surveyor.Core.Keymap ( Keymap )
@@ -180,8 +178,6 @@ data S e u (arch :: Type) s =
     , sLoader :: Maybe AsyncLoader
     , sDiagnosticLevel :: !SCL.Severity
     -- ^ The level of log to display
-    , sEchoArea :: !EA.EchoArea
-    -- ^ An area where one-line messages can be displayed
     , sUIMode :: !(SomeUIMode s)
     -- ^ The current UI mode, which drives rendering and keybindings available
     , sAppState :: AppState
@@ -221,7 +217,6 @@ L.makeLensesFor
   , ("sInputFile", "lInputFile")
   , ("sLogStore", "lLogStore")
   , ("sDiagnosticLevel", "diagnosticLevelL")
-  , ("sEchoArea", "lEchoArea")
   , ("sUIMode", "lUIMode")
   , ("sEventChannel", "lEventChannel")
   , ("sAppState", "lAppState")

surveyor-core/surveyor-core.cabal

@@ -46,7 +46,6 @@ library
                        Surveyor.Core.SymbolicExecution.Override
                        Surveyor.Core.SymbolicExecution.Session
                        Surveyor.Core.SymbolicExecution.State
-                       Surveyor.Core.EchoArea
                        Surveyor.Core.Events
                        Surveyor.Core.HandlerMonad
                        Surveyor.Core.IRRepr