coqdoc: fix a few issues with xhtml validity (backport 1636f7 and 754abf1 from v8.4)

- For the style of identifiers, coqdoc was using a 'type' attribute of tag <span>. But this attribute isn't a legal attribute of tag <span> according to the xhtml norm. Instead, I propose to use 'title' for that. The coqdoc.css now supports both approaches. - The names of inner links (cross references #foo) were containing arbitrary characters (in the case of a notation string). For instance in Utf8_core : <a name=":type_scope:'∀'_x_'..'_x_','_x"> Instead, when strange characters are detected, we now hash the string via Digest, and use this hexa hash as html label. - And some whitespace before />
author: Pierre Letouzey <pierre.letouzey@inria.fr> 2014-12-05 16:29:39 +0100
committer: Pierre Letouzey <pierre.letouzey@inria.fr> 2014-12-09 12:14:39 +0100
commit: 5d2b096f29adf3d139c4de46321e26790e9b4211 (patch)
tree: 4f3db111c2b4821d2f8908c79cc404ede0115095 /tools/coqdoc
parent: 484a0c35662d3bb78aa1f2cd83ffcc1b1f761968 (diff)
2 files changed, 86 insertions, 15 deletions
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index ccd285f18..44399cd8b 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -160,8 +160,65 @@ tr.infrulemiddle hr {
 #footer { font-size: 65%;
           font-family: sans-serif; }
 
+/* Identifiers: <span class="id" title="...">) */
+
 .id { display: inline; }
 
+.id[title="constructor"] {
+    color: rgb(60%,0%,0%);
+}
+
+.id[title="var"] {
+    color: rgb(40%,0%,40%);
+}
+
+.id[title="variable"] {
+    color: rgb(40%,0%,40%);
+}
+
+.id[title="definition"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="abbreviation"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="lemma"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="instance"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="projection"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="method"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="inductive"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="record"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="class"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="keyword"] {
+ color : #cf1d1d;
+/*     color: black; */
+}
+
+/* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */
+
 .id[type="constructor"] { 
     color: rgb(60%,0%,0%);
 }
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index a3e4c4000..78a73a88b 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -535,8 +535,8 @@ module Html = struct
 	  printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
 	  printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
 	  printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
-	  printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\"/>\n" !charset;
-	  printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\"/>\n";
+	  printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\" />\n" !charset;
+	  printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\" />\n";
 	  printf "<title>%s</title>\n</head>\n\n" !page_title;
 	  printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n";
 	  printf "<div id=\"main\">\n\n"
@@ -595,10 +595,24 @@ module Html = struct
 	| '<' -> Buffer.add_string buff "&lt;"
 	| '>' -> Buffer.add_string buff "&gt;"
 	| '&' -> Buffer.add_string buff "&amp;"
+        | '\'' -> Buffer.add_string buff "&acute;"
+        | '\"' -> Buffer.add_string buff "&quot;"
 	| c -> Buffer.add_char buff c
       done;
       Buffer.contents buff
 
+  let sanitize_name s =
+    let rec loop esc i =
+      if i < 0 then if esc then escaped s else s
+      else match s.[i] with
+      | 'a'..'z' | 'A'..'Z' | '0'..'9' | '.' | '_' -> loop esc (i-1)
+      | '<' | '>' | '&' | '\'' | '\"' -> loop true (i-1)
+      | _ ->
+        (* This name contains complex characters:
+           this is probably a notation string, we simply hash it. *)
+        Digest.to_hex (Digest.string s)
+    in loop false (String.length s - 1)
+
   let latex_char _ = ()
   let latex_string _ = ()
 
@@ -628,19 +642,19 @@ module Html = struct
   let ident_ref m fid typ s =
     match find_module m with
     | Local ->
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
-	printf "<span class=\"id\" type=\"%s\">%s</span></a>" typ s
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m (sanitize_name fid);
+	printf "<span class=\"id\" title=\"%s\">%s</span></a>" typ s
     | External m when !externals ->
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
-	printf "<span class=\"id\" type=\"%s\">%s</span></a>" typ s
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m (sanitize_name fid);
+	printf "<span class=\"id\" title=\"%s\">%s</span></a>" typ s
     | External _ | Unknown ->
-	printf "<span class=\"id\" type=\"%s\">%s</span>" typ s
+	printf "<span class=\"id\" title=\"%s\">%s</span>" typ s
 
   let reference s r =
     match r with
     | Def (fullid,ty) ->
-	printf "<a name=\"%s\">" fullid;
-	printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s
+	printf "<a name=\"%s\">" (sanitize_name fullid);
+	printf "<span class=\"id\" title=\"%s\">%s</span></a>" (type_name ty) s
     | Ref (m,fullid,ty) ->
 	ident_ref m fullid (type_name ty) s
 
@@ -650,7 +664,7 @@ module Html = struct
     | Some ref -> reference s ref
     | None ->
 	if issymbchar then output_string s
-	else printf "<span class=\"id\" type=\"var\">%s</span>" s
+	else printf "<span class=\"id\" title=\"var\">%s</span>" s
 
   let sublexer c loc =
     let tag =
@@ -670,11 +684,11 @@ module Html = struct
     match Tokens.translate s with Some s -> s | None -> escaped s
 
   let keyword s loc = 
-    printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
+    printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
 
   let ident s loc =
     if is_keyword s then begin
-      printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
+      printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
     end else begin
       try
         match loc with
@@ -683,7 +697,7 @@ module Html = struct
             reference (translate s) (Index.find (get_module false) loc)
       with Not_found ->
 	if is_tactic s then
-	  printf "<span class=\"id\" type=\"tactic\">%s</span>" (translate s)
+	  printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s)
 	else
 	  if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
 	  then
@@ -835,7 +849,7 @@ module Html = struct
 	       "[library]", m ^ ".html", t
 	else
 	 sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
-	sprintf "%s.html#%s" m s, t)
+	sprintf "%s.html#%s" m (sanitize_name s), t)
 
   let format_bytype_index = function
     | Library, idx ->
@@ -844,7 +858,7 @@ module Html = struct
 	Index.map
 	  (fun s m ->
 	     let text = sprintf "[in <a href=\"%s.html\">%s</a>]" m m in
-	       (text, sprintf "%s.html#%s" m s, t)) idx
+	       (text, sprintf "%s.html#%s" m (sanitize_name s), t)) idx
 
   (* Impression de la table d'index *)
   let print_index_table_item i =
author	Pierre Letouzey <pierre.letouzey@inria.fr>	2014-12-05 16:29:39 +0100
committer	Pierre Letouzey <pierre.letouzey@inria.fr>	2014-12-09 12:14:39 +0100
commit	5d2b096f29adf3d139c4de46321e26790e9b4211 (patch)
tree	4f3db111c2b4821d2f8908c79cc404ede0115095 /tools/coqdoc
parent	484a0c35662d3bb78aa1f2cd83ffcc1b1f761968 (diff)