diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index f4d11fd892..161f7e2613 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -27,6 +27,7 @@ library
   hs-source-dirs:     src
   exposed-modules:
     Ide.Plugin.Tactic
+    Refinery.Future
     Wingman.AbstractLSP
     Wingman.AbstractLSP.TacticActions
     Wingman.AbstractLSP.Types
@@ -93,6 +94,7 @@ library
     , refinery              ^>=0.4
     , retrie                >=0.1.1.0
     , syb
+    , unagi-chan
     , text
     , transformers
     , unordered-containers
diff --git a/plugins/hls-tactics-plugin/src/Refinery/Future.hs b/plugins/hls-tactics-plugin/src/Refinery/Future.hs
new file mode 100644
index 0000000000..51d844b3b4
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Refinery/Future.hs
@@ -0,0 +1,140 @@
+{-# LANGUAGE RankNTypes #-}
+
+------------------------------------------------------------------------------
+-- | Things that belong in the future release of refinery v5.
+module Refinery.Future
+  ( runStreamingTacticT
+  , hoistListT
+  , consume
+  ) where
+
+import Control.Applicative
+import Control.Monad (ap, (>=>))
+import Control.Monad.State.Lazy (runStateT)
+import Control.Monad.Trans
+import Data.Either (isRight)
+import Data.Functor ((<&>))
+import Data.Tuple (swap)
+import Refinery.ProofState
+import Refinery.Tactic.Internal
+
+
+
+hoistElem :: Functor m => (forall x. m x -> n x) -> Elem m a -> Elem n a
+hoistElem _ Done = Done
+hoistElem f (Next a lt) = Next a $ hoistListT f lt
+
+
+hoistListT :: Functor m => (forall x. m x -> n x) -> ListT m a -> ListT n a
+hoistListT f t = ListT $ f $ fmap (hoistElem f) $ unListT t
+
+
+consume :: Monad m => ListT m a -> (a -> m ()) -> m ()
+consume lt f = unListT lt >>= \case
+  Done -> pure ()
+  Next a lt' -> f a >> consume lt' f
+
+
+newHole :: MonadExtract meta ext err s m => s -> m (s, (meta, ext))
+newHole = fmap swap . runStateT hole
+
+runStreamingTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> ListT m (Either err (Proof s meta jdg ext))
+runStreamingTacticT t j s = streamProofs s $ fmap snd $ proofState t j
+
+data Elem m a
+    = Done
+    | Next a (ListT m a)
+    deriving stock Functor
+
+
+point :: Applicative m => a -> Elem m a
+point a = Next a $ ListT $ pure Done
+
+newtype ListT m a = ListT { unListT :: m (Elem m a) }
+
+cons :: (Applicative m) => a -> ListT m a -> ListT m a
+cons x xs = ListT $ pure $ Next x xs
+
+instance Functor m => Functor (ListT m) where
+    fmap f (ListT xs) = ListT $ xs <&> \case
+        Done -> Done
+        Next a xs -> Next (f a) (fmap f xs)
+
+instance (Monad m) => Applicative (ListT m) where
+    pure = return
+    (<*>) = ap
+
+instance (Monad m) => Alternative (ListT m) where
+    empty = ListT $ pure Done
+    (ListT xs) <|> (ListT ys) =
+        ListT $ xs >>= \case
+          Done -> ys
+          Next x xs -> pure (Next x (xs <|> ListT ys))
+
+instance (Monad m) => Monad (ListT m) where
+    return a = cons a empty
+    (ListT xs) >>= k =
+        ListT $ xs >>= \case
+          Done -> pure Done
+          Next x xs -> unListT $ k x <|> (xs >>= k)
+
+
+instance MonadTrans ListT where
+    lift m = ListT $ fmap (\x -> Next x empty) m
+
+
+interleaveT :: (Monad m) => Elem m a -> Elem m a -> Elem m a
+interleaveT xs ys =
+    case xs of
+      Done -> ys
+      Next x xs -> Next x $ ListT $ fmap (interleaveT ys) $ unListT xs
+
+--         ys <&> \case
+--           Done -> Next x xs
+--           Next y ys -> Next x (cons y (interleaveT xs ys))
+
+force :: (Monad m) => Elem m a -> m [a]
+force = \case
+    Done -> pure []
+    Next x xs' -> (x:) <$> (unListT xs' >>= force)
+
+ofList :: Monad m => [a] -> Elem m a
+ofList [] = Done
+ofList (x:xs) = Next x $ ListT $ pure $ ofList xs
+
+streamProofs :: forall ext err s m goal meta. (MonadExtract meta ext err s m) => s -> ProofStateT ext ext err s m goal -> ListT m (Either err (Proof s meta goal ext))
+streamProofs s p = ListT $ go s [] pure p
+    where
+      go :: s -> [(meta, goal)] -> (err -> m err) -> ProofStateT ext ext err s m goal -> m (Elem m (Either err (Proof s meta goal ext)))
+      go s goals _ (Subgoal goal k) = do
+         (s', (meta, h)) <- newHole s
+         -- Note [Handler Reset]:
+         -- We reset the handler stack to avoid the handlers leaking across subgoals.
+         -- This would happen when we had a handler that wasn't followed by an error call.
+         --     pair >> goal >>= \g -> (handler_ $ \_ -> traceM $ "Handling " <> show g) <|> failure "Error"
+         -- We would see the "Handling a" message when solving for b.
+         (go s' (goals ++ [(meta, goal)]) pure $ k h)
+      go s goals handlers (Effect m) = m >>= go s goals handlers
+      go s goals handlers (Stateful f) =
+          let (s', p) = f s
+          in go s' goals handlers p
+      go s goals handlers (Alt p1 p2) =
+          unListT $ ListT (go s goals handlers p1) <|> ListT (go s goals handlers p2)
+      go s goals handlers (Interleave p1 p2) =
+          interleaveT <$> (go s goals handlers p1) <*> (go s goals handlers p2)
+      go s goals handlers (Commit p1 p2) = do
+          solns <- force =<< go s goals handlers p1
+          if (any isRight solns) then pure $ ofList solns else go s goals handlers p2
+      go _ _ _ Empty = pure Done
+      go _ _ handlers (Failure err _) = do
+          annErr <- handlers err
+          pure $ point $ Left annErr
+      go s goals handlers (Handle p h) =
+          -- Note [Handler ordering]:
+          -- If we have multiple handlers in scope, then we want the handlers closer to the error site to
+          -- run /first/. This allows the handlers up the stack to add their annotations on top of the
+          -- ones lower down, which is the behavior that we desire.
+          -- IE: for @handler f >> handler g >> failure err@, @g@ ought to be run before @f@.
+          go s goals (h >=> handlers) p
+      go s goals _ (Axiom ext) = pure $ point $ Right (Proof ext s goals)
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs
index 0baf96a6d3..a7b83f0fd4 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs
@@ -13,8 +13,11 @@ import           Control.Monad.IO.Class
 import           Control.Monad.Trans (lift)
 import           Control.Monad.Trans.Maybe (MaybeT, mapMaybeT)
 import qualified Data.Aeson as A
+import           Data.Coerce
 import           Data.Foldable (traverse_)
+import           Data.Monoid (Last (..))
 import qualified Data.Text as T
+import           Data.Traversable (for)
 import           Data.Tuple.Extra (uncurry3)
 import           Development.IDE (IdeState)
 import           Development.IDE.Core.UseStale
@@ -93,26 +96,30 @@ runContinuation plId cont state (fc, b) = do
       env@LspEnv{..} <- buildEnv state plId fc
       let stale a = runStaleIde "runContinuation" state (fc_nfp le_fileContext) a
       args <- fetchTargetArgs @a env
-      c_runCommand cont env args fc b >>= \case
-        ErrorMessages errs -> do
-          traverse_ showUserFacingMessage errs
-          pure $ Right A.Null
-        RawEdit edits -> do
-          sendEdits edits
-          pure $ Right A.Null
-        GraftEdit gr -> do
-          ccs <- lift getClientCapabilities
-          TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource
-          case mkWorkspaceEdits le_dflags ccs (fc_uri le_fileContext) (unTrack pm) gr of
-            Left errs ->
-              pure $ Left $ ResponseError
-                { _code    = InternalError
-                , _message = T.pack $ show errs
-                , _xdata   = Nothing
-                }
-            Right edits -> do
-              sendEdits edits
-              pure $ Right A.Null
+      res <- c_runCommand cont env args fc b
+
+      -- This block returns a maybe error.
+      fmap (maybe (Right $ A.Null) Left . coerce . foldMap Last) $
+        for res $ \case
+          ErrorMessages errs -> do
+            traverse_ showUserFacingMessage errs
+            pure Nothing
+          RawEdit edits -> do
+            sendEdits edits
+            pure Nothing
+          GraftEdit gr -> do
+            ccs <- lift getClientCapabilities
+            TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource
+            case mkWorkspaceEdits le_dflags ccs (fc_uri le_fileContext) (unTrack pm) gr of
+              Left errs ->
+                pure $ Just $ ResponseError
+                  { _code    = InternalError
+                  , _message = T.pack $ show errs
+                  , _xdata   = Nothing
+                  }
+              Right edits -> do
+                sendEdits edits
+                pure $ Nothing
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs
index 62f51f7a34..89769ae8aa 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs
@@ -52,23 +52,38 @@ makeTacticInteraction cmd =
         pm_span <- liftMaybe $ mapAgeFrom pmmap span
         let t = commandTactic cmd var_name
 
-        res <- liftIO $ timeout (cfg_timeout_seconds le_config * seconds) $ do
-          runTactic hj_ctx hj_jdg t >>= \case
-            Left err -> pure $ ErrorMessages $ pure $ mkUserFacingMessage err
-            Right rtr ->
-              case rtr_extract rtr of
-                L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) ->
-                  pure $ ErrorMessages [NothingToDo]
-                _ -> do
-                  for_ (rtr_other_solns rtr) $ \soln -> do
-                    traceMX "other solution" $ syn_val soln
-                    traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) []
-                  traceMX "solution" $ rtr_extract rtr
-                  pure $ GraftEdit $ graftHole (RealSrcSpan $ unTrack pm_span) rtr
-
-        pure $ case res of
-          Nothing -> ErrorMessages $ pure TimedOut
-          Just c  -> c
+        liftIO $ runTactic (cfg_timeout_seconds le_config * seconds) hj_ctx hj_jdg t >>= \case
+          Left err ->
+            pure
+              $ pure
+              $ ErrorMessages
+              $ pure
+              $ mkUserFacingMessage err
+          Right rtr ->
+            case rtr_extract rtr of
+              L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) ->
+                pure
+                  $ addTimeoutMessage rtr
+                  $ pure
+                  $ ErrorMessages
+                  $ pure NothingToDo
+              _ -> do
+                for_ (rtr_other_solns rtr) $ \soln -> do
+                  traceMX "other solution" $ syn_val soln
+                  traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) []
+                traceMX "solution" $ rtr_extract rtr
+                pure
+                  $ addTimeoutMessage rtr
+                  $ pure
+                  $ GraftEdit
+                  $ graftHole (RealSrcSpan $ unTrack pm_span) rtr
+
+
+addTimeoutMessage :: RunTacticResults -> [ContinuationResult] -> [ContinuationResult]
+addTimeoutMessage rtr = mappend
+  [ ErrorMessages $ pure TimedOut
+  | rtr_timed_out rtr
+  ]
 
 
 ------------------------------------------------------------------------------
