snapshot

[helm.git] / helm / matita / matitaGtkMisc.mli

diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli
index 03847ac870b4d506c0ad7a6952787f49794ca0c5..6ad12a75643502795885a54f25ad32201d37ddf4 100644 (file)
--- a/helm/matita/matitaGtkMisc.mli
+++ b/helm/matita/matitaGtkMisc.mli
@@ -46,3 +46,20 @@ class stringListModel:
     method easy_selection:  unit -> string list
   end
 
+(** {2 Matita GUI components} *)
+
+class type gui =
+  object
+    method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+  end
+
+exception No_choice
+
+  (** @raise No_choice *)
+val interactive_user_uri_choice:
+  gui:#gui ->
+  selection_mode:Gtk.Tags.selection_mode -> title:string -> msg:string ->
+  ?nonvars_button:bool ->
+  string list ->
+    string list
+