When locate is used during the lexing phase, it may happen that no URI is

found or more than an URI is found. In those cases a window is now opened
and the user is asked to either enter the URI (if none was found) or
choose from the list of found URIs.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index da00761f932f2aa7842149c940e3fcd576839ee4..2b476a6745c278a7fe07953c747507344f630956 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1516,24 +1516,42 @@ let _ =
       let MathQL.MQRefs uris = MQueryGenerator.locate id in
        let uri = 
         match uris with
-           [] -> None
+           [] ->
+            (GToolbox.input_string ~title:"Unknown input"
+             ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
          | [uri] -> Some uri
-         | _ -> None (* here we must let the user choose one uri *)
+         | _ ->
+           let choice =
+            GToolbox.question_box ~title:"Ambiguous input."
+             ~buttons:uris ~default:1 "Ambiguous input. Please, choose one."
+           in
+            if choice > 0 then
+             Some (List.nth uris (choice - 1))
+            else
+             (* No choice from the user *)
+             None
        in
         match uri with
            Some uri' ->
+            (* Constant *)
             if String.sub uri' (String.length uri' - 4) 4 = ".con" then
 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
              Some (Cic.Const (UriManager.uri_of_string uri',0))
             else
-             let uri'',typeno =
-(*CSC: the locate query now looks only for inductive type blocks ;-( *)
-(*CSC: when it will be correctly implemented we will have to work    *)
-(*CSC: here on the fragment identifier                               *)
-              uri',0
-             in
+             (try
+               (* Inductive Type *)
+               let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
+(*CSC: what cooking number? Here I always use 0, which may be bugged *)
+                Some (Cic.MutInd (uri'',0,typeno))
+              with
+               _ ->
+                (* Constructor of an Inductive Type *)
+                let uri'',typeno,consno =
+                 CicTextualLexer.indconuri_of_uri uri'
+                in
 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
-              Some (Cic.MutInd (UriManager.uri_of_string uri'',0,typeno))
+                 Some (Cic.MutConstruct (uri'',0,typeno,consno))
+             )
          | None -> None
     )
   end ;