From: Andrea Asperti <andrea.asperti@unibo.it>
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