From 71b101172275a7c5872f6e8e70f9c0185f93f828 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 28 Jul 2015 12:30:14 +0200
Subject: Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)

File system.ml seemed like a better choice than util.ml for sharing the
code, but it was bringing a bunch of useless dependencies to the IDE.

There are presumably several other tools that would benefit from using
open_utf8_file_in instead of open_in, e.g. coqdoc.
---
 lib/util.ml  | 11 +++++++++++
 lib/util.mli |  3 +++
 2 files changed, 14 insertions(+)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index a8c25f7456..a20dba0fc4 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -132,3 +132,14 @@ let map_union f g = function
 type iexn = Exninfo.iexn
 
 let iraise = Exninfo.iraise
+
+let open_utf8_file_in fname =
+  let is_bom s =
+    Int.equal (Char.code s.[0]) 0xEF &&
+    Int.equal (Char.code s.[1]) 0xBB &&
+    Int.equal (Char.code s.[2]) 0xBF
+  in
+  let in_chan = open_in fname in
+  let s = "   " in
+  if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
+  in_chan
diff --git a/lib/util.mli b/lib/util.mli
index 4fce809c2c..1dc405fcbe 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -110,3 +110,6 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
 
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 (** Used for browsable-until structures. *)
+
+val open_utf8_file_in : string -> in_channel
+(** Open an utf-8 encoded file and skip the byte-order mark if any. *)
-- 
cgit v1.2.3


From e706bbd36237abc6c63d3e30cdaf9a42ac458215 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 28 Jul 2015 15:10:35 +0200
Subject: Fixing bug #4281: Better escaping of XML attributes.

---
 lib/xml_lexer.mll  | 10 ++++++++++
 lib/xml_printer.ml |  2 ++
 2 files changed, 12 insertions(+)

(limited to 'lib')

diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll
index a33be9da73..f6943dd132 100644
--- a/lib/xml_lexer.mll
+++ b/lib/xml_lexer.mll
@@ -281,6 +281,11 @@ and dq_string = parse
                         Buffer.add_char tmp (lexeme_char lexbuf 1);
                         dq_string lexbuf
                 }
+        | '&'
+                {
+                        Buffer.add_string tmp (entity lexbuf);
+                        dq_string lexbuf
+                }
         | eof
                 { raise (Error EUnterminatedString) }
         | _
@@ -297,6 +302,11 @@ and q_string = parse
                         Buffer.add_char tmp (lexeme_char lexbuf 1);
                         q_string lexbuf
                 }
+        | '&'
+                {
+                        Buffer.add_string tmp (entity lexbuf);
+                        q_string lexbuf
+                }
         | eof
                 { raise (Error EUnterminatedString) }
         | _
diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml
index eeddd53cb8..bbb7b51ba3 100644
--- a/lib/xml_printer.ml
+++ b/lib/xml_printer.ml
@@ -46,6 +46,8 @@ let buffer_attr tmp (n,v) =
     match v.[p] with
       | '\\' -> output "\\\\"
       | '"' -> output "\\\""
+      | '<' -> output "&lt;"
+      | '&' -> output "&amp;"
       | c -> output' c
   done;
   output' '"'
-- 
cgit v1.2.3