From 19713b321fef827960f8fac7c6bfeb50eac29ec4 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Dec 2002 18:42:31 +0000
Subject: [PATCH] Showing a query result which was an inductive type or
 constructor was bugged.

---
 helm/gTopLevel/gTopLevel.ml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 3909f06bf..afef8b4bb 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2400,8 +2400,17 @@ let show_query_results results =
   ignore
    (clist#connect#select_row
      (fun ~row ~column ~event ->
-       let (uri,_) = List.nth results row in
-        show_in_show_window_uri (UriManager.uri_of_string uri))
+       let (uristr,_) = List.nth results row in
+        match
+         cic_textual_parser_uri_of_string
+          (wrong_xpointer_format_from_wrong_xpointer_format' uristr)
+        with
+           CicTextualParser0.ConUri uri
+         | CicTextualParser0.VarUri uri
+         | CicTextualParser0.IndTyUri (uri,_)
+         | CicTextualParser0.IndConUri (uri,_,_) ->
+            show_in_show_window_uri uri
+     )
    ) ;
   window#show ()
 ;;
-- 
2.39.2