*** WARNING: DTD Change ***

@name of ht:SECTION renamed in @uri
Its semantics has not changed (it is the base URI of relative URIs defined
inside the section).

HELM/MoWGLI stylesheets updated accordingly.


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

1 files changed, 9 insertions, 9 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 628277b1a..44bf38b50 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -639,11 +639,16 @@ let _ =
       output_string (match !theory_channel with Some ch -> ch | _ -> stdout) s)
 ;;
 
+let uri_of_dirpath dir =
+  "/" ^ String.concat "/" 
+    (List.map Names.string_of_id (List.rev (Names.repr_dirpath dir)))
+;;
+
 let _ =
   Lib.set_xml_open_section
-    (fun id ->
-      let s = Names.string_of_id id in
-      theory_output_string ("<ht:SECTION name=\""^s^"\">"))
+    (fun _ ->
+      let s = "cic:" ^ uri_of_dirpath (Lib.cwd ()) in
+      theory_output_string ("<ht:SECTION uri=\""^s^"\">"))
 ;;
 
 let _ =
@@ -651,14 +656,9 @@ let _ =
     (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>.<br/>"
+      (Printf.sprintf "<b>Require</b> <a href=\"theory:%s.theory\">%s</a>.<br/>"
        (uri_of_dirpath d) (Names.string_of_dirpath d)))
 ;;