Fix: tooltip correctly handles the absence of info (empty string)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16457 85f007b7-540e-0410-9357-904b9bb8a0f7

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 ()