X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.mli;h=6c8b8660518eb70cf07d5ae20e6a0c3f839cb5cf;hb=fafa203bb8521f516a0e87ef28d2cedccb72f795;hp=6b9f235cd6ad6628d20aaa6632f0633a237a9585;hpb=6b5e1d495c61f459738187e8d71efadb162abdbe;p=helm.git diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index 6b9f235cd..6c8b86605 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -25,6 +25,7 @@ exception Drop exception UnableToInclude of string +exception IncludedFileNotCompiled of string type statement = (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement @@ -34,11 +35,13 @@ type statement = val eval_string: ?do_heavy_checks:bool -> ?include_paths:string list -> + ?clean_baseuri:bool -> MatitaTypes.status ref -> string -> unit val eval_from_stream: ?do_heavy_checks:bool -> ?include_paths:string list -> + ?clean_baseuri:bool -> MatitaTypes.status ref -> char Stream.t -> (MatitaTypes.status -> statement -> unit) -> unit @@ -46,6 +49,7 @@ val eval_from_stream: val eval_from_stream_greedy: ?do_heavy_checks:bool -> ?include_paths:string list -> + ?clean_baseuri:bool -> MatitaTypes.status ref-> char Stream.t -> (MatitaTypes.status -> statement -> unit) -> unit @@ -53,6 +57,7 @@ val eval_from_stream_greedy: val eval_ast: ?do_heavy_checks:bool -> ?include_paths:string list -> + ?clean_baseuri:bool -> MatitaTypes.status -> statement -> MatitaTypes.status