matitac now automatically cleans a non empty baseuri

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 9fc24acf1c5df35887cf2c10ef94db962559bd0c..3d738e1b9b74e62f2c7f21155dc56a19a96263cc 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -32,7 +32,11 @@ exception UnableToInclude of string;;
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
 
-type options = { do_heavy_checks: bool ; include_paths: string list }
+type options = { 
+  do_heavy_checks: bool ; 
+  include_paths: string list ;
+  clean_baseuri: bool
+}
 
 type statement =
   (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement
@@ -546,6 +550,15 @@ let eval_command opts status cmd =
         else
           value
       in
+      if not (MatitacleanLib.is_empty value) then
+        begin
+          MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
+          if opts.clean_baseuri then
+            begin 
+              MatitaLog.message ("cleaning baseuri " ^ value);
+              MatitacleanLib.clean_baseuris [value]
+            end
+        end;
       set_option status name value
   | GrafiteAst.Drop loc -> raise Drop
   | GrafiteAst.Qed loc ->
@@ -671,39 +684,47 @@ let eval_executable opts status ex =
 let eval_comment status c = status
             
 
-let eval_ast ?(do_heavy_checks=false) ?(include_paths=[]) status st =
-  let opts = 
-    {do_heavy_checks = do_heavy_checks ; include_paths = include_paths}
+let eval_ast 
+  ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st 
+=
+  let opts = {
+    do_heavy_checks = do_heavy_checks ; 
+    include_paths = include_paths;
+    clean_baseuri = clean_baseuri }
   in
   match st with
   | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex
   | GrafiteAst.Comment (_,c) -> eval_comment status c
 
-let eval_from_stream ?do_heavy_checks ?include_paths status str cb =
+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 := eval_ast ?do_heavy_checks ?include_paths !status ast
+      status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
     done
   with End_of_file -> ()
 
 (* to avoid a long list of recursive functions *)
 let _ = eval_from_stream_ref := eval_from_stream
   
-let eval_from_stream_greedy ?do_heavy_checks ?include_paths status str cb =
+let eval_from_stream_greedy 
+  ?do_heavy_checks ?include_paths ?clean_baseuri status str cb 
+=
   while true do
     print_string "matita> ";
     flush stdout;
     let ast = GrafiteParser.parse_statement str in
     cb !status ast;
-    status := eval_ast ?do_heavy_checks ?include_paths !status ast 
+    status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast 
   done
 ;;
 
-let eval_string ?do_heavy_checks ?include_paths status str =
+let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str =
   eval_from_stream 
-    ?do_heavy_checks ?include_paths status (Stream.of_string str) (fun _ _ ->())
+    ?do_heavy_checks ?include_paths ?clean_baseuri status (Stream.of_string str) (fun _ _ ->())
 
 let default_options () =
 (*