Showing a query result which was an inductive type or constructor was bugged.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 3909f06bfaf8090bf0a3d5f87a5730c33eeeb0e3..afef8b4bb3ed62dc2831e1d67dbad30380d6c52b 100644 (file)
--- 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 ()
 ;;