@@ -82,6 +97,7 @@ seconds = 1e6
 mkUserFacingMessage :: [TacticError] -> UserFacingMessage
 mkUserFacingMessage errs
   | elem OutOfGas errs = NotEnoughGas
+mkUserFacingMessage [] = NothingToDo
 mkUserFacingMessage _ = TacticErrors
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs
index 8b00f0b021..8555b880d2 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs
@@ -113,7 +113,7 @@ data Continuation sort target payload = Continuation
         -> TargetArgs target
         -> FileContext
         -> payload
-        -> MaybeT (LspM Plugin.Config) ContinuationResult
+        -> MaybeT (LspM Plugin.Config) [ContinuationResult]
   }
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
index 568ca69ca1..93deee4e3a 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
@@ -84,7 +84,7 @@ emptyCaseInteraction = Interaction $
           , edits
           )
     )
-  $ (\ _ _ _ we -> pure $ RawEdit we)
+  $ (\ _ _ _ we -> pure $ pure $ RawEdit we)
 
 
 scrutinzedType :: EmptyCaseSort Type -> Maybe Type
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
index 9eb6e1dc62..0cebec94b7 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
@@ -1,9 +1,11 @@
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TupleSections   #-}
+{-# LANGUAGE RankNTypes #-}
 
 module Wingman.Machinery where
 
 import           Control.Applicative (empty)
+import           Control.Concurrent.Chan.Unagi.NoBlocking (newChan, writeChan, OutChan, tryRead, tryReadChan)
 import           Control.Lens ((<>~))
 import           Control.Monad.Reader
 import           Control.Monad.State.Class (gets, modify, MonadState)
@@ -16,7 +18,7 @@ import           Data.Generics (everything, gcount, mkQ)
 import           Data.Generics.Product (field')
 import           Data.List (sortBy)
 import qualified Data.Map as M
-import           Data.Maybe (mapMaybe)
+import           Data.Maybe (mapMaybe, isJust)
 import           Data.Monoid (getSum)
 import           Data.Ord (Down (..), comparing)
 import qualified Data.Set as S
@@ -24,9 +26,11 @@ import           Data.Traversable (for)
 import           Development.IDE.Core.Compile (lookupName)
 import           Development.IDE.GHC.Compat
 import           GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv, varType)
+import           Refinery.Future
 import           Refinery.ProofState
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
+import           System.Timeout (timeout)
 import           TcType
 import           Type (tyCoVarsOfTypeWellScoped)
 import           Wingman.Context (getInstance)
@@ -71,15 +75,24 @@ tacticToRule :: Judgement -> TacticsM () -> Rule
 tacticToRule jdg (TacticT tt) = RuleT $ flip execStateT jdg tt >>= flip Subgoal Axiom
 
 
+consumeChan :: OutChan (Maybe a) -> IO [a]
+consumeChan chan = do
+  tryReadChan chan >>= tryRead >>= \case
+    Nothing -> pure []
+    Just (Just a) -> (:) <$> pure a <*> consumeChan chan
+    Just Nothing -> pure []
+
+
 ------------------------------------------------------------------------------
 -- | Attempt to generate a term of the right type using in-scope bindings, and
 -- a given tactic.
 runTactic
-    :: Context
+    :: Int          -- ^ Timeout
+    -> Context
     -> Judgement
-    -> TacticsM ()       -- ^ Tactic to use
+    -> TacticsM ()  -- ^ Tactic to use
     -> IO (Either [TacticError] RunTacticResults)
-runTactic ctx jdg t = do
+runTactic duration ctx jdg t = do
     let skolems = S.fromList
                 $ foldMap (tyCoVarsOfTypeWellScoped . unCType)
                 $ (:) (jGoal jdg)
@@ -91,31 +104,34 @@ runTactic ctx jdg t = do
           defaultTacticState
             { ts_skolems = skolems
             }
-    res <- flip runReaderT ctx
-         . unExtractM
-         $ runTacticT t jdg tacticState
-    pure $ case res of
-      (Left errs) -> Left $ take 50 errs
-      (Right solns) -> do
-        let sorted =
-              flip sortBy solns $ comparing $ \(Proof ext _ holes) ->
-                Down $ scoreSolution ext jdg $ fmap snd holes
-        case sorted of
-          ((Proof syn _ subgoals) : _) ->
-            Right $
-              RunTacticResults
-                { rtr_trace    = syn_trace syn
-                , rtr_extract  = simplify $ syn_val syn
-                , rtr_subgoals = fmap snd subgoals
-                , rtr_other_solns = reverse . fmap pf_extract $ sorted
-                , rtr_jdg = jdg
-                , rtr_ctx = ctx
-                }
-          -- guaranteed to not be empty
-          _ -> Left []
-
-assoc23 :: (a, b, c) -> (a, (b, c))
-assoc23 (a, b, c) = (a, (b, c))
+
+    let stream = hoistListT (flip runReaderT ctx . unExtractM)
+               $ runStreamingTacticT t jdg tacticState
+    (in_proofs, out_proofs) <- newChan
+    (in_errs, out_errs) <- newChan
+    timed_out <-
+      fmap (not. isJust) $ timeout duration $ consume stream $ \case
+        Left err -> writeChan in_errs $ Just err
+        Right proof -> writeChan in_proofs $ Just proof
+    writeChan in_proofs Nothing
+
+    solns <- consumeChan out_proofs
+    let sorted =
+          flip sortBy solns $ comparing $ \(Proof ext _ holes) ->
+            Down $ scoreSolution ext jdg $ fmap snd holes
+    case sorted of
+      ((Proof syn _ subgoals) : _) ->
+        pure $ Right $
+          RunTacticResults
+            { rtr_trace    = syn_trace syn
+            , rtr_extract  = simplify $ syn_val syn
+            , rtr_subgoals = fmap snd subgoals
+            , rtr_other_solns = reverse . fmap pf_extract $ sorted
+            , rtr_jdg = jdg
+            , rtr_ctx = ctx
+            , rtr_timed_out = timed_out
+            }
+      _ -> fmap Left $ consumeChan out_errs
 
 
 tracePrim :: String -> Trace
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 8277603faf..d22c20363e 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -447,10 +447,7 @@ attempt_it rsl ctx jdg program =
   case P.runParser tacticProgram "<splice>" (T.pack program) of
     Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty $ fixErrorOffset rsl peb
     Right tt -> do
-      res <- runTactic
-            ctx
-            jdg
-            tt
+      res <- runTactic 2e6 ctx jdg tt
       pure $ case res of
           Left tes -> Left $ wrapError $ show tes
           Right rtr -> Right
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index 8805ae2c99..a853335e35 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -6,7 +6,7 @@ module Wingman.Tactics
   ) where
 
 import           ConLike (ConLike(RealDataCon))
