Lean4
/-- Embeds a `CoreM` action in `CommandElabM` by supplying the information stored in `info`.
Copy of `ContextInfo.runCoreM` that makes use of the `CommandElabM` context for:
* logging messages produced by the `CoreM` action,
* metavariable generation,
* auxiliary declaration generation.
-/
def runCoreMWithMessages (info : ContextInfo) (x : CoreM α) : CommandElabM α := do
-- We assume that this function is used only outside elaboration, mostly in the language server,
-- and so we can and should provide access to information regardless whether it is exported.
let env := info.env.setExporting false
let ctx ← read
let (x, newState) ←
(withOptions (fun _ => info.options) x).toIO
{ currNamespace := info.currNamespace, openDecls := info.openDecls
fileName := ctx.fileName, fileMap := ctx.fileMap }
{ env, ngen := info.ngen, auxDeclNGen := { namePrefix := info.parentDecl?.getD .anonymous } }
-- Migrate logs back to the main context.
modify fun state =>
{ state with messages := state.messages ++ newState.messages,
traceState.traces := state.traceState.traces ++ newState.traceState.traces }
return x
