shares the function that formats a string in HTML, escaping special

characters '. ", <, > and &

src/session/session.ml

@@ -533,16 +533,7 @@ let shape_filename = "why3shapes"
 let compressed_shape_filename = "why3shapes.gz"
 let session_dir_for_save = ref "."
 
-let save_string fmt s =
-  for i=0 to String.length s - 1 do
-    match String.get s i 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
-  done
+let save_string = Pp.html_string
 
 let opt pr lab fmt = function
   | None -> ()

src/session/session.mli

@@ -205,7 +205,6 @@ val read_session: string -> unit session * bool
 
 *)
 
-
 val save_session : Whyconf.config -> 'key session -> unit
 (** Save a session on disk *)
 

src/util/pp.ml

@@ -206,6 +206,18 @@ let sprintf_wnl p =
   kfprintf (fun fmt -> Format.pp_print_flush fmt (); Buffer.contents b) fmt p
 
 
+let html_string fmt s =
+  for i=0 to String.length s - 1 do
+    match String.get s i 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
+  done
+
+
 module Ansi =
   struct
 

src/util/pp.mli

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

src/why3doc/doc_lexer.mll

@@ -81,6 +81,8 @@
       t
     end
 
+  let pp_html_escape = Pp.html_string
+
   let current_file = ref ""
 
   let print_ident fmt lexbuf s =
@@ -96,9 +98,11 @@
       try
         match Glob.find loc with
         | id, Glob.Def ->
-          fprintf fmt "<a name=\"%a\">%s</a>" Doc_def.pp_anchor id s
+          fprintf fmt "<a name=\"%a\">%a</a>"
+            Doc_def.pp_anchor id pp_html_escape s
         | id, Glob.Use ->
-          fprintf fmt "<a href=\"%a\">%s</a>" Doc_def.pp_locate id s
+          fprintf fmt "<a href=\"%a\">%a</a>"
+            Doc_def.pp_locate id pp_html_escape s
       with Not_found ->
         (* otherwise, just print it *)
         pp_print_string fmt s