From 411144ab18b81fdcca0b38ac378f64a6e48197ae Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Tue, 30 Mar 2004 16:31:02 +0000
Subject: *** 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
---
 contrib/xml/xmlcommand.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 628277b1ae..44bf38b503 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)))
 ;;
-- 
cgit v1.2.3