X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fextlib%2FhExtlib.ml;h=979b0c51956da0fadb906187f23b367d8cf0ef27;hb=7d7f729471b4d5ebafa1b915096974e726cc13c6;hp=a0f9d8d6cbb1ab0295b65035f873c724e6668d5d;hpb=0ac236dda6f80f6dc86a7f12d8c88b25e64e3251;p=helm.git diff --git a/helm/ocaml/extlib/hExtlib.ml b/helm/ocaml/extlib/hExtlib.ml index a0f9d8d6c..979b0c519 100644 --- a/helm/ocaml/extlib/hExtlib.ml +++ b/helm/ocaml/extlib/hExtlib.ml @@ -134,6 +134,16 @@ let list_concat ?(sep = []) = | hd :: tl -> aux ([sep; hd] @ acc) tl in aux [] + +let rec list_findopt f l = + let rec aux = function + | [] -> None + | x::tl -> + (match f x with + | None -> aux tl + | Some _ as rc -> rc) + in + aux l (** {2 File predicates} *) @@ -311,6 +321,16 @@ let loc_of_floc = function | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> (loc_begin, loc_end) +let floc_of_loc (loc_begin, loc_end) = + let floc_begin = + { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; + Lexing.pos_cnum = loc_begin } + in + let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in + (floc_begin, floc_end) + +let dummy_floc = floc_of_loc (-1, -1) + let raise_localized_exception ~offset floc exn = let (x, y) = loc_of_floc floc in let x = offset + x in