summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlain Frisch <alain@frisch.fr>2013-08-30 13:12:47 +0000
committerAlain Frisch <alain@frisch.fr>2013-08-30 13:12:47 +0000
commitbbb30a93b2aa3860456b411d5099f8320ed940c3 (patch)
tree82ff135a7164dbb419fe76d0a2da3ad77d4d0865
parent6afbdfb724d2747ee5adcd238a190b2a714eba79 (diff)
PR#6148: speed improvement for Buffer (patch by John Whitington).
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14048 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
-rw-r--r--Changes1
-rw-r--r--stdlib/buffer.ml10
2 files changed, 6 insertions, 5 deletions
diff --git a/Changes b/Changes
index 780ca0c30..5e94e7f0a 100644
--- a/Changes
+++ b/Changes
@@ -16,6 +16,7 @@ Bug fixes:
Standard library:
- PR#4986: add List.sort_uniq and Set.of_list
+- PR#6148: speed improvement for Buffer (patch by John Whitington)
Features wishes:
- PR#4243: make the Makefiles parallelizable
diff --git a/stdlib/buffer.ml b/stdlib/buffer.ml
index ffd6e5a4c..78a9e2611 100644
--- a/stdlib/buffer.ml
+++ b/stdlib/buffer.ml
@@ -32,7 +32,7 @@ let sub b ofs len =
then invalid_arg "Buffer.sub"
else begin
let r = String.create len in
- String.blit b.buffer ofs r 0 len;
+ String.unsafe_blit b.buffer ofs r 0 len;
r
end
;;
@@ -48,7 +48,7 @@ let blit src srcoff dst dstoff len =
let nth b ofs =
if ofs < 0 || ofs >= b.position then
invalid_arg "Buffer.nth"
- else String.get b.buffer ofs
+ else String.unsafe_get b.buffer ofs
;;
let length b = b.position
@@ -76,7 +76,7 @@ let resize b more =
let add_char b c =
let pos = b.position in
if pos >= b.length then resize b 1;
- b.buffer.[pos] <- c;
+ String.unsafe_set b.buffer pos c;
b.position <- pos + 1
let add_substring b s offset len =
@@ -84,14 +84,14 @@ let add_substring b s offset len =
then invalid_arg "Buffer.add_substring";
let new_position = b.position + len in
if new_position > b.length then resize b len;
- String.blit s offset b.buffer b.position len;
+ String.unsafe_blit s offset b.buffer b.position len;
b.position <- new_position
let add_string b s =
let len = String.length s in
let new_position = b.position + len in
if new_position > b.length then resize b len;
- String.blit s 0 b.buffer b.position len;
+ String.unsafe_blit s 0 b.buffer b.position len;
b.position <- new_position
let add_buffer b bs =