diff options
| author | Alasdair Armstrong | 2017-07-05 17:42:06 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-07-05 17:42:06 +0100 |
| commit | cd3f299735d11241f064e9832c177830b78dcca4 (patch) | |
| tree | 68371a087d7700c3d63834c3cc39e1c3ff970fc3 /src | |
| parent | 5f46cb01ed07fbca390535440f77f1816cb61684 (diff) | |
Added split_on_char as a utility function in Util.ml, and replaced usage in sail.ml
Current REMS install script and Jenkins CI server is on an older ocaml
which doesn't have this function in String.
Diffstat (limited to 'src')
| -rw-r--r-- | src/sail.ml | 2 | ||||
| -rw-r--r-- | src/util.ml | 9 | ||||
| -rw-r--r-- | src/util.mli | 2 |
3 files changed, 11 insertions, 2 deletions
diff --git a/src/sail.ml b/src/sail.ml index 41c42fe4..d84144e1 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -89,7 +89,7 @@ let options = Arg.align ([ " (debug) skip constraint resolution in type-checking"); ( "-mono-split", Arg.String (fun s -> - let l = String.split_on_char ':' s in + let l = Util.split_on_char ':' s in match l with | [fname;line;var] -> opt_mono_split := ((fname,int_of_string line),var)::!opt_mono_split | _ -> raise (Arg.Bad (s ^ " not of form <filename>:<line>:<variable>"))), diff --git a/src/util.ml b/src/util.ml index bb277016..9b76c118 100644 --- a/src/util.ml +++ b/src/util.ml @@ -144,7 +144,14 @@ let rec compare_list f l1 l2 = compare_list f l1 l2 else c - + +let rec split_on_char sep str = + try + let sep_pos = String.index str sep in + String.sub str 0 sep_pos :: split_on_char sep (String.sub str (sep_pos + 1) (String.length str - (sep_pos + 1))) + with + | Not_found -> [str] + let map_changed_default d f l = let rec g = function | [] -> ([],false) diff --git a/src/util.mli b/src/util.mli index 496c63cf..099839bb 100644 --- a/src/util.mli +++ b/src/util.mli @@ -198,3 +198,5 @@ module ExtraSet : functor (S : Set.S) -> (*Formatting functions*) val string_of_list : string -> ('a -> string) -> 'a list -> string + +val split_on_char : char -> string -> string list |