LexiconAstPp: fixed syntax for include

[helm.git] / components / lexicon / lexiconEngine.ml

diff --git a/components/lexicon/lexiconEngine.ml b/components/lexicon/lexiconEngine.ml
index 1e1fe61c05147eef1dd8df67231df4f18ee3b7b1..a0792d2281fd09bfc4ecf2fa0d05beb7ddf23327 100644 (file)
--- a/components/lexicon/lexiconEngine.ml
+++ b/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