- better names, interface simplified

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)
-;;

diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli
index 29f3a5a0b64169649655dfb29c1738b19d3b7aec..1175c24030a8f66e2521039f55a8ebdf39aafe09 100644 (file)
--- 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 6aae0020da0d3a0a6b2091b46f179dac8ea40890..8e1eb69d481d7d92fa4bf41f62937e3fe8acc787 100644 (file)
--- 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