X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FlexiconEngine.mli;h=eab7e53e75af3e059e60b8bf0c2a5df9c4aebde9;hb=cebed8851dcaf8ceeb4e5f74b52705bf0c18a456;hp=8e8b420ba03fabc9354a784b835e7313db38c3b9;hpb=004fbb54bc0a2b971f08bcf830ac8cbdafcdbe57;p=helm.git diff --git a/helm/software/components/lexicon/lexiconEngine.mli b/helm/software/components/lexicon/lexiconEngine.mli index 8e8b420ba..eab7e53e7 100644 --- a/helm/software/components/lexicon/lexiconEngine.mli +++ b/helm/software/components/lexicon/lexiconEngine.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -exception IncludedFileNotCompiled of string +exception IncludedFileNotCompiled of string * string type status = { aliases: DisambiguateTypes.environment; (** disambiguation aliases *) @@ -42,3 +42,5 @@ val set_proof_aliases: (DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item) list -> status +(* this callback is called on every lexicon command *) +val set_callback: (LexiconAst.command -> unit) -> unit