]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaEngine.ml
Debugging code commented out.
[helm.git] / helm / matita / matitaEngine.ml
index 3d738e1b9b74e62f2c7f21155dc56a19a96263cc..9707149d568cd52bb87de6846f782bebce038322 100644 (file)
@@ -501,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
@@ -531,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
@@ -627,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 ->