[ fix #201 ] Drop backend when running in interactive mode

agda · Oct 11, 2023 · 46c5473 · 46c5473
1 parent b9821f1
commit 46c5473
Showing 1 changed file with 8 additions and 1 deletion.
diff --git a/src/Main.hs b/src/Main.hs
@@ -1,6 +1,9 @@
 module Main where
 
+import Control.Monad.IO.Class ( MonadIO(..) )
+
 import System.Console.GetOpt
+import System.Environment ( getArgs )
 
 import qualified Language.Haskell.Exts.Syntax as Hs
 import qualified Language.Haskell.Exts.Build as Hs
@@ -71,4 +74,8 @@ backend = Backend'
   , mayEraseType          = \ _ -> return True
   }
 
-main = runAgda [Backend backend]
+main = do
+  -- Issue #201: drop backend when running in interactive mode
+  let interactionFlag = Option ['I'] ["interactive", "interaction", "interaction-json"] (NoArg ()) ""
+  (i , _ , _) <- getOpt Permute [interactionFlag] <$> getArgs
+  runAgda [Backend backend | null i ]