refactor: rename isExitCommand -> isTerminalCommand
This commit is contained in:
parent
8dfae9eb38
commit
c06cffa54f
3 changed files with 3 additions and 3 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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`.-/
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue