X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FlexiconEngine.ml;h=a0792d2281fd09bfc4ecf2fa0d05beb7ddf23327;hb=750d027aedc76aac9def8885dc2bdb6ccdc049d9;hp=1e1fe61c05147eef1dd8df67231df4f18ee3b7b1;hpb=14d7eabdb425c4dbcda5de18fac0735fde5d176b;p=helm.git

diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml
index 1e1fe61c0..a0792d228 100644
--- a/helm/software/components/lexicon/lexiconEngine.ml
+++ b/helm/software/components/lexicon/lexiconEngine.ml
@@ -25,6 +25,10 @@
 
 (* $Id$ *)
 
+let out = ref ignore
+
+let set_callback f = out := f
+
 (* lexicon file name * ma file name *)
 exception IncludedFileNotCompiled of string * string 
 exception MetadataNotFound of string        (* file name *)
@@ -112,6 +116,7 @@ let set_proof_aliases mode status new_aliases =
 
 
 let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd =
+ !out cmd;
  let notation_ids' = CicNotation.process_notation cmd in
  let status =
    { status with notation_ids = notation_ids' @ status.notation_ids } in