diff options
| -rw-r--r-- | ide/wg_Tooltip.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/ide/wg_Tooltip.ml b/ide/wg_Tooltip.ml index f85792a4ef..4a0b2c43c5 100644 --- a/ide/wg_Tooltip.ml +++ b/ide/wg_Tooltip.ml @@ -19,7 +19,12 @@ module Table = struct let remove_all l i = l := List.filter (fun (j,_) -> not (overlap_interval i j)) !l let find_all l x = - CList.map_filter (fun (i,c) -> if in_interval x i then Some c else None) !l + let res = + CList.map_filter + (fun (i,c) -> if in_interval x i then Some c else None) + !l + in + if res = [] then raise Not_found else res end let table : string lazy_t Table.t = Table.create () |