]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/grafiteParser.ml
- Procedural: moved in a directory on its own
[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml
index 9a0cc9f438ae90941aa7f41ddf169bf626777224..f3dd386a91540b15c729dbf22a0b4c7c25fcaf4a 100644 (file)
@@ -60,6 +60,10 @@ type by_continuation =
  | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
  | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
 
+let out = ref ignore
+
+let set_callback f = out := f
+
 EXTEND
   GLOBAL: term statement;
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
@@ -674,7 +678,8 @@ EXTEND
             (loc,GrafiteAst.Include (iloc,buri))))
     | scom = lexicon_command ; SYMBOL "." ->
        fun ~include_paths status ->
-        let status = LexiconEngine.eval_command status scom in
+        !out scom;
+       let status = LexiconEngine.eval_command status scom in
          status,LNone loc
     | EOI -> raise End_of_file
     ]