From 7c5b0dcd341196b80e4d3cfc1836c6baf6cd8f15 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 25 Apr 2013 14:32:02 +0000
Subject: 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
---
 ide/wg_Tooltip.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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 ()
-- 
cgit v1.2.3