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.

5 files changed, 15 insertions, 24 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 67e4bdb0c9..5892fb3d96 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -311,7 +311,7 @@ let read_buffer = Buffer.create maxread
     I/O Exceptions are propagated. *)
 
 let read_file name buf =
-  let ic = open_in name in
+  let ic = Util.open_utf8_file_in name in
   let len = ref 0 in
   try
     while len := input ic read_string 0 maxread; !len > 0 do
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. *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 966b952016..266d8f9b4f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -92,19 +92,6 @@ let disable_drop = function
 
 let user_error loc s = Errors.user_err_loc (loc,"_",str s)
 
-(* Open an utf-8 encoded file and skip the byte-order mark if any *)
-
-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
-
 (* Opening and closing a channel. Open it twice when verbose: the first
    channel is used to read the commands, and the second one to print them.
    Note: we could use only one thanks to seek_in, but seeking on and on in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6c5f10c20a..cfbdaccec4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1841,16 +1841,6 @@ let vernac_load interp fname =
     match Pcoq.Gram.entry_parse Pcoq.main_entry po with
       | Some x -> x
       | None -> raise End_of_input) in
-  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 in
   let fname =
     Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
   let fname = CUnix.make_suffix fname ".v" in