From: Andrea Asperti Date: Fri, 5 Nov 2010 12:56:55 +0000 (+0000) Subject: - better names, interface simplified X-Git-Tag: make_still_working~2710 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=098e3728bb1d993145b893b83ac6e01173b58486;p=helm.git - better names, interface simplified --- diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index 4489920a6..3e13a386a 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -366,14 +366,8 @@ module Make = Librarian.Make(F) (* FINE EX MATITACLIB *) - - -(* this function calls the parser in a way that it does not perform inclusions, - * so that we can ensure the inclusion is performed after the included file - * is compiled (if needed). matitac does not need that, since it compiles files - * in the good order, here files may be compiled on demand. *) -let wrap_with_make include_paths f x = - match f x with +let get_ast status ~include_paths text = + match GrafiteParser.parse_statement status (Ulexing.from_utf8_string text)with (GrafiteAst.Executable (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd -> @@ -389,9 +383,3 @@ let wrap_with_make include_paths f x = else raise (Failure ("Compiling: " ^ tgt)) | cmd -> cmd ;; - -let toplevel status ~include_paths text = - wrap_with_make include_paths - (GrafiteParser.parse_statement status) - (Ulexing.from_utf8_string text) -;; diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli index 29f3a5a0b..1175c2403 100644 --- a/matita/matita/matitaEngine.mli +++ b/matita/matita/matitaEngine.mli @@ -23,6 +23,12 @@ * http://helm.cs.unibo.it/ *) +val get_ast: + #GrafiteParser.status -> include_paths:string list -> string -> + GrafiteAst.statement + +(* heavy checks slow down the compilation process but give you some interesting + * infos like if the theorem is a duplicate *) val eval_ast : include_paths: string list -> ?do_heavy_checks:bool -> @@ -33,22 +39,8 @@ val eval_ast : (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) option) list -(* heavy checks slow down the compilation process but give you some interesting - * infos like if the theorem is a duplicate *) - exception EnrichedWithStatus of exn * GrafiteTypes.status -(* should be used only by the compiler since it looses the - * disambiguation_context (text,prefix_len,_) *) -val eval_from_stream : - include_paths:string list -> ?do_heavy_checks:bool -> GrafiteTypes.status -> - Ulexing.lexbuf -> (GrafiteTypes.status -> GrafiteAst.statement -> unit) -> - GrafiteTypes.status - -val toplevel: - #GrafiteParser.status -> include_paths:string list -> string -> - GrafiteParser.ast_statement - (* EX MATITACLIB *) module Make : sig val make: string -> string list -> bool diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 6aae0020d..8e1eb69d4 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -188,7 +188,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff match statement with | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; - let ast = MatitaEngine.toplevel grafite_status include_paths text in + let ast = MatitaEngine.get_ast grafite_status include_paths text in ast, text | `Ast (st, text) -> st, text in