+ (** TODO repellent code ... *)
+let moo_root_dir = lazy (
+ let url =
+ List.assoc "cic:/matita/"
+ (List.map
+ (fun pair ->
+ match
+ Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair)
+ with
+ | [a;b] -> a, b
+ | _ -> assert false)
+ (Helm_registry.get_list Helm_registry.string "getter.prefix"))
+ in
+ String.sub url 7 (String.length url - 7) (* remove heading "file:///" *)
+)
+
+let close_using_moos buris =
+ let rev_deps = Hashtbl.create 97 in
+ let all_moos =
+ HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo")
+ (Lazy.force moo_root_dir)
+ in
+ List.iter
+ (fun path ->
+ let _, metadata = MatitaMoo.load_moo ~fname:path in
+ let baseuri_of_current_moo =
+ let rec aux = function
+ | [] -> assert false
+ | GrafiteAst.Baseuri buri::_ -> buri
+ | _ :: tl -> aux tl
+ in
+ aux metadata
+ in
+ let deps =
+ HExtlib.filter_map
+ (function
+ | GrafiteAst.Dependency buri -> Some buri
+ | _ -> None )
+ metadata
+ in
+ List.iter
+ (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_moo) deps)
+ all_moos;
+ let buris_to_remove =
+ HExtlib.list_uniq
+ (List.fast_sort Pervasives.compare
+ (List.flatten (List.map (Hashtbl.find_all rev_deps) buris)))
+ in
+ let objects_to_remove =
+ let objs_of_buri buri =
+ HExtlib.filter_map
+ (function
+ | Http_getter_types.Ls_object o ->
+ Some (buri ^ "/" ^ o.Http_getter_types.uri)
+ | _ -> None)
+ (Http_getter.ls buri)
+ in
+ List.flatten (List.map objs_of_buri (buris @ buris_to_remove))
+ in
+ objects_to_remove
+