Export Require

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5599 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 1 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 74d7878e12..cddb0224d7 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -895,7 +895,7 @@ let _ =
            command (coqdoc^options^" -d "^dir^" "^fn^".v");
            let dot = if fn.[0]='/' then "." else "" in
            command ("mv "^dir^"/"^dot^"*.html "^fn^".xml ");
-           (*command ("rm "^fn^".v");*)
+           command ("rm "^fn^".v");
            print_string("\nWriting on file \"" ^ fn ^ ".xml\" was succesful\n"))
        (theory_filename xml_library_root))
 ;;
@@ -918,3 +918,15 @@ let _ =
   Lib.set_xml_close_section
     (fun _ -> theory_output_string "</ht:SECTION>")
 ;;
+
+let uri_of_dirpath dir =
+  "/" ^ String.concat "/" 
+    (List.map Names.string_of_id (List.rev (Names.repr_dirpath dir)))
+;;
+
+let _ =
+  Library.set_xml_require
+    (fun d -> theory_output_string 
+      (Printf.sprintf "Require <a href=\"theory:%s.theory\">%s</a>"
+       (uri_of_dirpath d) (Names.string_of_dirpath d)))
+;;