From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Dec 2002 18:42:31 +0000 (+0000)
Subject: Showing a query result which was an inductive type or constructor was bugged.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=19713b321fef827960f8fac7c6bfeb50eac29ec4;p=helm.git

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