Main.lean

@@ -23,10 +23,10 @@ def parseCommand (s: String): Except String Command := do
       return { cmd := s.take offset, payload := payload }
   | .none => throw "Command is empty"
 
-partial def loop : MainM Unit := do repeat do
+partial def loop : MainM Unit := do
   let state ← get
   let command ← (← IO.getStdin).getLine
-  if command.trim.length = 0 then break
+  if command.trim.length = 0 then return ()
   match parseCommand command with
   | .error error =>
     let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
@@ -43,6 +43,7 @@ partial def loop : MainM Unit := do repeat do
       let message ← e.toMessageData.toString
       let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
       IO.println error.compress
+  loop
 
 
 unsafe def main (args: List String): IO Unit := do

Test/Environment.lean

@@ -110,7 +110,7 @@ def test_symbol_location : TestT IO Unit := do
     checkTrue "file" result.sourceUri?.isNone
     checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
     checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
-    let .ok { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed"
+    let .ok { imports, constNames, extraConstNames } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed"
     checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
     checkTrue "constNames" $ constNames.contains "Nat.succ_add"