* Generic Toplevel.add_hook interface allows to analyze the result of transactions (including failed ones). For example, see src/Pure/ProofGeneral/proof_general_pgip.ML for theorem dependency output of transactions resulting in a new theory state.