X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatitadep%2Fmatitadep.ml;h=de8f3d65db7a03d2f9f88b814890bb38ba00c599;hb=520d4370a540a98f5e5e1d85acfef0c982cc1e04;hp=ebb87695ffe248e4fdc9cc0aefb852b9273ae368;hpb=fde3b3d2e6cc48f6c9880136b1a0d565e2c78c1f;p=helm.git

diff --git a/matita/components/binaries/matitadep/matitadep.ml b/matita/components/binaries/matitadep/matitadep.ml
index ebb87695f..de8f3d65d 100644
--- a/matita/components/binaries/matitadep/matitadep.ml
+++ b/matita/components/binaries/matitadep/matitadep.ml
@@ -7,6 +7,10 @@ type file = {
 
 let graph = Hashtbl.create 503
 
+let rec purge dname bdeps = match bdeps with
+   | []       -> bdeps
+   | hd :: tl -> if hd = dname then bdeps else purge dname tl 
+
 let add fname =
    if Hashtbl.mem graph fname then () else
    Hashtbl.add graph fname {ddeps = []; rdeps = None}
@@ -18,29 +22,32 @@ let add_ddep fname dname =
 let init fname dname =
    add fname; add dname; add_ddep fname dname 
 
-let rec compute fname file = match file.rdeps with
+let rec compute bdeps fname file = match file.rdeps with
    | Some rdeps -> rdeps
    | None       ->
-      let rdeps = List.fold_left (iter fname) StringSet.empty file.ddeps in
+      let bdeps = fname :: bdeps in
+      let rdeps = List.fold_left (iter fname bdeps) StringSet.empty file.ddeps in
       Hashtbl.replace graph fname {file with rdeps = Some rdeps};
       rdeps
 
-and iter fname rdeps dname =
-   if StringSet.mem dname rdeps then
-      begin Printf.printf "%s: redundant %s\n" fname dname; rdeps end
-   else
+and iter fname bdeps rdeps dname =
+   if StringSet.mem dname rdeps then begin
+      Printf.printf "%s: redundant %s\n" fname dname;
+      rdeps 
+   end else if List.mem dname bdeps then begin
+      let loop = purge dname (List.rev bdeps) in
+      Printf.printf "circular: %s\n" (String.concat " " loop);
+      StringSet.add dname rdeps
+   end else
      let file = Hashtbl.find graph dname in
-     StringSet.add dname (StringSet.union (compute dname file) rdeps)
+     StringSet.add dname (StringSet.union (compute bdeps dname file) rdeps)
 
 let check () = 
-   let iter fname file = 
-      if StringSet.mem fname (compute fname file) then
-         Printf.printf "%s: circular\n" fname 
-   in
+   let iter fname file = ignore (compute [] fname file) in
    Hashtbl.iter iter graph 
 
 let rec read ich = 
-   let _ = Scanf.fscanf ich "./%s@:include \"%s@\". " init in
+   let _ = Scanf.sscanf (input_line ich) "%s@:include \"%s@\"." init in
    read ich
    
 let _ =