Don't let Agda print to stdout

Author: nvarner

src/Options.hs

@@ -43,12 +43,13 @@ data Options = Options
     optRawResponses :: Bool,
     optSetup :: Bool,
     optHelp :: Bool,
-    optVersion :: Bool
+    optVersion :: Bool,
+    optStdin :: Bool
   }
 
 defaultOptions :: Options
 defaultOptions =
-  Options {optViaTCP = Nothing, optRawAgdaOptions = [], optRawResponses = False, optSetup = False, optHelp = False, optVersion = False}
+  Options {optViaTCP = Nothing, optRawAgdaOptions = [], optRawResponses = False, optSetup = False, optHelp = False, optVersion = False, optStdin = False}
 
 options :: [OptDescr (Options -> Options)]
 options =
@@ -84,7 +85,12 @@ options =
       ['V']
       ["version"]
       (NoArg (\opts -> opts {optVersion = True}))
-      "print version information and exit"
+      "print version information and exit",
+    Option
+      []
+      ["stdio"]
+      (NoArg (\opts -> opts {optStdin = True}))
+      "connect via stdio"
   ]
 
 versionNumber :: Int

src/Server/Model/AgdaLib.hs

@@ -71,7 +71,9 @@ initAgdaLibWithOrigin origin = do
   let libName = ""
   let tcState = TCM.initState
 #endif
-  tcStateRef <- liftIO $ newIORef tcState
+  let persistentState = TCM.stPersistentState tcState
+  let tcState' = tcState { TCM.stPersistentState = persistentState { TCM.stInteractionOutputCallback = \_ -> return () } }
+  tcStateRef <- liftIO $ newIORef tcState'
   let tcEnv = TCM.initEnv
   let optionsPragma = OptionsPragma [] empty
   return $ AgdaLib libName [] optionsPragma [] tcStateRef tcEnv origin