aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ideutils.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-02-23 13:46:07 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-14 22:19:26 +0100
commitfacf0520a47603d2679508136cbed43def0744cc (patch)
tree50e2870451436bf175f823689b0b3d54c65739f2 /ide/ideutils.ml
parent6b78d0602d46520ed1bd0cfbef120de3b06ca826 (diff)
[safe-string] ide
No functional change, one extra copy introduced but it seems hard to avoid.
Diffstat (limited to 'ide/ideutils.ml')
-rw-r--r--ide/ideutils.ml25
1 files changed, 14 insertions, 11 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 06a132732..c3a280796 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -294,18 +294,20 @@ let coqtop_path () =
match cmd_coqtop#get with
| Some s -> s
| None ->
- let prog = String.copy Sys.executable_name in
try
- let pos = String.length prog - 6 in
- let i = Str.search_backward (Str.regexp_string "coqide") prog pos
+ let old_prog = Sys.executable_name in
+ let pos = String.length old_prog - 6 in
+ let i = Str.search_backward (Str.regexp_string "coqide") old_prog pos
in
- String.blit "coqtop" 0 prog i 6;
- if Sys.file_exists prog then prog
+ let new_prog = Bytes.of_string old_prog in
+ Bytes.blit_string "coqtop" 0 new_prog i 6;
+ let new_prog = Bytes.to_string new_prog in
+ if Sys.file_exists new_prog then new_prog
else
let in_macos_bundle =
Filename.concat
- (Filename.dirname prog)
- (Filename.concat "../Resources/bin" (Filename.basename prog))
+ (Filename.dirname new_prog)
+ (Filename.concat "../Resources/bin" (Filename.basename new_prog))
in if Sys.file_exists in_macos_bundle then in_macos_bundle
else "coqtop"
with Not_found -> "coqtop"
@@ -357,7 +359,7 @@ let stat f =
let maxread = 4096
-let read_string = String.create maxread
+let read_string = Bytes.create maxread
let read_buffer = Buffer.create maxread
(** Read the content of file [f] and add it to buffer [b].
@@ -368,7 +370,7 @@ let read_file name buf =
let len = ref 0 in
try
while len := input ic read_string 0 maxread; !len > 0 do
- Buffer.add_substring buf read_string 0 !len
+ Buffer.add_subbytes buf read_string 0 !len
done;
close_in ic
with e -> close_in ic; raise e
@@ -381,8 +383,9 @@ let read_file name buf =
let io_read_all chan =
Buffer.clear read_buffer;
let read_once () =
- let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in
- Buffer.add_substring read_buffer read_string 0 len
+ (* XXX: Glib.Io must be converted to bytes / -safe-string upstream *)
+ let len = Glib.Io.read_chars ~buf:(Bytes.unsafe_to_string read_string) ~pos:0 ~len:maxread chan in
+ Buffer.add_subbytes read_buffer read_string 0 len
in
begin
try while true do read_once () done