diff options
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 14 |
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))) +;; |