[ agda#4647 ] option --top-level-interaction-no-private to disable fix

Should the new behavior of top-level interaction commands (reload on
not-in-scope errors) be disruptive to one's workflow, this option brings
back the old behavior (with private declarations not in scope).

src/full/Agda/Interaction/InteractionTop.hs

@@ -1,5 +1,6 @@
-{-# OPTIONS_GHC -fno-cse #-}
+{-# LANGUAGE NondecreasingIndentation #-}
 
+{-# OPTIONS_GHC -fno-cse #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 module Agda.Interaction.InteractionTop
@@ -942,6 +943,8 @@ withCurrentFile m = do
 -- | Top-level commands switch to 'TopLevelInteraction' mode if necessary.
 atTopLevel :: CommandM a -> CommandM a
 atTopLevel cmd = do
+  -- Don't switch if --top-level-interaction-no-private.
+  ifM (optTopLevelInteractionNoPrivate <$> pragmaOptions) continue $ {-else-} do
   gets interactionMode >>= \case
     TopLevelInteraction -> continue  -- Already in the correct mode.
     RegularInteraction  -> continue `handleNotInScope` do

src/full/Agda/Interaction/Options.hs

@@ -166,6 +166,10 @@ data PragmaOptions = PragmaOptions
   , optKeepPatternVariables      :: Bool
       -- ^ Should case splitting replace variables with dot patterns
       --   (False) or keep them as variables (True).
+  , optTopLevelInteractionNoPrivate :: Bool
+     -- ^ If @True@, disable reloading mechanism introduced in issue #4647
+     --   that brings private declarations in main module into scope
+     --   to remedy not-in-scope errors in top-level interaction commands.
   , optInstanceSearchDepth       :: Int
   , optOverlappingInstances      :: Bool
   , optQualifiedInstances        :: Bool  -- ^ Should instance search consider instances with qualified names?
@@ -283,6 +287,7 @@ defaultPragmaOptions = PragmaOptions
   , optCubical                   = False
   , optPostfixProjections        = False
   , optKeepPatternVariables      = False
+  , optTopLevelInteractionNoPrivate = False
   , optInstanceSearchDepth       = 500
   , optOverlappingInstances      = False
   , optQualifiedInstances        = True
@@ -741,6 +746,9 @@ postfixProjectionsFlag o = return $ o { optPostfixProjections = True }
 keepPatternVariablesFlag :: Flag PragmaOptions
 keepPatternVariablesFlag o = return $ o { optKeepPatternVariables = True }
 
+topLevelInteractionNoPrivateFlag :: Flag PragmaOptions
+topLevelInteractionNoPrivateFlag o = return $ o { optTopLevelInteractionNoPrivate = True }
+
 instanceDepthFlag :: String -> Flag PragmaOptions
 instanceDepthFlag s o = do
   d <- integerArgument "--instance-search-depth" s
@@ -1028,6 +1036,8 @@ pragmaOptions =
                     "make postfix projection notation the default"
     , Option []     ["keep-pattern-variables"] (NoArg keepPatternVariablesFlag)
                     "don't replace variables with dot patterns during case splitting"
+    , Option []     ["top-level-interaction-no-private"] (NoArg topLevelInteractionNoPrivateFlag)
+                    "in top-level interaction commands, don't reload file to bring private declarations into scope"
     , Option []     ["instance-search-depth"] (ReqArg instanceDepthFlag "N")
                     "set instance search depth to N (default: 500)"
     , Option []     ["overlapping-instances"] (NoArg overlappingInstancesFlag)

src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs

@@ -219,12 +219,12 @@ instance EmbPrj Doc where
 
 instance EmbPrj PragmaOptions where
   icod_ = \case
-    PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx ->
-      icodeN' PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx
+    PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy ->
+      icodeN' PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy
 
   value = vcase $ \case
-    [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, aa, bb, cc, dd, ee, ff, gg, hh, ii, jj, kk, ll, mm, nn, oo, pp, qq, rr, ss, tt, uu, vv, ww, xx] ->
-      valuN PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx
+    [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, aa, bb, cc, dd, ee, ff, gg, hh, ii, jj, kk, ll, mm, nn, oo, pp, qq, rr, ss, tt, uu, vv, ww, xx, yy] ->
+      valuN PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy
     _ -> malformed
 
 instance EmbPrj WarningMode where