X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.mli;h=47f0af02bf455ea6ba3f919a16b679f4fcbd81be;hb=dfc88cb4e7d0dca81cabe418d2c732cd22166726;hp=cb88940ffde19daea908157bc497b83acc0c4a3b;hpb=5ca23b5031f8bea8be8a60931affd9e19e389e4b;p=helm.git diff --git a/helm/software/components/grafite_parser/grafiteParser.mli b/helm/software/components/grafite_parser/grafiteParser.mli index cb88940ff..47f0af02b 100644 --- a/helm/software/components/grafite_parser/grafiteParser.mli +++ b/helm/software/components/grafite_parser/grafiteParser.mli @@ -29,10 +29,15 @@ type 'a localized_option = type ast_statement = (CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + CicNotationPt.term GrafiteAst.reduction, + CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement +exception NoInclusionPerformed of string (* full path *) + type statement = + ?never_include:bool -> + (* do not call LexiconEngine to do includes, always raise NoInclusionPerformed *) include_paths:string list -> LexiconEngine.status -> LexiconEngine.status * ast_statement localized_option @@ -41,3 +46,5 @@ val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *) val statement: statement Grammar.Entry.e +(* this callback is called on every include command *) +val set_callback: (string -> unit) -> unit