diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
index bacb831092..36dafd1a0d 100644
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -66,7 +66,7 @@ def processCommand : FrontendM Bool := do
       pure true -- Done
     else
       profileitM IO.Error "elaboration" scope.opts <| elabCommandAtFrontend cmd
-      pure (Parser.isExitCommand cmd)
+      pure (Parser.isTerminalCommand cmd)
 
 partial def processCommands : FrontendM Unit := do
   let done ← processCommand
diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean
index 40b0cd6795..c9cfdd2c4d 100644
--- a/src/Lean/Parser/Module.lean
+++ b/src/Lean/Parser/Module.lean
@@ -59,7 +59,7 @@ private def mkEOI (pos : String.Pos) : Syntax :=
 def isEOI (s : Syntax) : Bool :=
   s.isOfKind `Lean.Parser.Module.eoi
 
-def isExitCommand (s : Syntax) : Bool :=
+def isTerminalCommand (s : Syntax) : Bool :=
   s.isOfKind ``Command.exit || s.isOfKind ``Command.import
 
 private def consumeInput (c : ParserContext) (pos : String.Pos) : String.Pos :=
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index 01c9477c02..474692c36d 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -69,7 +69,7 @@ def infoTree (s : Snapshot) : InfoTree :=
   s.cmdState.infoState.trees[0]!
 
 def isAtEnd (s : Snapshot) : Bool :=
-  Parser.isEOI s.stx || Parser.isExitCommand s.stx
+  Parser.isEOI s.stx || Parser.isTerminalCommand s.stx
 
 open Command in
 /-- Use the command state in the given snapshot to run a `CommandElabM`.-/