String.sub s (String.length s - 4) 4 = ".var"
with Invalid_argument _ -> false
+(* this is a shit and should be changed :-{ *)
let interactive_uri_choice
?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
- ?(hide_try=false) ?(ok_label="_Auto") ?copy_cb ()
+ ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO)
+ ?copy_cb ()
~id uris
=
let gui = instance () in
ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
connect_button dialog#uriChoiceConstantsButton (fun _ ->
return (Some (Lazy.force nonvars_uris)));
- connect_button dialog#uriChoiceAutoButton (fun _ ->
- Helm_registry.set_bool "matita.auto_disambiguation" true;
- return (Some (Lazy.force nonvars_uris)));
+ if ok_action = `AUTO then
+ connect_button dialog#uriChoiceAutoButton (fun _ ->
+ Helm_registry.set_bool "matita.auto_disambiguation" true;
+ return (Some (Lazy.force nonvars_uris)))
+ else
+ connect_button dialog#uriChoiceAutoButton (fun _ ->
+ match model#easy_selection () with
+ | [] -> ()
+ | uris -> return (Some uris));
connect_button dialog#uriChoiceSelectedButton (fun _ ->
match model#easy_selection () with
| [] -> ()