diff options
| author | bcpierce00 <bcpierce00@users.noreply.github.com> | 2018-01-22 07:04:41 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-01-22 07:04:41 -0500 |
| commit | 1f692c6471ff194d58a0b67b159298836ccda3b7 (patch) | |
| tree | dd8e5aba0fa9421c41d9805c9fe90952bf36fb16 /src | |
| parent | 9e7c92e06b6e7a34e9d174d673a17c3ba8491648 (diff) | |
| parent | 94847a3da9de1d3f9d789fb5f27b1a5bdea0e9b8 (diff) | |
| download | unison-1f692c6471ff194d58a0b67b159298836ccda3b7.zip unison-1f692c6471ff194d58a0b67b159298836ccda3b7.tar.gz unison-1f692c6471ff194d58a0b67b159298836ccda3b7.tar.bz2 | |
Merge pull request #120 from g-raud/trimwhitespace-faster
Util: make trimWhitespace() linear and not quadratic
Diffstat (limited to 'src')
| -rw-r--r-- | src/ubase/util.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/src/ubase/util.ml b/src/ubase/util.ml index 1231eb6..9f4fe66 100644 --- a/src/ubase/util.ml +++ b/src/ubase/util.ml @@ -388,16 +388,18 @@ let removeTrailingCR s = if l = 0 || s.[l - 1] <> '\r' then s else String.sub s 0 (l - 1) -(* FIX: quadratic! *) -let rec trimWhitespace s = +let trimWhitespace s = let l = String.length s in - if l=0 then s - else if s.[0]=' ' || s.[0]='\t' || s.[0]='\n' || s.[0]='\r' then - trimWhitespace (String.sub s 1 (l-1)) - else if s.[l-1]=' ' || s.[l-1]='\t' || s.[l-1]='\n' || s.[l-1]='\r' then - trimWhitespace (String.sub s 0 (l-1)) - else - s + let rec loop lp rp = + if lp > rp then "" + else if s.[lp]=' ' || s.[lp]='\t' || s.[lp]='\n' || s.[lp]='\r' then + loop (lp+1) rp + else if s.[rp]=' ' || s.[rp]='\t' || s.[rp]='\n' || s.[rp]='\r' then + loop lp (rp-1) + else + String.sub s lp (rp+1-lp) + in + loop 0 (l-1) let splitIntoWords ?esc:(e='\\') (s:string) (c:char) = let rec inword acc eacc start pos = |