+ if !usedb then
+ begin
+ Mqint.init "host=mowgli.cs.unibo.it dbname=helm user=helm" ;
+ CicTextualParser0.set_locate_object
+ (function id ->
+ let result = MQueryGenerator.locate id in
+ let uris =
+ List.map
+ (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
+ result in
+ let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
+ begin
+ match !rendering_window with
+ None -> assert false
+ | Some rw -> output_html rw#outputhtml html ;
+ end ;
+ let uri =
+ match uris with
+ [] ->
+ (match
+ (GToolbox.input_string ~title:"Unknown input"
+ ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
+ with
+ None -> None
+ | Some uri -> Some ("cic:" ^ uri)
+ )
+ | [uri] -> Some 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
+ (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.MutConstruct (uri'',0,typeno,consno))
+ )
+ | None -> None
+ )
+ end ;