X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=9707149d568cd52bb87de6846f782bebce038322;hb=dc861d214cb992a898f81752614201b8074eef12;hp=9fc24acf1c5df35887cf2c10ef94db962559bd0c;hpb=cb473667ca89549ed0ca6dd2bfb03a5fe9eeaa82;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 9fc24acf1..9707149d5 100644
--- 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
@@ -497,12 +501,12 @@ let disambiguate_command status = function
       let status,obj = disambiguate_obj status obj in
        status, GrafiteAst.Obj (loc,obj)
 
-let try_open_in paths path =
+let try_open_in ~f paths path =
   let rec aux = function
-  | [] -> open_in path
+  | [] -> f path
   | p :: tl ->
       try
-        open_in (p ^ "/" ^ path)
+        f (p ^ "/" ^ path)
       with Sys_error _ -> aux tl
   in
   try
@@ -527,14 +531,14 @@ let eval_command opts status cmd =
         (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
   | GrafiteAst.Include (loc, path) ->
      let path = MatitaMisc.obj_file_of_script path in
-     let stream = 
-       try
-         Stream.of_channel (try_open_in opts.include_paths path) 
-       with Sys_error _ -> raise (UnableToInclude path)
-     in
-     let status = ref status in
-      !eval_from_stream_ref status stream (fun _ _ -> ());
-      !status
+     (try
+       let ic = try_open_in ~f:open_in opts.include_paths path in
+       let stream = Stream.of_channel ic in
+       let status = ref status in
+       !eval_from_stream_ref status stream (fun _ _ -> ());
+       close_in ic;
+       !status
+     with Sys_error _ -> raise (UnableToInclude path))
   | GrafiteAst.Set (loc, name, value) -> 
       let value = 
         if name = "baseuri" then
@@ -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 ->
@@ -614,6 +627,12 @@ let eval_command opts status cmd =
            begin
              let dbd = MatitaDb.instance () in
              let similar = MetadataQuery.match_term ~dbd ty in
+             let similar_len = List.length similar in
+             if similar_len> 30 then
+               (MatitaLog.message
+                 ("Duplicate check will compare your theorem with " ^ 
+                   string_of_int similar_len ^ 
+                   " theorems, this may take a while."));
              let convertible =
                List.filter (
                  fun u ->
@@ -671,39 +690,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 () =
 (*