From 72620f6ac574cbbaefc40158c209ec0823df1c92 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 29 Mar 2004 13:08:50 +0000 Subject: Export Require git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5599 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/xml/xmlcommand.ml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) 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 "") ;; + +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 %s" + (uri_of_dirpath d) (Names.string_of_dirpath d))) +;; -- cgit v1.2.3