- better names, interface simplified

[helm.git] / matita / matita / matitaEngine.ml

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 4489920a6bb36c547a718a7effb3e2e568c0b183..3e13a386a81e9b66248db5ba829f33520b293a92 100644 (file)
--- 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)
-;;