-import           Control.Applicative (Alternative(empty))
+import           Control.Applicative (Alternative(empty), (<|>))
 import           Control.Lens ((&), (%~), (<>~))
 import           Control.Monad (filterM)
 import           Control.Monad (unless)
@@ -465,17 +465,17 @@ auto' 0 = failure OutOfGas
 auto' n = do
   let loop = auto' (n - 1)
   try intros
-  choice
-    [ overFunctions $ \fname -> do
-        requireConcreteHole $ apply Saturated fname
-        loop
-    , overAlgebraicTerms $ \aname -> do
-        destructAuto aname
-        loop
-    , splitAuto >> loop
-    , assumption >> loop
-    , recursion
-    ]
+  assumption <|>
+    choice
+      [ overFunctions $ \fname -> do
+          requireConcreteHole $ apply Saturated fname
+          loop
+      , overAlgebraicTerms $ \aname -> do
+          destructAuto aname
+          loop
+      , splitAuto >> loop
+      , recursion
+      ]
 
 overFunctions :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
 overFunctions =
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index 0ccee7b977..491ff9724a 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
@@ -530,6 +530,7 @@ data RunTacticResults = RunTacticResults
   , rtr_other_solns :: [Synthesized (LHsExpr GhcPs)]
   , rtr_jdg         :: Judgement
   , rtr_ctx         :: Context
+  , rtr_timed_out   :: Bool
   } deriving Show
 
 
@@ -551,7 +552,7 @@ data UserFacingMessage
 instance Show UserFacingMessage where
   show NotEnoughGas = "Wingman ran out of gas when trying to find a solution.  \nTry increasing the `auto_gas` setting."
   show TacticErrors = "Wingman couldn't find a solution"
-  show TimedOut     = "Wingman timed out while trying to find a solution"
+  show TimedOut     = "Wingman timed out while finding a solution.  \nYou might get a better result if you increase the timeout duration."
   show NothingToDo  = "Nothing to do"
   show (InfrastructureError t) = "Internal error: " <> T.unpack t
 
diff --git a/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs b/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs
index a617683d6e..38306e55c7 100644
--- a/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs
+++ b/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE NumDecimals #-}
+
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 module AutoTupleSpec where
@@ -36,6 +38,7 @@ spec = describe "auto for tuple" $ do
           -- We should always be able to find a solution
           unsafePerformIO
             (runTactic
+              2e6
               emptyContext
               (mkFirstJudgement
                 emptyContext