1. Several files in grafite that should be in grafite_parser moved there.

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index c0f74962da394fd73325f75e869f637f45321603..cfbf74798d8ef661ee13395cd13e7153bfb2107f 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -31,7 +31,7 @@ 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 
+  ?do_heavy_checks ~include_paths ?clean_baseuri status str cb 
 =
   try
     while true do
@@ -39,14 +39,15 @@ let eval_from_stream
       cb !status ast;
       status :=
        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 ?include_paths ?clean_baseuri !status ast
+        ?do_heavy_checks ?clean_baseuri !status ast
     done
   with End_of_file -> ()
 
 let eval_from_stream_greedy 
-  ?do_heavy_checks ?include_paths ?clean_baseuri status str cb 
+  ?do_heavy_checks ~include_paths ?clean_baseuri status str cb 
 =
   while true do
     print_string "matita> ";
@@ -55,15 +56,16 @@ let eval_from_stream_greedy
     cb !status ast;
     status :=
      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 ?include_paths ?clean_baseuri !status ast 
+      ?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 =
   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