From cd5dbc66ce2fd6bf1d38e40599a279df8c01a9ce Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 May 2021 13:30:54 +0200
Subject: [PATCH] fix: isolate std streams for all commands in server mode

Fixes #475
---
 src/Lean/Server/Snapshots.lean                | 21 ++++++++++++++-----
 tests/lean/interactive/stdOutput.lean         |  5 +++++
 .../interactive/stdOutput.lean.expected.out   |  0
 3 files changed, 21 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/interactive/stdOutput.lean
 create mode 100644 tests/lean/interactive/stdOutput.lean.expected.out

diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index 103c4f81aa..55a7d1cbc8 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -103,11 +103,22 @@ def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot Mess
         fileName := inputCtx.fileName
         fileMap  := inputCtx.fileMap
       }
-    EIO.toIO ioErrorFromEmpty $
-      Elab.Command.catchExceptions
-        (Elab.Command.elabCommand cmdStx)
-        cmdCtx cmdStateRef
-    let postCmdState ← cmdStateRef.get
+    let (output, _) ← IO.FS.withIsolatedStreams do
+      EIO.toIO ioErrorFromEmpty do
+        Elab.Command.catchExceptions
+          (Elab.Command.elabCommand cmdStx)
+          cmdCtx cmdStateRef
+    let mut postCmdState ← cmdStateRef.get
+    if !output.isEmpty then
+      postCmdState := {
+        postCmdState with
+        messages := postCmdState.messages.add {
+          fileName := inputCtx.fileName
+          severity := MessageSeverity.information
+          pos      := inputCtx.fileMap.toPosition snap.endPos
+          data     := output
+        }
+      }
     let postCmdSnap : Snapshot := {
         beginPos := cmdPos
         stx := cmdStx
diff --git a/tests/lean/interactive/stdOutput.lean b/tests/lean/interactive/stdOutput.lean
new file mode 100644
index 0000000000..856a63b589
--- /dev/null
+++ b/tests/lean/interactive/stdOutput.lean
@@ -0,0 +1,5 @@
+import Lean
+
+elab "foo" : command => IO.println "hi"
+#eval "ho"
+foo
diff --git a/tests/lean/interactive/stdOutput.lean.expected.out b/tests/lean/interactive/stdOutput.lean.expected.out
new file mode 100644
index 0000000000..e69de29bb2