Function emit_document 

pub fn emit_document(
    imported: &ImportedContext,
    target: &str,
) -> Result<EmittedDocument, Verdict>

The dependency closure of target, as a LOGOS document.

A theorem’s proof is carried only when the import retained it (import_retaining_closure retains the whole closure); an opaque theorem in the closure whose proof was not retained is refused, never written as an axiom.