From 19713b321fef827960f8fac7c6bfeb50eac29ec4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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