Produce valid anchors in html files generated by why3doc.

src/why3doc/doc_def.ml

@@ -55,14 +55,44 @@ let get_file fname =
     Hashtbl.add files fname f;
     f
 
+let tag_allowed_char =
+  let tbl = Array.make 256 false in
+  let s = "-_:" in (* '.' is removed so as to be used as an escape char below *)
+  for i = 0 to String.length s - 1 do tbl.(Char.code s.[i]) <- true done;
+  let span m n = for i = Char.code m to Char.code n do tbl.(i) <- true done in
+  span 'A' 'Z';
+  span 'a' 'z';
+  span '0' '9';
+  fun c -> tbl.(Char.code c)
+
+let tag_escape s =
+  let len = ref 0 in
+  String.iter (fun c ->
+    if tag_allowed_char c then incr len else len := !len + 3) s;
+  let len' = !len in
+  let len = String.length s in
+  if len = len' then s else begin
+    let hex = "0123456789ABCDEF" in
+    let t = String.create len' in
+    let j = ref 0 in
+    for i = 0 to len - 1 do
+      let c = s.[i] in
+      if tag_allowed_char c then begin
+        t.[!j] <- c;
+        incr j
+      end else begin
+        let c = Char.code c in
+        t.[!j] <- '.';
+        t.[!j + 1] <- hex.[c / 16];
+        t.[!j + 2] <- hex.[c mod 16];
+        j := !j + 3
+      end
+    done;
+    t
+  end
+
 let make_tag s l =
-  let t =
-    s ^ "_" ^ string_of_int l (* TODO: improve? *)
-  in
-  for i = 0 to String.length s - 1 do
-    if t.[i] = ' ' then t.[i] <- '_'
-  done;
-  t
+  tag_escape s ^ "_" ^ string_of_int l
 
 let add_ident id = match id.id_loc with
   | None ->