- Lazy.force only_constant_choices
- else begin
- let win = gui#uriChoice in
- let choices = ref [] in
- let chosen = ref false in
- let use_only_constants = ref false in
- win#uriChoiceDialog#set_title title;
- win#uriChoiceLabel#set_text msg;
- gui#uriChoices#list_store#clear ();
- List.iter gui#uriChoices#easy_append uris;
- win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
- let bye = ref (fun () -> ()) in
- let id1 =
- win#uriChoiceConstantsButton#connect#clicked (fun _ ->
- use_only_constants := true;
- !bye ())
- in
- let id2 =
- win#uriChoiceAutoButton#connect#clicked (fun _ ->
- use_only_constants := true ;
- Helm_registry.set_bool "matita.auto_disambiguation" true;
- !bye ())
- in
- let id3 =
- win#uriChoiceSelectedButton#connect#clicked (fun _ ->
- choices := gui#uriChoices#easy_selection ();
- !bye ())
- in
- bye := (fun () ->
- win#uriChoiceDialog#misc#hide ();
- win#uriChoiceConstantsButton#misc#disconnect id1;
- win#uriChoiceAutoButton#misc#disconnect id2;
- win#uriChoiceSelectedButton#misc#disconnect id3;
- prerr_endline "quit";
- GMain.Main.quit ());
- win#uriChoiceDialog#show ();
- GtkThread.main ();
- if !use_only_constants then
- Lazy.force only_constant_choices
- else
- match !choices with
- | [] -> error "No choice"
- | choices -> choices
- end