captureException

Mathlib.Util.ParseCommand

URI: https://scilib.ai/kg/mathlib#Mathlib.GuardExceptions.captureException

Lean4

/-- `captureException env s input` uses the given `Environment` `env` to parse the `String` `input`
using the `ParserFn` `s`.

This is a variation of `Lean.Parser.runParserCategory`.
-/
def captureException (env : Environment) (s : ParserFn) (input : String) : Except String Syntax :=
  let ictx := mkInputContext input "<input>"
  let s := s.run ictx { env, options := { } } (getTokenTable env) (mkParserState input)
  if !s.allErrors.isEmpty then .error (s.toErrorMsg ictx)
  else if ictx.atEnd s.pos then .ok s.stxStack.back else .error ((s.mkError "end of input").toErrorMsg ictx)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru