X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaEngine.ml;h=430151d9a42fbd1594391aac8a1722bb4f8eff81;hb=41be5e85a1103a5b14495bb487995a6a88e79c48;hp=c0f74962da394fd73325f75e869f637f45321603;hpb=3ce38077e0b1e2a38ad513d3c108d7ef3c09bb7c;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index c0f74962d..430151d9a 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -30,54 +30,29 @@ open GrafiteTypes
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
 
-let eval_from_stream 
-  ?do_heavy_checks ?include_paths ?clean_baseuri status str cb 
-=
-  try
-    while true do
-      let ast = GrafiteParser.parse_statement str in
-      cb !status ast;
-      status :=
-       GrafiteEngine.eval_ast
-        ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
-        ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
-        ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
-    done
-  with End_of_file -> ()
-
-let eval_from_stream_greedy 
-  ?do_heavy_checks ?include_paths ?clean_baseuri status str cb 
+let eval_ast ~include_paths ?do_heavy_checks ?clean_baseuri status ast =
+ GrafiteEngine.eval_ast
+  ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths)
+  ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
+  ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
+  ?do_heavy_checks ?clean_baseuri status ast
+
+let eval_from_stream ?(prompt=false) ?do_heavy_checks ~include_paths
+ ?clean_baseuri status str cb 
 =
   while true do
-    print_string "matita> ";
-    flush stdout;
+    if prompt then (print_string "matita> "; flush stdout);
     let ast = GrafiteParser.parse_statement str in
     cb !status ast;
     status :=
-     GrafiteEngine.eval_ast
-      ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
-      ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
-      ?do_heavy_checks ?include_paths ?clean_baseuri !status ast 
+     eval_ast ~include_paths ?do_heavy_checks ?clean_baseuri !status ast
   done
 ;;
 
-let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str =
+let eval_string ?do_heavy_checks ~include_paths ?clean_baseuri status str =
+ try
   eval_from_stream 
-    ?do_heavy_checks ?include_paths ?clean_baseuri status
+    ?do_heavy_checks ~include_paths ?clean_baseuri status
       (Ulexing.from_utf8_string str) (fun _ _ -> ())
-
-let default_options () = no_options
-
-let initial_status =
-  lazy {
-    aliases = DisambiguateTypes.Environment.empty;
-    multi_aliases = DisambiguateTypes.Environment.empty;
-    moo_content_rev = [];
-    metadata = [];
-    proof_status = No_proof;
-    options = default_options ();
-    objects = [];
-    coercions = [];
-    notation_ids = [];
-  }
+ with End_of_file -> ()