Merge PR#134: Enable `-safe-string`

4 files changed, 22 insertions, 27 deletions

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 4842a89151..4dfb7af6aa 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";
@@ -524,10 +521,10 @@ let variables is_install opt (args,defs) =
     List.iter (fun c -> print " \\
   -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
     print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
-    print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread\n";
-    print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n";
-    print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n";
-    print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n";
+    print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -safe-string\n";
+    print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -safe-string\n";
+    print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread -safe-string\n";
+    print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread -safe-string\n";
     print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n";
     print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n";
     print "GRAMMARS?=grammar.cma\n";
@@ -767,9 +764,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
     begin
       print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
       print "\t mkdir $@ || rm -rf $@/*\n";
-      print "\t$(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "\t$(OCAMLFIND) ocamldoc -html -safe-string -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
       print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
-      print "\t$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "\t$(OCAMLFIND) ocamldoc -latex -safe-string -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
     end;
   if !some_vfile then
     begin
@@ -885,7 +882,7 @@ let check_overlapping_include (_,inc_i,inc_r) =
  *)
 let merlin targets (ml_inc,_,_) =
   print ".merlin:\n";
-  print "\t@echo 'FLG -rectypes' > .merlin\n" ;
+  print "\t@echo 'FLG -rectypes -safe-string' > .merlin\n" ;
   List.iter (fun c ->
       printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c)
     lib_dirs ;
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index f817ed5a2a..3d92c9356b 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 9be791a8de..34108eff42 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
@@ -205,22 +205,22 @@ let prepare_entry s = function
       while !j <= l do
 	if not !quoted then begin
 	  (match s.[!j] with
-	  | '_' -> ntn.[!k] <- ' '; incr k
-	  | 'x' -> ntn.[!k] <- '_'; incr k
+	  | '_' -> Bytes.set ntn !k ' '; incr k
+	  | 'x' -> Bytes.set ntn !k '_'; incr k
 	  | '\'' -> quoted := true
 	  | _ -> assert false)
 	end
 	else
 	  if s.[!j] = '\'' then
 	    if (!j = l || s.[!j+1] = '_') then quoted := false
-	    else (incr j; ntn.[!k] <- s.[!j]; incr k)
+	    else (incr j; Bytes.set ntn !k s.[!j]; incr k)
 	  else begin
-	    ntn.[!k] <- s.[!j];
+	    Bytes.set ntn !k s.[!j];
 	    incr k
 	  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 d7bdf907a2..b8e69d6c6d 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