From 92579449f62f0fd7699b0b447f3aee0d82d1b5c3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 23 Feb 2017 13:48:47 +0100
Subject: [safe-string] tools

No functional changes.
---
 tools/coq_makefile.ml | 7 ++-----
 tools/coqdoc/alpha.ml | 7 +------
 tools/coqdoc/index.ml | 4 ++--
 tools/coqworkmgr.ml   | 9 ++++++---
 4 files changed, 11 insertions(+), 16 deletions(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 4842a8915..23479aee5 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -125,12 +125,9 @@ let physical_dir_of_logical_dir ldir =
   let le = String.length ldir - 1 in
   let pdir =
     if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1)
-    else String.copy ldir
+    else ldir
   in
-  for i = 0 to le - 1 do
-    if pdir.[i] = '.' then pdir.[i] <- '/';
-  done;
-  pdir
+  String.map (fun c -> if c = '.' then '/' else c) pdir
 
 let standard opt =
   print "byte:\n";
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index f817ed5a2..3d92c9356 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -26,12 +26,7 @@ let norm_char c =
   if !latin1 then norm_char_latin1 c else
   Char.uppercase c
 
-let norm_string s =
-  let u = String.copy s in
-  for i = 0 to String.length s - 1 do
-    u.[i] <- norm_char s.[i]
-  done;
-  u
+let norm_string = String.map (fun s -> norm_char s)
 
 let compare_char c1 c2 = match norm_char c1, norm_char c2 with
   | ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 9be791a8d..c9cb676e9 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -197,7 +197,7 @@ let prepare_entry s = function
       let h = try String.index_from s 0 ':' with _ -> err () in
       let i = try String.index_from s (h+1) ':' with _ -> err () in
       let sc = String.sub s (h+1) (i-h-1) in
-      let ntn = String.make (String.length s - i) ' ' in
+      let ntn = Bytes.make (String.length s - i) ' ' in
       let k = ref 0 in
       let j = ref (i+1) in
       let quoted = ref false in
@@ -220,7 +220,7 @@ let prepare_entry s = function
 	  end;
 	incr j
       done;
-      let ntn = String.sub ntn 0 !k in
+      let ntn = Bytes.sub_string ntn 0 !k in
       if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
   | _ ->
       s
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index d7bdf907a..b8e69d6c6 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -72,10 +72,13 @@ let really_read_fd fd s off len =
 let raw_input_line fd =
   try
     let b = Buffer.create 80 in
-    let s = String.make 1 '\000' in
-    while s <> "\n" do
+    let s = Bytes.make 1 '\000' in
+    let endl = Bytes.of_string "\n" in
+    let endr = Bytes.of_string "\r" in
+    while Bytes.compare s endl <> 0 do
       really_read_fd fd s 0 1;
-      if s <> "\n" && s <> "\r" then Buffer.add_string b s;
+      if Bytes.compare s endl <> 0 && Bytes.compare s endr <> 0
+      then Buffer.add_bytes b s;
     done;
     Buffer.contents b
   with Unix.Unix_error _ -> raise End_of_file
-- 
cgit v1.2.3