Share also the function which outputs a single char in HTML

src/util/pp.ml

@@ -205,16 +205,18 @@ let sprintf_wnl p =
   wnl fmt;
   kfprintf (fun fmt -> Format.pp_print_flush fmt (); Buffer.contents b) fmt p
 
+let html_char fmt c =
+  match c with
+  | '\"' -> pp_print_string fmt """
+  | '\'' -> pp_print_string fmt "'"
+  | '<' -> pp_print_string fmt "&lt;"
+  | '>' -> pp_print_string fmt "&gt;"
+  | '&' -> pp_print_string fmt "&amp;"
+  | c -> pp_print_char fmt c
 
 let html_string fmt s =
   for i=0 to String.length s - 1 do
-    match String.get s i with
-      | '\"' -> pp_print_string fmt "&quot;"
-      | '\'' -> pp_print_string fmt "&apos;"
-      | '<' -> pp_print_string fmt "&lt;"
-      | '>' -> pp_print_string fmt "&gt;"
-      | '&' -> pp_print_string fmt "&amp;"
-      | c -> pp_print_char fmt c
+    html_char fmt (String.get s i)
   done
 
 

src/util/pp.mli

@@ -147,6 +147,7 @@ val sprintf :
 val sprintf_wnl :
   ('b,  formatter, unit, string) Pervasives.format4 -> 'b
 
+val html_char : Format.formatter -> char -> unit
 val html_string : Format.formatter -> string -> unit
   (** formats the string by escaping special HTML characters
       quote, double quote, <, > and & *)

src/why3doc/doc_lexer.mll

@@ -51,38 +51,6 @@
   let get_loc lb =
     Loc.extract (Lexing.lexeme_start_p lb, Lexing.lexeme_end_p lb)
 
-  let html_char fmt c =
-    pp_print_string fmt (match c with
-      | '<' -> "&lt;"
-      | '>' -> "&gt;"
-      | '&' -> "&amp;"
-      | _ -> assert false)
-
-  let html_escape s =
-    let len = ref 0 in
-    String.iter (function '<' | '>' -> len := !len + 4
-      | '&' -> len := !len + 5 | _ -> incr len) s;
-    let len' = !len in
-    let len = String.length s in
-    if len = len' then s else begin
-      let t = String.create len' in
-      let j = ref 0 in
-      let app u =
-        let l = String.length u in
-        String.blit u 0 t !j l;
-        j := !j + l in
-      for i = 0 to len - 1 do
-        match s.[i] with
-        | '<' -> app "&lt;"
-        | '>' -> app "&gt;"
-        | '&' -> app "&amp;"
-        | c -> t.[!j] <- c; incr j
-      done;
-      t
-    end
-
-  let pp_html_escape = Pp.html_string
-
   let current_file = ref ""
 
   let print_ident fmt lexbuf s =
@@ -94,15 +62,14 @@
       let (* f,l,c as *) loc = get_loc lexbuf in
       (* Format.eprintf "  IDENT %s/%d/%d@." f l c; *)
       (* is this a def point? *)
-      let s = html_escape s in
       try
         match Glob.find loc with
         | id, Glob.Def ->
           fprintf fmt "<a name=\"%a\">%a</a>"
-            Doc_def.pp_anchor id pp_html_escape s
+            Doc_def.pp_anchor id Pp.html_string s
         | id, Glob.Use ->
           fprintf fmt "<a href=\"%a\">%a</a>"
-            Doc_def.pp_locate id pp_html_escape s
+            Doc_def.pp_locate id Pp.html_string s
       with Not_found ->
         (* otherwise, just print it *)
         pp_print_string fmt s
@@ -135,7 +102,7 @@ let operator =
 
 let space = [' ' '\t']
 let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* | operator
-let special = ['<' '>' '&']
+let special = ['\'' '"' '<' '>' '&']
 
 rule scan fmt empty = parse
   | "(*)" as s
@@ -212,7 +179,7 @@ and comment fmt do_output = parse
              string fmt do_output lexbuf;
              comment fmt do_output lexbuf }
   | special as c
-           { if do_output then html_char fmt c;
+           { if do_output then Pp.html_char fmt c;
              comment fmt do_output lexbuf }
   | "'\"'"
   | _ as s { if do_output then pp_print_string fmt s;
@@ -224,7 +191,7 @@ and string fmt do_output = parse
              string fmt do_output lexbuf }
   | '"'    { if do_output then pp_print_string fmt "&quot;" }
   | special as c
-           { if do_output then html_char fmt c;
+           { if do_output then Pp.html_char fmt c;
              string fmt do_output lexbuf }
   | "\\" _
   | _ as s { if do_output then pp_print_string fmt s;
@@ -274,7 +241,7 @@ and doc fmt block headings = parse
              doc fmt block headings lexbuf }
   | special as c
            { if not block then pp_print_string fmt "<p>";
-             html_char fmt c;
+             Pp.html_char fmt c;
              doc fmt true headings lexbuf }
   | _ as c { if not block then pp_print_string fmt "<p>";
              pp_print_char fmt c;