X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.mli;h=d657e49752e2e23ac0e64dfcc2448cf6a12625a7;hb=a18562238677261e3d0b590e046290a14fe62e74;hp=1413e93fd97409b96518496a0fcf993d61007fe7;hpb=6cc401c4136bafb6515bd39d86db6b5a917318bf;p=helm.git diff --git a/helm/software/components/grafite_parser/grafiteParser.mli b/helm/software/components/grafite_parser/grafiteParser.mli index 1413e93fd..d657e4975 100644 --- a/helm/software/components/grafite_parser/grafiteParser.mli +++ b/helm/software/components/grafite_parser/grafiteParser.mli @@ -35,24 +35,24 @@ type ast_statement = exception NoInclusionPerformed of string (* full path *) -type statement = +type 'status 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 + (#LexiconEngine.status as 'status) -> + 'status * ast_statement localized_option -val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *) +val parse_statement: Ulexing.lexbuf -> #LexiconEngine.status statement (** @raise End_of_file *) -val statement: unit -> statement Grammar.Entry.e +val statement: unit -> #LexiconEngine.status statement Grammar.Entry.e (* this callback is called before every grafite statement *) val set_grafite_callback: - (LexiconEngine.status -> ast_statement -> unit) -> unit + (ast_statement -> unit) -> unit (* this callback is called before every lexicon command *) val set_lexicon_callback: - (LexiconEngine.status -> LexiconAst.command -> unit) -> unit + (LexiconAst.command -> unit) -> unit val push : unit -> unit val pop : unit -> unit